5394N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

5394N/A{- |

5394N/AModule : $Header$

5394N/ADescription : Extension of CFOL2IsabelleHOL to CoCASL

5394N/ACopyright : (c) Till Mossakowski and Uni Bremen 2003-2005

5394N/ALicense : GPLv2 or higher, see LICENSE.txt

5394N/A

5394N/AMaintainer : hausmann@informatik.uni-bremen.de

5394N/AStability : provisional

5394N/APortability : non-portable (imports Logic.Logic)

5394N/A

5394N/AThe embedding comorphism from CoCASL to Isabelle-HOL.

5394N/A-}

5394N/A

5394N/Amodule Comorphisms.CoCFOL2IsabelleHOL (CoCFOL2IsabelleHOL (..)) where

5394N/A

5394N/Aimport Logic.Logic as Logic

5394N/Aimport Logic.Comorphism

5394N/A-- CoCASL

5394N/Aimport CoCASL.Logic_CoCASL

5394N/Aimport CoCASL.CoCASLSign

5394N/Aimport CoCASL.AS_CoCASL

5394N/Aimport CoCASL.StatAna

5394N/Aimport CoCASL.Sublogic

6238N/A

5394N/Aimport CASL.Sublogic as SL

5394N/Aimport CASL.AS_Basic_CASL

5394N/Aimport CASL.Sign

5394N/Aimport CASL.Morphism

5394N/A

5394N/Aimport Comorphisms.CFOL2IsabelleHOL

5394N/A

5394N/A-- Isabelle

5394N/Aimport Isabelle.IsaSign as IsaSign

5394N/Aimport Isabelle.IsaConsts

5394N/Aimport Isabelle.Logic_Isabelle

5394N/A

5394N/Aimport Common.Utils (number)

5394N/A

6399N/Aimport Data.Char (ord, chr)

5394N/Aimport Data.Maybe (fromMaybe)

5394N/A

5394N/A-- | The identity of the comorphism

5394N/Adata CoCFOL2IsabelleHOL = CoCFOL2IsabelleHOL deriving Show

6399N/A

5394N/Ainstance Language CoCFOL2IsabelleHOL where

5394N/A language_name CoCFOL2IsabelleHOL = "CoCASL2Isabelle"

5394N/A

5394N/Ainstance Comorphism CoCFOL2IsabelleHOL

5394N/A CoCASL CoCASL_Sublogics

5714N/A C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

5394N/A CSign

6399N/A CoCASLMor

6399N/A Symbol RawSymbol ()

6399N/A Isabelle () () IsaSign.Sentence () ()

5394N/A IsaSign.Sign

5394N/A IsabelleMorphism () () () where

5394N/A sourceLogic CoCFOL2IsabelleHOL = CoCASL

5394N/A sourceSublogic CoCFOL2IsabelleHOL = SL.cFol

6399N/A targetLogic CoCFOL2IsabelleHOL = Isabelle

5394N/A mapSublogic cid sl = if sl `isSubElem` sourceSublogic cid

5394N/A then Just () else Nothing

5394N/A map_theory CoCFOL2IsabelleHOL =

5394N/A return . transTheory sigTrCoCASL formTrCoCASL

5394N/A map_sentence CoCFOL2IsabelleHOL sign =

5394N/A return . mapSen formTrCoCASL sign (typeToks sign)

5394N/A has_model_expansion CoCFOL2IsabelleHOL = True

5394N/A is_weakly_amalgamable CoCFOL2IsabelleHOL = True

5394N/A

5394N/Axvar :: Int -> String

5394N/Axvar i = if i <= 26 then [chr (i + ord 'a')] else 'x' : show i

6238N/A

5947N/Arvar :: Int -> String

5947N/Arvar i = if i <= 9 then [chr (i + ord 'R' )] else 'R' : show i

5947N/A

5947N/A-- | extended signature translation for CoCASL

5947N/AsigTrCoCASL :: SignTranslator C_FORMULA CoCASLSign

5947N/AsigTrCoCASL _ _ = id

5947N/A

5947N/Aconjs :: [Term] -> Term

5947N/Aconjs l = if null l then true else foldr1 binConj l

