Hets - the Heterogeneous Tool Set

Copyright(c) Liam O'Reilly and Markus Roggenbach, Swansea University 2009
LicenseGPLv2 or higher, see LICENSE.txt
Safe HaskellNone



Utilities for CspCASLProver related to Isabelle. The functions here typically manipulate Isabelle signatures.



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.

writeIsaTheory :: String -> Theory Sign Sentence () -> IO ()

Write out an Isabelle Theory. The theory should just run through in Isabelle without any user interactions. This is based heavily off Isabelle.IsaProve.isaProve