CoCFOL2IsabelleHOL.hs revision d877a849f19860d779f44cb9a06df127975383e8
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) Till Mossakowski and Uni Bremen 2003-2005
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuMaintainer : hausmann@tzi.de
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuStability : provisional
431571057e88a650a974adec93ea4bb5173b6213Felix Gabriel MancePortability : non-portable (imports Logic.Logic)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuThe embedding comorphism from CoCASL to Isabelle-HOL.
19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance encoding of cofreeness
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mancemodule Comorphisms.CoCFOL2IsabelleHOL where
1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Isabelle.IsaSign as IsaSign
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | The identity of the comorphism
27fdf879983dd28e211b41f3be6c0e930b7c816bFelix Gabriel Mancedata CoCFOL2IsabelleHOL = CoCFOL2IsabelleHOL deriving (Show)
1a38107941725211e7c3f051f7a8f5e12199f03acmaederinstance Language CoCFOL2IsabelleHOL -- default definition is okay
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuinstance Comorphism CoCFOL2IsabelleHOL
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu CoCASL CoCASL.Sublogic.CoCASL_Sublogics
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu CASL.Morphism.Symbol CASL.Morphism.RawSymbol ()
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu Isabelle () () IsaSign.Sentence () ()
be00381168b3f10192afabbba136fb06d3a9f358Christian Maeder IsabelleMorphism () () () where
be00381168b3f10192afabbba136fb06d3a9f358Christian Maeder sourceLogic CoCFOL2IsabelleHOL = CoCASL
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu sourceSublogic CoCFOL2IsabelleHOL =
27fdf879983dd28e211b41f3be6c0e930b7c816bFelix Gabriel Mance CASL_SL { sub_features = NoSub,
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu has_part = False,
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu cons_features = SortGen { emptyMapping = False,
27fdf879983dd28e211b41f3be6c0e930b7c816bFelix Gabriel Mance onlyInjConstrs = False},
d0f58d27c2536eba454d8f77de8617bc6a2c99cdFelix Gabriel Mance has_eq = True,
d0f58d27c2536eba454d8f77de8617bc6a2c99cdFelix Gabriel Mance has_pred = True,
d0f58d27c2536eba454d8f77de8617bc6a2c99cdFelix Gabriel Mance which_logic = FOL
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu targetLogic CoCFOL2IsabelleHOL = Isabelle
27fdf879983dd28e211b41f3be6c0e930b7c816bFelix Gabriel Mance targetSublogic CoCFOL2IsabelleHOL = ()
424860079d47bf490fa98d5d7498096a0447c569mcodescu map_theory CoCFOL2IsabelleHOL = transTheory sigTrCoCASL formTrCoCASL
60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel Mance map_morphism CoCFOL2IsabelleHOL mor = do
60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel Mance (sig1,_) <- map_sign CoCFOL2IsabelleHOL (Logic.dom CoCASL mor)
0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maeder (sig2,_) <- map_sign CoCFOL2IsabelleHOL (cod CoCASL mor)
424860079d47bf490fa98d5d7498096a0447c569mcodescu inclusion Isabelle sig1 sig2
424860079d47bf490fa98d5d7498096a0447c569mcodescu map_sentence CoCFOL2IsabelleHOL sign =
424860079d47bf490fa98d5d7498096a0447c569mcodescu return . mapSen formTrCoCASL sign
60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel Mance map_symbol CoCFOL2IsabelleHOL _ = error "CoCFOL2IsabelleHOL.map_symbol"
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | extended signature translation for CoCASL
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiusigTrCoCASL :: SignTranslator C_FORMULA CoCASLSign
60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel MancesigTrCoCASL _ _ = id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiuconjs :: [Term] -> Term
60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel Manceconjs l = if null l then true else foldr1 binConj l
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu-- | extended formula translation for CoCASL
7852de3551fc797566ee71165bafe05b6d81728cnotanartistformTrCoCASL :: FormulaTranslator C_FORMULA CoCASLSign
80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskiformTrCoCASL sign (CoSort_gen_ax sorts ops _) =
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski foldr (quantifyIsa "All") phi (predDecls++[("u",ts),("v",ts)])
0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maeder ts = transSort $ head sorts
0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maeder -- phi expresses: all bisimulations are the equality
424860079d47bf490fa98d5d7498096a0447c569mcodescu phi = prems `binImpl` concls
0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maeder -- indices and predicates for all involved sorts
0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maeder indices = [0..length sorts - 1]
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu predDecls = zip [rvar i | i<-indices] (map binPred sorts)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu binPred s = let s' = transSort s in mkCurryFunType [s',s'] boolType
d0f58d27c2536eba454d8f77de8617bc6a2c99cdFelix Gabriel Mance -- premises: all relations are bisimulations
60f30f0eeeacdfc1e0dfe39664373ddf5a0675adFelix Gabriel Mance prems = conjs (map prem (zip sorts indices))
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu {- generate premise for s, where s is the i-th sort
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu for all x,y of that sort,
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu if all sel_j(x) R_j sel_j(y), where sel_j ranges over the selectors for s
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu here, R_i is the relation for the result type of sel_j, or the equality
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let -- get all selectors with first argument sort s
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu sels = filter isSelForS ops
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu isSelForS (Qual_op_name _ t _) = case args_OP_TYPE t of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (s1:_) -> s1 == s
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder isSelForS _ = False
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder premSel opsymb@(Qual_op_name _n t _) =
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu let -- get extra parameters of the selectors
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu args = tail $ args_OP_TYPE t
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu indicesArgs = [1..length args]
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu res = res_OP_TYPE t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- variables for the extra parameters
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu varDecls = zip [xvar j | j <- indicesArgs] (map transSort args)
31e9d2a02e15b7dbc157e0d3fb3b84f6c8666482Christian Maeder -- the selector ...
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu topC = con (transOP_SYMB sign opsymb)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu -- applied to x and extra parameter vars
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder appFold = foldl ( \ t1 t2 -> App t1 t2 NotCont)
d3cb3401882f6956de016f8eecbec1cd3b868acbFelix Gabriel Mance rhs = appFold (App topC (var "x") NotCont)
d3cb3401882f6956de016f8eecbec1cd3b868acbFelix Gabriel Mance (map (var . xvar) indicesArgs)
d3cb3401882f6956de016f8eecbec1cd3b868acbFelix Gabriel Mance -- applied to y and extra parameter vars
d3cb3401882f6956de016f8eecbec1cd3b868acbFelix Gabriel Mance lhs = appFold (App topC (var "y") NotCont)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu (map (var . xvar) indicesArgs)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu chi = -- is the result of selector non-observable?
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu if res `elem` sorts
7852de3551fc797566ee71165bafe05b6d81728cnotanartist -- then apply corresponding relation
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu then App (App (var $
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu rvar $ maybe (error "CoCASL2Isabelle.premSel.chi") id
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu $ findIndex (==res) sorts)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu rhs NotCont) lhs NotCont
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu -- else use equality
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu else binEq rhs lhs
0dd6e7830de0887c9a12356447975a826b3b3db2Christian Maeder in foldr (quantifyIsa "All") chi varDecls
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu premSel _ = error "CoCASL2Isabelle.premSel"
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu prem1 = conjs (map premSel sels)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu concl1 = App (App (var $ rvar i) (var "x") NotCont) (var "y") NotCont
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu psi = concl1 `binImpl` prem1
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu typS = transSort s
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu in foldr (quantifyIsa "All") psi [("x",typS),("y",typS)]
06acd8a23b2f06e7b2373d53f738cf56c7f03223Francisc Nicolae Bungiu -- conclusion: all relations are the equality
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu concls = conjs (map concl (zip sorts indices))
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu concl (_,i) = binImpl (App (App (var $ rvar i) (var "u") NotCont)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu (var "v") NotCont)
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae Bungiu (binEq (var "u") (var "v"))
ee93ea764a2b8189253e912c8447f9419033f6d4Francisc Nicolae BungiuformTrCoCASL _sign (BoxOrDiamond _ _mod _phi _) =
7852de3551fc797566ee71165bafe05b6d81728cnotanartist trace "WARNING: ignoring modal forumla"