Copyright	(c) Liam O'Reilly and Markus Roggenbach, Swansea University 2008
License	GPLv2 or higher, see LICENSE.txt
Maintainer	csliam@swansea.ac.uk
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

CspCASLProver.Consts

Description

Constants and related fucntions for CspCASLProver.

Synopsis

Documentation

alphabetS :: String

Name for the CspCASLProver's Alphabet

alphabetType :: Typ

Type for the CspCASLProver's Alphabet

binEq_PreAlphabet :: Term -> Term -> Term

Isabelle fucntion to compare eqaulity of two elements of the PreAlphabet.

classOp :: Term -> Term

Isabelle operation for the class operation

classS :: String

String for the class operation

convertChannelString :: CHANNEL_NAME -> String

Function that takes a channel name produces the CspCASLProver's constructor for that channel.

convertFQProcessName2String :: FQ_PROCESS_NAME -> String

Convert a process name to a string

convertSort2String :: SORT -> String

Convert a SORT to a string

cspFThyS :: String

Theory file name for CSP_F of CSP-Prover

eq_PreAlphabetS :: String

String of the name of the function to compare eqaulity of two elements of the PreAlphabet.

eq_PreAlphabetV :: VName

VName of the name of the function to compare eqaulity of two elements of the PreAlphabet.

equivTypeClassS :: String

String for the name of the axiomatic type class of equivalence relations part 2

eventS :: String

String of the name of CspCASLProver's Event datatype.

eventType :: Typ

Type for the CspCASLProver's Event datatype

flatS :: String

String of the name of constructor for a plain event without a channel, effectivly this is the channel whos name is Flat. Also used for the names of the flat types.

flatOp :: Term -> Term

Function that takes a Term and adds a flat around it

preAlphabetQuotType :: Typ

Type for CspCASLProver's preAlphabet quot

preAlphabetS :: String

Name for CspCASLProver's PreAlphabet

preAlphabetSimS :: String

preAlphabetType :: Typ

Type for CspCASLProver's PreAlphabet

projFlatS :: String

Name of CspCASLProver's function for projecting a Flat Event back to the type Alphabet

projFlatOp :: Term -> Term

Apply the CspCASLProvers projFlat function to an isabelle term

lemmasCCProverDecompositionThmsS :: String

Name for the lemma which is the collection of our decomposition axioms that we produce.

lemmasCCProverInjectivityThmsS :: String

Name for the lemma which is the collection of our injectivity axioms that we produce.

lemmasEmbInjAxS :: String

Name for the lemma which is the collection of embedding injectivity axioms.

lemmasIdentityAxS :: String

Name for the lemma which is the collection of identity axioms.

lemmasNotDefBotAxS :: String

Name for the lemma which is the collection of not defined bottom axioms.

lemmasTotalityAxS :: String

Name for the lemma which is the collection of totality axioms.

lemmasTransAxS :: String

Name for the lemma which is the collection of transitivity axioms.

mkChooseFunName :: SORT -> String

Function that takes a sort and outputs the function name for the corresponing choose function

mkChooseFunOp :: SORT -> Term -> Term

Function that takes a sort and outputs the Isabelle function for the corresponing choose function

mkCompareWithFunName :: SORT -> String

Function that takes a sort and outputs the function name for the corresponing compare_with function

mkPreAlphabetConstructor :: SORT -> String

Function that returns the constructor of PreAlphabet for a given sort

mkPreAlphabetConstructorOp :: SORT -> Term -> Term

Function that returns the (Isabelle function for the) constructor of PreAlphabet for a given sort

mkProcNameConstructor :: FQ_PROCESS_NAME -> String

Given a process name this fucntion returns a unique constructor for that process name. This is a helper functin when buildign the process name data type.

mkSortBarAbsString :: SORT -> String

Given a sort this function produces the function name (string) of the built in Isabelle fucntion that corresponds to the abstraction function of the type that sort_bar.

mkSortBarAbsOp :: SORT -> Term -> Term

Given a sort this function produces the a function on the abstract syntax of Isabelle that represents the built in Isabelle fucntion that corresponds to the abstraction function of the type sort_bar.

mkSortBarRepOp :: SORT -> Term -> Term

Given a sort this function produces the a function on the abstract syntax of Isabelle that represents the built in Isabelle fucntion that corresponds to the representation function of the type sort_bar.

mkSortBarString :: SORT -> String

Converts a sort in to the corresponding bar sort represented as a string

mkSortBarType :: SORT -> Typ

Converts a sort in to the corresponding bar sort type

mkSortFlatString :: SORT -> String

Converts asort in to the corresponding flat type for that sort represented as a string. This is used in the construction of the channels and is linked with the type event.

mkThyNameAlphabet :: String -> String

Created a name for the theory file which stores the alphabet construction for CspCASLProver.

mkThyNameDataEnc :: String -> String

Created a name for the theory file which stores the data encoding for CspCASLProver.

mkThyNameIntThms :: String -> String

Created a name for the theory file which stores the Integration Theorems for CspCASLProver.

mkThyNamePreAlphabet :: String -> String

Created a name for the theory file which stores the Alphabet construction and instances code for CspCASLProver.

procMapS :: String

Name for CspCASLProver's function for mapping process names to actual processes

procMapType :: Typ

Type for CspCASLProver's function for mapping process names to actual processes

procNameType :: Typ

Type for CspCASLProver's datatype of process names

quotEqualityS :: String

quotientThyS :: String

reflexivityTheoremS :: String

symmetryTheoremS :: String

transitivityS :: String