Theory T

section‹Tag-Based Encodings›
theory T 
imports T_G_Prelim
begin


subsection‹The tag translation›

text‹The extension of the function symbols with type tags and type witnesses:›

datatype ('fsym,'tp) efsym = Oldf 'fsym | Tag 'tp | Wit 'tp


context ProblemIkTpart
begin

text‹``TE'' stands for ``tag encoding''›

fun TE_wtFsym where
 "TE_wtFsym (Oldf f) ⟷ wtFsym f"
|"TE_wtFsym (Tag σ) ⟷ True"
|"TE_wtFsym (Wit σ) ⟷ ¬ isRes σ"

fun TE_arOf where
 "TE_arOf (Oldf f) = arOf f"
|"TE_arOf (Tag σ) = [σ]"
|"TE_arOf (Wit σ) = []"

fun TE_resOf where
 "TE_resOf (Oldf f) = resOf f"
|"TE_resOf (Tag σ) = σ"
|"TE_resOf (Wit σ) = σ"

lemma countable_TE_wtFsym: "countable (Collect TE_wtFsym)" (is "countable ?K")
proof-
  let ?F = "λ ef. case ef of Oldf f ⇒ Inl f | Tag σ ⇒ Inr (Inl σ) | Wit σ ⇒ Inr (Inr σ)"
  let ?U = "(UNIV::'tp set) <+> (UNIV::'tp set)"
  let ?L = "(Collect wtFsym) <+> ?U"
  have "inj_on ?F ?K" unfolding inj_on_def apply clarify
  apply(case_tac x, simp_all) by (case_tac y, simp_all)+
  moreover have "?F ` ?K ⊆ ?L" apply clarify by (case_tac ef, auto)
  ultimately have "|?K| ≤o |?L|" unfolding card_of_ordLeq[symmetric] by auto
  moreover have "countable ?L" using countable_wtFsym countable_tp
  by (metis countable_Plus)
  ultimately show ?thesis by(rule countable_ordLeq)
qed

end (* context ProblemIkTpart *)

sublocale ProblemIkTpart < TE? : Signature
where wtFsym = TE_wtFsym and arOf = TE_arOf and resOf = TE_resOf
apply standard
using countable_tp countable_TE_wtFsym countable_wtPsym by auto


context ProblemIkTpart
begin

(* encoding of non-naked terms *)
fun tNN where
"tNN (Var x) =
 (if unprot (tpOfV x) ∨ protFw (tpOfV x) then Var x else Fn (Tag (tpOfV x)) [Var x])"
|
"tNN (Fn f Tl) = (if unprot (resOf f) ∨ protFw (resOf f)
                    then Fn (Oldf f) (map tNN Tl)
                    else Fn (Tag (resOf f)) [Fn (Oldf f) (map tNN Tl)])"

fun tT where
"tT (Var x) = (if unprot (tpOfV x) then Var x else Fn (Tag (tpOfV x)) [Var x])"
|
"tT t = tNN t"

fun tL where
"tL (Pos (Eq T1 T2)) = Pos (Eq (tT T1) (tT T2))"
|
"tL (Neg (Eq T1 T2)) = Neg (Eq (tNN T1) (tNN T2))"
|
"tL (Pos (Pr p Tl)) = Pos (Pr p (map tNN Tl))"
|
"tL (Neg (Pr p Tl)) = Neg (Pr p (map tNN Tl))"

definition "tC ≡ map tL"

(* The extra axioms: *)

(* The function axioms: *)
(* Lefthand side: *)
definition "rOfFax f = Fn (Oldf f) (getTvars (arOf f))"
(* Righthand side: *)
definition "lOfFax f = Fn (Tag (resOf f)) [rOfFax f]"
definition "Fax ≡ {[Pos (Eq (lOfFax f) (rOfFax f))] | f. wtFsym f}"

(* The witness axioms: *)
(* Lefthand side: *)
definition "rOfWax σ = Fn (Wit σ) []"
(* Righthand side: *)
definition "lOfWax σ = Fn (Tag σ) [rOfWax σ]"
definition "Wax ≡ {[Pos (Eq (lOfWax σ) (rOfWax σ))] | σ. ¬ isRes σ ∧ protFw σ}"

definition "tPB = tC ` Φ ∪ Fax ∪ Wax"

(* Well-typedness of the translation: *)
lemma tpOf_tNN[simp]: "TE.tpOf (tNN T) = Ik.tpOf T"
by (induct T) auto

lemma tpOf_t[simp]: "TE.tpOf (tT T) = Ik.tpOf T"
by (cases T) auto

lemma wt_tNN[simp]: "Ik.wt T ⟹ TE.wt (tNN T)"
by (induct T, auto simp add: list_all_iff)

