e3169126793f43be3d840874ffb3935a51097001Patrik Flykt{- |

e3169126793f43be3d840874ffb3935a51097001Patrik FlyktModule : $Header$

e3169126793f43be3d840874ffb3935a51097001Patrik FlyktDescription : abstract Isabelle HOL and HOLCF syntax

e3169126793f43be3d840874ffb3935a51097001Patrik FlyktCopyright : (c) University of Cambridge, Cambridge, England

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt adaption (c) Till Mossakowski, Uni Bremen 2002-2005

e3169126793f43be3d840874ffb3935a51097001Patrik FlyktLicense : GPLv2 or higher, see LICENSE.txt

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt

e3169126793f43be3d840874ffb3935a51097001Patrik FlyktMaintainer : Christian.Maeder@dfki.de

e3169126793f43be3d840874ffb3935a51097001Patrik FlyktStability : provisional

e3169126793f43be3d840874ffb3935a51097001Patrik FlyktPortability : portable

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt

e3169126793f43be3d840874ffb3935a51097001Patrik FlyktData structures for Isabelle signatures and theories.

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt Adapted from Isabelle.

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt-}

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt

e3169126793f43be3d840874ffb3935a51097001Patrik Flyktmodule Isabelle.IsaSign where

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt

e3169126793f43be3d840874ffb3935a51097001Patrik Flyktimport qualified Data.Map as Map

e3169126793f43be3d840874ffb3935a51097001Patrik Flyktimport Data.List

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt--------------- not quite from src/Pure/term.ML ------------------------

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt------------------------ Names -----------------------------------------

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt-- | type names

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykttype TName = String

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt-- | names for values or constants (non-classes and non-types)

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flyktdata VName = VName

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt { new :: String -- ^ name within Isabelle

a9aff3615b430f86bd0a824214d95f634efaf894Patrik Flykt , altSyn :: Maybe AltSyntax -- ^ mixfix template syntax

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt } deriving Show

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flyktdata AltSyntax = AltSyntax String [Int] Int deriving (Show, Eq, Ord)

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt-- | the original (Haskell) name

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flyktorig :: VName -> String

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flyktorig = new

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flyktinstance Eq VName where

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt v1 == v2 = new v1 == new v2

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flyktinstance Ord VName where

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt v1 <= v2 = new v1 <= new v2

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt{- | Indexnames can be quickly renamed by adding an offset to

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt the integer part, for resolution. -}

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flyktdata Indexname = Indexname

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt { unindexed :: String

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt , indexOffset :: Int

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt } deriving (Ord, Eq, Show)

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt{- Types are classified by sorts. -}

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flyktdata IsaClass = IsaClass String deriving (Ord, Eq, Show)

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykttype Sort = [IsaClass]

f12abb48fc510b8b349c05e35ba048134debaf25Patrik Flykt

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt{- The sorts attached to TFrees and TVars specify the sort of

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt that variable -}

e3169126793f43be3d840874ffb3935a51097001Patrik Flyktdata Typ = Type { typeId :: TName,

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt typeSort :: Sort,

e3169126793f43be3d840874ffb3935a51097001Patrik Flykt typeArgs :: [Typ] }

f12ed3bf0b315fc88d5fbdf5bdca14b218c86e0cPatrik Flykt | TFree { typeId :: TName,

f12ed3bf0b315fc88d5fbdf5bdca14b218c86e0cPatrik Flykt typeSort :: Sort }

f12ed3bf0b315fc88d5fbdf5bdca14b218c86e0cPatrik Flykt | TVar { indexname :: Indexname,

f12ed3bf0b315fc88d5fbdf5bdca14b218c86e0cPatrik Flykt typeSort :: Sort }

f12ed3bf0b315fc88d5fbdf5bdca14b218c86e0cPatrik Flykt deriving (Eq, Ord, Show)

f12ed3bf0b315fc88d5fbdf5bdca14b218c86e0cPatrik Flykt

