{-

sublanguage of CASL: FinCommSubPCFOL=

signatures:

finite set of sorts

local top elements

see CASL.Sublogic, add beyondCommSubPCFOL field to CASL_Sublogics

adapt functions

is_in_sign :: CASL -> CASL_Sublogics -> Sign () () -> Bool

(you need to test only if beyondCommSubPCFOL==False)

min_sublogic_sign :: CASL -> Sign () () -> CASL_Sublogics

(test signature, set beyondCommSubPCFOL=False if test succeeds)

proj_sublogic_sign :: CASL -> CASL_Sublogics -> Sign () () -> Sign () ()

(if beyondCommSubPCFOL=False, then remove all components without top)

signature morphisms:

refl, non-ext

adapt functions

is_in_morphism :: CASL -> CASL_Sublogics -> Morphism () () () -> Bool

(you need to test only if beyondCommSubPCFOL==False)

min_sublogic_morphism :: CASL -> Morphism () () () -> CASL_Sublogics

(test signature, set beyondCommSubPCFOL=False if test succeeds)

proj_sublogic_morphism :: CASL -> CASL_Sublogics -> Morphism () () () -> Morphism () () ()

(if beyondCommSubPCFOL=False, then remove all components without top)

formulas are those of CASL (i.e. not all of FinCommSubPFOL= as in the paper)

translation FinCommSubPCFOL= to CASL (comorphism FinCommSubPCFOL2CASL)

signature translation:

FinCommSubPFOL=-signature to CASL signature (construction of alphabet, see paper)

see CASL.Sign, Data.Set, Data.Map, Common.Lib.Rel

+ axioms (see paper p. 28f.) for construction of quotient of sum of types

see CASL.AS_BASIC_CASL.hs, datatype FORMULA

sentence translation: identity

first step (hybrid system) comorphism CASL to IsabelleCspProver

use FinCommSubPCFOL2CASL

on the output, use CASL2PCFOL; PFCOL2CFOL; CASL2IsabelleHOL

(code out subsorts, code out partiality, translate to Isabelle syntax)

for the resulting Isabelle signature:

chage "basesig" (see Isabelle.IsaSign) into "CspProver"

full step CspCASL -> Isabelle-CspProver

signature translation :

use CASL2IsabelleCspProver

translate process names into constants of process type

channels? code them out before data construction

formula translation

process equation systems -> Isabelle

(reusing CASL terms -> Isabelle

+ using CSP infrastructure of CSP-Prover)

refinement/views in CspCASL then state

"each refinement of Sp1 is a refinement of Sp2"

Csp-Prover should prove that this is equivalent to

"Sp2 is a refinement of Sp1"

-}