lemma wt_t[simp]: "Ik.wt T ⟹ TE.wt (tT T)"
by (cases T, auto simp add: list_all_iff)

lemma wtL_tL[simp]: "Ik.wtL l ⟹ TE.wtL (tL l)"
apply(cases l) apply (rename_tac [!] atm) apply(case_tac [!] atm)
by (auto simp add: list_all_iff)

lemma wtC_tC[simp]: "Ik.wtC c ⟹ TE.wtC (tC c)"
unfolding tC_def Ik.wtC_def TE.wtC_def by (induct c, auto)

lemma tpOf_rOfFax[simp]: "TE.tpOf (rOfFax f) = resOf f"
unfolding rOfFax_def by simp

lemma tpOf_lOfFax[simp]: "TE.tpOf (lOfFax f) = resOf f"
unfolding lOfFax_def by simp

lemma tpOf_rOfWax[simp]: "TE.tpOf (rOfWax σ) = σ"
unfolding rOfWax_def by simp

lemma tpOf_lOfWax[simp]: "TE.tpOf (lOfWax σ) = σ"
unfolding lOfWax_def by simp

lemma wt_rOfFax[simp]: "wtFsym f ⟹ TE.wt (rOfFax f)"
unfolding rOfFax_def by simp

lemma wt_lOfFax[simp]: "wtFsym f ⟹ TE.wt (lOfFax f)"
unfolding lOfFax_def by simp

lemma wt_rOfWax[simp]: "¬ isRes σ ⟹ TE.wt (rOfWax σ)"
unfolding rOfWax_def by simp

lemma wt_lOfWax[simp]: "¬ isRes σ ⟹ TE.wt (lOfWax σ)"
unfolding lOfWax_def by simp

lemma wtPB_Fax[simp]: "TE.wtPB Fax" unfolding Fax_def TE.wtPB_def TE.wtC_def by auto

lemma wtPB_Wax[simp]: "TE.wtPB Wax" unfolding Wax_def TE.wtPB_def TE.wtC_def by auto

lemma wtPB_tC_Φ[simp]: "TE.wtPB (tC ` Φ)"
using Ik.wt_Φ unfolding Ik.wtPB_def TE.wtPB_def by auto

lemma wtPB_tPB[simp]: "TE.wtPB tPB" unfolding tPB_def by simp
(*  *)

lemma wt_Tag:
assumes "TE.wt (Fn (Tag σ) Tl)"
shows "∃ T. Tl = [T] ∧ TE.wt T ∧ tpOf T = σ"
using assms 
by simp (metis (opaque_lifting, no_types) list.inject list_all_simps(1) map_eq_Cons_conv neq_Nil_conv)

lemma tpOf_Tag: "TE.tpOf (Fn (Tag σ) Tl) = σ" by simp

lemma wt_Wit:
assumes "TE.wt (Fn (Wit σ) Tl)"
shows "Tl = []"
using assms by simp

lemma tpOf_Wit: "TE.tpOf (Fn (Wit σ) Tl) = σ" by simp

end (* context ProblemIkTpart *)


subsection‹Soundness›

context ModelIkTpart begin

(* The identity-tag extension of a given structure of the original signature *)
fun TE_intF where
 "TE_intF (Oldf f) al = intF f al"
|"TE_intF (Tag σ) al = hd al"
|"TE_intF (Wit σ) al = pickT σ"
(* note: for tags, we only care about al being the singleton list [a],
   and hence the interpretation returns a; for witnesses, we only care
   about al being [] *)

end (* context ModelIkTpart *)

sublocale ModelIkTpart < TE? : Struct
where wtFsym = TE_wtFsym and arOf = TE_arOf and resOf = TE_resOf and intF = TE_intF
proof
  fix ef al assume "TE_wtFsym ef" and "list_all2 intT (TE_arOf ef) al"
  thus "intT (TE_resOf ef) (TE_intF ef al)"
  using intF by (cases ef, auto)
qed auto

context ModelIkTpart begin

lemma tNN_int[simp]: "TE.int ξ (tNN T) = Ik.int ξ T"
proof(induct T)
  case (Fn f Tl)
  hence 0: "map (TE.int ξ ∘ tNN) Tl = map (Ik.int ξ) Tl"
  unfolding list_eq_iff list_all_iff by auto
  show ?case by (simp add: 0)
qed auto

lemma map_tNN_int[simp]: "map (TE.int ξ ∘ tNN) Tl = map (Ik.int ξ) Tl"
unfolding list_eq_iff list_all_iff by auto

lemma t_int[simp]: "TE.int ξ (tT T) = Ik.int ξ T"
by (cases T, auto)

lemma map_t_int[simp]: "map (TE.int ξ ∘ tT) Tl = map (Ik.int ξ) Tl"
unfolding list_eq_iff list_all_iff by auto

