| 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 {
- definitionName :: QName
- definitionMixfix :: Maybe Mixfix
- definitionTarget :: Maybe String
- definitionType :: Typ
- definitionVars :: [Term]
- definitionTerm :: Term
- | 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 {
- instanceProof :: String
- | InstanceArity {
- instanceTypes :: [TName]
- instanceArity :: (Sort, [Sort])
- instanceProof :: String
- | InstanceSubclass {
- instanceClass :: String
- instanceRel :: String
- instanceClass1 :: String
- instanceProof :: String
- | Subclass {
- subclassClass :: String
- subclassTarget :: Maybe QName
- subclassProof :: String
- | Typedef {
- typedefName :: QName
- typedefVars :: [(String, Sort)]
- typedefMixfix :: Maybe Mixfix
- typedefMorphisms :: Maybe (QName, QName)
- typedefTerm :: Term
- typedefProof :: String
- | Defs {
- defsUnchecked :: Bool
- defsOverloaded :: Bool
- defsEquations :: [DefEquation]
- data DefEquation = DefEquation {
- defEquationName :: QName
- defEquationConst :: String
- defEquationConstType :: Typ
- defEquationTerm :: Term
- defEquationArgs :: String
- data FixrecEquation = FixrecEquation {}
- data Ctxt = Ctxt {}
- data Mixfix = Mixfix {
- mixfixNargs :: Int
- mixfixPrio :: Int
- mixfixPretty :: String
- mixfixTemplate :: [MixfixTemplate]
- data MixfixTemplate
- = Arg Int
- | Str String
- | Break Int
- | Block Int [MixfixTemplate]
- data Datatype = Datatype {
- datatypeName :: QName
- datatypeTVars :: [Typ]
- datatypeMixfix :: Maybe Mixfix
- datatypeConstructors :: [DatatypeConstructor]
- data DatatypeConstructor
- = DatatypeConstructor {
- constructorName :: QName
- constructorType :: Typ
- constructorMixfix :: Maybe Mixfix
- constructorArgs :: [Typ]
- | DatatypeNoConstructor {
- constructorArgs :: [Typ]
- = DatatypeConstructor {
- data Domain = Domain {
- domainName :: QName
- domainTVars :: [Typ]
- domainMixfix :: Maybe Mixfix
- domainConstructors :: [DomainConstructor]
- data DomainConstructor = DomainConstructor {}
- data DomainConstructorArg = DomainConstructorArg {
- domainConstructorArgSel :: Maybe QName
- domainConstructorArgType :: Typ
- domainConstructorArgLazy :: Bool
- 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
Constructors
| AltSyntax String [Int] Int |
names for values or constants (non-classes and non-types)
Constructors
| VName | |
Constructors
| QName | |
Fields
| |
Indexnames can be quickly renamed by adding an offset to the integer part, for resolution.
Constructors
| Indexname | |
Fields
| |
Constructors
| IsaClass String |
data Continuity Source #
Instances
| Eq Continuity Source # | |
| Data Continuity Source # | |
| Ord Continuity Source # | |
| Show Continuity Source # | |
Constructors
| Const | |
| Free | |
| Abs | |
Fields
| |
| App | |
Fields
| |
| If | |
Fields
| |
| Case | |
| Let | |
| IsaEq | |
Fields
| |
| Tuplex [Term] Continuity | |
| Set SetDecl | |
Constructors
Instances
data DefEquation Source #
Constructors
| DefEquation | |
Fields
| |
Instances
| Eq DefEquation Source # | |
| Data DefEquation Source # | |
| Ord DefEquation Source # | |
| Show DefEquation Source # | |
data FixrecEquation Source #
Constructors
| FixrecEquation | |
Fields
| |
Instances
| Eq FixrecEquation Source # | |
| Data FixrecEquation Source # | |
| Ord FixrecEquation Source # | |
| Show FixrecEquation Source # | |
Constructors
| Mixfix | |
Fields
| |
data MixfixTemplate Source #
Constructors
| Arg Int | |
| Str String | |
| Break Int | |
| Block Int [MixfixTemplate] |
Instances
| Eq MixfixTemplate Source # | |
| Data MixfixTemplate Source # | |
| Ord MixfixTemplate Source # | |
| Show MixfixTemplate Source # | |
Constructors
| Datatype | |
Fields
| |
data DatatypeConstructor Source #
Constructors
| DatatypeConstructor | |
Fields
| |
| DatatypeNoConstructor | |
Fields
| |
Instances
| Eq DatatypeConstructor Source # | |
| Data DatatypeConstructor Source # | |
| Ord DatatypeConstructor Source # | |
| Show DatatypeConstructor Source # | |
Constructors
| Domain | |
Fields
| |
data DomainConstructor Source #
Constructors
| DomainConstructor | |
Instances
| Eq DomainConstructor Source # | |
| Data DomainConstructor Source # | |
| Ord DomainConstructor Source # | |
| Show DomainConstructor Source # | |
data DomainConstructorArg Source #
Constructors
| DomainConstructorArg | |
Fields
| |
Instances
| Eq DomainConstructorArg Source # | |
| Data DomainConstructorArg Source # | |
| Ord DomainConstructorArg Source # | |
| Show DomainConstructorArg Source # | |
Constructors
| FunSig | |
Fields
| |
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] |
Constructors
| Term Term | |
| Conditional [Term] Term |
mkRefuteSen :: Term -> Sentence Source #
type LocaleDecl = ([String], [(String, Term)], [(String, Term)], [(String, Typ, Maybe AltSyntax)]) Source #
type Locales = Map String LocaleDecl Source #
Constructors
| TySg | |
isSubTypeSig :: TypeSig -> TypeSig -> Bool Source #
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 |
Constructors
| Sign | |
Instances
type DomainTab = [[DomainEntry]] Source #
Constructors
| IsaProof | |
Fields
| |
data ProofCommand Source #
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 |
Instances
| Eq ProofCommand Source # | |
| Data ProofCommand Source # | |
| Ord ProofCommand Source # | |
| Show ProofCommand Source # | |
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 Source #
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 |
Instances
| Eq ProofMethod Source # | |
| Data ProofMethod Source # | |
| Ord ProofMethod Source # | |
| Show ProofMethod Source # | |
toIsaProof :: ProofEnd -> IsaProof Source #