c6affce8740bb0cee42eebf6d1d44dd518035e88Patrik Flykt{- Terms. Bound variables are indicated by depth number.

c6affce8740bb0cee42eebf6d1d44dd518035e88Patrik Flykt Free variables, (scheme) variables and constants have names.

34e8c5a23cd1c53ef3c1169388dabe1f6dfd7319Patrik Flykt A term is "closed" if every bound variable of level "lev"

34e8c5a23cd1c53ef3c1169388dabe1f6dfd7319Patrik Flykt is enclosed by at least "lev" abstractions.

34e8c5a23cd1c53ef3c1169388dabe1f6dfd7319Patrik Flykt

34e8c5a23cd1c53ef3c1169388dabe1f6dfd7319Patrik Flykt It is possible to create meaningless terms containing loose bound vars

a9aff3615b430f86bd0a824214d95f634efaf894Patrik Flykt or type mismatches. But such terms are not allowed in rules. -}

a9aff3615b430f86bd0a824214d95f634efaf894Patrik Flykt

a9aff3615b430f86bd0a824214d95f634efaf894Patrik Flykt-- IsCont True - lifted; IsCont False - not lifted, used for constructors

631bbe71298ec892f77f44f94feb612646fe6853Patrik Flyktdata Continuity = IsCont Bool | NotCont deriving (Eq, Ord, Show)

631bbe71298ec892f77f44f94feb612646fe6853Patrik Flykt

data TAttr = TFun | TMet | TCon | NA deriving (Eq, Ord, Show)

data DTyp = Hide { typ :: Typ,

kon :: TAttr,

arit :: Maybe Int }

| Disp { typ :: Typ,

kon :: TAttr,

arit :: Maybe Int }

deriving (Eq, Ord, Show)

data Term =

Const { termName :: VName,

termType :: DTyp }

| Free { termName :: VName }

| Abs { absVar :: Term,

termId :: Term,

continuity :: Continuity } -- lambda abstraction

| App { funId :: Term,

argId :: Term,

continuity :: Continuity } -- application

| If { ifId :: Term,

thenId :: Term,

elseId :: Term,

continuity :: Continuity }

| Case { termId :: Term,

caseSubst :: [(Term, Term)] }

| Let { letSubst :: [(Term, Term)],

inId :: Term }

| IsaEq { firstTerm :: Term,

secondTerm :: Term }

| Tuplex [Term] Continuity

| Set SetDecl

deriving (Eq, Ord, Show)

data Sentence =

Sentence { isSimp :: Bool -- True for "[simp]"

, isRefuteAux :: Bool

, metaTerm :: MetaTerm

, thmProof :: Maybe IsaProof }

| Instance { tName :: TName

, arityArgs :: [Sort]

, arityRes :: Sort

-- | Definitons for the instansiation with the name of the sentence (String)

, definitions :: [(String, Term)]

, instProof :: IsaProof }

| ConstDef { senTerm :: Term }

| RecDef { keyword :: Maybe String

, constName :: VName

, constType :: (Maybe Typ)

, primRecSenTerms :: [Term] }

| TypeDef { newType :: Typ

, typeDef :: SetDecl

, nonEmptyPr :: IsaProof}

-- |Isabelle syntax for grouping multiple lemmas in to a single lemma.

| Lemmas { lemmaName :: String

, lemmasList :: [String]}

deriving (Eq, Ord, Show)

-- Other SetDecl variants to be added later

data SetDecl

-- | Create a set using a subset. First parameter is the variable

-- | Second is the type of the variable third is the formula

-- | describing the set comprehension e.g. x Nat "even x" would be

-- | produce the isabelle code: {x::Nat . even x}

= SubSet Term Typ Term

-- | A set declared using a list of terms. e.g. {1,2,3} would be Set [1,2,3]

| FixedSet [Term]

deriving (Eq, Ord, Show)

data MetaTerm = Term Term

| Conditional [Term] Term -- List of preconditions, conclusion.

deriving (Eq, Ord, Show)

mkSenAux :: Bool -> MetaTerm -> Sentence

mkSenAux b t = Sentence

{ isSimp = False

, isRefuteAux = b

, thmProof = Nothing

, metaTerm = t }

mkSen :: Term -> Sentence

mkSen = mkSenAux False . Term

mkCond :: [Term] -> Term -> Sentence

mkCond conds = mkSenAux False . Conditional conds

mkRefuteSen :: Term -> Sentence

mkRefuteSen = mkSenAux True . Term

isRefute :: Sentence -> Bool

isRefute s = case s of

Sentence { isRefuteAux = b } -> b

_ -> False

-------------------- from src/Pure/sorts.ML ------------------------

{-- type classes and sorts --}

