Hets - the Heterogeneous Tool Set

Copyright(c) Liam O'Reilly and Markus Roggenbach
Swansea University 2009
LicenseGPLv2 or higher, see LICENSE.txt
Maintainercsliam@swansea.ac.uk
Stabilityprovisional
Portabilityportable
Safe HaskellNone

CspCASLProver.IsabelleUtils

Description

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

Synopsis

Documentation

addConst :: String -> Typ -> IsaTheory -> IsaTheory Source #

Add a single constant to the signature of an Isabelle theory

addDef :: String -> Term -> Term -> IsaTheory -> IsaTheory Source #

Function to add a def command to an Isabelle theory

addInstanceOf :: String -> [Sort] -> Sort -> [(String, Term)] -> IsaProof -> IsaTheory -> IsaTheory Source #

Function to add an instance of command to an Isabelle theory. The sort parameters here are basically strings.

addLemmasCollection :: String -> [String] -> IsaTheory -> IsaTheory Source #

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 Source #

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 Source #

Add a theorem with proof to an Isabelle theory

updateDomainTab :: DomainEntry -> IsaTheory -> IsaTheory Source #

Add a DomainEntry to the domain tab of an Isabelle signature.

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

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