Utils.hs revision c3efd4f435e954846981cf46bca64e0485266634
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaModule : $Header$
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaDescription : Utilities for CspCASLProver related to the actual
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova construction of Isabelle theories.
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaCopyright : (c) Liam O'Reilly and Markus Roggenbach,
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu Swansea University 2009
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaMaintainer : csliam@swansea.ac.uk
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaStability : provisional
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaPortability : portable
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaUtilities for CspCASLProver related to the actual construction of
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina SojakovaIsabelle theories.
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova ( addAlphabetType
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova , addAllBarTypes
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova , addAllChooseFunctions
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova , addAllCompareWithFun
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova , addAllIntegrationTheorems
669b4334be8eb3313ca146137db1b83a8873632aKristina Sojakova , addInstansanceOfEquiv
669b4334be8eb3313ca146137db1b83a8873632aKristina Sojakova , addJustificationTheorems
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova , addPreAlphabet
0737dd44f9a47bb91233ffdb7a03bc657dfc7c5eKristina Sojakova , addProcNameDatatype
0737dd44f9a47bb91233ffdb7a03bc657dfc7c5eKristina Sojakovaimport CASL.AS_Basic_CASL (SORT, OpKind(..))
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport qualified CASL.Sign as CASLSign
669b4334be8eb3313ca146137db1b83a8873632aKristina Sojakovaimport qualified CASL.Inject as CASLInject
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Common.AS_Annotation (makeNamed, Named, SenAttr(..))
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport qualified Common.Lib.Rel as Rel
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport Comorphisms.CFOL2IsabelleHOL (IsaTheory)
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport CspCASL.AS_CspCASL_Process (PROCESS_NAME)
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakovaimport CspCASL.SignCSP (CspSign(..), ProcProfile(..), CspCASLSen(..)
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova , isProcessEq)
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport CspCASLProver.TransProcesses (transProcess)
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport qualified Data.List as List
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport qualified Data.Map as Map
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport qualified Data.Set as Set
669b4334be8eb3313ca146137db1b83a8873632aKristina Sojakova-------------------------------------------------------------------------
53d7a124a59889b9de5c6ffa856a5e697b043c90Kristina Sojakova-- Functions for adding the PreAlphabet datatype to an Isabelle theory --
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova-------------------------------------------------------------------------
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova-- | Add the PreAlphabet (built from a list of sorts) to an Isabelle
e7cedce0d43b62593b8d5d552bdc36eb5ba73409Kristina SojakovaaddPreAlphabet :: [SORT] -> IsaTheory -> IsaTheory
228124cdf2560445e7f1b5312476935b51887463Kristina SojakovaaddPreAlphabet sortList isaTh =
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova let preAlphabetDomainEntry = mkPreAlphabetDE sortList
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova -- Add to the isabelle signature the new domain entry
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova in updateDomainTab preAlphabetDomainEntry isaTh
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova-- | Make a Domain Entry for the PreAlphabet from a list of sorts.
228124cdf2560445e7f1b5312476935b51887463Kristina SojakovamkPreAlphabetDE :: [SORT] -> DomainEntry
228124cdf2560445e7f1b5312476935b51887463Kristina SojakovamkPreAlphabetDE sorts =
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova (Type {typeId = preAlphabetS, typeSort = [isaTerm], typeArgs = []},
53d7a124a59889b9de5c6ffa856a5e697b043c90Kristina Sojakova (mkVName (mkPreAlphabetConstructor sort),
669b4334be8eb3313ca146137db1b83a8873632aKristina Sojakova [Type {typeId = convertSort2String sort,
53d7a124a59889b9de5c6ffa856a5e697b043c90Kristina Sojakova typeSort = [isaTerm],
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova typeArgs = []}])
53d7a124a59889b9de5c6ffa856a5e697b043c90Kristina Sojakova----------------------------------------------------------------
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova-- Functions for adding the eq functions and the compare_with --
53d7a124a59889b9de5c6ffa856a5e697b043c90Kristina Sojakova-- functions to an Isabelle theory --
53d7a124a59889b9de5c6ffa856a5e697b043c90Kristina Sojakova----------------------------------------------------------------
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova-- | Add the eq function to an Isabelle theory using a list of sorts
228124cdf2560445e7f1b5312476935b51887463Kristina SojakovaaddEqFun :: [SORT] -> IsaTheory -> IsaTheory
228124cdf2560445e7f1b5312476935b51887463Kristina SojakovaaddEqFun sortList isaTh =
53d7a124a59889b9de5c6ffa856a5e697b043c90Kristina Sojakova let eqtype = mkFunType preAlphabetType $ mkFunType preAlphabetType boolType
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova isaThWithConst = addConst eq_PreAlphabetS eqtype isaTh
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova let x = mkFree "x"
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova y = mkFree "y"
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova lhs = binEq_PreAlphabet lhs_a y
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova lhs_a = termAppl (conDouble (mkPreAlphabetConstructor sort)) x
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova rhs = termAppl rhs_a y
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova rhs_a = termAppl (conDouble (mkCompareWithFunName sort)) x
669b4334be8eb3313ca146137db1b83a8873632aKristina Sojakova in binEq lhs rhs
228124cdf2560445e7f1b5312476935b51887463Kristina Sojakova eqs = map mkEq sortList
669b4334be8eb3313ca146137db1b83a8873632aKristina Sojakova in addPrimRec eqs isaThWithConst
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova-- | Add all compare_with functions for a given list of sorts to an
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova-- Isabelle theory. We need to know about the casl signature (data
27bdba808fa9637ef10b739233fde57c77245f5dKristina Sojakova-- part of a CspCASL spec) so that we can pass it on to the
27bdba808fa9637ef10b739233fde57c77245f5dKristina Sojakova-- addCompareWithFun function
27bdba808fa9637ef10b739233fde57c77245f5dKristina SojakovaaddAllCompareWithFun :: CASLSign.CASLSign -> IsaTheory -> IsaTheory
27bdba808fa9637ef10b739233fde57c77245f5dKristina SojakovaaddAllCompareWithFun caslSign isaTh =
27bdba808fa9637ef10b739233fde57c77245f5dKristina Sojakova let sortList = Set.toList(CASLSign.sortSet caslSign)
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova in foldl (addCompareWithFun caslSign) isaTh sortList
14650c9e129d8dc51ed55b2edc6ec27d9f0f6d00Kristina Sojakova-- | Add a single compare_with function for a given sort to an
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova-- Isabelle theory. We need to know about the casl signature (data
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova-- part of a CspCASL spec) to work out the RHS of the equations.
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaaddCompareWithFun :: CASLSign.CASLSign -> IsaTheory -> SORT -> IsaTheory
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaaddCompareWithFun caslSign isaTh sort =
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova let sortList = Set.toList(CASLSign.sortSet caslSign)
sortSuperSet = CASLSign.supersortsOf sort caslSign
sort'SuperSet =CASLSign.supersortsOf sort' caslSign
test2 = if (Set.member sort sort'SuperSet)
test3 = if (Set.member sort' sortSuperSet)
-- translation to PCFOL (i.e. without subsorting)
addAllDecompositionTheorem :: CASLSign.CASLSign -> [SORT] -> [(SORT,SORT)] ->
-- sorts. e.g. (S,T,U) means produce the lemma and proof for
addDecompositionTheorem :: CASLSign.CASLSign -> [SORT] -> [(SORT,SORT)] ->
addAllInjectivityTheorems :: CASLSign.CASLSign -> [SORT] -> [(SORT,SORT)] ->
addInjectivityTheorem :: CASLSign.CASLSign -> [SORT] -> [(SORT,SORT)] ->
abbrsNew = Map.insert alphabetS ([], preAlphabetQuotType) myabbrs
addAllIntegrationTheorems :: [SORT] -> CASLSign.CASLSign -> IsaTheory ->
addIntegrationTheorem_A :: CASLSign.CASLSign -> IsaTheory -> (SORT,SORT) ->
s1SuperSet = CASLSign.supersortsOf s1 caslSign
s2SuperSet = CASLSign.supersortsOf s2 caslSign
(Set.insert s1 s1SuperSet)
(Set.insert s2 s2SuperSet))
procSetList = Map.toList (procSet cspSign)
-- and the alphabet i.e., ProcName => (ProcName, Alphabet) proc. We
addProcMap :: [Named CspCASLSen] -> CASLSign.Sign () () -> IsaTheory ->
getCollectionTotAx :: CASLSign.CASLSign -> [String]
totFilter (_,setOpType) = let listOpType = Set.toList setOpType
in CASLSign.opKind (head listOpType) == Total
let index = List.elemIndex s sorts
CASLSign.opArgs = [s],
CASLSign.opRes = s'})
injName = show $ CASLInject.uniqueInjName t