| Copyright | (c) University of Cambridge, Cambridge, England adaption (c) Till Mossakowski, Uni Bremen 2002-2005 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
Isabelle.IsaSign
Description
Data structures for Isabelle signatures and theories. Adapted from Isabelle.
- type TName = String
- data AltSyntax = AltSyntax String [Int] Int
- data VName = VName {}
- orig :: VName -> String
- data QName = QName {
- qname :: String
- qualifiers :: [String]
- mkQName :: String -> QName
- data Indexname = Indexname {
- unindexed :: String
- indexOffset :: Int
- data IsaClass = IsaClass String
- type Sort = [IsaClass]
- data Typ
- data Continuity
- data TAttr
- data DTyp
- data Term
- = Const { }
- | Free { }
- | Abs {
- absVar :: Term
- termId :: Term
- continuity :: Continuity
- | App {
- funId :: Term
- argId :: Term
- continuity :: Continuity
- | If {
- ifId :: Term
- thenId :: Term
- elseId :: Term
- continuity :: Continuity
- | Case { }
- | Let { }
- | IsaEq {
- firstTerm :: Term
- secondTerm :: Term
- | Tuplex [Term] Continuity
- | Set SetDecl
- data Prop = Prop {}
- data Props = Props {}
- data Sentence
- = Sentence { }
- | Instance { }
- | ConstDef { }
- | RecDef { }
- | TypeDef { }
- | Lemmas {
- lemmaName :: String
- lemmasList :: [String]
- | Locale {
- localeName :: QName
- localeContext :: Ctxt
- localeParents :: [QName]
- localeBody :: [Sentence]
- | Class {
- className :: QName
- classContext :: Ctxt
- classParents :: [QName]
- classBody :: [Sentence]
- | Datatypes [Datatype]
- | Domains [Domain]
- | Consts [(String, Maybe Mixfix, Typ)]
- | TypeSynonym QName (Maybe Mixfix) [String] Typ
- | Axioms [Axiom]
- | Lemma {
- lemmaTarget :: Maybe QName
- lemmaContext :: Ctxt
- lemmaProof :: Maybe String
- lemmaProps :: [Props]
- | Definition { }
- | Fun {
- funTarget :: Maybe QName
- funSequential :: Bool
- funDefault :: Maybe String
- funDomintros :: Bool
- funPartials :: Bool
- funEquations :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
- | Primrec {
- primrecTarget :: Maybe QName
- primrecEquations :: [(String, Maybe Mixfix, Typ, [([Term], Term)])]
- | Fixrec [(String, Maybe Mixfix, Typ, [FixrecEquation])]
- | Instantiation {
- instantiationType :: TName
- instantiationArity :: (Sort, [Sort])
- instantiationBody :: [Sentence]
- | InstanceProof { }
- | InstanceArity {
- instanceTypes :: [TName]
- instanceArity :: (Sort, [Sort])
- instanceProof :: String
- | InstanceSubclass { }
- | Subclass { }
- | Typedef {
- typedefName :: QName
- typedefVars :: [(String, Sort)]
- typedefMixfix :: Maybe Mixfix
- typedefMorphisms :: Maybe (QName, QName)
- typedefTerm :: Term
- typedefProof :: String
- | Defs { }
- data DefEquation = DefEquation {}
- data FixrecEquation = FixrecEquation {}
- data Ctxt = Ctxt {}
- data Mixfix = Mixfix {}
- data MixfixTemplate
- data Datatype = Datatype {}
- data DatatypeConstructor
- = DatatypeConstructor { }
- | DatatypeNoConstructor {
- constructorArgs :: [Typ]
- data Domain = Domain {}
- data DomainConstructor = DomainConstructor {}
- data DomainConstructorArg = DomainConstructorArg {}
- data Axiom = Axiom {}
- data FunSig = FunSig {
- funSigName :: QName
- funSigType :: Maybe Typ
- data SetDecl
- data MetaTerm
- = Term Term
- | Conditional [Term] Term
- mkSenAux :: Bool -> MetaTerm -> Sentence
- mkSen :: Term -> Sentence
- mkCond :: [Term] -> Term -> Sentence
- mkRefuteSen :: Term -> Sentence
- isRefute :: Sentence -> Bool
- type ClassDecl = ([IsaClass], [(String, Term)], [(String, Typ)])
- type Classrel = Map IsaClass ClassDecl
- type LocaleDecl = ([String], [(String, Term)], [(String, Term)], [(String, Typ, Maybe AltSyntax)])
- type Def = (Typ, [(String, Typ)], Term)
- type FunDef = (Typ, [([Term], Term)])
- type Locales = Map String LocaleDecl
- type Defs = Map String Def
- type Funs = Map String FunDef
- type Arities = Map TName [(IsaClass, [(Typ, Sort)])]
- type Abbrs = Map TName ([TName], Typ)
- data TypeSig = TySg {}
- emptyTypeSig :: TypeSig
- isSubTypeSig :: TypeSig -> TypeSig -> Bool
- data BaseSig
- data Sign = Sign {}
- type ConstTab = Map VName Typ
- type DomainTab = [[DomainEntry]]
- type DomainEntry = (Typ, [(VName, [Typ])])
- emptySign :: Sign
- isSubSign :: Sign -> Sign -> Bool
- union_tsig :: TypeSig -> TypeSig -> TypeSig
- union_sig :: Sign -> Sign -> Sign
- data IsaProof = IsaProof {
- proof :: [ProofCommand]
- end :: ProofEnd
- data ProofCommand
- data ProofEnd
- data Modifier
- data ProofMethod
- toIsaProof :: ProofEnd -> IsaProof
- mkOops :: IsaProof
Documentation
data AltSyntax
data Indexname
Indexnames can be quickly renamed by adding an offset to the integer part, for resolution.
Constructors
| Indexname | |
Fields
| |
data IsaClass
data Continuity
data TAttr
data Term
Constructors
| Const | |
| Free | |
| Abs | |
Fields
| |
| App | |
Fields
| |
| If | |
Fields
| |
| Case | |
| Let | |
| IsaEq | |
Fields
| |
| Tuplex [Term] Continuity | |
| Set SetDecl | |
data Prop
data Props
data Sentence
Constructors
Instances
data DefEquation
Constructors
| DefEquation | |
Fields | |
data FixrecEquation
Constructors
| FixrecEquation | |
Fields | |
data Ctxt
data Mixfix
Constructors
| Mixfix | |
Fields
| |
data MixfixTemplate
data DatatypeConstructor
Constructors
| DatatypeConstructor | |
Fields
| |
| DatatypeNoConstructor | |
Fields
| |
data Domain
Constructors
| Domain | |
Fields
| |
data DomainConstructor
Constructors
| DomainConstructor | |
data DomainConstructorArg
Constructors
| DomainConstructorArg | |
data Axiom
data FunSig
Constructors
| FunSig | |
Fields
| |
data SetDecl
Constructors
| SubSet Term Typ Term | 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} |
| FixedSet [Term] | A set declared using a list of terms. e.g. {1,2,3} would be Set [1,2,3] |
mkRefuteSen :: Term -> Sentence
type Locales = Map String LocaleDecl
isSubTypeSig :: TypeSig -> TypeSig -> Bool
data BaseSig
Constructors
| 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 |
data Sign
Constructors
| Sign | |
Instances
type DomainTab = [[DomainEntry]]
type DomainEntry = (Typ, [(VName, [Typ])])
union_tsig :: TypeSig -> TypeSig -> TypeSig
data ProofCommand
Constructors
| Apply [ProofMethod] Bool | 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)+" |
| Using [String] | |
| Back | |
| Defer Int | |
| Prefer Int | |
| Refute |
data ProofEnd
data Modifier
Constructors
| No_asm | No_asm means that assumptions are completely ignored. |
| No_asm_simp | No_asm_simp means that the assumptions are not simplified but are used in the simplification of the conclusion. |
| No_asm_use | No_asm_use means that the assumptions are simplified but are not used in the simplification of each other or the conclusion. |
data ProofMethod
Constructors
| Auto | This is a plain auto with no parameters - it is used so often it warents its own constructor |
| Simp | This is a plain auto with no parameters - it is used so often it warents its own constructor |
| AutoSimpAdd (Maybe Modifier) [String] | 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 |
| SimpAdd (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 |
| Induct Term | Induction proof method. This performs induction upon a variable |
| CaseTac Term | Case_tac proof method. This perfom a case distinction on a term |
| SubgoalTac Term | Subgoal_tac proof method . Adds a term to the local assumptions and also creates a sub-goal of this term |
| Insert [String] | Insert proof method. Inserts a lemma or theorem name to the assumptions of the first goal |
| Other String | Used for proof methods that have not been implemented yet. This includes auto and simp with parameters |
toIsaProof :: ProofEnd -> IsaProof