lemma tL_satL[simp]: "TE.satL ξ (tL l) ⟷ Ik.satL ξ l"
apply(cases l) apply (rename_tac [!] atm) apply(case_tac [!] atm) by auto

lemma tC_satC[simp]: "TE.satC ξ (tC c) ⟷ Ik.satC ξ c"
unfolding TE.satC_def Ik.satC_def tC_def by (induct c, auto)

lemma tC_Φ_satPB[simp]: "TE.satPB ξ (tC ` Φ) ⟷ Ik.satPB ξ Φ"
unfolding TE.satPB_def Ik.satPB_def by auto

lemma Fax_Wax_satPB:
"TE.satPB ξ (Fax) ∧ TE.satPB ξ (Wax)"
unfolding TE.satPB_def TE.satC_def Fax_def Wax_def
by (auto simp add: lOfFax_def rOfFax_def lOfWax_def rOfWax_def)

lemmas Fax_satPB[simp] = Fax_Wax_satPB[THEN conjunct1]
lemmas Wax_satPB[simp] = Fax_Wax_satPB[THEN conjunct2]

lemma soundness: "TE.SAT tPB"
unfolding TE.SAT_def tPB_def using SAT unfolding Ik.SAT_def by auto

theorem T_soundness:
"Model TE_wtFsym wtPsym TE_arOf TE_resOf parOf tPB intT TE_intF intP"
apply standard using wtPB_tPB soundness by auto

end (* context ModelIkTpart *)



(* Soundness theorem in sublocale form: Given a problem (with indicated
type partition) and a model for it, we obtain a model of the tag-extended (TE)
problem: *)
sublocale ModelIkTpart < TE? : Model
where wtFsym = TE_wtFsym and arOf = TE_arOf and resOf = TE_resOf
and Φ = tPB and intF = TE_intF
apply standard using wtPB_tPB soundness by auto


subsection‹Completeness›

(* iimg B f transforms f into a function f' having the same B-range as f
and such that it is the identity on its B-image, namely, ∀ b ∈ B. f' (f' a) = f' a;
also, it holds that ∀ b ∈ B. f' (f b) = f b *)
definition "iimg B f a ≡ if a ∈ f ` B then a else f a"

lemma inImage_iimg[simp]: "a ∈ f ` B ⟹ iimg B f a = a"
unfolding iimg_def by auto

lemma not_inImage_iimg[simp]: "a ∉ f ` B ⟹ iimg B f a = f a"
unfolding iimg_def by auto

lemma iimg[simp]: "a ∈ B ⟹ iimg B f (f a) = f a"
by (cases "a ∈ f ` B", auto)

(* Problem with type partition and model of its tag-encoding translation: *)

locale ProblemIkTpart_TEModel =
Ik? : ProblemIkTpart wtFsym wtPsym arOf resOf parOf Φ infTp prot protFw +
TE? : Model "ProblemIkTpart.TE_wtFsym wtFsym resOf" wtPsym
           "ProblemIkTpart.TE_arOf arOf" "ProblemIkTpart.TE_resOf resOf" parOf
           tPB eintT eintF eintP
for wtFsym :: "'fsym ⇒ bool"
and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and Φ and infTp and prot and protFw
and eintT and eintF and eintP

context ProblemIkTpart_TEModel begin

(* new tag semantics (taking as input elements, instead of singleton lists): *)
definition
"ntsem σ ≡
 if unprot σ ∨ protFw σ then id
                   else iimg {b. eintT σ b} (eintF (Tag σ) o singl)"

lemma unprot_ntsem[simp]: "unprot σ ∨ protFw σ ⟹ ntsem σ a = a"
unfolding ntsem_def by simp

lemma protFw_ntsem[simp]: "protFw σ ⟹ ntsem σ a = a"
unfolding ntsem_def by simp

lemma inImage_ntsem[simp]:
"a ∈ (eintF (Tag σ) o singl) ` {b. eintT σ b} ⟹ ntsem σ a = a"
unfolding ntsem_def by simp

lemma not_unprot_inImage_ntsem[simp]:
assumes "¬ unprot σ" and "¬ protFw σ" and "a ∉ (eintF (Tag σ) o singl) ` {b. eintT σ b}"
shows "ntsem σ a = eintF (Tag σ) [a]"
using assms unfolding ntsem_def by (simp add: singl_def)

(* crucial: *)
lemma ntsem[simp]:
"eintT σ b ⟹ ntsem σ (eintF (Tag σ) [b]) = eintF (Tag σ) [b]"
unfolding singl_def[symmetric] by simp

