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 |

Utilities for CspCASLProver related to the actual construction of Isabelle theories.

- addAlphabetType :: IsaTheory -> IsaTheory
- addAllBarTypes :: [SORT] -> IsaTheory -> IsaTheory
- addAllChooseFunctions :: [SORT] -> IsaTheory -> IsaTheory
- addAllCompareWithFun :: CASLSign -> IsaTheory -> IsaTheory
- addAllIntegrationTheorems :: [SORT] -> CASLSign -> IsaTheory -> IsaTheory
- addAllGaAxiomsCollections :: CASLSign -> CASLSign -> IsaTheory -> IsaTheory
- addEqFun :: [SORT] -> IsaTheory -> IsaTheory
- addEventDataType :: Rel SORT -> ChanNameMap -> IsaTheory -> IsaTheory
- addFlatTypes :: [SORT] -> IsaTheory -> IsaTheory
- addInstanceOfEquiv :: IsaTheory -> IsaTheory
- addJustificationTheorems :: CASLSign -> CASLSign -> IsaTheory -> IsaTheory
- addPreAlphabet :: [SORT] -> IsaTheory -> IsaTheory
- addProcMap :: [Named CspCASLSen] -> CspCASLSign -> Sign () () -> Sign () () -> IsaTheory -> IsaTheory
- addProcNameDatatype :: CspSign -> IsaTheory -> IsaTheory
- addProjFlatFun :: IsaTheory -> IsaTheory
- addProcTheorems :: [Named CspCASLSen] -> CspCASLSign -> Sign () () -> Sign () () -> IsaTheory -> IsaTheory

# Documentation

addAlphabetType :: IsaTheory -> IsaTheory

Function to add the Alphabet type (type syonnym) to an Isabelle theory

addAllBarTypes :: [SORT] -> IsaTheory -> IsaTheory

Function to add all the bar types to an Isabelle theory.

addAllChooseFunctions :: [SORT] -> IsaTheory -> IsaTheory

Add all choose functions for a given list of sorts to an Isabelle theory.

addAllCompareWithFun :: CASLSign -> IsaTheory -> IsaTheory

Add all compare_with functions for a given list of sorts to an Isabelle theory. We need to know about the casl signature (data part of a CspCASL spec) so that we can pass it on to the addCompareWithFun function

addAllIntegrationTheorems :: [SORT] -> CASLSign -> IsaTheory -> IsaTheory

Add all the integration theorems. We need to know all the sorts to produce all the theorems. We need to know the CASL signature of the data part to pass it on as an argument.

addAllGaAxiomsCollections :: CASLSign -> CASLSign -> IsaTheory -> IsaTheory

Add a series of lemmas sentences that collect together all the automatically generate axioms. This 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. We need to the CASL signature (from the datapart) and the PFOL Signature to pass it on. We could recalculate the PFOL signature from the CASL signature here, but we dont as it can be passed in. We need the PFOL signature which is the data part CASL signature after translation to PCFOL (i.e. without subsorting)

addEqFun :: [SORT] -> IsaTheory -> IsaTheory

Add the eq function to an Isabelle theory using a list of sorts

addEventDataType :: Rel SORT -> ChanNameMap -> IsaTheory -> IsaTheory

Add the Event datatype (built from a list of channels and the subsort relation) to an Isabelle theory.

addFlatTypes :: [SORT] -> IsaTheory -> IsaTheory

Function to add all the Flat types. These capture the original sorts, but use the bar values instead wrapped up in the Flat constructor(the Flat channel). We use this as a set of normal communications (action prefix, send, recieve).

addInstanceOfEquiv :: IsaTheory -> IsaTheory

Function to add preAlphabet as an equivalence relation to an Isabelle theory

addJustificationTheorems :: CASLSign -> CASLSign -> IsaTheory -> IsaTheory

Add all justification theorems to an Isabelle Theory. We need to the CASL signature (from the datapart) and the PFOL Signature to pass it on. We could recalculate the PFOL signature from the CASL signature here, but we dont as it can be passed in. We need the PFOL signature which is the data part CASL signature after translation to PCFOL (i.e. without subsorting)

addPreAlphabet :: [SORT] -> IsaTheory -> IsaTheory

Add the PreAlphabet (built from a list of sorts) to an Isabelle theory.

addProcMap :: [Named CspCASLSen] -> CspCASLSign -> Sign () () -> Sign () () -> IsaTheory -> IsaTheory

Add the function procMap to an Isabelle theory. This function maps process names to real processes build using the same names and the alphabet i.e., in CSP-Prover syntax: ProcName => (ProcName, Alphabet) proc. We need to know the CspCASL sentences and the casl signature (data part). We need the PCFOL and CFOL signatures of the data part after translation to PCFOL and CFOL to pass along the process translation.

addProcNameDatatype :: CspSign -> IsaTheory -> IsaTheory

Add process name datatype which has a constructor for each process name (along with the arguments for the process) in the CspCASL Signature to an Isabelle theory

addProjFlatFun :: IsaTheory -> IsaTheory

Add the eq function to an Isabelle theory using a list of sorts

addProcTheorems :: [Named CspCASLSen] -> CspCASLSign -> Sign () () -> Sign () () -> IsaTheory -> IsaTheory

Add the implied process equations as theorems to be proven by the user. We need to know the CspCASL sentences and the casl signature (data part). We need the PCFOL and CFOL signatures of the data part after translation to PCFOL and CFOL to pass along the process translation.