5947N/A

5947N/A-- | extended formula translation for CoCASL

5947N/AformTrCoCASL :: FormulaTranslator C_FORMULA CoCASLSign

5947N/AformTrCoCASL sign tyToks (CoSort_gen_ax sorts ops _) =

5947N/A foldr (quantifyIsa "All") phi $ predDecls ++ [("u", ts), ("v", ts)]

5947N/A where

5947N/A ts = transSort $ head sorts

5947N/A -- phi expresses: all bisimulations are the equality

5947N/A phi = prems `binImpl` concls

5947N/A -- indices and predicates for all involved sorts

5394N/A indexedSorts = number sorts

5394N/A predDecls = map (\ (s, i) -> (rvar i, binPred s)) indexedSorts

5395N/A binPred s = let s' = transSort s in mkCurryFunType [s', s'] boolType

5394N/A -- premises: all relations are bisimulations

5394N/A prems = conjs (map prem indexedSorts)

5394N/A {- generate premise for s, where s is the i-th sort

5394N/A for all x,y of that sort,

5394N/A if all sel_j(x) R_j sel_j(y), where sel_j ranges over the selectors for s

5394N/A then x R y

5947N/A here, R_i is the relation for the result type of sel_j, or the equality

5394N/A -}

5394N/A prem (s, i) =

5394N/A let -- get all selectors with first argument sort s

5394N/A sels = filter isSelForS ops

5394N/A isSelForS (Qual_op_name _ t _) = case args_OP_TYPE t of

5394N/A s1 : _ -> s1 == s

5394N/A _ -> False

5394N/A isSelForS _ = False

5394N/A premSel opsymb@(Qual_op_name _n t _) =

5394N/A let -- get extra parameters of the selectors

5394N/A args = tail $ args_OP_TYPE t

5394N/A indicesArgs = number args

5394N/A res = res_OP_TYPE t

5394N/A -- variables for the extra parameters

5394N/A varDecls = map (\ (a, j) -> (xvar j, transSort a))

5394N/A indicesArgs

5394N/A -- the selector ...

5394N/A topC = con (transOpSymb sign tyToks opsymb)

5394N/A -- applied to x and extra parameter vars

5394N/A appFold = foldl termAppl

5394N/A rhs = appFold (termAppl topC $ mkFree "x")

5394N/A $ map (mkFree . xvar . snd) indicesArgs

5394N/A -- applied to y and extra parameter vars

5457N/A lhs = appFold (termAppl topC $ mkFree "y")

5394N/A $ map (mkFree . xvar . snd) indicesArgs

5394N/A chi = -- is the result of selector non-observable?

5394N/A if res `elem` sorts

5423N/A -- then apply corresponding relation

5947N/A then termAppl (termAppl (mkFree $

5947N/A rvar $ fromMaybe

5947N/A (error "CoCASL2Isabelle.premSel.chi")

5947N/A $ lookup res indexedSorts )

5947N/A rhs) lhs

5947N/A -- else use equality

5947N/A else binEq rhs lhs

5947N/A in foldr (quantifyIsa "All") chi varDecls

5947N/A premSel _ = error "CoCASL2Isabelle.premSel"

5947N/A prem1 = conjs (map premSel sels)

5947N/A concl1 = termAppl (termAppl (mkFree $ rvar i) $ mkFree "x")

5947N/A (mkFree "y")

5443N/A psi = concl1 `binImpl` prem1

5423N/A typS = transSort s

5423N/A in foldr (quantifyIsa "All") psi [("x", typS), ("y", typS)]

5454N/A -- conclusion: all relations are the equality

5423N/A concls = conjs (map concl indexedSorts)

5423N/A concl (_, i) = binImpl (termAppl (termAppl (mkFree $ rvar i) $ mkFree "u")

5454N/A $ mkFree "v")

5454N/A $ binEq (mkFree "u") $ mkFree "v"

5454N/AformTrCoCASL _sign _ (BoxOrDiamond _ _mod _phi _) =

5454N/A error "CoCFOL2IsabelleHOL.formTrCoCASL.BoxOrDiamond"

5423N/A