| Copyright | (c) Liam O'Reilly and Markus Roggenbach, Swansea University 2009 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | csliam@swansea.ac.uk |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | None |
CspCASLProver.IsabelleUtils
Description
Utilities for CspCASLProver related to Isabelle. The functions here typically manipulate Isabelle signatures.
- addConst :: String -> Typ -> IsaTheory -> IsaTheory
- addDef :: String -> Term -> Term -> IsaTheory -> IsaTheory
- addInstanceOf :: String -> [Sort] -> Sort -> [(String, Term)] -> IsaProof -> IsaTheory -> IsaTheory
- addLemmasCollection :: String -> [String] -> IsaTheory -> IsaTheory
- addPrimRec :: String -> Typ -> [Term] -> IsaTheory -> IsaTheory
- addTheoremWithProof :: String -> [Term] -> Term -> IsaProof -> IsaTheory -> IsaTheory
- updateDomainTab :: DomainEntry -> IsaTheory -> IsaTheory
- writeIsaTheory :: String -> Theory Sign Sentence () -> IO ()
Documentation
addConst :: String -> Typ -> IsaTheory -> IsaTheory
Add a single constant to the signature of an Isabelle theory
addDef :: String -> Term -> Term -> IsaTheory -> IsaTheory
Function to add a def command to an Isabelle theory
addInstanceOf :: String -> [Sort] -> Sort -> [(String, Term)] -> IsaProof -> IsaTheory -> IsaTheory
Function to add an instance of command to an Isabelle theory. The sort parameters here are basically strings.
addLemmasCollection :: String -> [String] -> IsaTheory -> IsaTheory
Add a lemmas sentence (definition) that allow us to group large collections of lemmas in to a single lemma. This cuts down on the repreated addition of lemmas in the proofs.
addPrimRec :: String -> Typ -> [Term] -> IsaTheory -> IsaTheory
Add a constant with a primrec defintion to the sentences of an Isabelle theory. Parameters: constant name, type, primrec defintions and isabelle theory to be added to.
addTheoremWithProof :: String -> [Term] -> Term -> IsaProof -> IsaTheory -> IsaTheory
Add a theorem with proof to an Isabelle theory
updateDomainTab :: DomainEntry -> IsaTheory -> IsaTheory
Add a DomainEntry to the domain tab of an Isabelle signature.