lemma eintT_ntsem:
assumes a: "eintT σ a"  shows "eintT σ (ntsem σ a)"
proof(cases "unprot σ ∨ protFw σ")
  case False note unprot = False show ?thesis
  proof(cases "a ∈ (eintF (Tag σ) o singl) ` {b. eintT σ b}")
    case False hence 1: "ntsem σ a = eintF (Tag σ) [a]" using unprot by simp
    show ?thesis unfolding 1 using a TE.intF
    by (metis TE_arOf.simps TE_resOf.simps TE_wtFsym.simps list_all2_Cons list_all2_Nil)
  qed(insert a, auto)
qed(insert a, simp)

(* The reduct structure of a given structure in the tag-extended signature: *)
definition
"intT σ a ≡
 if unprot σ then eintT σ a
 else if protFw σ then eintT σ a ∧ eintF (Tag σ) [a] = a
 else eintT σ a ∧ a ∈ (eintF (Tag σ) o singl) ` {b. eintT σ b}"
definition
"intF f al ≡
 if unprot (resOf f) ∨ protFw (resOf f)
   then eintF (Oldf f) (map2 ntsem (arOf f) al)
   else eintF (Tag (resOf f)) [eintF (Oldf f) (map2 ntsem (arOf f) al)]"
definition
"intP p al ≡ eintP p (map2 ntsem (parOf p) al)"

(* Semantic rephrasings of the fact that the (tagged problem) model satisfies
   Fax and Wax *)
lemma TE_Tag: (* fixme: messy proof *)
assumes f: "wtFsym f" and al: "list_all2 eintT (arOf f) al"
shows "eintF (Tag (resOf f)) [eintF (Oldf f) al] = eintF (Oldf f) al"
proof-
  define xl where "xl = getVars (arOf f)"
  have l[simp]: "length xl = length al" "length al = length (arOf f)"
  unfolding xl_def using al unfolding list_all2_iff by auto
  have 1[simp]: "⋀ i. i < length (arOf f) ⟹ tpOfV (xl!i) = (arOf f)!i"
  unfolding xl_def by auto
  have xl[simp]: "distinct xl" unfolding xl_def using distinct_getVars by auto
  define ξ where "ξ = pickE xl al"
  have ξ: "TE.wtE ξ" unfolding ξ_def apply(rule wtE_pickE)
  using al  list_all2_nthD by auto
  have [simp]: "⋀ i. i < length (arOf f) ⟹ ξ (xl ! i) = al ! i"
  using al unfolding ξ_def by (auto simp: list_all2_length intro: pickE)
  have 0: "map (TE.int ξ) (getTvars (arOf f)) = al"
  apply(rule nth_equalityI)
  using al by (auto simp: list_all2_length getTvars_def xl_def[symmetric])
  have "TE.satPB ξ Fax" using TE.sat_Φ[OF ξ] unfolding tPB_def by simp
  hence "TE.satC ξ [Pos (Eq (lOfFax f) (rOfFax f))]"
  unfolding TE.satPB_def Fax_def using f by auto
  hence "TE.satA ξ (Eq (lOfFax f) (rOfFax f))" unfolding TE.satC_def by simp
  thus ?thesis using al by (simp add: lOfFax_def rOfFax_def 0)
qed

lemma TE_Wit:
assumes σ: "¬ isRes σ" "protFw σ"
shows "eintF (Tag σ) [eintF (Wit σ) []] = eintF (Wit σ) []"
proof-
  define ξ where "ξ = pickE [] []"
  have ξ: "TE.wtE ξ" unfolding ξ_def apply(rule wtE_pickE) by auto
  have "TE.satPB ξ Wax" using TE.sat_Φ[OF ξ] unfolding tPB_def by simp
  hence "TE.satC ξ [Pos (Eq (lOfWax σ) (rOfWax σ))]"
  unfolding TE.satPB_def Wax_def using σ by auto
  hence "TE.satA ξ (Eq (lOfWax σ) (rOfWax σ))" unfolding TE.satC_def by auto
  thus ?thesis unfolding TE.satA.simps lOfWax_def rOfWax_def by simp
qed

lemma NE_intT_forget: "NE (intT σ)"
proof-
  obtain b where b: "eintT σ b" using TE.NE_intT by blast
  show ?thesis proof(cases "unprot σ")
    case True thus ?thesis using b unfolding intT_def by auto
  next
    case False note unprot = False show ?thesis
    proof(cases "protFw σ")
      case True note protFw = True show ?thesis proof(cases "isRes σ")
        case True then obtain f where f: "wtFsym f" and σ: "σ = resOf f"
        unfolding isRes_def by auto
        define al where "al = map pickT (arOf f)"
        have al: "list_all2 eintT (arOf f) al"
        unfolding al_def list_all2_map2 unfolding list_all2_length by auto
        define a where "a = eintF (Oldf f) al"
        have "eintT σ a" unfolding a_def σ using f al
        by (metis TE_arOf.simps TE_resOf.simps TE_wtFsym.simps TE.intF)
        moreover have "eintF (Tag σ) [a] = a" unfolding σ a_def using TE_Tag[OF f al] .
        ultimately show ?thesis using unprot protFw unfolding intT_def by auto
      next
        case False
        define a where "a = eintF (Wit σ) []"
        have "eintT σ a" unfolding a_def
        by (metis False TE_arOf.simps TE_resOf.simps TE_wtFsym.simps TE.intF list_all2_NilR)
        moreover have "eintF (Tag σ) [a] = a" unfolding a_def using TE_Wit[OF False protFw] .
        ultimately show ?thesis using unprot protFw unfolding intT_def by auto
      qed
    next
      case False  hence "eintT σ (eintF (Tag σ) [b])"
      using b list_all2_Cons list_all2_NilL
      by (metis TE.intF TE_arOf.simps TE_resOf.simps TE_wtFsym.simps)
      hence "intT σ (eintF (Tag σ) [b])"
      unfolding intT_def singl_def[abs_def] using b False by auto
      thus ?thesis by blast
    qed
  qed
qed

lemma wt_intF:
assumes f: "wtFsym f" and al: "list_all2 intT (arOf f) al"
shows "intT (resOf f) (intF f al)"
proof-
  let ?t = "eintF (Tag (resOf f))"
  let ?t'al = "map2 ntsem (arOf f) al"
  have al: "list_all2 eintT (arOf f) al"
  using al unfolding list_all2_length intT_def by metis
  have 0: "list_all2 eintT (arOf f) ?t'al"
  proof(rule listAll2_map2I)
    show l: "length (arOf f) = length al"
    using al unfolding list_all2_length by simp
    fix i assume "i < length (arOf f)"
    hence 1: "eintT (arOf f ! i) (al ! i)"
    using al unfolding list_all2_length by simp
    show "eintT (arOf f ! i) (ntsem (arOf f ! i) (al ! i))"
    using eintT_ntsem[OF 1] .
  qed
  hence 1: "eintT (resOf f) (eintF (Oldf f) ?t'al)"
  by (metis TE_arOf.simps TE_resOf.simps TE_wtFsym.simps f TE.intF)
  show ?thesis  proof(cases "unprot (resOf f)")
    case True thus ?thesis unfolding intF_def intT_def by (simp add: 1)
  next
    case False note unprot = False show ?thesis proof(cases "protFw (resOf f)")
      case True thus ?thesis using unprot TE_Tag[OF f 0] 1
      unfolding intF_def intT_def by simp
    next
      case False
      have "eintT (resOf f) (intF f al)" using intF_def 0 1 TE_Tag f by auto
      moreover have
      "intF f al ∈ (eintF (Tag (resOf f)) o singl) ` {b. eintT (resOf f) b}"
      unfolding intF_def using 1 unprot False by (auto simp add: singl_def)
      ultimately show ?thesis using False unfolding intT_def by simp
    qed
  qed
