Documentation

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

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

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

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

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.

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)

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

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

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).

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

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)

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

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.

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

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

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.