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 #