{- |
Module      :  ./CspCASLProver/Utils.hs
Description :  Utilities for CspCASLProver related to the actual
               construction of Isabelle theories.
Copyright   :  (c) Liam O'Reilly and Markus Roggenbach,
               Swansea University 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  csliam@swansea.ac.uk
Stability   :  provisional
Portability :  portable

Utilities for CspCASLProver related to the actual construction of
Isabelle theories.
-}

module CspCASLProver.Utils
    ( addAlphabetType
    , addAllBarTypes
    , addAllChooseFunctions
    , addAllCompareWithFun
    , addAllIntegrationTheorems
    , addAllGaAxiomsCollections
    , addEqFun
    , addEventDataType
    , addFlatTypes
    , addInstanceOfEquiv
    , addJustificationTheorems
    , addPreAlphabet
    , addProcMap
    , addProcNameDatatype
    , addProjFlatFun
    , addProcTheorems
    ) where

import CASL.AS_Basic_CASL
import qualified CASL.Fold as CASL_Fold
import qualified CASL.Sign as CASLSign
import qualified CASL.Inject as CASLInject

import Common.AS_Annotation (makeNamed, Named, SenAttr (..))
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet
import Common.Id (nullRange)

import Comorphisms.CASL2PCFOL (mkEmbInjName, mkTransAxiomName, mkIdAxiomName)
import Comorphisms.CASL2SubCFOL (mkNotDefBotAxiomName, mkTotalityAxiomName)

import Comorphisms.CFOL2IsabelleHOL (IsaTheory)
import qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL

import CspCASL.AS_CspCASL_Process (FQ_PROCESS_NAME (..), ProcProfile (..),
                                  PROCESS (..))
import CspCASL.SignCSP

import CspCASLProver.Consts
import CspCASLProver.CspProverConsts
import CspCASLProver.IsabelleUtils
import CspCASLProver.TransProcesses (transProcess, VarSource (..))

import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set

import Isabelle.IsaConsts
import Isabelle.IsaSign
import Isabelle.Translate (transString)

{- -----------------------------------------------------------------------
Functions for adding the PreAlphabet datatype to an Isabelle theory --
----------------------------------------------------------------------- -}

{- | Add the PreAlphabet (built from a list of sorts) to an Isabelle
theory. -}
addPreAlphabet :: [SORT] -> IsaTheory -> IsaTheory
addPreAlphabet :: [SORT] -> IsaTheory -> IsaTheory
addPreAlphabet sortList :: [SORT]
sortList isaTh :: IsaTheory
isaTh =
   let preAlphabetDomainEntry :: DomainEntry
preAlphabetDomainEntry = [SORT] -> DomainEntry
mkPreAlphabetDE [SORT]
sortList
       -- Add to the isabelle signature the new domain entry
   in DomainEntry -> IsaTheory -> IsaTheory
updateDomainTab DomainEntry
preAlphabetDomainEntry IsaTheory
isaTh

-- | Make a Domain Entry for the PreAlphabet from a list of sorts.
mkPreAlphabetDE :: [SORT] -> DomainEntry
mkPreAlphabetDE :: [SORT] -> DomainEntry
mkPreAlphabetDE sorts :: [SORT]
sorts =
    (String -> Typ
mkSType String
preAlphabetS,
         (SORT -> (VName, [Typ])) -> [SORT] -> [(VName, [Typ])]
forall a b. (a -> b) -> [a] -> [b]
map (\ sort :: SORT
sort ->
                  (String -> VName
mkVName (SORT -> String
mkPreAlphabetConstructor SORT
sort),
                               [String -> Typ
mkSType (String -> Typ) -> String -> Typ
forall a b. (a -> b) -> a -> b
$ SORT -> String
convertSort2String SORT
sort])
             ) [SORT]
sorts
    )

{- --------------------------------------------------------------
Functions for adding the eq functions and the compare_with --
functions to an Isabelle theory                            --
-------------------------------------------------------------- -}

-- | Add the eq function to an Isabelle theory using a list of sorts
addEqFun :: [SORT] -> IsaTheory -> IsaTheory
addEqFun :: [SORT] -> IsaTheory -> IsaTheory
addEqFun sortList :: [SORT]
sortList isaTh :: IsaTheory
isaTh =
    let eqtype :: Typ
eqtype = Typ -> Typ -> Typ
mkFunType Typ
preAlphabetType (Typ -> Typ) -> Typ -> Typ
forall a b. (a -> b) -> a -> b
$ Typ -> Typ -> Typ
mkFunType Typ
preAlphabetType Typ
boolType
        mkEq :: SORT -> Term
mkEq sort :: SORT
sort =
            let x :: Term
x = String -> Term
mkFree "x"
                y :: Term
y = String -> Term
mkFree "y"
                lhs :: Term
lhs = Term -> Term -> Term
binEq_PreAlphabet Term
lhs_a Term
y
                lhs_a :: Term
lhs_a = Term -> Term -> Term
termAppl (String -> Term
conDouble (SORT -> String
mkPreAlphabetConstructor SORT
sort)) Term
x
                rhs :: Term
rhs = Term -> Term -> Term
termAppl Term
rhs_a Term
y
                rhs_a :: Term
rhs_a = Term -> Term -> Term
termAppl (String -> Term
conDouble (SORT -> String
mkCompareWithFunName SORT
sort)) Term
x
            in Term -> Term -> Term
binEq Term
lhs Term
rhs
        eqs :: [Term]
eqs = (SORT -> Term) -> [SORT] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Term
mkEq [SORT]
sortList
    in String -> Typ -> [Term] -> IsaTheory -> IsaTheory
addPrimRec String
eq_PreAlphabetS Typ
eqtype [Term]
eqs IsaTheory
isaTh

{- | Add all compare_with functions for a given list of sorts to an
Isabelle theory. We need to know about the casl signature (data
part of a CspCASL spec) so that we can pass it on to the
addCompareWithFun function -}
addAllCompareWithFun :: CASLSign.CASLSign -> IsaTheory -> IsaTheory
addAllCompareWithFun :: CASLSign -> IsaTheory -> IsaTheory
addAllCompareWithFun caslSign :: CASLSign
caslSign isaTh :: IsaTheory
isaTh =
    let sortList :: [SORT]
sortList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
CASLSign.sortSet CASLSign
caslSign)
    in (IsaTheory -> SORT -> IsaTheory)
-> IsaTheory -> [SORT] -> IsaTheory
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (CASLSign -> IsaTheory -> SORT -> IsaTheory
addCompareWithFun CASLSign
caslSign) IsaTheory
isaTh [SORT]
sortList

{- | Add a single compare_with function for a given sort to an
Isabelle theory.  We need to know about the casl signature (data
part of a CspCASL spec) to work out the RHS of the equations. -}
addCompareWithFun :: CASLSign.CASLSign -> IsaTheory -> SORT -> IsaTheory
addCompareWithFun :: CASLSign -> IsaTheory -> SORT -> IsaTheory
addCompareWithFun caslSign :: CASLSign
caslSign isaTh :: IsaTheory
isaTh sort :: SORT
sort =
    let sortList :: [SORT]
sortList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
CASLSign.sortSet CASLSign
caslSign)
        sortType :: Typ
sortType = Type :: String -> Sort -> [Typ] -> Typ
Type {typeId :: String
typeId = SORT -> String
convertSort2String SORT
sort, typeSort :: Sort
typeSort = [],
                                  typeArgs :: [Typ]
typeArgs = []}
        funName :: String
funName = SORT -> String
mkCompareWithFunName SORT
sort
        funType :: Typ
funType = Typ -> Typ -> Typ
mkFunType Typ
sortType (Typ -> Typ) -> Typ -> Typ
forall a b. (a -> b) -> a -> b
$ Typ -> Typ -> Typ
mkFunType Typ
preAlphabetType Typ
boolType
        sortSuperSet :: Set SORT
sortSuperSet = SORT -> CASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
CASLSign.supersortsOf SORT
sort CASLSign
caslSign
        mkEq :: SORT -> Term
mkEq sort' :: SORT
sort' =
            let x :: Term
x = String -> Term
mkFree "x"
                y :: Term
y = String -> Term
mkFree "y"
                sort'Constructor :: String
sort'Constructor = SORT -> String
mkPreAlphabetConstructor SORT
sort'
                lhs :: Term
lhs = Term -> Term -> Term
termAppl Term
lhs_a Term
lhs_b
                lhs_a :: Term
lhs_a = Term -> Term -> Term
termAppl (String -> Term
conDouble String
funName) Term
x
                lhs_b :: Term
lhs_b = Term -> Term -> Term
termAppl (String -> Term
conDouble String
sort'Constructor) Term
y
                sort'SuperSet :: Set SORT
sort'SuperSet = SORT -> CASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
CASLSign.supersortsOf SORT
sort' CASLSign
caslSign
                commonSuperList :: [SORT]
commonSuperList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                                                 Set SORT
sortSuperSet
                                                 Set SORT
sort'SuperSet)

                {- If there are no tests then the rhs=false else
                combine all tests using binConj -}
                rhs :: Term
rhs = if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
allTests
                      then Term
false
                      else (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Term -> Term -> Term
binConj [Term]
allTests

                {- The tests produce a list of equations for each test
                Test 1 =  test equality at: current sort vs current sort
                Test 2 =  test equality at: current sort vs super sorts
                Test 3 =  test equality at: super sorts  vs current sort
                Test 4 =  test equality at: super sorts  vs super sorts -}
                allTests :: [Term]
allTests = [[Term]] -> [Term]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Term]
test1, [Term]
test2, [Term]
test3, [Term]
test4]
                test1 :: [Term]
