content: {- |
  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 sortList isaTh =
     let preAlphabetDomainEntry = mkPreAlphabetDE sortList
         -- Add to the isabelle signature the new domain entry
     in updateDomainTab preAlphabetDomainEntry isaTh
  
  -- | Make a Domain Entry for the PreAlphabet from a list of sorts.
  mkPreAlphabetDE :: [SORT] -> DomainEntry
  mkPreAlphabetDE sorts =
      (mkSType preAlphabetS,
           map (\ sort ->
                    (mkVName (mkPreAlphabetConstructor sort),
                                 [mkSType $ convertSort2String 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 sortList isaTh =
      let eqtype = mkFunType preAlphabetType $ mkFunType preAlphabetType boolType
          mkEq sort =
              let x = mkFree "x"
                  y = mkFree "y"
                  lhs = binEq_PreAlphabet lhs_a y
                  lhs_a = termAppl (conDouble (mkPreAlphabetConstructor sort)) x
                  rhs = termAppl rhs_a y
                  rhs_a = termAppl (conDouble (mkCompareWithFunName sort)) x
              in binEq lhs rhs
          eqs = map mkEq sortList
      in addPrimRec eq_PreAlphabetS eqtype eqs 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 isaTh =
      let sortList = Set.toList (CASLSign.sortSet caslSign)
      in foldl (addCompareWithFun caslSign) isaTh 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 isaTh sort =
      let sortList = Set.toList (CASLSign.sortSet caslSign)
          sortType = Type {typeId = convertSort2String sort, typeSort = [],
                                    typeArgs = []}
          funName = mkCompareWithFunName sort
          funType = mkFunType sortType $ mkFunType preAlphabetType boolType
          sortSuperSet = CASLSign.supersortsOf sort caslSign
          mkEq sort' =
              let x = mkFree "x"
                  y = mkFree "y"
                  sort'Constructor = mkPreAlphabetConstructor sort'
                  lhs = termAppl lhs_a lhs_b
                  lhs_a = termAppl (conDouble funName) x
                  lhs_b = termAppl (conDouble sort'Constructor) y
                  sort'SuperSet = CASLSign.supersortsOf sort' caslSign
                  commonSuperList = Set.toList (Set.intersection
                                                   sortSuperSet
                                                   sort'SuperSet)
  
                  {- If there are no tests then the rhs=false else
                  combine all tests using binConj -}
                  rhs = if null allTests
                        then false
                        else foldr1 binConj 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 = concat [test1, test2, test3, test4]
                  test1 = [binEq x y | sort == sort']
                  test2 = [binEq x (mkInjection sort' sort y) |
                           Set.member sort sort'SuperSet]
                  test3 = [binEq (mkInjection sort sort' x) y |
                           Set.member sort' sortSuperSet]
                  test4 = map test4_atSort commonSuperList
                  test4_atSort s = binEq (mkInjection sort s x)
                                         (mkInjection sort' s y)
              in binEq lhs rhs
          eqs = map mkEq sortList
      in addPrimRec funName funType eqs 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 pfolSign isaTh =
      let sortRel = Rel.toList (CASLSign.sortRel caslSign)
          sorts = Set.toList (CASLSign.sortSet caslSign)
      in addLemmasCollection lemmasEmbInjAxS (getCollectionEmbInjAx sortRel)
       $ addLemmasCollection lemmasIdentityAxS (getCollectionIdentityAx caslSign)
       $ addLemmasCollection lemmasNotDefBotAxS (getCollectionNotDefBotAx sorts)
       $ addLemmasCollection lemmasTotalityAxS (getCollectionTotAx pfolSign)
       $ addLemmasCollection lemmasTransAxS (getCollectionTransAx caslSign)
         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 pfolSign isaTh =
      let sortRel = Rel.toList (CASLSign.sortRel caslSign)
          sorts = Set.toList (CASLSign.sortSet caslSign)
      in addTransitivityTheorem sorts sortRel
         $ addAllInjectivityTheorems pfolSign sorts sortRel
         $ addAllDecompositionTheorem caslSign pfolSign sorts sortRel
         $ addSymmetryTheorem sorts
         $ addReflexivityTheorem
           isaTh
  
  -- | Add the reflexivity theorem and proof to an Isabelle Theory
  addReflexivityTheorem :: IsaTheory -> IsaTheory
  addReflexivityTheorem isaTh =
      let name = reflexivityTheoremS
          x = mkFree "x"
          thmConds = []
          thmConcl = binEq_PreAlphabet x x
          proof' = IsaProof {
                     proof = [Apply [Induct x, Auto] False],
                     end = Done
                   }
      in addTheoremWithProof name thmConds thmConcl proof' 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 _ isaTh =
      let -- numSorts = length(sorts)
          name = symmetryTheoremS
          x = mkFree "x"
          y = mkFree "y"
          thmConds = [binEq_PreAlphabet x y]
          thmConcl = binEq_PreAlphabet y 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 = [Apply [Induct y, Auto] True]
          proof' = IsaProof {
                     -- Add in front of inductY a apply induct on x
                     proof = Apply [Induct x] False : inductY,
                     end = Done
                   }
      in addTheoremWithProof name thmConds thmConcl proof' isaTh
  
  -- | Add all the decoposition theorems and proofs
  addAllDecompositionTheorem :: CASLSign.CASLSign -> CASLSign.CASLSign
                             -> [SORT] -> [(SORT, SORT)]
                             -> IsaTheory -> IsaTheory
  addAllDecompositionTheorem caslSign pfolSign sorts sortRel isaTh =
      let tripples = [(s1, s2, s3) |
                      (s1, s2) <- sortRel, (s2', s3) <- sortRel, s2 == s2']
      in foldl (addDecompositionTheorem caslSign pfolSign sorts)
         isaTh 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 pfolSign sorts isaTh (s1, s2, s3) =
      let x = mkFree "x"
          -- These 5 lines make use of currying
          injOp_s1_s2 = mkInjection s1 s2
          injOp_s2_s3 = mkInjection s2 s3
          injOp_s1_s3 = mkInjection s1 s3
          inj_s1_s2_s3_x = injOp_s2_s3 (injOp_s1_s2 x)
          inj_s1_s3_x = injOp_s1_s3 x
          definedOp_s1 = getDefinedOp sorts s1
          definedOp_s3 = getDefinedOp sorts s3
  
          name = getDecompositionThmName (s1, s2, s3)
          conds = []
          concl = binEq inj_s1_s2_s3_x inj_s1_s3_x
          -- We only want to add these lemma sets if they exist
          lemmasIdentityAxS' = if null $ getCollectionIdentityAx caslSign
                               then []
                               else [lemmasIdentityAxS]
          lemmasTransAxS' = if null $ getCollectionTransAx caslSign
                            then []
                            else [lemmasTransAxS]
          lemmasTotalityAxS' = if null $ getCollectionTotAx pfolSign
                               then []
                               else [lemmasTotalityAxS]
          lemmasNotDefBotAxS' = if null $ getCollectionNotDefBotAx sorts
                                then []
                                else [lemmasNotDefBotAxS]
          proof' = IsaProof [Apply [CaseTac (definedOp_s3 inj_s1_s2_s3_x)] False,
                             -- Case 1
                             Apply [SubgoalTac (definedOp_s1 x)] False,
                             Apply [Insert $ lemmasIdentityAxS' ++
                                          lemmasTransAxS'] False,
                             Apply [Simp] False,
                             Apply [SimpAdd Nothing lemmasTotalityAxS'] False,
  
                             -- Case 2
                             Apply [SubgoalTac (
                               termAppl notOp (definedOp_s3 inj_s1_s3_x))] False,
                             Apply [SimpAdd Nothing lemmasNotDefBotAxS'] False,
                             Apply [SimpAdd Nothing lemmasTotalityAxS'] False]
                             Done
      in addTheoremWithProof name conds concl proof' isaTh
  
  -- | Add all the injectivity theorems and proofs
  addAllInjectivityTheorems :: CASLSign.CASLSign -> [SORT] -> [(SORT, SORT)] ->
                               IsaTheory -> IsaTheory
  addAllInjectivityTheorems pfolSign sorts sortRel isaTh =
      foldl (addInjectivityTheorem pfolSign sorts sortRel) isaTh 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 pfolSign sorts sortRel isaTh (s1, s2) =
      let x = mkFree "x"
          y = mkFree "y"
          injX = mkInjection s1 s2 x
          injY = mkInjection s1 s2 y
          definedOp_s1 = getDefinedOp sorts s1
          definedOp_s2 = getDefinedOp sorts s2
          name = getInjectivityThmName (s1, s2)
          conds = [binEq injX injY]
          concl = binEq x y
          -- We only want to add these lemma sets if they exist
          lemmasEmbInjAxS' = if null $ getCollectionEmbInjAx sortRel
                             then []
                             else [lemmasEmbInjAxS]
          lemmasTotalityAxS' = if null $ getCollectionTotAx pfolSign
                               then []
                               else [lemmasTotalityAxS]
          lemmasNotDefBotAxS' = if null $ getCollectionNotDefBotAx sorts
                                then []
                                else [lemmasNotDefBotAxS]
  
          proof' = IsaProof [Apply [CaseTac (definedOp_s2 injX)] False,
                             -- Case 1
                             Apply [SubgoalTac (definedOp_s1 x)] False,
                             Apply [SubgoalTac (definedOp_s1 y)] False,
                             Apply [Insert lemmasEmbInjAxS'] False,
                             Apply [Simp] False,
                             Apply [SimpAdd Nothing lemmasTotalityAxS'] False,
                             Apply [SimpAdd (Just No_asm_use) lemmasTotalityAxS']
                                  False,
                             -- Case 2
                             Apply [SubgoalTac (termAppl notOp (definedOp_s1 x))]
                                  False,
                             Apply [SubgoalTac (termAppl notOp (definedOp_s1 y))]
                                  False,
                             Apply [SimpAdd Nothing lemmasNotDefBotAxS'] False,
                             Apply [SimpAdd Nothing lemmasTotalityAxS'] False,
                             Apply [SimpAdd (Just No_asm_use) lemmasTotalityAxS']
                                  False]
                             Done
      in addTheoremWithProof name conds concl proof' 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 sorts sortRel isaTh =
      let {- First we extend the theory to include the collections of CspCASL
          prover's injectivity and decomposition theorems -}
          isaThExt =
              addLemmasCollection lemmasCCProverInjectivityThmsS
                  (getColInjectivityThmName sortRel)
            $ addLemmasCollection lemmasCCProverDecompositionThmsS
                  (getColDecompositionThmName sortRel)
              isaTh
          numSorts = length sorts
          name = transitivityS
          x = mkFree "x"
          y = mkFree "y"
          z = mkFree "z"
          thmConds = [binEq_PreAlphabet x y, binEq_PreAlphabet y z]
          thmConcl = binEq_PreAlphabet x z
          -- We only want to add these lemma sets if they exist
          lemmasCCProverDecompositionThmsS' =
              if null $ getColDecompositionThmName sortRel
              then []
              else [lemmasCCProverDecompositionThmsS]
          lemmasCCProverInjectivityThmsS' =
              if null $ getColInjectivityThmName sortRel
              then []
              else [lemmasCCProverInjectivityThmsS]
  
          simpPlus = SimpAdd Nothing (lemmasCCProverDecompositionThmsS' ++
                                      lemmasCCProverInjectivityThmsS')
          {- We want to induct Y, Z and perfom simplification is a clever way,
          namely,
          apply(induct y, (induct z, simp * numSorts) * numSorts)+ -}
          inductZ = Induct z : replicate numSorts simpPlus
          inductYZ = Induct y : concat (replicate numSorts inductZ)
          -- Main induction and simplification proof command
          inductPC = [Apply inductYZ True]
          proof' = IsaProof {
                     proof = Apply [Induct x] False : inductPC,
                     end = Done
                   }
      in addTheoremWithProof name thmConds thmConcl proof' isaThExt
  
  {- -----------------------------------------------------------
  Functions for producing instances of equivalence classes --
  ------------------------------------------------------------ -}
  
  {- | Function to add preAlphabet as an equivalence relation to an
  Isabelle theory -}
  addInstanceOfEquiv :: IsaTheory -> IsaTheory
  addInstanceOfEquiv isaTh =
      let equivSort = [IsaClass equivTypeClassS]
          equivProof = IsaProof [Apply [Other "intro_classes"] False,
                                 Apply [Other ("unfold " ++ preAlphabetSimS
                                               ++ "_def")] False,
                                 Apply [Other ("rule " ++ reflexivityTheoremS)]
                                       False,
                                 Apply [Other ("rule " ++ transitivityS
                                                  ++ ", auto")] False,
                                 Apply [Other ("rule " ++ symmetryTheoremS
                                                  ++ ", simp")] False]
                                 Done
          x = mkFree "x"
          y = mkFree "y"
          defLhs = binEqvSim x y
          defRhs = binEq_PreAlphabet x y
          def = IsaEq defLhs defRhs
      in addInstanceOf preAlphabetS [] equivSort
             [(preAlphabetSimS, def)] equivProof isaTh
  
  {- -----------------------------------------------------------
  Functions for producing the alphabet type               --
  ----------------------------------------------------------- -}
  
  -- | Function to add the Alphabet type (type syonnym) to an Isabelle theory
  addAlphabetType :: IsaTheory -> IsaTheory
  addAlphabetType isaTh =
      let isaTh_sign = fst isaTh
          isaTh_sign_tsig = tsig isaTh_sign
          myabbrs = abbrs isaTh_sign_tsig
          abbrsNew = Map.insert alphabetS ([], preAlphabetQuotType) myabbrs
  
          isaTh_sign_updated = isaTh_sign {
                                 tsig = isaTh_sign_tsig {abbrs = abbrsNew}
                               }
      in (isaTh_sign_updated, snd isaTh)
  
  {- -----------------------------------------------------------
  Functions for producing the bar types                   --
  ----------------------------------------------------------- -}
  
  -- | Function to add all the bar types to an Isabelle theory.
  addAllBarTypes :: [SORT] -> IsaTheory -> IsaTheory
  addAllBarTypes sorts isaTh = foldl addBarType isaTh sorts
  
  -- | Function to add the bar types of a sort to an Isabelle theory.
  addBarType :: IsaTheory -> SORT -> IsaTheory
  addBarType isaTh sort =
      let sortBarString = mkSortBarString sort
          barType = mkSortBarType sort
          isaTh_sign = fst isaTh
          isaTh_sen = snd isaTh
          x = mkFree "x"
          y = mkFree "y"
          rhs = termAppl (conDouble (mkPreAlphabetConstructor sort)) y
          bin_eq = binEq x $ termAppl (conDouble classS ) rhs
          exist_eq = termAppl (conDouble exS) (Abs y bin_eq NotCont)
          subset = SubSet x alphabetType exist_eq
          sen = TypeDef barType subset (IsaProof [] (By Auto))
          namedSen = makeNamed sortBarString sen
      in (isaTh_sign, isaTh_sen ++ [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 sorts isaTh =
      let isaTh' = foldl addChooseFunction isaTh sorts -- add function and def
      in foldl addChooseFunctionLemma isaTh' 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 isaTh sort =
      let -- constant
          sortType = Type {typeId = convertSort2String sort,
                           typeSort = [],
                           typeArgs = []}
          chooseFunName = mkChooseFunName sort
          chooseFunType = mkFunType alphabetType sortType
          -- definition
          x = mkFree "x"
          y = mkFree "y"
          contentsOp = termAppl (conDouble "the_elem")
          sortConsOp = termAppl (conDouble (mkPreAlphabetConstructor sort))
          bin_eq = binEq (classOp $ sortConsOp y) x
          subset = SubSet y sortType bin_eq
          lhs = mkChooseFunOp sort x
          rhs = contentsOp (Set subset)
      in  -- Add defintion to theory
          addDef chooseFunName lhs rhs
          -- Add constant to theory
        $ addConst chooseFunName chooseFunType 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 isaTh sort =
      let sortType = Type {typeId = convertSort2String sort,
                           typeSort = [],
                           typeArgs = []}
          chooseFunName = mkChooseFunName sort
          x = mkFree "x"
          y = mkFree "y"
          sortConsOp = termAppl (conDouble (mkPreAlphabetConstructor sort))
          -- theorm
          subgoalTacTermLhsBinEq = binEq (classOp $ sortConsOp y)
                                         (classOp $ sortConsOp x)
          subgoalTacTermLhs = Set $ SubSet y sortType subgoalTacTermLhsBinEq
          subgoalTacTermRhs = Set $ FixedSet [x]
          subgoalTacTerm = binEq subgoalTacTermLhs subgoalTacTermRhs
          thmConds = []
          thmConcl = binEq (mkChooseFunOp sort $ classOp $ sortConsOp x) x
          proof' = IsaProof [Apply [Other ("unfold " ++ chooseFunName ++ "_def")]
                                  False,
                             Apply [SubgoalTac subgoalTacTerm] False,
                             Apply [Simp] False,
                             Apply [SimpAdd Nothing [quotEqualityS]] False,
                             Apply [Other ("unfold " ++ preAlphabetSimS
                                             ++ "_def")] False,
                             Apply [Auto] False]
                             Done
      in addTheoremWithProof chooseFunName thmConds thmConcl proof' 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 sorts caslSign isaTh =
      let pairs = [(s1, s2) | s1 <- sorts, s2 <- sorts]
      in foldl (addIntegrationTheorem_A caslSign) isaTh 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 isaTh (s1, s2) =
      let sortRel = Rel.toList (CASLSign.sortRel caslSign)
          s1SuperSet = CASLSign.supersortsOf s1 caslSign
          s2SuperSet = CASLSign.supersortsOf s2 caslSign
          commonSuperList = Set.toList (Set.intersection
                                           (Set.insert s1 s1SuperSet)
                                           (Set.insert s2 s2SuperSet))
          x = mkFree "x"
          y = mkFree "y"
          s1ConsOp = termAppl (conDouble (mkPreAlphabetConstructor s1))
          s2ConsOp = termAppl (conDouble (mkPreAlphabetConstructor s2))
          rhs = binEq (classOp $ s1ConsOp x) (classOp $ s2ConsOp y)
          lhs = if null commonSuperList
                then false
                else
                    {- BUG pick any common sort for now (this does hold
                    and is valid) we should pick the top most one. -}
                    let s' = head commonSuperList
                    in binEq (mkInjection s1 s' x) (mkInjection s2 s' y)
          thmConds = []
          thmConcl = binEq rhs lhs
          -- theorem names for proof
          colInjThmNames = getColInjectivityThmName sortRel
          colDecompThmNames = getColDecompositionThmName sortRel
          proof' = IsaProof [Apply [SimpAdd Nothing [quotEqualityS]] False,
                             Apply [Other ("unfold " ++ preAlphabetSimS
                                               ++ "_def")] False,
                             Apply [AutoSimpAdd Nothing
                                    (colDecompThmNames ++ colInjThmNames)] False]
                             Done
      in addTheoremWithProof "IntegrationTheorem_A"
         thmConds thmConcl proof' 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 sortRel chanNameMap isaTh =
      let eventDomainEntry = mkEventDE sortRel chanNameMap
         -- Add to the isabelle signature the new domain entry
      in updateDomainTab eventDomainEntry isaTh
  
  -- | Make a Domain Entry for the Event from a list of sorts.
  mkEventDE :: Rel.Rel SORT -> ChanNameMap -> DomainEntry
  mkEventDE _ chanNameMap =
      let flat = (mkVName flatS, [alphabetType])
          -- Make a constuctor type for a channel with a target sort
          mkChanCon (c, s) = (mkVName (convertChannelString c),
                                          [mkSortBarType s])
          {- Make pairs of channel and sorts, where we only build the declared
          channels and not the subsorted channels. -}
          mkAllChanCons = map mkChanCon $ CASLSign.mapSetToList chanNameMap
          {- We build the event type out of the flat constructions and the list of
          channel constructions -}
      in (eventType, flat : mkAllChanCons)
  
  -- | Add the eq function to an Isabelle theory using a list of sorts
  addProjFlatFun :: IsaTheory -> IsaTheory
  addProjFlatFun isaTh =
      let eqtype = mkFunType eventType alphabetType
          x = mkFree "x"
          lhs = termAppl (conDouble projFlatS) flatX
          flatX = termAppl (conDouble flatS) x
          rhs = x
          -- projFlat(Flat x) = x
          eqs = [binEq lhs rhs]
      in addPrimRec projFlatS eqtype eqs 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 sorts isaTh = foldl addFlatType isaTh sorts
  
  -- | Function to add the flat type of a sort to an Isabelle theory.
  addFlatType :: IsaTheory -> SORT -> IsaTheory
  addFlatType isaTh sort =
      let sortFlatString = mkSortFlatString sort
          flatType = Type {typeId = sortFlatString, typeSort = [], typeArgs = []}
          isaTh_sign = fst isaTh
          isaTh_sen = snd isaTh
          x = mkFree "x"
          y = mkFree "y"
          flatY = termAppl (conDouble flatS) y
          -- y in sort_Bar
          condition1 = binMembership y (conDouble $ mkSortBarString sort)
          -- x = Flat y
          condition2 = binEq x flatY
          -- y in sort_Bar /\ x = Flat y
          condition_eq = binConj condition1 condition2
          exist_eq = termAppl (conDouble exS) (Abs y condition_eq NotCont)
          subset = SubSet x eventType exist_eq
          proof' = AutoSimpAdd Nothing [mkSortBarString sort ++ "_def"]
          sen = TypeDef flatType subset (IsaProof [] (By proof'))
          namedSen = makeNamed sortFlatString sen
      in (isaTh_sign, isaTh_sen ++ [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 isaTh =
      let -- Create a list of pairs of process names and thier profiles
          procNamesAndProfileSet = MapSet.toList (procSet cspSign)
          f (name, profileSet) = case profileSet of
               [h] -> FQ_PROCESS_NAME name h -- Just keep the first one
               _ ->
                 error "CspCASLProver.Utils.addProcNameDatatype: CSP-CASL-Prover\
                       \ does not support overloaded process names yet."
          procNameDomainEntry = mkFQProcNameDE $ map f procNamesAndProfileSet
      in updateDomainTab procNameDomainEntry 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 fqProcesses =
      let -- The a list of pairs of constructors and their arguments
          constructors = map mk_cons 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 fqProcName = case fqProcName of
            FQ_PROCESS_NAME _ (ProcProfile argSorts _) ->
              (mkVName (mkProcNameConstructor fqProcName),
               map mkSortBarType argSorts)
            _ -> error "CspCASLProver.Utils.mkFQProcNameDE: Applied to non fully\
                        \ qualified processes name."
      in
      (procNameType, 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 namedSens ccSign pcfolSign cfolSign isaTh =
      let caslSign = ccSig2CASLSign ccSign
          -- Translate a fully qualified variable (CASL term) to Isabelle
          tyToks = CFOL2IsabelleHOL.typeToks caslSign
          trForm = CFOL2IsabelleHOL.formTrCASL
          strs = CFOL2IsabelleHOL.getAssumpsToks caslSign
          transVar = CASL_Fold.foldTerm
                      (CFOL2IsabelleHOL.transRecord
                       caslSign tyToks trForm 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 = map sentence $ filter isAxiom namedSens
          -- Filter so we only have proccess equations and no CASL senetences
          processEqs = filter isProcessEq sens
          {- the term representing the procMap that takes a term as a
          parameter -}
          procMapTerm = termAppl (conDouble procMapS)
          -- Make a single equation for the primrec from a process equation
          mkEq f = case f of
            ExtFORMULA (ProcessEq fqProcName fqVars _ proc) ->
              let -- Make the name (string) for this process
                  procNameString = convertFQProcessName2String fqProcName
                  -- Change the name to a term
                  procNameTerm = conDouble procNameString
                  {- Turn the list of variables into a list of Isabelle
                  free variables -}
                  varTerms = map transVar fqVars
                  lhs = procMapTerm (foldl termAppl procNameTerm varTerms)
                  addToVdm fqvar vdm' =
                      case fqvar of
                        Qual_var v _ _ -> Map.insert v GlobalParameter vdm'
                        _ -> error "CspCASLProver.Utils.addProcMap: Term other\
                                  \ than fully qualified variable in process\
                                  \ parameter variable list"
                  vdm = foldr addToVdm Map.empty fqVars
                  rhs = transProcess ccSign pcfolSign cfolSign vdm proc
               in binEq lhs rhs
            _ -> error "addProcMap: no ProcessEq"
          -- Build equations for primrec using process equations
          eqs = map mkEq processEqs
      in addPrimRec procMapS procMapType eqs 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 namedSens ccSign pcfolSign cfolSign 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 = map sentence $ filter (not . isAxiom) namedSens
          -- Filter so we only have proccess equations and no CASL senetences
          processEqs = filter isProcessEq sens
          {- Make a single equation for the primrec from a process equation
          mkEq (ProcessEq procName fqVars _ proc) = -}
          mkEq f = case f of
            ExtFORMULA (ProcessEq fqProcName fqVars _ proc) ->
              let {- the LHS a a process in abstract syntax i.e. process name with
                  variables as arguments -}
                  lhs' = NamedProcess fqProcName fqVars nullRange
                  addToVdm fqvar vdm' =
                      case fqvar of
                        Qual_var v _ _ -> Map.insert v GlobalParameter vdm'
                        _ -> error "CspCASLProver.Utils.addProcMap: Term other\
                                  \ than fully qualified variable in process\
                                  \ parameter variable list"
                  vdm = foldr addToVdm Map.empty fqVars
                  lhs = transProcess ccSign pcfolSign cfolSign vdm lhs'
                  rhs = transProcess ccSign pcfolSign cfolSign vdm proc
               in cspProverbinEqF lhs rhs
            _ -> error "addProcTheorems: no ProcessEq"
          eqs = map mkEq processEqs
          proof' = toIsaProof Sorry
          addTheorem eq' = addTheoremWithProof "UserTheorem" [] eq' proof'
      in foldr addTheorem isaTh 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 pfolSign =
      let totOpList = MapSet.toList . MapSet.filter CASLSign.isTotal
                   $ CASLSign.opMap pfolSign
      in map (mkTotalityAxiomName . fst) 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 sorts s =
      let index = List.elemIndex s sorts
          str = case index of
                  Nothing -> ""
                  Just i -> show (i + 1)
      in "gn_definedX" ++ 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 s s' =
      let t = CASLSign.toOP_TYPE $ CASLSign.mkTotOpType [s] s'
          injName = show $ CASLInject.uniqueInjName t
      in 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 sorts s =
      termAppl (con $ VName (getDefinedName sorts s) 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 s s' t =
      let injName = getInjectionName s s'
          replace string c s1 = concatMap (\ x -> if x == c
                                                   then s1
                                                   else [x]) string
          injOp = Const {
                    termName = VName {
                                new = "X_" ++ injName,
                                altSyn = Just (AltSyntax
                                               (replace injName '_' "'_"
                                                ++ "/'(_')") [3] 999)
                              },
                    termType = Hide {
                                 typ = Type {
                                         typeId = "dummy",
                                         typeSort = [IsaClass "type"],
                                         typeArgs = []
                                       },
                                 kon = NA,
                                 arit = Nothing
                               }
                  }
      in if s == s'
         then t
         else termAppl injOp t
  
  {- | Return the list of string of all ga_embedding_injectivity axioms
  produced by the translation CASL2PCFOL; CASL2SubCFOL. -}
  getCollectionEmbInjAx :: [(SORT, SORT)] -> [String]
  getCollectionEmbInjAx sortRel =
      let mkName (s, s') = transString $ mkEmbInjName s s'
      in map mkName sortRel
  
  {- | Return the list of strings of all ga_notDefBottom axioms produced by
  the translation CASL2PCFOL; CASL2SubCFOL. -}
  getCollectionNotDefBotAx :: [SORT] -> [String]
  getCollectionNotDefBotAx = map $ transString . mkNotDefBotAxiomName
  
  {- | Return the list of strings of all the transitivity axioms names produced by
  the translation CASL2PCFOL; CASL2SubCFOL. -}
  getCollectionTransAx :: CASLSign.CASLSign -> [String]
  getCollectionTransAx caslSign =
      let sorts = Set.toList $ CASLSign.sortSet caslSign
          allSupers s s' s'' =
              Set.member s' (CASLSign.supersortsOf s caslSign) &&
              Set.member s'' (CASLSign.supersortsOf s' caslSign) && (s /= s'')
      in [transString $ mkTransAxiomName s s' s''
              | s <- sorts, s' <- sorts, s'' <- sorts, allSupers s s' s'']
  
  {- | Return the list of strings of all the identity axioms names produced by
  the translation CASL2PCFOL; CASL2SubCFOL. -}
  getCollectionIdentityAx :: CASLSign.CASLSign -> [String]
  getCollectionIdentityAx caslSign =
      let sorts = Set.toList $ CASLSign.sortSet caslSign
          isomorphic s s' = Set.member s (CASLSign.supersortsOf s' caslSign) &&
                            Set.member s' (CASLSign.supersortsOf s caslSign)
      in [transString $ mkIdAxiomName s s'
              | s <- sorts, s' <- sorts, isomorphic s 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 sortRel =
      let tripples = [(s1, s2, s3) |
                      (s1, s2) <- sortRel, (s2', s3) <- sortRel, s2 == s2']
      in map getDecompositionThmName tripples
  
  {- | Produce the theorem name of the decomposition theorem that we produce for a
  gievn tripple of sorts. -}
  getDecompositionThmName :: (SORT, SORT, SORT) -> String
  getDecompositionThmName (s, s', s'') =
      "ccprover_decomposition_" ++ convertSort2String s ++ "_" ++
      convertSort2String s' ++ "_" ++ convertSort2String 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 = map getInjectivityThmName
  
  {- | Produce the theorem name of the injectivity theorem that we produce for a
  gievn pair of sorts. -}
  getInjectivityThmName :: (SORT, SORT) -> String
  getInjectivityThmName (s, s') =
      "ccprover_injectivity_" ++ convertSort2String s ++ "_" ++
      convertSort2String s'
  