qed

lemma Struct: "Struct wtFsym wtPsym arOf resOf intT intF intP"
apply standard using NE_intT_forget wt_intF by auto

end (* context ProblemIkTpart_TEModel *)

sublocale ProblemIkTpart_TEModel < Ik? : Struct
where intT = intT and intF = intF and intP = intP
using Struct .


context ProblemIkTpart_TEModel begin

(* The inverse of the tag function (required for translating environments backwards)*)
definition
"invt σ a ≡ if unprot σ ∨ protFw σ then a else (SOME b. eintT σ b ∧ eintF (Tag σ) [b] = a)"

lemma unprot_invt[simp]: "unprot σ ∨ protFw σ ⟹ invt σ a = a"
unfolding invt_def by auto

lemma invt_invt_inImage:
assumes σ: "¬ unprot σ" "¬ protFw σ"
and a: "a ∈ (eintF (Tag σ) o singl) ` {b. eintT σ b}"
shows "eintT σ (invt σ a) ∧ eintF (Tag σ) [invt σ a] = a"
proof-
  obtain b where "eintT σ b" and "eintF (Tag σ) [b] = a"
  using a unfolding image_def singl_def[symmetric] by auto
  thus ?thesis using σ unfolding invt_def apply simp apply(rule someI_ex) by auto
qed

lemmas invt[simp] = invt_invt_inImage[THEN conjunct1]
lemmas invt_inImage[simp] = invt_invt_inImage[THEN conjunct2]


(* We translate the environments of the tag-extended-problem model
to environments of its original-signature reduct: *)  term invt
definition "eenv ξ x ≡ invt (tpOfV x) (ξ x)"