test1 = [Term -> Term -> Term
binEq Term
x Term
y | SORT
sort SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
sort']
                test2 :: [Term]
test2 = [Term -> Term -> Term
binEq Term
x (SORT -> SORT -> Term -> Term
mkInjection SORT
sort' SORT
sort Term
y) |
                         SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
sort Set SORT
sort'SuperSet]
                test3 :: [Term]
test3 = [Term -> Term -> Term
binEq (SORT -> SORT -> Term -> Term
mkInjection SORT
sort SORT
sort' Term
x) Term
y |
                         SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
sort' Set SORT
sortSuperSet]
                test4 :: [Term]
test4 = (SORT -> Term) -> [SORT] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Term
test4_atSort [SORT]
commonSuperList
                test4_atSort :: SORT -> Term
test4_atSort s :: SORT
s = Term -> Term -> Term
binEq (SORT -> SORT -> Term -> Term
mkInjection SORT
sort SORT
s Term
x)
                                       (SORT -> SORT -> Term -> Term
mkInjection SORT
sort' SORT
s Term
y)
            in Term -> Term -> Term
binEq Term
lhs Term
rhs
        eqs :: [Term]
eqs = (SORT -> Term) -> [SORT] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Term
mkEq [SORT]
sortList
    in String -> Typ -> [Term] -> IsaTheory -> IsaTheory
addPrimRec String
funName Typ
funType [Term]
eqs IsaTheory
isaTh

{- ------------------------------------------------------
Functions that creates a lemma for group many lemmas
------------------------------------------------------ -}

{- | Add a series of lemmas sentences that collect together all the
automatically generate axioms. This allow us to group large collections of
lemmas in to a single lemma. This cuts down on the repreated addition of
lemmas in the proofs. We need to the CASL signature (from the datapart) and
the PFOL Signature to pass it on. We could recalculate the PFOL signature
from the CASL signature here, but we dont as it can be passed in. We need
the PFOL signature which is the data part CASL signature after translation
to PCFOL (i.e. without subsorting) -}
addAllGaAxiomsCollections :: CASLSign.CASLSign -> CASLSign.CASLSign ->
                        IsaTheory -> IsaTheory
addAllGaAxiomsCollections :: CASLSign -> CASLSign -> IsaTheory -> IsaTheory
addAllGaAxiomsCollections caslSign :: CASLSign
caslSign pfolSign :: CASLSign
pfolSign isaTh :: IsaTheory
isaTh =
    let sortRel :: [(SORT, SORT)]
sortRel = Rel SORT -> [(SORT, SORT)]
forall a. Rel a -> [(a, a)]
Rel.toList (CASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
CASLSign.sortRel CASLSign
caslSign)
        sorts :: [SORT]
sorts = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
CASLSign.sortSet CASLSign
caslSign)
    in String -> [String] -> IsaTheory -> IsaTheory
addLemmasCollection String
lemmasEmbInjAxS ([(SORT, SORT)] -> [String]
getCollectionEmbInjAx [(SORT, SORT)]
sortRel)
     (IsaTheory -> IsaTheory) -> IsaTheory -> IsaTheory
forall a b. (a -> b) -> a -> b
$ String -> [String] -> IsaTheory -> IsaTheory
addLemmasCollection String
lemmasIdentityAxS (CASLSign -> [String]
getCollectionIdentityAx CASLSign
caslSign)
     (IsaTheory -> IsaTheory) -> IsaTheory -> IsaTheory
forall a b. (a -> b) -> a -> b
$ String -> [String] -> IsaTheory -> IsaTheory
addLemmasCollection String
lemmasNotDefBotAxS ([SORT] -> [String]
getCollectionNotDefBotAx [SORT]
sorts)
     (IsaTheory -> IsaTheory) -> IsaTheory -> IsaTheory
forall a b. (a -> b) -> a -> b
$ String -> [String] -> IsaTheory -> IsaTheory
addLemmasCollection String
lemmasTotalityAxS (CASLSign -> [String]
getCollectionTotAx CASLSign
pfolSign)
     (IsaTheory -> IsaTheory) -> IsaTheory -> IsaTheory
forall a b. (a -> b) -> a -> b
$ String -> [String] -> IsaTheory -> IsaTheory
addLemmasCollection String
lemmasTransAxS (CASLSign -> [String]
getCollectionTransAx CASLSign
caslSign)
       IsaTheory
isaTh

{- ------------------------------------------------------
Functions for producing the Justification theorems --
------------------------------------------------------ -}

{- | Add all justification theorems to an Isabelle Theory. We need to
the CASL signature (from the datapart) and the PFOL Signature to
pass it on. We could recalculate the PFOL signature from the CASL
signature here, but we dont as it can be passed in. We need the
PFOL signature which is the data part CASL signature after
translation to PCFOL (i.e. without subsorting) -}
addJustificationTheorems :: CASLSign.CASLSign -> CASLSign.CASLSign ->
                            IsaTheory -> IsaTheory
addJustificationTheorems :: CASLSign -> CASLSign -> IsaTheory -> IsaTheory
addJustificationTheorems caslSign :: CASLSign
caslSign pfolSign :: CASLSign
pfolSign isaTh :: IsaTheory
isaTh =
    let sortRel :: [(SORT, SORT)]
sortRel = Rel SORT -> [(SORT, SORT)]
forall a. Rel a -> [(a, a)]
Rel.toList (CASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
CASLSign.sortRel CASLSign
caslSign)
        sorts :: [SORT]
sorts = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
CASLSign.sortSet CASLSign
caslSign)
    in [SORT] -> [(SORT, SORT)] -> IsaTheory -> IsaTheory
addTransitivityTheorem [SORT]
sorts [(SORT, SORT)]
sortRel
       (IsaTheory -> IsaTheory) -> IsaTheory -> IsaTheory
forall a b. (a -> b) -> a -> b
$ CASLSign -> [SORT] -> [(SORT, SORT)] -> IsaTheory -> IsaTheory
addAllInjectivityTheorems CASLSign
pfolSign [SORT]
sorts [(SORT, SORT)]
sortRel
       (IsaTheory -> IsaTheory) -> IsaTheory -> IsaTheory
forall a b. (a -> b) -> a -> b
$ CASLSign
-> CASLSign -> [SORT] -> [(SORT, SORT)] -> IsaTheory -> IsaTheory
addAllDecompositionTheorem CASLSign
caslSign CASLSign
pfolSign [SORT]
sorts [(SORT, SORT)]
sortRel
       (IsaTheory -> IsaTheory) -> IsaTheory -> IsaTheory
forall a b. (a -> b) -> a -> b
$ [SORT] -> IsaTheory -> IsaTheory
addSymmetryTheorem [SORT]
sorts
       (IsaTheory -> IsaTheory) -> IsaTheory -> IsaTheory
forall a b. (a -> b) -> a -> b
$ IsaTheory -> IsaTheory
addReflexivityTheorem
         IsaTheory
isaTh

-- | Add the reflexivity theorem and proof to an Isabelle Theory
addReflexivityTheorem :: IsaTheory -> IsaTheory
addReflexivityTheorem :: IsaTheory -> IsaTheory
addReflexivityTheorem isaTh :: IsaTheory
isaTh =
    let name :: String
name = String
reflexivityTheoremS
        x :: Term
x = String -> Term
mkFree "x"
        thmConds :: [a]
thmConds = []
        thmConcl :: Term
thmConcl = Term -> Term -> Term
binEq_PreAlphabet Term
x Term
x
        proof' :: IsaProof
proof' = IsaProof :: [ProofCommand] -> ProofEnd -> IsaProof
IsaProof {
                   proof :: [ProofCommand]
proof = [[ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
Induct Term
x, ProofMethod
Auto] Bool
False],
                   end :: ProofEnd
end = ProofEnd
Done
                 }
    in String -> [Term] -> Term -> IsaProof -> IsaTheory -> IsaTheory
addTheoremWithProof String
name [Term]
forall a. [a]
thmConds Term
thmConcl IsaProof
proof' IsaTheory
isaTh

{- | Add the symmetry theorem and proof to an Isabelle Theory. We need
to know the number of sorts, but instead we are given a list of
all sorts -}
addSymmetryTheorem :: [SORT] -> IsaTheory -> IsaTheory
addSymmetryTheorem :: [SORT] -> IsaTheory -> IsaTheory
addSymmetryTheorem _ isaTh :: IsaTheory
isaTh =
    let -- numSorts = length(sorts)
        name :: String
name = String
symmetryTheoremS
        x :: Term
x = String -> Term
mkFree "x"
        y :: Term
y = String -> Term
mkFree "y"
        thmConds :: [Term]
thmConds = [Term -> Term -> Term
binEq_PreAlphabet Term
x Term
y]
        thmConcl :: Term
thmConcl = Term -> Term -> Term
binEq_PreAlphabet Term
y Term
x
        {- We want to induct Y then apply simp numSorts times and reapeat this
        apply as many times as possibe, thus the true at the end
        inductY = [Apply ((Induct y):(replicate numSorts Simp)) True]
        Bug in above in isabelle?? not sure - does not work for all specs?
        Now we do induction on Y then auto - I think this works for all specs -}
        inductY :: [ProofCommand]
inductY = [[ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
Induct Term
y, ProofMethod
Auto] Bool
True]
        proof' :: IsaProof
proof' = IsaProof :: [ProofCommand] -> ProofEnd -> IsaProof
IsaProof {
                   -- Add in front of inductY a apply induct on x
                   proof :: [ProofCommand]
proof = [ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
Induct Term
x] Bool
False ProofCommand -> [ProofCommand] -> [ProofCommand]
forall a. a -> [a] -> [a]
: [ProofCommand]
inductY,
                   end :: ProofEnd
end = ProofEnd
Done
                 }
    in String -> [Term] -> Term -> IsaProof -> IsaTheory -> IsaTheory
addTheoremWithProof String
name [Term]
thmConds Term
thmConcl IsaProof
proof' IsaTheory
isaTh

-- | Add all the decoposition theorems and proofs
addAllDecompositionTheorem :: CASLSign.CASLSign -> CASLSign.CASLSign
                           -> [SORT] -> [(SORT, SORT)]
                           -> IsaTheory -> IsaTheory
addAllDecompositionTheorem :: CASLSign
-> CASLSign -> [SORT] -> [(SORT, SORT)] -> IsaTheory -> IsaTheory
addAllDecompositionTheorem caslSign :: CASLSign
caslSign pfolSign :: CASLSign
pfolSign sorts :: [SORT]
sorts sortRel :: [(SORT, SORT)]
sortRel isaTh :: IsaTheory
isaTh =
    let tripples :: [(SORT, SORT, SORT)]
