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

alphabetS :: String
alphabetType :: Typ
binEq_PreAlphabet :: Term -> Term -> Term
classOp :: Term -> Term
classS :: String
convertChannelString :: CHANNEL_NAME -> String
convertFQProcessName2String :: FQ_PROCESS_NAME -> String
convertSort2String :: SORT -> String
cspFThyS :: String
eq_PreAlphabetS :: String
eq_PreAlphabetV :: VName
equivTypeClassS :: String
eventS :: String
eventType :: Typ
flatS :: String
flatOp :: Term -> Term
preAlphabetQuotType :: Typ
preAlphabetS :: String
preAlphabetSimS :: String
preAlphabetType :: Typ
projFlatS :: String
projFlatOp :: Term -> Term
lemmasCCProverDecompositionThmsS :: String
lemmasCCProverInjectivityThmsS :: String
lemmasEmbInjAxS :: String
lemmasIdentityAxS :: String
lemmasNotDefBotAxS :: String
lemmasTotalityAxS :: String
lemmasTransAxS :: String
mkChooseFunName :: SORT -> String
mkChooseFunOp :: SORT -> Term -> Term
mkCompareWithFunName :: SORT -> String
mkPreAlphabetConstructor :: SORT -> String
mkPreAlphabetConstructorOp :: SORT -> Term -> Term
mkProcNameConstructor :: FQ_PROCESS_NAME -> String
mkSortBarAbsString :: SORT -> String
mkSortBarAbsOp :: SORT -> Term -> Term
mkSortBarRepOp :: SORT -> Term -> Term
mkSortBarString :: SORT -> String
mkSortBarType :: SORT -> Typ
mkSortFlatString :: SORT -> String
mkThyNameAlphabet :: String -> String
mkThyNameDataEnc :: String -> String
mkThyNameIntThms :: String -> String
mkThyNamePreAlphabet :: String -> String
procMapS :: String
procMapType :: Typ
procNameType :: Typ
quotEqualityS :: String
quotientThyS :: String
reflexivityTheoremS :: String
symmetryTheoremS :: String
transitivityS :: String

Documentation

alphabetS :: String Source #

Name for the CspCASLProver's Alphabet

alphabetType :: Typ Source #

Type for the CspCASLProver's Alphabet

binEq_PreAlphabet :: Term -> Term -> Term Source #

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

classOp :: Term -> Term Source #

Isabelle operation for the class operation

classS :: String Source #

String for the class operation

convertChannelString :: CHANNEL_NAME -> String Source #

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

convertFQProcessName2String :: FQ_PROCESS_NAME -> String Source #

Convert a process name to a string

convertSort2String :: SORT -> String Source #

Convert a SORT to a string

cspFThyS :: String Source #

Theory file name for CSP_F of CSP-Prover

eq_PreAlphabetS :: String Source #

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

eq_PreAlphabetV :: VName Source #

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

equivTypeClassS :: String Source #

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

eventS :: String Source #

String of the name of CspCASLProver's Event datatype.

eventType :: Typ Source #

Type for the CspCASLProver's Event datatype

flatS :: String Source #

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

Function that takes a Term and adds a flat around it

preAlphabetQuotType :: Typ Source #

Type for CspCASLProver's preAlphabet quot

preAlphabetS :: String Source #

Name for CspCASLProver's PreAlphabet

preAlphabetSimS :: String Source #

preAlphabetType :: Typ Source #

Type for CspCASLProver's PreAlphabet

projFlatS :: String Source #

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

projFlatOp :: Term -> Term Source #

Apply the CspCASLProvers projFlat function to an isabelle term

lemmasCCProverDecompositionThmsS :: String Source #

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

lemmasCCProverInjectivityThmsS :: String Source #

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

lemmasEmbInjAxS :: String Source #

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

lemmasIdentityAxS :: String Source #

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

lemmasNotDefBotAxS :: String Source #

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

lemmasTotalityAxS :: String Source #

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

lemmasTransAxS :: String Source #

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

mkChooseFunName :: SORT -> String Source #

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

mkChooseFunOp :: SORT -> Term -> Term Source #

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

mkCompareWithFunName :: SORT -> String Source #

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

mkPreAlphabetConstructor :: SORT -> String Source #

Function that returns the constructor of PreAlphabet for a given sort

mkPreAlphabetConstructorOp :: SORT -> Term -> Term Source #

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

mkProcNameConstructor :: FQ_PROCESS_NAME -> String Source #

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

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

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

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

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

mkSortBarType :: SORT -> Typ Source #

Converts a sort in to the corresponding bar sort type

mkSortFlatString :: SORT -> String Source #

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

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

mkThyNameDataEnc :: String -> String Source #

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

mkThyNameIntThms :: String -> String Source #

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

mkThyNamePreAlphabet :: String -> String Source #

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

procMapS :: String Source #

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

procMapType :: Typ Source #

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

procNameType :: Typ Source #

Type for CspCASLProver's datatype of process names

quotEqualityS :: String Source #

quotientThyS :: String Source #

reflexivityTheoremS :: String Source #

symmetryTheoremS :: String Source #

transitivityS :: String Source #