lemma wt_eenv:
assumes ξ: "Ik.wtE ξ"  shows "TE.wtE (eenv ξ)"
unfolding TE.wtE_def proof safe
  fix x let ?σ = "TE.tpOfV x"
  show "eintT ?σ (eenv ξ x)" proof(cases "unprot ?σ")
    case True note unprot = True
    thus ?thesis unfolding eenv_def by (metis ξ Ik.wtTE_intT intT_def unprot_invt)
  next
    case False note unprot = False show ?thesis proof(cases "protFw ?σ")
      case True thus ?thesis unfolding eenv_def using unprot ξ
      by (metis Ik.wtTE_intT intT_def unprot_invt)
    next
      case False thus ?thesis unfolding eenv_def using unprot ξ
      by (metis (no_types) ξ Ik.wtE_def intT_def invt)
    qed
  qed
qed

lemma int_tNN[simp]:
assumes T: "Ik.Ik.wt T" and ξ: "Ik.wtE ξ"
shows "TE.int (eenv ξ) (tNN T) = Ik.int ξ T"
using T proof(induct T)
  case (Var x) let ?σ = "TE.tpOfV x"  show ?case
  proof(cases "unprot ?σ")
    case False note unprot = False
    show ?thesis proof(cases "protFw ?σ")
      case True thus ?thesis using unprot ξ
      unfolding eenv_def Ik.wtE_def intT_def by simp
    next
      case False  hence "ξ x ∈ (eintF (Tag ?σ) ∘ singl) ` {b. eintT ?σ b}"
        using ξ unprot unfolding wtE_def intT_def singl_def[abs_def] by (simp cong del: image_cong_simp)
      thus ?thesis using unprot unfolding eenv_def using False by simp
    qed
  qed(unfold eenv_def, simp)
next
  case (Fn f Tl)
  let ?eξ = "eenv ξ" let ?ar = "arOf f" let ?r = "resOf f"
  have l: "length ?ar = length Tl" using Fn by simp
  have 0: "map2 ntsem ?ar (map (Ik.int ξ) Tl) =
           map (TE.int ?eξ ∘ tNN) Tl"  (is "?L = ?R")
  proof(rule nth_equalityI)
    fix i assume "i < length ?L"
    hence i: "i < length ?ar" using l by simp
    hence 1: "TE.int (eenv ξ) (tNN (Tl!i)) = Ik.int ξ (Tl!i)"
      using Fn by (auto simp: list_all_length)
    have 2: "?ar ! i = Ik.Ik.tpOf (Tl!i)" using Fn i by simp
    have 3: "intT (?ar ! i) (Ik.int ξ (Tl ! i))"
      unfolding 2 apply(rule wt_int)
      using Fn ξ i by (auto simp: list_all_length)
    show "?L!i = ?R!i" apply (cases "unprot (?ar ! i) ∨ protFw (?ar ! i)")
      using i 1 l 3 unfolding intT_def by auto
  qed(insert l, auto)
  show ?case apply(cases "unprot ?r ∨ protFw ?r")
    using [[unfold_abs_def = false]]
    unfolding Ik.int.simps TE.int.simps tT.simps unfolding intF_def using Fn 0 by auto
qed

lemma map_int_tNN[simp]:
assumes Tl: "list_all Ik.Ik.wt Tl" and ξ: "Ik.wtE ξ"
shows
"map2 ntsem (map Ik.Ik.tpOf Tl) (map (Ik.int ξ) Tl) =
 map (TE.int (eenv ξ) ∘ tNN) Tl"
proof-
  {fix i assume i: "i < length Tl"
   hence wt: "Ik.Ik.wt (Tl!i)" using Tl unfolding list_all_length by simp
   have "intT (Ik.Ik.tpOf (Tl!i)) (Ik.int ξ (Tl!i))" using Ik.wt_int[OF ξ wt] .
  }
  thus ?thesis
  using [[unfold_abs_def = false]]
  using assms unfolding intT_def list_all_length
  unfolding list_eq_iff apply clarsimp by (metis inImage_ntsem unprot_ntsem)
qed

lemma int_t[simp]:
assumes T: "Ik.Ik.wt T" and ξ: "Ik.wtE ξ"
shows "TE.int (eenv ξ) (tT T) = Ik.int ξ T"
using T proof(induct T)
  case (Var x) let ?σ = "tpOfV x"  show ?case
  proof(cases "unprot ?σ")
    case False note unprot = False
    show ?thesis proof(cases "protFw ?σ")
      case True thus ?thesis using unprot ξ
      unfolding eenv_def Ik.wtE_def intT_def by simp
    next
      case False  hence "ξ x ∈ (eintF (Tag ?σ) ∘ singl) ` {b. eintT ?σ b}"
      using ξ unprot unfolding wtE_def intT_def singl_def[abs_def] by (simp cong del: image_cong_simp)
      thus ?thesis using unprot unfolding eenv_def using False by simp
    qed
  qed(unfold eenv_def, simp)