tripples = [(SORT
s1, SORT
s2, SORT
s3) |
                    (s1 :: SORT
s1, s2 :: SORT
s2) <- [(SORT, SORT)]
sortRel, (s2' :: SORT
s2', s3 :: SORT
s3) <- [(SORT, SORT)]
sortRel, SORT
s2 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s2']
    in (IsaTheory -> (SORT, SORT, SORT) -> IsaTheory)
-> IsaTheory -> [(SORT, SORT, SORT)] -> IsaTheory
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (CASLSign
-> CASLSign
-> [SORT]
-> IsaTheory
-> (SORT, SORT, SORT)
-> IsaTheory
addDecompositionTheorem CASLSign
caslSign CASLSign
pfolSign [SORT]
sorts)
       IsaTheory
isaTh [(SORT, SORT, SORT)]
tripples

{- | Add the decomposition theorem and proof which should be deduced
from the transitivity axioms from the translation CASL2PCFOL;
CASL2SubCFOL for a pair of injections represented as a tripple of
sorts. e.g. (S,T,U) means produce the lemma and proof for
inj_T_U(inj_S_T(x)) = inj_S_U(x). As a work around, we need to
know all sorts to pass them on. -}
addDecompositionTheorem :: CASLSign.CASLSign -> CASLSign.CASLSign -> [SORT]
                        -> IsaTheory -> (SORT, SORT, SORT)
                        -> IsaTheory
addDecompositionTheorem :: CASLSign
-> CASLSign
-> [SORT]
-> IsaTheory
-> (SORT, SORT, SORT)
-> IsaTheory
addDecompositionTheorem caslSign :: CASLSign
caslSign pfolSign :: CASLSign
pfolSign sorts :: [SORT]
sorts isaTh :: IsaTheory
isaTh (s1 :: SORT
s1, s2 :: SORT
s2, s3 :: SORT
s3) =
    let x :: Term
x = String -> Term
mkFree "x"
        -- These 5 lines make use of currying
        injOp_s1_s2 :: Term -> Term
injOp_s1_s2 = SORT -> SORT -> Term -> Term
mkInjection SORT
s1 SORT
s2
        injOp_s2_s3 :: Term -> Term
injOp_s2_s3 = SORT -> SORT -> Term -> Term
mkInjection SORT
s2 SORT
s3
        injOp_s1_s3 :: Term -> Term
injOp_s1_s3 = SORT -> SORT -> Term -> Term
mkInjection SORT
s1 SORT
s3
        inj_s1_s2_s3_x :: Term
inj_s1_s2_s3_x = Term -> Term
injOp_s2_s3 (Term -> Term
injOp_s1_s2 Term
x)
        inj_s1_s3_x :: Term
inj_s1_s3_x = Term -> Term
injOp_s1_s3 Term
x
        definedOp_s1 :: Term -> Term
definedOp_s1 = [SORT] -> SORT -> Term -> Term
getDefinedOp [SORT]
sorts SORT
s1
        definedOp_s3 :: Term -> Term
definedOp_s3 = [SORT] -> SORT -> Term -> Term
getDefinedOp [SORT]
sorts SORT
s3

        name :: String
name = (SORT, SORT, SORT) -> String
getDecompositionThmName (SORT
s1, SORT
s2, SORT
s3)
        conds :: [a]
conds = []
        concl :: Term
concl = Term -> Term -> Term
binEq Term
inj_s1_s2_s3_x Term
inj_s1_s3_x
        -- We only want to add these lemma sets if they exist
        lemmasIdentityAxS' :: [String]
lemmasIdentityAxS' = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ CASLSign -> [String]
getCollectionIdentityAx CASLSign
caslSign
                             then []
                             else [String
lemmasIdentityAxS]
        lemmasTransAxS' :: [String]
lemmasTransAxS' = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ CASLSign -> [String]
getCollectionTransAx CASLSign
caslSign
                          then []
                          else [String
lemmasTransAxS]
        lemmasTotalityAxS' :: [String]
lemmasTotalityAxS' = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ CASLSign -> [String]
getCollectionTotAx CASLSign
pfolSign
                             then []
                             else [String
lemmasTotalityAxS]
        lemmasNotDefBotAxS' :: [String]
lemmasNotDefBotAxS' = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ [SORT] -> [String]
getCollectionNotDefBotAx [SORT]
sorts
                              then []
                              else [String
lemmasNotDefBotAxS]
        proof' :: IsaProof
proof' = [ProofCommand] -> ProofEnd -> IsaProof
IsaProof [[ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
CaseTac (Term -> Term
definedOp_s3 Term
inj_s1_s2_s3_x)] Bool
False,
                           -- Case 1
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
SubgoalTac (Term -> Term
definedOp_s1 Term
x)] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [[String] -> ProofMethod
Insert ([String] -> ProofMethod) -> [String] -> ProofMethod
forall a b. (a -> b) -> a -> b
$ [String]
lemmasIdentityAxS' [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                                        [String]
lemmasTransAxS'] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [ProofMethod
Simp] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Maybe Modifier -> [String] -> ProofMethod
SimpAdd Maybe Modifier
forall a. Maybe a
Nothing [String]
lemmasTotalityAxS'] Bool
False,

                           -- Case 2
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
SubgoalTac (
                             Term -> Term -> Term
termAppl Term
notOp (Term -> Term
definedOp_s3 Term
inj_s1_s3_x))] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Maybe Modifier -> [String] -> ProofMethod
SimpAdd Maybe Modifier
forall a. Maybe a
Nothing [String]
lemmasNotDefBotAxS'] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Maybe Modifier -> [String] -> ProofMethod
SimpAdd Maybe Modifier
forall a. Maybe a
Nothing [String]
lemmasTotalityAxS'] Bool
False]
                           ProofEnd
Done
    in String -> [Term] -> Term -> IsaProof -> IsaTheory -> IsaTheory
addTheoremWithProof String
name [Term]
forall a. [a]
conds Term
concl IsaProof
proof' IsaTheory
isaTh

-- | Add all the injectivity theorems and proofs
addAllInjectivityTheorems :: CASLSign.CASLSign -> [SORT] -> [(SORT, SORT)] ->
                             IsaTheory -> IsaTheory
addAllInjectivityTheorems :: CASLSign -> [SORT] -> [(SORT, SORT)] -> IsaTheory -> IsaTheory
addAllInjectivityTheorems pfolSign :: CASLSign
pfolSign sorts :: [SORT]
sorts sortRel :: [(SORT, SORT)]
sortRel isaTh :: IsaTheory
isaTh =
    (IsaTheory -> (SORT, SORT) -> IsaTheory)
-> IsaTheory -> [(SORT, SORT)] -> IsaTheory
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (CASLSign
-> [SORT]
-> [(SORT, SORT)]
-> IsaTheory
-> (SORT, SORT)
-> IsaTheory
addInjectivityTheorem CASLSign
pfolSign [SORT]
sorts [(SORT, SORT)]
sortRel) IsaTheory
isaTh [(SORT, SORT)]
sortRel

{- | Add the injectivity theorem and proof which should be deduced
from the embedding_Injectivity axioms from the translation
CASL2PCFOL; CASL2SubCFOL for a single injection represented as a
pair of sorts. As a work around, we need to know all sorts to
pass them on -}
addInjectivityTheorem :: CASLSign.CASLSign -> [SORT] -> [(SORT, SORT)] ->
                         IsaTheory -> (SORT, SORT) -> IsaTheory
addInjectivityTheorem :: CASLSign
-> [SORT]
-> [(SORT, SORT)]
-> IsaTheory
-> (SORT, SORT)
-> IsaTheory
addInjectivityTheorem pfolSign :: CASLSign
pfolSign sorts :: [SORT]
sorts sortRel :: [(SORT, SORT)]
sortRel isaTh :: IsaTheory
isaTh (s1 :: SORT
s1, s2 :: SORT
s2) =
    let x :: Term
x = String -> Term
mkFree "x"
        y :: Term
y = String -> Term
mkFree "y"
        injX :: Term
injX = SORT -> SORT -> Term -> Term
mkInjection SORT
s1 SORT
s2 Term
x
        injY :: Term
injY = SORT -> SORT -> Term -> Term
mkInjection SORT
s1 SORT
s2 Term
y
        definedOp_s1 :: Term -> Term
definedOp_s1 = [SORT] -> SORT -> Term -> Term
getDefinedOp [SORT]
sorts SORT
s1
        definedOp_s2 :: Term -> Term
definedOp_s2 = [SORT] -> SORT -> Term -> Term
getDefinedOp [SORT]
sorts SORT
s2
        name :: String
name = (SORT, SORT) -> String
getInjectivityThmName (SORT
s1, SORT
s2)
        conds :: [Term]
conds = [Term -> Term -> Term
binEq Term
injX Term
injY]
        concl :: Term
concl = Term -> Term -> Term
binEq Term
x Term
y
        -- We only want to add these lemma sets if they exist
        lemmasEmbInjAxS' :: [String]
lemmasEmbInjAxS' = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ [(SORT, SORT)] -> [String]
getCollectionEmbInjAx [(SORT, SORT)]
sortRel
                           then []
                           else [String
lemmasEmbInjAxS]
        lemmasTotalityAxS' :: [String]
lemmasTotalityAxS' = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ CASLSign -> [String]
getCollectionTotAx CASLSign
pfolSign
                             then []
                             else [String
lemmasTotalityAxS]
        lemmasNotDefBotAxS' :: [String]
lemmasNotDefBotAxS' = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ [SORT] -> [String]
getCollectionNotDefBotAx [SORT]
sorts
                              then []
                              else [String
lemmasNotDefBotAxS]

        proof' :: IsaProof
proof' = [ProofCommand] -> ProofEnd -> IsaProof
IsaProof [[ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
CaseTac (Term -> Term
definedOp_s2 Term
injX)] Bool
False,
                           -- Case 1
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
SubgoalTac (Term -> Term
definedOp_s1 Term
x)] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
SubgoalTac (Term -> Term
definedOp_s1 Term
y)] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [[String] -> ProofMethod
Insert [String]
lemmasEmbInjAxS'] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [ProofMethod
Simp] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Maybe Modifier -> [String] -> ProofMethod
SimpAdd Maybe Modifier
forall a. Maybe a
Nothing [String]
lemmasTotalityAxS'] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Maybe Modifier -> [String] -> ProofMethod
SimpAdd (Modifier -> Maybe Modifier
forall a. a -> Maybe a
Just Modifier
No_asm_use) [String]
lemmasTotalityAxS']
                                Bool
False,
                           -- Case 2
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
SubgoalTac (Term -> Term -> Term
termAppl Term
notOp (Term -> Term
definedOp_s1 Term
x))]
                                Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
SubgoalTac (Term -> Term -> Term
termAppl Term
notOp (Term -> Term
definedOp_s1 Term
y))]
                                Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Maybe Modifier -> [String] -> ProofMethod
SimpAdd Maybe Modifier
forall a. Maybe a
Nothing [String]
lemmasNotDefBotAxS'] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Maybe Modifier -> [String] -> ProofMethod
SimpAdd Maybe Modifier
forall a. Maybe a
Nothing [String]
lemmasTotalityAxS'] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Maybe Modifier -> [String] -> ProofMethod
SimpAdd (Modifier -> Maybe Modifier
forall a. a -> Maybe a
Just Modifier
No_asm_use) [String]
lemmasTotalityAxS']
                                Bool
False]
                           ProofEnd
Done
    in String -> [Term] -> Term -> IsaProof -> IsaTheory -> IsaTheory
addTheoremWithProof String
name [Term]
conds Term
concl IsaProof
proof' IsaTheory
isaTh

