{- |
Module      :  $Header$
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, Nothing),
         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 = if sort == sort' then [binEq x y] else []
                test2 = if Set.member sort sort'SuperSet
                        then [binEq x (mkInjection sort' sort y)]
                        else []
                test3 = if Set.member sort' sortSuperSet
                        then [binEq (mkInjection sort sort' x) y]
                        else []
                test4 = if null commonSuperList
                        then []
                        else 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,Nothing), (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,Nothing), 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 fqVar = CASL_Fold.foldTerm
                         (CFOL2IsabelleHOL.transRecord
                          caslSign tyToks trForm strs) fqVar
        -- 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' isaTh' = addTheoremWithProof "UserTheorem" [] eq'
                               proof' isaTh'
    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 t =
    termAppl (con $ VName (getDefinedName sorts s) Nothing) t

-- | 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 = concat (map (\ 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 sortRel = map getInjectivityThmName sortRel

-- | 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'