next
  case (Fn f Tl)
  let ?eξ = "eenv ξ"  let ?ar = "arOf f"  let ?r = "resOf f"
  have l: "length ?ar = length Tl" using Fn by simp
  have ar: "?ar = map Ik.Ik.tpOf Tl" using Fn by simp
  have 0: "map2 ntsem ?ar (map (Ik.int ξ) Tl) = map (TE.int ?eξ ∘ tNN) Tl"
  unfolding ar apply(rule map_int_tNN[OF _ ξ]) using Fn by simp
  show ?case apply(cases "unprot ?r ∨ protFw ?r")
  using [[unfold_abs_def = false]]
  unfolding  Ik.int.simps TE.int.simps tT.simps unfolding intF_def using Fn 0 by auto
qed

lemma map_int_t[simp]:
assumes Tl: "list_all Ik.Ik.wt Tl" and ξ: "Ik.wtE ξ"
shows
"map2 ntsem (map Ik.Ik.tpOf Tl) (map (Ik.int ξ) Tl) =
 map (TE.int (eenv ξ) ∘ tT) Tl"
proof-
  {fix i assume i: "i < length Tl"
   hence wt: "Ik.Ik.wt (Tl!i)" using Tl unfolding list_all_length by simp
   have "intT (Ik.Ik.tpOf (Tl!i)) (Ik.int ξ (Tl!i))" using wt_int[OF ξ wt] .
  }
  thus ?thesis
  using [[unfold_abs_def = false]]
  using assms unfolding intT_def list_all_length
  unfolding list_eq_iff apply clarsimp by (metis inImage_ntsem unprot_ntsem)
qed

lemma satL_tL[simp]:
assumes l: "Ik.Ik.wtL l" and ξ: "Ik.wtE ξ"
shows "TE.satL (eenv ξ) (tL l) ⟷ Ik.satL ξ l"
using assms apply(cases l) apply (rename_tac [!] atm) by (case_tac [!] atm) (auto simp add: intP_def)

lemma satC_tC[simp]:
assumes l: "Ik.Ik.wtC c" and ξ: "Ik.wtE ξ"
shows "TE.satC (eenv ξ) (tC c) ⟷ Ik.satC ξ c"
unfolding TE.satC_def Ik.satC_def
using assms by (induct c, auto simp add: Ik.Ik.wtC_def tC_def)

lemma satPB_tPB[simp]:
assumes ξ: "Ik.wtE ξ"
shows "TE.satPB (eenv ξ) (tC ` Φ) ⟷ Ik.satPB ξ Φ"
using Ik.wt_Φ assms unfolding TE.satPB_def Ik.satPB_def by (auto simp add: Ik.Ik.wtPB_def)

lemma completeness: "Ik.SAT Φ"
unfolding Ik.SAT_def proof safe
  fix ξ assume ξ: "Ik.wtE ξ" hence "TE.wtE (eenv ξ)" by(rule wt_eenv)
  hence "TE.satPB (eenv ξ) tPB" by (rule TE.sat_Φ)
  hence "TE.satPB (eenv ξ) (tC ` Φ)" unfolding tPB_def by simp
  thus "Ik.satPB ξ Φ" using ξ by simp
qed

lemma T_completeness: "Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP"
by standard (rule completeness)

end (* context ProblemIkTpart_TEModel *)

(* Completeness theorem in sublocale form: Given a problem (with indicated
type partition) and a model for its tag-translated problem,
we obtain a model of the original problem: *)

sublocale ProblemIkTpart_TEModel < O? : Model
where intT = intT and intF = intF and intP = intP
using T_completeness .


subsection‹The result of the tag translation is an infiniteness-augmented problem›

(* Note that basic fact, merely stating that
the translation is well-defined between infiniteness-augmented problems,
is only proved at this late stage since it requires completeness.
This is an interesting dependency, not spotted in the paper. *)

sublocale ProblemIkTpart < TE? : Problem
where wtFsym = TE_wtFsym and arOf = TE_arOf and resOf = TE_resOf
and Φ = tPB
apply standard by auto