{- | Add the transitivity theorem and proof to an Isabelle Theory. We
need to know the number of sorts to know how much induction to
perfom and also the sub-sort relation to build the collection of
injectivity theorem names -}
addTransitivityTheorem :: [SORT] -> [(SORT, SORT)] -> IsaTheory -> IsaTheory
addTransitivityTheorem :: [SORT] -> [(SORT, SORT)] -> IsaTheory -> IsaTheory
addTransitivityTheorem sorts :: [SORT]
sorts sortRel :: [(SORT, SORT)]
sortRel isaTh :: IsaTheory
isaTh =
    let {- First we extend the theory to include the collections of CspCASL
        prover's injectivity and decomposition theorems -}
        isaThExt :: IsaTheory
isaThExt =
            String -> [String] -> IsaTheory -> IsaTheory
addLemmasCollection String
lemmasCCProverInjectivityThmsS
                ([(SORT, SORT)] -> [String]
getColInjectivityThmName [(SORT, SORT)]
sortRel)
          (IsaTheory -> IsaTheory) -> IsaTheory -> IsaTheory
forall a b. (a -> b) -> a -> b
$ String -> [String] -> IsaTheory -> IsaTheory
addLemmasCollection String
lemmasCCProverDecompositionThmsS
                ([(SORT, SORT)] -> [String]
getColDecompositionThmName [(SORT, SORT)]
sortRel)
            IsaTheory
isaTh
        numSorts :: Int
numSorts = [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SORT]
sorts
        name :: String
name = String
transitivityS
        x :: Term
x = String -> Term
mkFree "x"
        y :: Term
y = String -> Term
mkFree "y"
        z :: Term
z = String -> Term
mkFree "z"
        thmConds :: [Term]
thmConds = [Term -> Term -> Term
binEq_PreAlphabet Term
x Term
y, Term -> Term -> Term
binEq_PreAlphabet Term
y Term
z]
        thmConcl :: Term
thmConcl = Term -> Term -> Term
binEq_PreAlphabet Term
x Term
z
        -- We only want to add these lemma sets if they exist
        lemmasCCProverDecompositionThmsS' :: [String]
lemmasCCProverDecompositionThmsS' =
            if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ [(SORT, SORT)] -> [String]
getColDecompositionThmName [(SORT, SORT)]
sortRel
            then []
            else [String
lemmasCCProverDecompositionThmsS]
        lemmasCCProverInjectivityThmsS' :: [String]
lemmasCCProverInjectivityThmsS' =
            if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ [(SORT, SORT)] -> [String]
getColInjectivityThmName [(SORT, SORT)]
sortRel
            then []
            else [String
lemmasCCProverInjectivityThmsS]

        simpPlus :: ProofMethod
simpPlus = Maybe Modifier -> [String] -> ProofMethod
SimpAdd Maybe Modifier
forall a. Maybe a
Nothing ([String]
lemmasCCProverDecompositionThmsS' [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                                    [String]
lemmasCCProverInjectivityThmsS')
        {- We want to induct Y, Z and perfom simplification is a clever way,
        namely,
        apply(induct y, (induct z, simp * numSorts) * numSorts)+ -}
        inductZ :: [ProofMethod]
inductZ = Term -> ProofMethod
Induct Term
z ProofMethod -> [ProofMethod] -> [ProofMethod]
forall a. a -> [a] -> [a]
: Int -> ProofMethod -> [ProofMethod]
forall a. Int -> a -> [a]
replicate Int
numSorts ProofMethod
simpPlus
        inductYZ :: [ProofMethod]
inductYZ = Term -> ProofMethod
Induct Term
y ProofMethod -> [ProofMethod] -> [ProofMethod]
forall a. a -> [a] -> [a]
: [[ProofMethod]] -> [ProofMethod]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Int -> [ProofMethod] -> [[ProofMethod]]
forall a. Int -> a -> [a]
replicate Int
numSorts [ProofMethod]
inductZ)
        -- Main induction and simplification proof command
        inductPC :: [ProofCommand]
inductPC = [[ProofMethod] -> Bool -> ProofCommand
Apply [ProofMethod]
inductYZ Bool
True]
        proof' :: IsaProof
proof' = IsaProof :: [ProofCommand] -> ProofEnd -> IsaProof
IsaProof {
                   proof :: [ProofCommand]
proof = [ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
Induct Term
x] Bool
False ProofCommand -> [ProofCommand] -> [ProofCommand]
forall a. a -> [a] -> [a]
: [ProofCommand]
inductPC,
                   end :: ProofEnd
end = ProofEnd
Done
                 }
    in String -> [Term] -> Term -> IsaProof -> IsaTheory -> IsaTheory
addTheoremWithProof String
name [Term]
thmConds Term
thmConcl IsaProof
proof' IsaTheory
isaThExt

{- -----------------------------------------------------------
Functions for producing instances of equivalence classes --
------------------------------------------------------------ -}

{- | Function to add preAlphabet as an equivalence relation to an
Isabelle theory -}
addInstanceOfEquiv :: IsaTheory -> IsaTheory
addInstanceOfEquiv :: IsaTheory -> IsaTheory
addInstanceOfEquiv isaTh :: IsaTheory
isaTh =
    let equivSort :: Sort
equivSort = [String -> IsaClass
IsaClass String
equivTypeClassS]
        equivProof :: IsaProof
equivProof = [ProofCommand] -> ProofEnd -> IsaProof
IsaProof [[ProofMethod] -> Bool -> ProofCommand
Apply [String -> ProofMethod
Other "intro_classes"] Bool
False,
                               [ProofMethod] -> Bool -> ProofCommand
Apply [String -> ProofMethod
Other ("unfold " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
preAlphabetSimS
                                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_def")] Bool
False,
                               [ProofMethod] -> Bool -> ProofCommand
Apply [String -> ProofMethod
Other ("rule " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
reflexivityTheoremS)]
                                     Bool
False,
                               [ProofMethod] -> Bool -> ProofCommand
Apply [String -> ProofMethod
Other ("rule " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
transitivityS
                                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ ", auto")] Bool
False,
                               [ProofMethod] -> Bool -> ProofCommand
Apply [String -> ProofMethod
Other ("rule " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
symmetryTheoremS
                                                String -> String -> String
forall a. [a] -> [a] -> [a]
++ ", simp")] Bool
False]
                               ProofEnd
Done
        x :: Term
x = String -> Term
mkFree "x"
        y :: Term
y = String -> Term
mkFree "y"
        defLhs :: Term
defLhs = Term -> Term -> Term
binEqvSim Term
x Term
y
        defRhs :: Term
defRhs = Term -> Term -> Term
binEq_PreAlphabet Term
x Term
y
        def :: Term
def = Term -> Term -> Term
IsaEq Term
defLhs Term
defRhs
    in String
-> [Sort]
-> Sort
-> [(String, Term)]
-> IsaProof
-> IsaTheory
-> IsaTheory
addInstanceOf String
preAlphabetS [] Sort
equivSort
           [(String
preAlphabetSimS, Term
def)] IsaProof
equivProof IsaTheory
isaTh

{- -----------------------------------------------------------
Functions for producing the alphabet type               --
----------------------------------------------------------- -}

-- | Function to add the Alphabet type (type syonnym) to an Isabelle theory
addAlphabetType :: IsaTheory -> IsaTheory
addAlphabetType :: IsaTheory -> IsaTheory
addAlphabetType isaTh :: IsaTheory
isaTh =
    let isaTh_sign :: Sign
isaTh_sign = IsaTheory -> Sign
forall a b. (a, b) -> a
fst IsaTheory
isaTh
        isaTh_sign_tsig :: TypeSig
isaTh_sign_tsig = Sign -> TypeSig
tsig Sign
isaTh_sign
        myabbrs :: Abbrs
myabbrs = TypeSig -> Abbrs
abbrs TypeSig
isaTh_sign_tsig
        abbrsNew :: Abbrs
abbrsNew = String -> ([String], Typ) -> Abbrs -> Abbrs
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
alphabetS ([], Typ
preAlphabetQuotType) Abbrs
myabbrs

        isaTh_sign_updated :: Sign
isaTh_sign_updated = Sign
isaTh_sign {
                               tsig :: TypeSig
tsig = TypeSig
isaTh_sign_tsig {abbrs :: Abbrs
abbrs = Abbrs
abbrsNew}
                             }
    in (Sign
isaTh_sign_updated, IsaTheory -> [Named Sentence]
forall a b. (a, b) -> b
snd IsaTheory
isaTh)

{- -----------------------------------------------------------
Functions for producing the bar types                   --
----------------------------------------------------------- -}

-- | Function to add all the bar types to an Isabelle theory.
addAllBarTypes :: [SORT] -> IsaTheory -> IsaTheory
addAllBarTypes :: [SORT] -> IsaTheory -> IsaTheory
addAllBarTypes sorts :: [SORT]
sorts isaTh :: IsaTheory
isaTh = (IsaTheory -> SORT -> IsaTheory)
-> IsaTheory -> [SORT] -> IsaTheory
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl IsaTheory -> SORT -> IsaTheory
addBarType IsaTheory
isaTh [SORT]
sorts

-- | Function to add the bar types of a sort to an Isabelle theory.
addBarType :: IsaTheory -> SORT -> IsaTheory
addBarType :: IsaTheory -> SORT -> IsaTheory
addBarType isaTh :: IsaTheory
isaTh sort :: SORT
sort =
    let sortBarString :: String
sortBarString = SORT -> String
mkSortBarString SORT
sort
        barType :: Typ
barType = SORT -> Typ
mkSortBarType SORT
sort
        isaTh_sign :: Sign
isaTh_sign = IsaTheory -> Sign
forall a b. (a, b) -> a
fst IsaTheory
isaTh
        isaTh_sen :: [Named Sentence]
isaTh_sen = IsaTheory -> [Named Sentence]
forall a b. (a, b) -> b
snd IsaTheory
isaTh
        x :: Term
x = String -> Term
mkFree "x"
        y :: Term
y = String -> Term
mkFree "y"
        rhs :: Term
rhs = Term -> Term -> Term
termAppl (String -> Term
conDouble (SORT -> String
mkPreAlphabetConstructor SORT
sort)) Term
y
        bin_eq :: Term
bin_eq = Term -> Term -> Term
binEq Term
x (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
termAppl (String -> Term
conDouble String
classS ) Term
rhs
        exist_eq :: Term
exist_eq = Term -> Term -> Term
termAppl (String -> Term
conDouble String
exS) (Term -> Term -> Continuity -> Term
Abs Term
y Term
bin_eq Continuity
NotCont)
        subset :: SetDecl
subset = Term -> Typ -> Term -> SetDecl
SubSet Term
x Typ
alphabetType Term
exist_eq
        sen :: Sentence
sen = Typ -> SetDecl -> IsaProof -> Sentence
TypeDef Typ
barType SetDecl
subset ([ProofCommand] -> ProofEnd -> IsaProof
IsaProof [] (ProofMethod -> ProofEnd
By ProofMethod
Auto))
        namedSen :: Named Sentence
namedSen = String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
sortBarString Sentence
sen
    in (Sign
isaTh_sign, [Named Sentence]
isaTh_sen [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence
namedSen])

{- -----------------------------------------------------------
Functions for producing the choose functions            --
----------------------------------------------------------- -}

{- | Add all choose functions for a given list of sorts to an Isabelle
theory. -}
addAllChooseFunctions :: [SORT] -> IsaTheory -> IsaTheory
addAllChooseFunctions :: [SORT] -> IsaTheory -> IsaTheory
addAllChooseFunctions sorts :: [SORT]
sorts isaTh :: IsaTheory
isaTh =
    let isaTh' :: IsaTheory
isaTh' = (IsaTheory -> SORT -> IsaTheory)
-> IsaTheory -> [SORT] -> IsaTheory
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl IsaTheory -> SORT -> IsaTheory
addChooseFunction IsaTheory
isaTh [SORT]
sorts -- add function and def
    in (IsaTheory -> SORT -> IsaTheory)
-> IsaTheory -> [SORT] -> IsaTheory
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl IsaTheory -> SORT -> IsaTheory
addChooseFunctionLemma IsaTheory
isaTh' [SORT]
sorts -- add theorem and proof

{- | Add a single choose function for a given sort to an Isabelle
theory.  The following Isabelle code is produced by this function:
consts choose_Nat :: "Alphabet => Nat"
defs choose_Nat_def: "choose_Nat x == the_elem{y . class(C_Nat y) = x}" -}
addChooseFunction :: IsaTheory -> SORT -> IsaTheory
addChooseFunction :: IsaTheory -> SORT -> IsaTheory
addChooseFunction isaTh :: IsaTheory
isaTh sort :: SORT
sort =
    let -- constant
        sortType :: Typ
sortType = Type :: String -> Sort -> [Typ] -> Typ
Type {typeId :: String
typeId = SORT -> String
convertSort2String SORT
sort,
                         typeSort :: Sort
typeSort = [],
                         typeArgs :: [Typ]
typeArgs = []}
        chooseFunName :: String
chooseFunName = SORT -> String
mkChooseFunName SORT
sort
        chooseFunType :: Typ
chooseFunType = Typ -> Typ -> Typ
mkFunType Typ
alphabetType Typ
sortType
        -- definition
        x :: Term
x = String -> Term
mkFree "x"
        y :: Term
y = String -> Term
mkFree "y"
        contentsOp :: Term -> Term
contentsOp = Term -> Term -> Term
termAppl (String -> Term
conDouble "the_elem")
        sortConsOp :: Term -> Term
sortConsOp = Term -> Term -> Term
termAppl (String -> Term
conDouble (SORT -> String
mkPreAlphabetConstructor SORT
sort))
        bin_eq :: Term
bin_eq = Term -> Term -> Term
binEq (Term -> Term
classOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
sortConsOp Term
y) Term
x
        subset :: SetDecl
subset = Term -> Typ -> Term -> SetDecl
SubSet Term
y Typ
sortType Term
bin_eq
        lhs :: Term
lhs = SORT -> Term -> Term
mkChooseFunOp SORT
sort Term
x
        rhs :: Term
rhs = Term -> Term
contentsOp (SetDecl -> Term
Set SetDecl
subset)
    in  -- Add defintion to theory
        String -> Term -> Term -> IsaTheory -> IsaTheory
addDef String
chooseFunName Term
lhs Term
rhs
        -- Add constant to theory
      (IsaTheory -> IsaTheory) -> IsaTheory -> IsaTheory
forall a b. (a -> b) -> a -> b
$ String -> Typ -> IsaTheory -> IsaTheory
addConst String
chooseFunName Typ
chooseFunType IsaTheory
isaTh

{- | Add a single choose function lemma for a given sort to an
Isabelle theory.  The following Isabelle code is produced by this
function: lemma "choose_Nat (class (C_Nat x)) = x". The proof is
also produced. -}

addChooseFunctionLemma :: IsaTheory -> SORT -> IsaTheory
addChooseFunctionLemma :: IsaTheory -> SORT -> IsaTheory
addChooseFunctionLemma isaTh :: IsaTheory
isaTh sort :: SORT
sort =
    let sortType :: Typ
sortType = Type :: String -> Sort -> [Typ] -> Typ
Type {typeId :: String
typeId = SORT -> String
convertSort2String SORT
sort,
                         typeSort :: Sort
typeSort = [],
                         typeArgs :: [Typ]
typeArgs = []}
        chooseFunName :: String
chooseFunName = SORT -> String
mkChooseFunName SORT
sort
        x :: Term
x = String -> Term
mkFree "x"
        y :: Term
y = String -> Term
mkFree "y"
        sortConsOp :: Term -> Term
sortConsOp = Term -> Term -> Term
termAppl (String -> Term
conDouble (SORT -> String
mkPreAlphabetConstructor SORT
sort))
        -- theorm
        subgoalTacTermLhsBinEq :: Term
subgoalTacTermLhsBinEq = Term -> Term -> Term
binEq (Term -> Term
classOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
sortConsOp Term
y)
                                       (Term -> Term
classOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
sortConsOp Term
x)
        subgoalTacTermLhs :: Term
subgoalTacTermLhs = SetDecl -> Term
Set (SetDecl -> Term) -> SetDecl -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Typ -> Term -> SetDecl
SubSet Term
y Typ
sortType Term
subgoalTacTermLhsBinEq
        subgoalTacTermRhs :: Term
subgoalTacTermRhs = SetDecl -> Term
Set (SetDecl -> Term) -> SetDecl -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> SetDecl
FixedSet [Term
x]
        subgoalTacTerm :: Term
subgoalTacTerm = Term -> Term -> Term
binEq Term
subgoalTacTermLhs Term
subgoalTacTermRhs
        thmConds :: [a]
thmConds = []
        thmConcl :: Term
thmConcl = Term -> Term -> Term
binEq (SORT -> Term -> Term
mkChooseFunOp SORT
sort (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
classOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
sortConsOp Term
x) Term
x
        proof' :: IsaProof
proof' = [ProofCommand] -> ProofEnd -> IsaProof
IsaProof [[ProofMethod] -> Bool -> ProofCommand
Apply [String -> ProofMethod
Other ("unfold " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
chooseFunName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_def")]
                                Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Term -> ProofMethod
SubgoalTac Term
subgoalTacTerm] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [ProofMethod
Simp] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Maybe Modifier -> [String] -> ProofMethod
SimpAdd Maybe Modifier
forall a. Maybe a
Nothing [String
quotEqualityS]] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [String -> ProofMethod
Other ("unfold " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
preAlphabetSimS
                                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_def")] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [ProofMethod
Auto] Bool
False]
                           ProofEnd
Done
    in String -> [Term] -> Term -> IsaProof -> IsaTheory -> IsaTheory
addTheoremWithProof String
chooseFunName [Term]
forall a. [a]
thmConds Term
thmConcl IsaProof
proof' IsaTheory
isaTh

{- -----------------------------------------------------------
Functions for producing the integration theorems        --
----------------------------------------------------------- -}

{- | Add all the integration theorems. We need to know all the sorts
to produce all the theorems. We need to know the CASL signature
of the data part to pass it on as an argument. -}
addAllIntegrationTheorems :: [SORT] -> CASLSign.CASLSign -> IsaTheory ->
                             IsaTheory
addAllIntegrationTheorems :: [SORT] -> CASLSign -> IsaTheory -> IsaTheory
addAllIntegrationTheorems sorts :: [SORT]
sorts caslSign :: CASLSign
caslSign isaTh :: IsaTheory
isaTh =
    let pairs :: [(SORT, SORT)]
pairs = [(SORT
s1, SORT
s2) | SORT
s1 <- [SORT]
sorts, SORT
s2 <- [SORT]
sorts]
    in (IsaTheory -> (SORT, SORT) -> IsaTheory)
-> IsaTheory -> [(SORT, SORT)] -> IsaTheory
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (CASLSign -> IsaTheory -> (SORT, SORT) -> IsaTheory
addIntegrationTheorem_A CASLSign
caslSign) IsaTheory
isaTh [(SORT, SORT)]
pairs

{- | Add Integration theorem A -- Compare to elements of the Alphabet.
We add the integration theorem based on the sorts of both
elements of the alphabet. We need to know the subsort relation to
find the highest common sort, but we pass in the CASL signature
for the data part. -}
addIntegrationTheorem_A :: CASLSign.CASLSign -> IsaTheory -> (SORT, SORT) ->
                           IsaTheory
addIntegrationTheorem_A :: CASLSign -> IsaTheory -> (SORT, SORT) -> IsaTheory
addIntegrationTheorem_A caslSign :: CASLSign
caslSign isaTh :: IsaTheory
isaTh (s1 :: SORT
s1, s2 :: SORT
s2) =
    let sortRel :: [(SORT, SORT)]
sortRel = Rel SORT -> [(SORT, SORT)]
forall a. Rel a -> [(a, a)]
Rel.toList (CASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
CASLSign.sortRel CASLSign
caslSign)
        s1SuperSet :: Set SORT
s1SuperSet = SORT -> CASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
CASLSign.supersortsOf SORT
s1 CASLSign
caslSign
        s2SuperSet :: Set SORT
s2SuperSet = SORT -> CASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
CASLSign.supersortsOf SORT
s2 CASLSign
caslSign
        commonSuperList :: [SORT]
commonSuperList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                                         (SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert SORT
s1 Set SORT
s1SuperSet)
                                         (SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert SORT
s2 Set SORT
s2SuperSet))
        x :: Term
x = String -> Term
mkFree "x"
        y :: Term
y = String -> Term
mkFree "y"
        s1ConsOp :: Term -> Term
s1ConsOp = Term -> Term -> Term
termAppl (String -> Term
conDouble (SORT -> String
mkPreAlphabetConstructor SORT
s1))
        s2ConsOp :: Term -> Term
s2ConsOp = Term -> Term -> Term
termAppl (String -> Term
conDouble (SORT -> String
mkPreAlphabetConstructor SORT
s2))
        rhs :: Term
rhs = Term -> Term -> Term
binEq (Term -> Term
classOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
s1ConsOp Term
x) (Term -> Term
classOp (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
s2ConsOp Term
y)
        lhs :: Term
lhs = if [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
commonSuperList
              then Term
false
              else
                  {- BUG pick any common sort for now (this does hold
                  and is valid) we should pick the top most one. -}
                  let s' :: SORT
s' = [SORT] -> SORT
forall a. [a] -> a
head [SORT]
commonSuperList
                  in Term -> Term -> Term
binEq (SORT -> SORT -> Term -> Term
mkInjection SORT
s1 SORT
s' Term
x) (SORT -> SORT -> Term -> Term
mkInjection SORT
s2 SORT
s' Term
y)
        thmConds :: [a]
thmConds = []
        thmConcl :: Term
thmConcl = Term -> Term -> Term
binEq Term
rhs Term
lhs
        -- theorem names for proof
        colInjThmNames :: [String]
colInjThmNames = [(SORT, SORT)] -> [String]
getColInjectivityThmName [(SORT, SORT)]
sortRel
        colDecompThmNames :: [String]
colDecompThmNames = [(SORT, SORT)] -> [String]
getColDecompositionThmName [(SORT, SORT)]
sortRel
        proof' :: IsaProof
proof' = [ProofCommand] -> ProofEnd -> IsaProof
IsaProof [[ProofMethod] -> Bool -> ProofCommand
Apply [Maybe Modifier -> [String] -> ProofMethod
SimpAdd Maybe Modifier
forall a. Maybe a
Nothing [String
quotEqualityS]] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [String -> ProofMethod
Other ("unfold " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
preAlphabetSimS
                                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_def")] Bool
False,
                           [ProofMethod] -> Bool -> ProofCommand
Apply [Maybe Modifier -> [String] -> ProofMethod
AutoSimpAdd Maybe Modifier
forall a. Maybe a
Nothing
                                  ([String]
colDecompThmNames [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
colInjThmNames)] Bool
False]
                           ProofEnd
Done
    in String -> [Term] -> Term -> IsaProof -> IsaTheory -> IsaTheory
addTheoremWithProof "IntegrationTheorem_A"
       [Term]
forall a. [a]
thmConds Term
thmConcl IsaProof
proof' IsaTheory
isaTh

{- ------------------------------------------------------------------------
Functions for adding the Event datatype and the channel encoding     --
------------------------------------------------------------------------ -}

{- | Add the Event datatype (built from a list of channels and the subsort
relation) to an Isabelle theory. -}
addEventDataType :: Rel.Rel SORT -> ChanNameMap -> IsaTheory -> IsaTheory
addEventDataType :: Rel SORT -> ChanNameMap -> IsaTheory -> IsaTheory
addEventDataType sortRel :: Rel SORT
sortRel chanNameMap :: ChanNameMap
chanNameMap isaTh :: IsaTheory
isaTh =
    let eventDomainEntry :: DomainEntry
eventDomainEntry = Rel SORT -> ChanNameMap -> DomainEntry
mkEventDE Rel SORT
sortRel ChanNameMap
chanNameMap
       -- Add to the isabelle signature the new domain entry
    in DomainEntry -> IsaTheory -> IsaTheory
updateDomainTab DomainEntry
eventDomainEntry IsaTheory
isaTh

-- | Make a Domain Entry for the Event from a list of sorts.
mkEventDE :: Rel.Rel SORT -> ChanNameMap -> DomainEntry
mkEventDE :: Rel SORT -> ChanNameMap -> DomainEntry
mkEventDE _ chanNameMap :: ChanNameMap
chanNameMap =
    let flat :: (VName, [Typ])
flat = (String -> VName
mkVName String
flatS, [Typ
alphabetType])
        -- Make a constuctor type for a channel with a target sort
        mkChanCon :: (SORT, SORT) -> (VName, [Typ])
mkChanCon (c :: SORT
c, s :: SORT
s) = (String -> VName
mkVName (SORT -> String
convertChannelString SORT
c),
                                        [SORT -> Typ
mkSortBarType SORT
s])
        {- Make pairs of channel and sorts, where we only build the declared
        channels and not the subsorted channels. -}
        mkAllChanCons :: [(VName, [Typ])]
mkAllChanCons = ((SORT, SORT) -> (VName, [Typ]))
-> [(SORT, SORT)] -> [(VName, [Typ])]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, SORT) -> (VName, [Typ])
mkChanCon ([(SORT, SORT)] -> [(VName, [Typ])])
-> [(SORT, SORT)] -> [(VName, [Typ])]
forall a b. (a -> b) -> a -> b
$ ChanNameMap -> [(SORT, SORT)]
forall a b. MapSet a b -> [(a, b)]
CASLSign.mapSetToList ChanNameMap
chanNameMap
        {- We build the event type out of the flat constructions and the list of
        channel constructions -}
    in (Typ
eventType, (VName, [Typ])
flat (VName, [Typ]) -> [(VName, [Typ])] -> [(VName, [Typ])]
forall a. a -> [a] -> [a]
: [(VName, [Typ])]
mkAllChanCons)

-- | Add the eq function to an Isabelle theory using a list of sorts
addProjFlatFun :: IsaTheory -> IsaTheory
addProjFlatFun :: IsaTheory -> IsaTheory
addProjFlatFun isaTh :: IsaTheory
isaTh =
    let eqtype :: Typ
eqtype = Typ -> Typ -> Typ
mkFunType Typ
eventType Typ
alphabetType
        x :: Term
x = String -> Term
mkFree "x"
        lhs :: Term
lhs = Term -> Term -> Term
termAppl (String -> Term
conDouble String
projFlatS) Term
flatX
        flatX :: Term
flatX = Term -> Term -> Term
termAppl (String -> Term
conDouble String
flatS) Term
x
        rhs :: Term
rhs = Term
x
        -- projFlat(Flat x) = x
        eqs :: [Term]
eqs = [Term -> Term -> Term
binEq Term
lhs Term
rhs]
    in String -> Typ -> [Term] -> IsaTheory -> IsaTheory
addPrimRec String
projFlatS Typ
eqtype [Term]
eqs IsaTheory
isaTh

{- | Function to add all the Flat types. These capture the original sorts, but
use the bar values instead wrapped up in the Flat constructor(the Flat
channel). We use this as a set of normal communications (action prefix,
send, recieve). -}
addFlatTypes :: [SORT] -> IsaTheory -> IsaTheory
addFlatTypes :: [SORT] -> IsaTheory -> IsaTheory
addFlatTypes sorts :: [SORT]
sorts isaTh :: IsaTheory
isaTh = (IsaTheory -> SORT -> IsaTheory)
-> IsaTheory -> [SORT] -> IsaTheory
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl IsaTheory -> SORT -> IsaTheory
addFlatType IsaTheory
isaTh [SORT]
sorts

-- | Function to add the flat type of a sort to an Isabelle theory.
addFlatType :: IsaTheory -> SORT -> IsaTheory
addFlatType :: IsaTheory -> SORT -> IsaTheory
addFlatType isaTh :: IsaTheory
isaTh sort :: SORT
sort =
    let sortFlatString :: String
sortFlatString = SORT -> String
mkSortFlatString SORT
sort
        flatType :: Typ
flatType = Type :: String -> Sort -> [Typ] -> Typ
Type {typeId :: String
typeId = String
sortFlatString, typeSort :: Sort
typeSort = [], typeArgs :: [Typ]
typeArgs = []}
        isaTh_sign :: Sign
isaTh_sign = IsaTheory -> Sign
forall a b. (a, b) -> a
fst IsaTheory
isaTh
        isaTh_sen :: [Named Sentence]
isaTh_sen = IsaTheory -> [Named Sentence]
forall a b. (a, b) -> b
snd IsaTheory
isaTh
        x :: Term
x = String -> Term
mkFree "x"
        y :: Term
y = String -> Term
mkFree "y"
        flatY :: Term
flatY = Term -> Term -> Term
termAppl (String -> Term
conDouble String
flatS) Term
y
        -- y in sort_Bar
        condition1 :: Term
condition1 = Term -> Term -> Term
binMembership Term
y (String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> String
mkSortBarString SORT
sort)
        -- x = Flat y
        condition2 :: Term
condition2 = Term -> Term -> Term
binEq Term
x Term
flatY
        -- y in sort_Bar /\ x = Flat y
        condition_eq :: Term
condition_eq = Term -> Term -> Term
binConj Term
condition1 Term
condition2
        exist_eq :: Term
exist_eq = Term -> Term -> Term
termAppl (String -> Term
conDouble String
exS) (Term -> Term -> Continuity -> Term
Abs Term
y Term
condition_eq Continuity
NotCont)
        subset :: SetDecl
subset = Term -> Typ -> Term -> SetDecl
SubSet Term
x Typ
eventType Term
exist_eq
        proof' :: ProofMethod
proof' = Maybe Modifier -> [String] -> ProofMethod
AutoSimpAdd Maybe Modifier
forall a. Maybe a
Nothing [SORT -> String
mkSortBarString SORT
sort String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_def"]
        sen :: Sentence
sen = Typ -> SetDecl -> IsaProof -> Sentence
TypeDef Typ
flatType SetDecl
subset ([ProofCommand] -> ProofEnd -> IsaProof
IsaProof [] (ProofMethod -> ProofEnd
By ProofMethod
proof'))
        namedSen :: Named Sentence
namedSen = String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
sortFlatString Sentence
sen
    in (Sign
isaTh_sign, [Named Sentence]
isaTh_sen [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence
namedSen])

{- ------------------------------------------------------------------------
Functions for adding the process name datatype to an Isabelle theory --
------------------------------------------------------------------------ -}

{- | Add process name datatype which has a constructor for each
process name (along with the arguments for the process) in the
CspCASL Signature to an Isabelle theory -}
addProcNameDatatype :: CspSign -> IsaTheory -> IsaTheory
addProcNameDatatype :: CspSign -> IsaTheory -> IsaTheory
addProcNameDatatype cspSign :: CspSign
cspSign isaTh :: IsaTheory
isaTh =
    let -- Create a list of pairs of process names and thier profiles
        procNamesAndProfileSet :: [(SORT, [ProcProfile])]
procNamesAndProfileSet = MapSet SORT ProcProfile -> [(SORT, [ProcProfile])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList (CspSign -> MapSet SORT ProcProfile
procSet CspSign
cspSign)
        f :: (SORT, [ProcProfile]) -> FQ_PROCESS_NAME
f (name :: SORT
name, profileSet :: [ProcProfile]
profileSet) = case [ProcProfile]
profileSet of
             [h :: ProcProfile
h] -> SORT -> ProcProfile -> FQ_PROCESS_NAME
FQ_PROCESS_NAME SORT
name ProcProfile
h -- Just keep the first one
             _ ->
               String -> FQ_PROCESS_NAME
forall a. HasCallStack => String -> a
error "CspCASLProver.Utils.addProcNameDatatype: CSP-CASL-Prover\
                     \ does not support overloaded process names yet."
        procNameDomainEntry :: DomainEntry
procNameDomainEntry = [FQ_PROCESS_NAME] -> DomainEntry
mkFQProcNameDE ([FQ_PROCESS_NAME] -> DomainEntry)
-> [FQ_PROCESS_NAME] -> DomainEntry
forall a b. (a -> b) -> a -> b
$ ((SORT, [ProcProfile]) -> FQ_PROCESS_NAME)
-> [(SORT, [ProcProfile])] -> [FQ_PROCESS_NAME]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, [ProcProfile]) -> FQ_PROCESS_NAME
f [(SORT, [ProcProfile])]
procNamesAndProfileSet
    in DomainEntry -> IsaTheory -> IsaTheory
updateDomainTab DomainEntry
procNameDomainEntry IsaTheory
isaTh

{- | Make a proccess name Domain Entry from a list of fully qualified Process
names. This creates a data type for the process names. -}
mkFQProcNameDE :: [FQ_PROCESS_NAME] -> DomainEntry
mkFQProcNameDE :: [FQ_PROCESS_NAME] -> DomainEntry
mkFQProcNameDE fqProcesses :: [FQ_PROCESS_NAME]
fqProcesses =
    let -- The a list of pairs of constructors and their arguments
        constructors :: [(VName, [Typ])]
constructors = (FQ_PROCESS_NAME -> (VName, [Typ]))
-> [FQ_PROCESS_NAME] -> [(VName, [Typ])]
forall a b. (a -> b) -> [a] -> [b]
map FQ_PROCESS_NAME -> (VName, [Typ])
mk_cons [FQ_PROCESS_NAME]
fqProcesses
        {- Take a proccess name and its argument sorts (also its
        commAlpha - thrown away) and make a pair representing the
        constructor and the argument types
        Note: The processes need to have arguments of the bar variants of the
        sorts not the original sorts -}
        mk_cons :: FQ_PROCESS_NAME -> (VName, [Typ])
mk_cons fqProcName :: FQ_PROCESS_NAME
fqProcName = case FQ_PROCESS_NAME
fqProcName of
          FQ_PROCESS_NAME _ (ProcProfile argSorts :: [SORT]
argSorts _) ->
            (String -> VName
mkVName (FQ_PROCESS_NAME -> String
mkProcNameConstructor FQ_PROCESS_NAME
fqProcName),
             (SORT -> Typ) -> [SORT] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Typ
mkSortBarType [SORT]
argSorts)
          _ -> String -> (VName, [Typ])
forall a. HasCallStack => String -> a
error "CspCASLProver.Utils.mkFQProcNameDE: Applied to non fully\
                      \ qualified processes name."
    in
    (Typ
procNameType, [(VName, [Typ])]
constructors)

{- -----------------------------------------------------------------------
Functions adding the process map function to an Isabelle theory     --
----------------------------------------------------------------------- -}

{- | Add the function procMap to an Isabelle theory. This function maps process
names to real processes build using the same names and the alphabet i.e.,
in CSP-Prover syntax:
ProcName => (ProcName, Alphabet) proc. We need to know the CspCASL
sentences and the casl signature (data part). We need the PCFOL and CFOL
signatures of the data part after translation to PCFOL and CFOL to pass
along the process translation. -}
addProcMap :: [Named CspCASLSen] -> CspCASLSign ->
              CASLSign.Sign () () -> CASLSign.Sign () () ->
              IsaTheory -> IsaTheory
addProcMap :: [Named CspCASLSen]
-> CspCASLSign -> CASLSign -> CASLSign -> IsaTheory -> IsaTheory
addProcMap namedSens :: [Named CspCASLSen]
namedSens ccSign :: CspCASLSign
ccSign pcfolSign :: CASLSign
pcfolSign cfolSign :: CASLSign
cfolSign isaTh :: IsaTheory
isaTh =
    let caslSign :: CASLSign
caslSign = CspCASLSign -> CASLSign
ccSig2CASLSign CspCASLSign
ccSign
        -- Translate a fully qualified variable (CASL term) to Isabelle
        tyToks :: Set String
tyToks = CASLSign -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.typeToks CASLSign
caslSign
        trForm :: FormulaTranslator () ()
trForm = FormulaTranslator () ()
CFOL2IsabelleHOL.formTrCASL
        strs :: Set String
strs = CASLSign -> Set String
forall f e. Sign f e -> Set String
CFOL2IsabelleHOL.getAssumpsToks CASLSign
caslSign
        transVar :: TERM () -> Term
transVar = Record () Term Term -> TERM () -> Term
forall f a b. Record f a b -> TERM f -> b
CASL_Fold.foldTerm
                    (CASLSign
-> Set String
-> FormulaTranslator () ()
-> Set String
-> Record () Term Term
forall f e.
Sign f e
-> Set String
-> FormulaTranslator f e
-> Set String
-> Record f Term Term
CFOL2IsabelleHOL.transRecord
                     CASLSign
caslSign Set String
tyToks FormulaTranslator () ()
trForm Set String
strs)
        {- Get the plain sentences from the named senetences which are not
        implied i.e., where axiom=true. first filter the axioms only then
        stip the named annotation off them. -}
        sens :: [CspCASLSen]
sens = (Named CspCASLSen -> CspCASLSen)
-> [Named CspCASLSen] -> [CspCASLSen]
forall a b. (a -> b) -> [a] -> [b]
map Named CspCASLSen -> CspCASLSen
forall s a. SenAttr s a -> s
sentence ([Named CspCASLSen] -> [CspCASLSen])
-> [Named CspCASLSen] -> [CspCASLSen]
forall a b. (a -> b) -> a -> b
$ (Named CspCASLSen -> Bool)
-> [Named CspCASLSen] -> [Named CspCASLSen]
forall a. (a -> Bool) -> [a] -> [a]
filter Named CspCASLSen -> Bool
forall s a. SenAttr s a -> Bool
isAxiom [Named CspCASLSen]
namedSens
        -- Filter so we only have proccess equations and no CASL senetences
        processEqs :: [CspCASLSen]
processEqs = (CspCASLSen -> Bool) -> [CspCASLSen] -> [CspCASLSen]
forall a. (a -> Bool) -> [a] -> [a]
filter CspCASLSen -> Bool
isProcessEq [CspCASLSen]
sens
        {- the term representing the procMap that takes a term as a
        parameter -}
        procMapTerm :: Term -> Term
procMapTerm = Term -> Term -> Term
termAppl (String -> Term
conDouble String
procMapS)
        -- Make a single equation for the primrec from a process equation
        mkEq :: CspCASLSen -> Term
mkEq f :: CspCASLSen
f = case CspCASLSen
f of
          ExtFORMULA (ProcessEq fqProcName :: FQ_PROCESS_NAME
fqProcName fqVars :: FQProcVarList
fqVars _ proc :: PROCESS
proc) ->
            let -- Make the name (string) for this process
                procNameString :: String
procNameString = FQ_PROCESS_NAME -> String
convertFQProcessName2String FQ_PROCESS_NAME
fqProcName
                -- Change the name to a term
                procNameTerm :: Term
procNameTerm = String -> Term
conDouble String
procNameString
                {- Turn the list of variables into a list of Isabelle
                free variables -}
                varTerms :: [Term]
varTerms = (TERM () -> Term) -> FQProcVarList -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map TERM () -> Term
transVar FQProcVarList
fqVars
                lhs :: Term
lhs = Term -> Term
procMapTerm ((Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> Term -> Term
termAppl Term
procNameTerm [Term]
varTerms)
                addToVdm :: TERM f -> Map VAR VarSource -> Map VAR VarSource
addToVdm fqvar :: TERM f
fqvar vdm' :: Map VAR VarSource
vdm' =
                    case TERM f
fqvar of
                      Qual_var v :: VAR
v _ _ -> VAR -> VarSource -> Map VAR VarSource -> Map VAR VarSource
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VAR
v VarSource
GlobalParameter Map VAR VarSource
vdm'
                      _ -> String -> Map VAR VarSource
forall a. HasCallStack => String -> a
error "CspCASLProver.Utils.addProcMap: Term other\
                                \ than fully qualified variable in process\
                                \ parameter variable list"
                vdm :: Map VAR VarSource
vdm = (TERM () -> Map VAR VarSource -> Map VAR VarSource)
-> Map VAR VarSource -> FQProcVarList -> Map VAR VarSource
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TERM () -> Map VAR VarSource -> Map VAR VarSource
forall f. TERM f -> Map VAR VarSource -> Map VAR VarSource
addToVdm Map VAR VarSource
forall k a. Map k a
Map.empty FQProcVarList
fqVars
                rhs :: Term
rhs = CspCASLSign
-> CASLSign -> CASLSign -> Map VAR VarSource -> PROCESS -> Term
transProcess CspCASLSign
ccSign CASLSign
pcfolSign CASLSign
cfolSign Map VAR VarSource
vdm PROCESS
proc
             in Term -> Term -> Term
binEq Term
lhs Term
rhs
          _ -> String -> Term
forall a. HasCallStack => String -> a
error "addProcMap: no ProcessEq"
        -- Build equations for primrec using process equations
        eqs :: [Term]
eqs = (CspCASLSen -> Term) -> [CspCASLSen] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map CspCASLSen -> Term
mkEq [CspCASLSen]
processEqs
    in String -> Typ -> [Term] -> IsaTheory -> IsaTheory
addPrimRec String
procMapS Typ
procMapType [Term]
eqs IsaTheory
isaTh

{- | Add the implied process equations as theorems to be proven by the user. We
need to know the CspCASL sentences and the casl signature (data part). We
need the PCFOL and CFOL signatures of the data part after translation to
PCFOL and CFOL to pass along the process translation. -}
addProcTheorems :: [Named CspCASLSen] -> CspCASLSign ->
                   CASLSign.Sign () () -> CASLSign.Sign () () ->
                   IsaTheory -> IsaTheory
addProcTheorems :: [Named CspCASLSen]
-> CspCASLSign -> CASLSign -> CASLSign -> IsaTheory -> IsaTheory
addProcTheorems namedSens :: [Named CspCASLSen]
namedSens ccSign :: CspCASLSign
ccSign pcfolSign :: CASLSign
pcfolSign cfolSign :: CASLSign
cfolSign isaTh :: IsaTheory
isaTh =
    let {- Get the plain sentences from the named senetences which are
        implied i.e., where axiom=false. first filter the axioms only then
        stip the named annotation off them. -}
        sens :: [CspCASLSen]
sens = (Named CspCASLSen -> CspCASLSen)
-> [Named CspCASLSen] -> [CspCASLSen]
forall a b. (a -> b) -> [a] -> [b]
map Named CspCASLSen -> CspCASLSen
forall s a. SenAttr s a -> s
sentence ([Named CspCASLSen] -> [CspCASLSen])
-> [Named CspCASLSen] -> [CspCASLSen]
forall a b. (a -> b) -> a -> b
$ (Named CspCASLSen -> Bool)
-> [Named CspCASLSen] -> [Named CspCASLSen]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (Named CspCASLSen -> Bool) -> Named CspCASLSen -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named CspCASLSen -> Bool
forall s a. SenAttr s a -> Bool
isAxiom) [Named CspCASLSen]
namedSens
        -- Filter so we only have proccess equations and no CASL senetences
        processEqs :: [CspCASLSen]
processEqs = (CspCASLSen -> Bool) -> [CspCASLSen] -> [CspCASLSen]
forall a. (a -> Bool) -> [a] -> [a]
filter CspCASLSen -> Bool
isProcessEq [CspCASLSen]
sens
        {- Make a single equation for the primrec from a process equation
        mkEq (ProcessEq procName fqVars _ proc) = -}
        mkEq :: CspCASLSen -> Term
mkEq f :: CspCASLSen
f = case CspCASLSen
f of
          ExtFORMULA (ProcessEq fqProcName :: FQ_PROCESS_NAME
fqProcName fqVars :: FQProcVarList
fqVars _ proc :: PROCESS
proc) ->
            let {- the LHS a a process in abstract syntax i.e. process name with
                variables as arguments -}
                lhs' :: PROCESS
lhs' = FQ_PROCESS_NAME -> FQProcVarList -> Range -> PROCESS
NamedProcess FQ_PROCESS_NAME
fqProcName FQProcVarList
fqVars Range
nullRange
                addToVdm :: TERM f -> Map VAR VarSource -> Map VAR VarSource
addToVdm fqvar :: TERM f
fqvar vdm' :: Map VAR VarSource
vdm' =
                    case TERM f
fqvar of
                      Qual_var v :: VAR
v _ _ -> VAR -> VarSource -> Map VAR VarSource -> Map VAR VarSource
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VAR
v VarSource
GlobalParameter Map VAR VarSource
vdm'
                      _ -> String -> Map VAR VarSource
forall a. HasCallStack => String -> a
error "CspCASLProver.Utils.addProcMap: Term other\
                                \ than fully qualified variable in process\
                                \ parameter variable list"
                vdm :: Map VAR VarSource
vdm = (TERM () -> Map VAR VarSource -> Map VAR VarSource)
-> Map VAR VarSource -> FQProcVarList -> Map VAR VarSource
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TERM () -> Map VAR VarSource -> Map VAR VarSource
forall f. TERM f -> Map VAR VarSource -> Map VAR VarSource
addToVdm Map VAR VarSource
forall k a. Map k a
Map.empty FQProcVarList
fqVars
                lhs :: Term
lhs = CspCASLSign
-> CASLSign -> CASLSign -> Map VAR VarSource -> PROCESS -> Term
transProcess CspCASLSign
ccSign CASLSign
pcfolSign CASLSign
cfolSign Map VAR VarSource
vdm PROCESS
lhs'
                rhs :: Term
rhs = CspCASLSign
-> CASLSign -> CASLSign -> Map VAR VarSource -> PROCESS -> Term
transProcess CspCASLSign
ccSign CASLSign
pcfolSign CASLSign
cfolSign Map VAR VarSource
vdm PROCESS
proc
             in Term -> Term -> Term
cspProverbinEqF Term
lhs Term
rhs
          _ -> String -> Term
forall a. HasCallStack => String -> a
error "addProcTheorems: no ProcessEq"
        eqs :: [Term]
eqs = (CspCASLSen -> Term) -> [CspCASLSen] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map CspCASLSen -> Term
mkEq [CspCASLSen]
processEqs
        proof' :: IsaProof
proof' = ProofEnd -> IsaProof
toIsaProof ProofEnd
Sorry
        addTheorem :: Term -> IsaTheory -> IsaTheory
addTheorem eq' :: Term
eq' = String -> [Term] -> Term -> IsaProof -> IsaTheory -> IsaTheory
addTheoremWithProof "UserTheorem" [] Term
eq' IsaProof
proof'
    in (Term -> IsaTheory -> IsaTheory)
-> IsaTheory -> [Term] -> IsaTheory
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Term -> IsaTheory -> IsaTheory
addTheorem IsaTheory
isaTh [Term]
eqs


{- ----------------------------------------------------------
Basic function to help keep strings consistent         --
---------------------------------------------------------- -}

{- | Return the list of strings of all gn_totality axiom names produced by the
translation CASL2PCFOL; CASL2SubCFOL. This function is not implemented in a
satisfactory way. -}
getCollectionTotAx :: CASLSign.CASLSign -> [String]
getCollectionTotAx :: CASLSign -> [String]
getCollectionTotAx pfolSign :: CASLSign
pfolSign =
    let totOpList :: [(SORT, [OpType])]
totOpList = MapSet SORT OpType -> [(SORT, [OpType])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList (MapSet SORT OpType -> [(SORT, [OpType])])
-> (MapSet SORT OpType -> MapSet SORT OpType)
-> MapSet SORT OpType
-> [(SORT, [OpType])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpType -> Bool) -> MapSet SORT OpType -> MapSet SORT OpType
forall a b.
(Ord a, Ord b) =>
(b -> Bool) -> MapSet a b -> MapSet a b
MapSet.filter OpType -> Bool
CASLSign.isTotal
                 (MapSet SORT OpType -> [(SORT, [OpType])])
-> MapSet SORT OpType -> [(SORT, [OpType])]
forall a b. (a -> b) -> a -> b
$ CASLSign -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
CASLSign.opMap CASLSign
pfolSign
    in ((SORT, [OpType]) -> String) -> [(SORT, [OpType])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SORT -> String
mkTotalityAxiomName (SORT -> String)
-> ((SORT, [OpType]) -> SORT) -> (SORT, [OpType]) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT, [OpType]) -> SORT
forall a b. (a, b) -> a
fst) [(SORT, [OpType])]
totOpList

{- | Return the name of the definedness function for a sort. We need
to know all sorts to perform this workaround
This function is not implemented in a satisfactory way -}
getDefinedName :: [SORT] -> SORT -> String
getDefinedName :: [SORT] -> SORT -> String
getDefinedName sorts :: [SORT]
sorts s :: SORT
s =
    let index :: Maybe Int
index = SORT -> [SORT] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex SORT
s [SORT]
sorts
        str :: String
str = case Maybe Int
index of
                Nothing -> ""
                Just i :: Int
i -> Int -> String
forall a. Show a => a -> String
show (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
    in "gn_definedX" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str

{- | Return the name of the injection as it is used in the alternative
syntax of the injection from one sort to another.
This function is not implemented in a satisfactory way -}
getInjectionName :: SORT -> SORT -> String
getInjectionName :: SORT -> SORT -> String
getInjectionName s :: SORT
s s' :: SORT
s' =
    let t :: OP_TYPE
t = OpType -> OP_TYPE
CASLSign.toOP_TYPE (OpType -> OP_TYPE) -> OpType -> OP_TYPE
forall a b. (a -> b) -> a -> b
$ [SORT] -> SORT -> OpType
CASLSign.mkTotOpType [SORT
s] SORT
s'
        injName :: String
injName = SORT -> String
forall a. Show a => a -> String
show (SORT -> String) -> SORT -> String
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> SORT
CASLInject.uniqueInjName OP_TYPE
t
    in String
injName

{- | Return the injection name of the injection from one sort to another
This function is not implemented in a satisfactory way -}
getDefinedOp :: [SORT] -> SORT -> Term -> Term
getDefinedOp :: [SORT] -> SORT -> Term -> Term
getDefinedOp sorts :: [SORT]
sorts s :: SORT
s =
    Term -> Term -> Term
termAppl (VName -> Term
con (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ String -> Maybe AltSyntax -> VName
VName ([SORT] -> SORT -> String
getDefinedName [SORT]
sorts SORT
s) Maybe AltSyntax
forall a. Maybe a
Nothing)

{- | Return the term representing the injection of a term from one sort to
another. Note: the term is returned if both sorts are the same. This
function is not implemented in a satisfactory way. -}
mkInjection :: SORT -> SORT -> Term -> Term
mkInjection :: SORT -> SORT -> Term -> Term
mkInjection s :: SORT
s s' :: SORT
s' t :: Term
t =
    let injName :: String
injName = SORT -> SORT -> String
getInjectionName SORT
s SORT
s'
        replace :: t b -> b -> [b] -> [b]
replace string :: t b
string c :: b
c s1 :: [b]
s1 = (b -> [b]) -> t b -> [b]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ x :: b
x -> if b
x b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
c
                                                 then [b]
s1
                                                 else [b
x]) t b
string
        injOp :: Term
injOp = Const :: VName -> DTyp -> Term
Const {
                  termName :: VName
termName = VName :: String -> Maybe AltSyntax -> VName
VName {
                              new :: String
new = "X_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
injName,
                              altSyn :: Maybe AltSyntax
altSyn = AltSyntax -> Maybe AltSyntax
forall a. a -> Maybe a
Just (String -> [Int] -> Int -> AltSyntax
AltSyntax
                                             (String -> Char -> String -> String
forall (t :: * -> *) b.
(Foldable t, Eq b) =>
t b -> b -> [b] -> [b]
replace String
injName '_' "'_"
                                              String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/'(_')") [3] 999)
                            },
                  termType :: DTyp
termType = Hide :: Typ -> TAttr -> Maybe Int -> DTyp
Hide {
                               typ :: Typ
typ = Type :: String -> Sort -> [Typ] -> Typ
Type {
                                       typeId :: String
typeId = "dummy",
                                       typeSort :: Sort
typeSort = [String -> IsaClass
IsaClass "type"],
                                       typeArgs :: [Typ]
typeArgs = []
                                     },
                               kon :: TAttr
kon = TAttr
NA,
                               arit :: Maybe Int
arit = Maybe Int
forall a. Maybe a
Nothing
                             }
                }
    in if SORT
s SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s'
       then Term
t
       else Term -> Term -> Term
termAppl Term
injOp Term
t

{- | Return the list of string of all ga_embedding_injectivity axioms
produced by the translation CASL2PCFOL; CASL2SubCFOL. -}
getCollectionEmbInjAx :: [(SORT, SORT)] -> [String]
getCollectionEmbInjAx :: [(SORT, SORT)] -> [String]
getCollectionEmbInjAx sortRel :: [(SORT, SORT)]
sortRel =
    let mkName :: (SORT, SORT) -> String
mkName (s :: SORT
s, s' :: SORT
s') = String -> String
transString (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ SORT -> SORT -> String
mkEmbInjName SORT
s SORT
s'
    in ((SORT, SORT) -> String) -> [(SORT, SORT)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, SORT) -> String
mkName [(SORT, SORT)]
sortRel

{- | Return the list of strings of all ga_notDefBottom axioms produced by
the translation CASL2PCFOL; CASL2SubCFOL. -}
getCollectionNotDefBotAx :: [SORT] -> [String]
getCollectionNotDefBotAx :: [SORT] -> [String]
getCollectionNotDefBotAx = (SORT -> String) -> [SORT] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((SORT -> String) -> [SORT] -> [String])
-> (SORT -> String) -> [SORT] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> String
transString (String -> String) -> (SORT -> String) -> SORT -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> String
mkNotDefBotAxiomName

{- | Return the list of strings of all the transitivity axioms names produced by
the translation CASL2PCFOL; CASL2SubCFOL. -}
getCollectionTransAx :: CASLSign.CASLSign -> [String]
getCollectionTransAx :: CASLSign -> [String]
getCollectionTransAx caslSign :: CASLSign
caslSign =
    let sorts :: [SORT]
sorts = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
CASLSign.sortSet CASLSign
caslSign
        allSupers :: SORT -> SORT -> SORT -> Bool
allSupers s :: SORT
s s' :: SORT
s' s'' :: SORT
s'' =
            SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s' (SORT -> CASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
CASLSign.supersortsOf SORT
s CASLSign
caslSign) Bool -> Bool -> Bool
&&
            SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s'' (SORT -> CASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
CASLSign.supersortsOf SORT
s' CASLSign
caslSign) Bool -> Bool -> Bool
&& (SORT
s SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
/= SORT
s'')
    in [String -> String
transString (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ SORT -> SORT -> SORT -> String
mkTransAxiomName SORT
s SORT
s' SORT
s''
            | SORT
s <- [SORT]
sorts, SORT
s' <- [SORT]
sorts, SORT
s'' <- [SORT]
sorts, SORT -> SORT -> SORT -> Bool
allSupers SORT
s SORT
s' SORT
s'']

{- | Return the list of strings of all the identity axioms names produced by
the translation CASL2PCFOL; CASL2SubCFOL. -}
getCollectionIdentityAx :: CASLSign.CASLSign -> [String]
getCollectionIdentityAx :: CASLSign -> [String]
getCollectionIdentityAx caslSign :: CASLSign
caslSign =
    let sorts :: [SORT]
sorts = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
CASLSign.sortSet CASLSign
caslSign
        isomorphic :: SORT -> SORT -> Bool
isomorphic s :: SORT
s s' :: SORT
s' = SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s (SORT -> CASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
CASLSign.supersortsOf SORT
s' CASLSign
caslSign) Bool -> Bool -> Bool
&&
                          SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s' (SORT -> CASLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
CASLSign.supersortsOf SORT
s CASLSign
caslSign)
    in [String -> String
transString (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ SORT -> SORT -> String
mkIdAxiomName SORT
s SORT
s'
            | SORT
s <- [SORT]
sorts, SORT
s' <- [SORT]
sorts, SORT -> SORT -> Bool
isomorphic SORT
s SORT
s']


{- | Return the list of string of all decomposition theorem names that we
generate. This function is not implemented in a satisfactory way -}
getColDecompositionThmName :: [(SORT, SORT)] -> [String]
getColDecompositionThmName :: [(SORT, SORT)] -> [String]
getColDecompositionThmName sortRel :: [(SORT, SORT)]
sortRel =
    let tripples :: [(SORT, SORT, SORT)]
tripples = [(SORT
s1, SORT
s2, SORT
s3) |
                    (s1 :: SORT
s1, s2 :: SORT
s2) <- [(SORT, SORT)]
sortRel, (s2' :: SORT
s2', s3 :: SORT
s3) <- [(SORT, SORT)]
sortRel, SORT
s2 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s2']
    in ((SORT, SORT, SORT) -> String) -> [(SORT, SORT, SORT)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, SORT, SORT) -> String
getDecompositionThmName [(SORT, SORT, SORT)]
tripples

{- | Produce the theorem name of the decomposition theorem that we produce for a
gievn tripple of sorts. -}
getDecompositionThmName :: (SORT, SORT, SORT) -> String
getDecompositionThmName :: (SORT, SORT, SORT) -> String
getDecompositionThmName (s :: SORT
s, s' :: SORT
s', s'' :: SORT
s'') =
    "ccprover_decomposition_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String
convertSort2String SORT
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++
    SORT -> String
convertSort2String SORT
s' String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String
convertSort2String SORT
s''

{- | Return the list of strings of the injectivity theorem names that we
generate.  This function is not implemented in a satisfactory way -}
getColInjectivityThmName :: [(SORT, SORT)] -> [String]
getColInjectivityThmName :: [(SORT, SORT)] -> [String]
getColInjectivityThmName = ((SORT, SORT) -> String) -> [(SORT, SORT)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, SORT) -> String
getInjectivityThmName

{- | Produce the theorem name of the injectivity theorem that we produce for a
gievn pair of sorts. -}
getInjectivityThmName :: (SORT, SORT) -> String
getInjectivityThmName :: (SORT, SORT) -> String
getInjectivityThmName (s :: SORT
s, s' :: SORT
s') =
    "ccprover_injectivity_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String
convertSort2String SORT
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++
    SORT -> String
convertSort2String SORT
s'