{- Classes denote (possibly empty) collections of types that are

partially ordered by class inclusion. They are represented

symbolically by strings.

Sorts are intersections of finitely many classes. They are

represented by lists of classes. Normal forms of sorts are sorted

lists of minimal classes (wrt. current class inclusion).

(already defined in Pure/term.ML)

classrel:

table representing the proper subclass relation; entries (c, (cs,a,f))

represent the superclasses cs, the assumptions a and the fixed

names f of c

arities:

table of association lists of all type arities; (t, ars) means

that type constructor t has the arities ars; an element (c, Ss) of

ars represents the arity t::(Ss)c;

-}

type ClassDecl = ([IsaClass],[(String,Term)],[(String,Typ)])

type Classrel = Map.Map IsaClass ClassDecl

type LocaleDecl = ([String],[(String,Term)],[(String,Term)],

[(String,Typ,Maybe AltSyntax)])

-- parents * internal axioms * external axiosm * params

type Def = (Typ,[(String,Typ)],Term)

type FunDef = (Typ,[([Term],Term)])

type Locales = Map.Map String LocaleDecl

type Defs = Map.Map String Def

type Funs = Map.Map String FunDef

type Arities = Map.Map TName [(IsaClass, [(Typ, Sort)])]

type Abbrs = Map.Map TName ([TName], Typ)

data TypeSig =

TySg {

classrel :: Classrel, -- domain of the map yields the classes

locales :: Locales,

defs :: Defs,

funs :: Funs,

defaultSort :: Sort,

log_types :: [TName],

univ_witness:: Maybe (Typ, Sort),

abbrs :: Abbrs, -- constructor name, variable names, type.

arities :: Arities }

-- actually isa-instances. the former field tycons can be computed.

deriving (Eq, Ord, Show)

emptyTypeSig :: TypeSig

emptyTypeSig = TySg {

classrel = Map.empty,

locales = Map.empty,

defs = Map.empty,

funs = Map.empty,

defaultSort = [],

log_types = [],

univ_witness = Nothing,

abbrs = Map.empty,

arities = Map.empty }

isSubTypeSig :: TypeSig -> TypeSig -> Bool

isSubTypeSig t1 t2 =

null (defaultSort t1 \\ defaultSort t2) &&

Map.isSubmapOf (classrel t1) (classrel t2) &&

Map.isSubmapOf (locales t1) (locales t2) &&

Map.isSubmapOf (defs t1) (defs t2) &&

Map.isSubmapOf (funs t1) (funs t2) &&

null (log_types t1 \\ log_types t2) &&

(case univ_witness t1 of

Nothing -> True

w1 -> w1 == univ_witness t2) &&

Map.isSubmapOf (abbrs t1) (abbrs t2) &&

Map.isSubmapOf (arities t1) (arities t2)

-------------------- from src/Pure/sign.ML ------------------------

data BaseSig =

Main_thy -- ^ main theory of higher order logic (HOL)

| Custom_thy

| MainHC_thy -- ^ extend main theory of HOL logic for HasCASL

| MainHCPairs_thy -- ^ for HasCASL translation to bool pairs

| HOLCF_thy -- ^ higher order logic for continuous functions

| HsHOLCF_thy -- ^ HOLCF for Haskell

| HsHOL_thy -- ^ HOL for Haskell

| MHsHOL_thy

| MHsHOLCF_thy

| CspHOLComplex_thy

deriving (Eq, Ord, Show)

{- possibly simply supply a theory like MainHC as string

or recursively as Isabelle.Sign -}

data Sign = Sign

{ theoryName :: String

, baseSig :: BaseSig -- like Main etc.

, imports :: [String] -- additional imports

, tsig :: TypeSig

, constTab :: ConstTab -- value cons with type

, domainTab :: DomainTab

, showLemmas :: Bool

} deriving (Eq, Ord, Show)

{- list of datatype definitions

each of these consists of a list of (mutually recursive) datatypes

each datatype consists of its name (Typ) and a list of constructors

each constructor consists of its name (String) and list of argument

types

-}

type ConstTab = Map.Map VName Typ

-- same types for data types and domains

-- the optional string is only relevant for alternative type names

type DomainTab = [[DomainEntry]]

type DomainEntry = (Typ, [(VName, [Typ])])

emptySign :: Sign

emptySign = Sign

{ theoryName = "thy"

, baseSig = Main_thy

, imports = []

, tsig = emptyTypeSig

, constTab = Map.empty

, domainTab = []

, showLemmas = False }