sublocale ProblemIkTpart < TE? : ProblemIk
where wtFsym = TE_wtFsym and arOf = TE_arOf and resOf = TE_resOf
and Φ = tPB
proof
  fix σ eintT eintF eintP a  assume σ: "infTp σ"
  assume M: "Model TE_wtFsym wtPsym TE_arOf TE_resOf parOf tPB eintT eintF eintP"
  let ?TE_intT = "ProblemIkTpart_TEModel.intT prot protFw eintT eintF"
  let ?TE_intF = "ProblemIkTpart_TEModel.intF arOf resOf prot protFw eintT eintF"
  let ?TE_intP = "ProblemIkTpart_TEModel.intP parOf prot protFw eintT eintF eintP"
  have 0: "ProblemIkTpart_TEModel wtFsym wtPsym arOf resOf parOf
                                   Φ infTp prot protFw eintT eintF eintP"
  using M unfolding ProblemIkTpart_TEModel_def apply safe apply standard done
  hence MM: "Ik.MModel ?TE_intT ?TE_intF ?TE_intP"
  by (rule ProblemIkTpart_TEModel.T_completeness)
  have "infinite {a. ?TE_intT σ a}" using infTp[OF σ MM] .
  moreover have "{a. ?TE_intT σ a} ⊆ {a. eintT σ a}"
  using ProblemIkTpart_TEModel.intT_def[OF 0] by auto
  ultimately show "infinite {a. eintT σ a}" using infinite_super by blast
qed


subsection‹The verification of the first monotonicity calculus criterion
for the tagged problem›

context ProblemIkTpart begin

lemma nvT_t[simp]: "¬ unprot σ ⟹ (∀ x ∈ TE.nvT (tT T). tpOfV x ≠ σ)"
apply(induct T) by auto

lemma nvL_tL[simp]: "¬ unprot σ ⟹ (∀ x ∈ TE.nvL (tL l). tpOfV x ≠ σ)"
apply(cases l) apply(rename_tac [!] atm) apply(case_tac [!] atm) by auto (metis nvT_t)+

lemma nvC_tC[simp]: "¬ unprot σ ⟹ (∀ x ∈ TE.nvC (tC c). tpOfV x ≠ σ)"
unfolding tC_def TE.nvC_def apply (induct c)
by auto (metis (full_types) nvL_tL)+

lemma unprot_nvT_t[simp]:
"unprot (tpOfV x) ⟹ x ∈ TE.nvT (tT T) ⟷ x ∈  TE.nvT T"
by (induct T, auto)

lemma tpL_nvT_tL[simp]:
"unprot (tpOfV x) ⟹ x ∈ TE.nvL (tL l) ⟷ x ∈ TE.nvL l"
by (cases l, rename_tac [!] atm, case_tac [!] atm, auto)

lemma unprot_nvC_tC[simp]:
"unprot (tpOfV x) ⟹ x ∈ TE.nvC (tC c) ⟷ x ∈ TE.nvC c"
unfolding tC_def TE.nvC_def apply (induct c) by auto

(* The added axioms are monotonic *)
lemma nv_OfFax[simp]:
"x ∉ TE.nvT (lOfFax f)"  "x ∉ TE.nvT (rOfFax f)"
unfolding lOfFax_def rOfFax_def lOfWax_def rOfWax_def by auto

lemma nv_OfWax[simp]:
"x ∉ TE.nvT (lOfWax σ')"  "x ∉ TE.nvT (rOfWax σ')"
unfolding lOfFax_def rOfFax_def lOfWax_def rOfWax_def by auto

lemma nvC_Fax: "c ∈ Fax ⟹ TE.nvC c = {}" unfolding Fax_def TE.nvC_def by auto
lemma mcalc_Fax: "c ∈ Fax ⟹ TE.mcalc σ c" using nvC_Fax unfolding TE.mcalc_iff by auto
lemma nvC_Wax: "c ∈ Wax ⟹ TE.nvC c = {}" unfolding Wax_def TE.nvC_def by auto
lemma mcalc_Wax: "c ∈ Wax ⟹ TE.mcalc σ c" using nvC_Wax[of c] by simp


end (* context ProblemIkTpart *)

sublocale ProblemIkTpart < TE?: ProblemIkMcalc
where wtFsym = TE_wtFsym and arOf = TE_arOf and resOf = TE_resOf
and Φ = tPB
proof
  fix σ c assume "c ∈ tPB"
  thus "TE.mcalc σ c" unfolding tPB_def proof safe
    fix d assume d: "d ∈ Φ" thus "TE.mcalc σ (tC d)"
    using unprot_mcalc[OF _ d] unfolding TE.mcalc_iff by (cases "unprot σ", auto, force)
  qed(insert mcalc_Fax mcalc_Wax, blast+)
qed

(* We already know that ProblemIkMcalc < MonotProblem, so by transitivity we obtain
the following main theorem, stating that the tag translation yields a monotonic
problem *)
context ProblemIkTpart begin

theorem T_monotonic:
"MonotProblem TE_wtFsym wtPsym TE_arOf TE_resOf parOf tPB" ..

end (* context ProblemIkTpart *)


sublocale ProblemIkTpart < TE?: MonotProblem
where wtFsym = TE_wtFsym and arOf = TE_arOf and resOf = TE_resOf and Φ = tPB
using T_monotonic .


end