isSubSign :: Sign -> Sign -> Bool

isSubSign s1 s2 =

isSubTypeSig (tsig s1) (tsig s2) &&

Map.isSubmapOf (constTab s1) (constTab s2) &&

null (domainTab s1 \\ domainTab s2)

union_tsig :: TypeSig -> TypeSig -> TypeSig

union_tsig t1 t2 = t1 {

classrel = Map.union (classrel t1) (classrel t2),

locales = Map.union (locales t1) (locales t2),

defs = Map.union (defs t1) (defs t2),

funs = Map.union (funs t1) (funs t2),

log_types = Data.List.union (log_types t1) (log_types t2),

abbrs = Map.union (abbrs t1) (abbrs t2),

arities = Map.union (arities t1) (arities t2)

}

union_sig :: Sign -> Sign -> Sign

union_sig s1 s2 = s1 {

tsig = union_tsig (tsig s1) (tsig s2),

constTab = Map.union (constTab s1) (constTab s2),

domainTab = Data.List.union (domainTab s1) (domainTab s2)

}

------------------------ Sentence -------------------------------------

{- Instances in Haskell have form:

instance (MyClass a, MyClass b) => MyClass (MyTypeConst a b)

In Isabelle:

instance MyTypeConst :: (MyClass, MyClass) MyClass

Note that the Isabelle syntax does not allows for multi-parameter classes.

Rather, it subsumes the syntax for arities.

Type constraints are applied to value constructors in Haskell as follows:

MyValCon :: (MyClass a, MyClass b) => MyTypeConst a b

In Isabelle:

MyValCon :: MyTypeConst (a::MyClass) (b::MyClass)

In both cases, the typing expressions may be encoded as schemes.

Schemes and instances allows for the inference of type constraints over

values of functions.

-}

-- Data structures for Isabelle Proofs

data IsaProof = IsaProof

{ proof :: [ProofCommand],

end :: ProofEnd

} deriving (Show, Eq, Ord)

data ProofCommand

-- | Apply a list of proof methods, which will be applied in sequence

-- withing the apply proof command. The boolean is if the + modifier

-- should be used at the end of the apply proof method. e.g. Apply(A,B,C)

-- True would represent the Isabelle proof command "apply(A,B,C)+"

= Apply [ProofMethod] Bool

| Using [String]

| Back

| Defer Int

| Prefer Int

| Refute

deriving (Show, Eq, Ord)

data ProofEnd

= By ProofMethod

| DotDot

| Done

| Oops

| Sorry

deriving (Show, Eq, Ord)

data Modifier

-- | No_asm means that assumptions are completely ignored.

= No_asm

-- | No_asm_simp means that the assumptions are not simplified but

-- | are used in the simplification of the conclusion.

| No_asm_simp

-- | No_asm_use means that the assumptions are simplified but are

-- | not used in the simplification of each other or the

-- | conclusion.

| No_asm_use

deriving (Show, Eq, Ord)

data ProofMethod

-- | This is a plain auto with no parameters - it is used

-- so often it warents its own constructor

= Auto

-- | This is a plain auto with no parameters - it is used

-- so often it warents its own constructor

| Simp

-- | This is an auto where the simpset has been temporarily

-- extended with a listof lemmas, theorems and axioms. An

-- optional modifier can also be used to control how the

-- assumptions are used. It is used so often it warents its own

-- constructor

| AutoSimpAdd (Maybe Modifier) [String]

-- | This is a simp where the simpset has been temporarily

-- extended with a listof lemmas, theorems and axioms. An

-- optional modifier can also be used to control how the

-- assumptions are used. It is used so often it warents its own

-- constructor

| SimpAdd (Maybe Modifier) [String]

-- | Induction proof method. This performs induction upon a variable

| Induct Term

-- | Case_tac proof method. This perfom a case distinction on a term

| CaseTac Term

-- | Subgoal_tac proof method . Adds a term to the local

-- assumptions and also creates a sub-goal of this term

| SubgoalTac Term

-- | Insert proof method. Inserts a lemma or theorem name to the assumptions

-- of the first goal

| Insert [String]

-- | Used for proof methods that have not been implemented yet.

-- This includes auto and simp with parameters

| Other String

deriving (Show, Eq, Ord)

toIsaProof :: ProofEnd -> IsaProof

toIsaProof = IsaProof []

mkOops :: IsaProof

mkOops = toIsaProof Oops