Theory G

section‹Guard-Based Encodings›
theory G
imports T_G_Prelim Mcalc2C
begin


subsection‹The guard translation›

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

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

text‹The extension of the predicate symbols with type guards:›

datatype ('psym,'tp) epsym = Oldp 'psym | Guard 'tp

text‹Extension of the partitioned infinitely augmented problem
for dealing with guards:›

locale ProblemIkTpartG =
Ik? : ProblemIkTpart wtFsym wtPsym arOf resOf parOf Φ infTp prot protFw
for wtFsym :: "'fsym ⇒ bool"
and wtPsym :: "'psym ⇒ bool"
and arOf :: "'fsym ⇒ 'tp list"
and resOf and parOf and Φ and infTp and prot and protFw +
fixes (* Further refinement of prot: *)
    protCl :: "'tp ⇒ bool" (* types aimed to be classically protected *)
assumes
    protCl_prot[simp]: "⋀ σ. protCl σ ⟹ prot σ"
    (* In order to add classical (implicational) guards, one needs
      backwards closure on the ranks of function symbols*)
and protCl_fsym: "⋀ f. protCl (resPf f) ⟹ list_all protCl (arOf f)"

locale ModelIkTpartG =
Ik? : ProblemIkTpartG wtFsym wtPsym arOf resOf parOf Φ infTp prot protFw protCl +
Ik? : ModelIkTpart wtFsym wtPsym arOf resOf parOf Φ infTp prot protFw intT intF intP
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 protCl
and intT and intF and intP


context ProblemIkTpartG
begin

lemma protCl_resOf_arOf[simp]:
assumes "protCl (resOf f)" and "i < length (arOf f)"
shows "protCl (arOf f ! i)"
using assms protCl_fsym unfolding list_all_length by auto

text‹``GE'' stands for ``guard encoding'':›

fun GE_wtFsym where
 "GE_wtFsym (Oldf f) ⟷ wtFsym f"
|"GE_wtFsym (Wit σ) ⟷ ¬ isRes σ ∨ protCl σ"

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

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

fun GE_wtPsym where
 "GE_wtPsym (Oldp p) ⟷ wtPsym p"
|"GE_wtPsym (Guard σ) ⟷ ¬ unprot σ"

fun GE_parOf where
 "GE_parOf (Oldp p) = parOf p"
|"GE_parOf (Guard σ) = [σ]"


lemma countable_GE_wtFsym: "countable (Collect GE_wtFsym)" (is "countable ?K")
proof-
  let ?F = "λ ef. case ef of Oldf f ⇒ Inl f | Wit σ ⇒ Inr σ"
  let ?U = "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

lemma countable_GE_wtPsym: "countable (Collect GE_wtPsym)" (is "countable ?K")
proof-
  let ?F = "λ ep. case ep of Oldp p ⇒ Inl p | Guard σ ⇒ Inr σ"
  let ?U = "UNIV::'tp set"  let ?L = "(Collect wtPsym) <+> ?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 ep, auto)
  ultimately have "|?K| ≤o |?L|" unfolding card_of_ordLeq[symmetric] by auto
  moreover have "countable ?L" using countable_wtPsym countable_tp
  by (metis countable_Plus)
  ultimately show ?thesis by(rule countable_ordLeq)
qed

end (* context ProblemIkTpartG *)

sublocale ProblemIkTpartG < GE? : Signature
where wtFsym = GE_wtFsym and wtPsym = GE_wtPsym
and arOf = GE_arOf and resOf = GE_resOf and parOf = GE_parOf
apply standard
using countable_tp countable_GE_wtFsym countable_GE_wtPsym by auto


context ProblemIkTpartG
begin

text‹The guarding literal of a variable:›

definition grdLit :: "var ⇒ (('fsym, 'tp) efsym, ('psym, 'tp) epsym) lit"
where "grdLit x ≡ Neg (Pr (Guard (tpOfV x)) [Var x])"

text‹The (set of) guarding literals of a literal and of a clause:›

(* of a literal: *)
fun glitOfL ::
"('fsym, 'psym) lit ⇒ (('fsym, 'tp) efsym, ('psym, 'tp) epsym) lit set"
where
"glitOfL (Pos at) =
 {grdLit x | x. x ∈ varsA at ∧ (prot (tpOfV x) ∨ (protFw (tpOfV x) ∧ x ∈ nvA at))}"
|
"glitOfL (Neg at) = {grdLit x | x. x ∈ varsA at ∧ prot (tpOfV x)}"

(* of a clause: *)
definition "glitOfC c ≡ ⋃ (set (map glitOfL c))"

lemma finite_glitOfL[simp]: "finite (glitOfL l)"
proof-
  have "glitOfL l ⊆ grdLit ` {x . x ∈ varsL l}" by (cases l, auto)
  thus ?thesis by (metis Collect_mem_eq finite_surj finite_varsL)
qed

lemma finite_glitOfC[simp]: "finite (glitOfC c)"
unfolding glitOfC_def apply(rule finite_Union) using finite_glitOfL by auto

fun gT where
"gT (Var x) = Var x"
|
"gT (Fn f Tl) = Fn (Oldf f) (map gT Tl)"

fun gA where
"gA (Eq T1 T2) = Eq (gT T1) (gT T2)"
|
"gA (Pr p Tl) = Pr (Oldp p) (map gT Tl)"

fun gL where
"gL (Pos at) = Pos (gA at)"
|
"gL (Neg at) = Neg (gA at)"

definition "gC c ≡ (map gL c) @ (list (glitOfC c))"

lemma set_gC[simp]: "set (gC c) = gL ` (set c) ∪ glitOfC c"
unfolding gC_def by simp


text‹The extra axioms:›

text‹The function axioms:›

(* conclusion (atom): *)
definition "cOfFax f = Pr (Guard (resOf f)) [Fn (Oldf f) (getTvars (arOf f))]"
(* hypotheses (list of atoms): *)
definition "hOfFax f = map2 (Pr o Guard) (arOf f) (map singl (getTvars (arOf f)))"
(* The axiom (clause) for non-classically-decorated (lightweight and featherweigh) types: *)
definition "fax f ≡ [Pos (cOfFax f)]"
(* The axiom (clause) for classically-decorated types: *)
definition "faxCD f ≡ map Neg (hOfFax f) @ fax f"
(* The set of axioms: *)
definition
"Fax ≡ {fax f | f. wtFsym f ∧ ¬ unprot (resOf f) ∧ ¬ protCl (resOf f)} ∪
       {faxCD f | f. wtFsym f ∧ protCl (resOf f)}"

text‹The witness axioms:›

(* The axiom (clause): *)
definition "wax σ ≡ [Pos (Pr (Guard σ) [Fn (Wit σ) []])]"
(* The set of axioms: *)
definition "Wax ≡ {wax σ | σ. ¬ unprot σ ∧ (¬ isRes σ ∨ protCl σ)}"

definition "gPB = gC ` Φ ∪ Fax ∪ Wax"

text‹Well-typedness of the translation:›

lemma tpOf_g[simp]: "GE.tpOf (gT T) = Ik.tpOf T"
by (cases T) auto

lemma wt_g[simp]: "Ik.wt T ⟹ GE.wt (gT T)"
by (induct T, auto simp add: list_all_iff)

lemma wtA_gA[simp]: "Ik.wtA at ⟹ GE.wtA (gA at)"
by (cases at, auto simp add: list_all_iff)

lemma wtL_gL[simp]: "Ik.wtL l ⟹ GE.wtL (gL l)"
by (cases l, auto)

lemma wtC_map_gL[simp]: "Ik.wtC c ⟹ GE.wtC (map gL c)"
unfolding Ik.wtC_def GE.wtC_def by (induct c, auto)

lemma wtL_grdLit_unprot[simp]: "¬ unprot (tpOfV x) ⟹ GE.wtL (grdLit x)"
unfolding grdLit_def by auto

lemma wtL_grdLit[simp]: "prot (tpOfV x) ∨ protFw (tpOfV x) ⟹ GE.wtL (grdLit x)"
apply(rule wtL_grdLit_unprot) unfolding unprot_def by auto

lemma wtL_glitOfL[simp]: "l' ∈ glitOfL l ⟹ GE.wtL l'"
by (cases l, auto)

lemma wtL_glitOfC[simp]: "l' ∈ glitOfC c ⟹ GE.wtL l'"
unfolding glitOfC_def GE.wtC_def by (induct c, auto)

lemma wtC_list_glitOfC[simp]: "GE.wtC (list (glitOfC c))"
unfolding glitOfC_def GE.wtC_def by auto

lemma wtC_gC[simp]: "Ik.wtC c ⟹ GE.wtC (gC c)"
unfolding gC_def by simp

lemma wtA_cOfFax_unprot[simp]: "⟦wtFsym f; ¬ unprot (resOf f)⟧ ⟹ GE.wtA (cOfFax f)"
unfolding cOfFax_def by simp

lemma wtA_cOfFax[simp]:
"⟦wtFsym f; prot (resOf f) ∨ protFw (resOf f)⟧ ⟹ GE.wtA (cOfFax f)"
apply(rule wtA_cOfFax_unprot) unfolding unprot_def by auto

lemma wtA_hOfFax[simp]:
"⟦wtFsym f; protCl (resOf f)⟧ ⟹ list_all GE.wtA (hOfFax f)"
unfolding hOfFax_def unfolding list_all_length
by (auto simp add: singl_def unprot_def)

lemma wtC_fax_unprot[simp]: "⟦wtFsym f; ¬ unprot (resOf f)⟧ ⟹ GE.wtC (fax f)"
unfolding fax_def GE.wtC_def by auto

lemma wtC_fax[simp]: "⟦wtFsym f; prot (resOf f) ∨ protFw (resOf f)⟧ ⟹ GE.wtC (fax f)"
apply(rule wtC_fax_unprot) unfolding unprot_def by auto

lemma wtC_faxCD[simp]: "⟦wtFsym f; protCl (resOf f)⟧ ⟹ GE.wtC (faxCD f)"
unfolding faxCD_def GE.wtC_append apply(rule conjI)
  using wtA_hOfFax[unfolded list_all_length] apply(simp add: GE.wtC_def list_all_length)
  by simp

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

lemma wtC_wax_unprot[simp]: "⟦¬ unprot σ; ¬ isRes σ ∨ protCl σ⟧ ⟹ GE.wtC (wax σ)"
unfolding wax_def GE.wtC_def by simp

lemma wtC_wax[simp]: "⟦prot σ ∨ protFw σ; ¬ isRes σ ∨ protCl σ⟧ ⟹ GE.wtC (wax σ)"
apply(rule wtC_wax_unprot) unfolding unprot_def by auto

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

lemma wtPB_gC_Φ[simp]: "GE.wtPB (gC ` Φ)"
using Ik.wt_Φ unfolding Ik.wtPB_def GE.wtPB_def by auto

lemma wtPB_tPB[simp]: "GE.wtPB gPB" unfolding gPB_def by simp
(*  *)

lemma wtA_Guard:
assumes "GE.wtA (Pr (Guard σ) Tl)"
shows "∃ T. Tl = [T] ∧ GE.wt T ∧ tpOf T = σ"
using assms by simp (metis (opaque_lifting, no_types) list.inject map_eq_Cons_conv 
                           list_all_simps map_is_Nil_conv neq_Nil_conv)

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

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

end (* context ProblemIkTpartG *)


subsection‹Soundness›

context ModelIkTpartG begin

(* The identity-guard extension of a given structure of the original signature *)
fun GE_intF where
 "GE_intF (Oldf f) al = intF f al"
|"GE_intF (Wit σ) al = pickT σ"
(* note: for witnesses, we only care about al being [] *)

fun GE_intP where
 "GE_intP (Oldp p) al = intP p al"
|"GE_intP (Guard σ) al = True"
(* note: for guards, we only care about al being a singleton *)

end (* context ModelIkTpartG *)

sublocale ModelIkTpartG < GE? : Struct
where wtFsym = GE_wtFsym and wtPsym = GE_wtPsym and
arOf = GE_arOf and resOf = GE_resOf and parOf = GE_parOf
and intF = GE_intF and intP = GE_intP
proof
  fix ef al assume "GE_wtFsym ef" and "list_all2 intT (GE_arOf ef) al"
  thus "intT (GE_resOf ef) (GE_intF ef al)"
  using intF by (cases ef, auto)
qed auto

context ModelIkTpartG begin

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

lemma map_g_int[simp]: "map (GE.int ξ ∘ gT) Tl = map (Ik.int ξ) Tl"
unfolding list_eq_iff list_all_iff by auto

lemma gA_satA[simp]: "GE.satA ξ (gA at) ⟷ Ik.satA ξ at"
apply(cases at) by auto

lemma gL_satL[simp]: "GE.satL ξ (gL l) ⟷ Ik.satL ξ l"
apply(cases l) by auto

lemma map_gL_satC[simp]: "GE.satC ξ (map gL c) ⟷ Ik.satC ξ c"
unfolding GE.satC_def Ik.satC_def by (induct c, auto)

lemma gC_satC[simp]:
assumes "Ik.satC ξ c"  shows "GE.satC ξ (gC c)"
using assms unfolding gC_def by simp

lemma gC_Φ_satPB[simp]:
assumes "Ik.satPB ξ Φ"  shows "GE.satPB ξ (gC ` Φ)"
using assms unfolding GE.satPB_def Ik.satPB_def by auto

lemma Fax_Wax_satPB:
"GE.satPB ξ (Fax) ∧ GE.satPB ξ (Wax)"
unfolding GE.satPB_def GE.satC_def Fax_def Wax_def
by (auto simp add: cOfFax_def hOfFax_def fax_def faxCD_def wax_def)

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

lemma soundness: "GE.SAT gPB"
unfolding GE.SAT_def gPB_def using SAT unfolding Ik.SAT_def by auto

theorem G_soundness:
"Model GE_wtFsym GE_wtPsym GE_arOf GE_resOf GE_parOf gPB intT GE_intF GE_intP"
apply standard using wtPB_tPB soundness by auto

end (* context ModelIkTpartG *)

(* 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 (GE)
problem: *)
sublocale ModelIkTpartG < GE? : Model
where wtFsym = GE_wtFsym and wtPsym = GE_wtPsym and
arOf = GE_arOf and resOf = GE_resOf and parOf = GE_parOf
and Φ = gPB and intF = GE_intF and intP = GE_intP
using G_soundness .


subsection‹Completeness›

(* Problem with type partition and model of its guard-encoding translation: *)
locale ProblemIkTpartG_GEModel =
Ik? : ProblemIkTpartG wtFsym wtPsym arOf resOf parOf Φ infTp prot protFw protCl +
GE? : Model "ProblemIkTpartG.GE_wtFsym wtFsym resOf protCl"
            "ProblemIkTpartG.GE_wtPsym wtPsym prot protFw"
            "ProblemIkTpartG.GE_arOf arOf" "ProblemIkTpartG.GE_resOf resOf"
            "ProblemIkTpartG.GE_parOf parOf"
            gPB 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 protCl
and eintT and eintF and eintP

context ProblemIkTpartG_GEModel begin

text‹The reduct structure of a given structure in the guard-extended signature:›
definition
"intT σ a ≡
 if unprot σ then eintT σ a
 else eintT σ a ∧ eintP (Guard σ) [a]"
definition
"intF f al ≡ eintF (Oldf f) al"
definition
"intP p al ≡ eintP (Oldp p) al"

(* Semantic rephrasings of the fact that the (guarded problem) model satisfies
   Fax and Wax *)
lemma GE_Guard_all: (* fixme: messy proof *)
assumes f: "wtFsym f"
and al: "list_all2 eintT (arOf f) al"
shows
"(¬ unprot (resOf f) ∧ ¬ protCl (resOf f)
  ⟶ eintP (Guard (resOf f)) [eintF (Oldf f) al])
 ∧
 (protCl (resOf f) ⟶
  list_all2 (eintP ∘ Guard) (arOf f) (map singl al)
  ⟶ eintP (Guard (resOf f)) [eintF (Oldf f) al])"
(is "(?A1 ⟶ ?C) ∧
     (?A2 ⟶ ?H2 ⟶ ?C)")
proof(intro conjI impI)
  define xl where "xl = getVars (arOf f)"
  have l[simp]: "length xl = length al" "length al = length (arOf f)"
                "length (getTvars (arOf f)) = 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 ξ: "GE.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 (GE.int ξ) (getTvars (arOf f)) = al"
  apply(rule nth_equalityI)
  using al by (auto simp: list_all2_length getTvars_def xl_def[symmetric])
  have 1:
  "GE.satC ξ (map Neg (map2 (Pr ∘ Guard) (arOf f) (map singl (getTvars (arOf f))))) ⟷
   ¬ list_all2 (eintP ∘ Guard) (arOf f) (map singl al)"
  unfolding GE.satC_def list_ex_length list_all2_map2 singl_def
  unfolding list_all2_length
  by (auto simp add: map_zip_map2 singl_def getTvars_def xl_def[symmetric])
  have Fax: "GE.satPB ξ Fax" using GE.sat_Φ[OF ξ] unfolding gPB_def by simp
  {assume ?A1
   hence "GE.satC ξ (fax f)" using f Fax unfolding GE.satPB_def Fax_def by auto
   thus ?C unfolding fax_def cOfFax_def GE.satC_def by (simp add: 0)
  }
  {assume ?A2 and ?H2
   hence "GE.satC ξ (faxCD f)" using f Fax unfolding GE.satPB_def Fax_def by auto
   thus ?C using ‹?H2›
   unfolding faxCD_def fax_def cOfFax_def hOfFax_def
   unfolding GE.satC_append 1 unfolding GE.satC_def by (simp add: 0)
  }
qed

lemma GE_Guard_not_unprot_protCl:
assumes f: "wtFsym f" and f2: "¬ unprot (resOf f)" "¬ protCl (resOf f)"
and al: "list_all2 eintT (arOf f) al"
shows "eintP (Guard (resOf f)) [intF f al]"
using GE_Guard_all[OF f al] f2 unfolding intF_def by auto

lemma GE_Guard_protCl:
assumes f: "wtFsym f" and f2: "protCl (resOf f)" and al: "list_all2 eintT (arOf f) al"
and H: "list_all2 (eintP ∘ Guard) (arOf f) (map singl al)"
shows "eintP (Guard (resOf f)) [intF f al]"
using GE_Guard_all[OF f al] f2 H unfolding intF_def by auto

lemma GE_Guard_not_unprot:
assumes f: "wtFsym f" and f2: "¬ unprot (resOf f)" and al: "list_all2 eintT (arOf f) al"
and H: "list_all2 (eintP ∘ Guard) (arOf f) (map singl al)"
shows "eintP (Guard (resOf f)) [intF f al]"
apply(cases "protCl (resOf f)")
  using GE_Guard_protCl[OF f _ al H] apply fastforce
  using GE_Guard_not_unprot_protCl[OF f f2 _ al] by simp

lemma GE_Wit:
assumes σ: "¬ unprot σ" "¬ isRes σ ∨ protCl σ"
shows "eintP (Guard σ) [eintF (Wit σ) []]"
proof-
  define ξ where "ξ = pickE [] []"
  have ξ: "GE.wtE ξ" unfolding ξ_def apply(rule wtE_pickE) by auto
  have "GE.satPB ξ Wax" using GE.sat_Φ[OF ξ] unfolding gPB_def by simp
  hence "GE.satC ξ (wax σ)" unfolding Wax_def GE.satPB_def using σ by auto
  thus ?thesis unfolding satC_def wax_def by simp
qed

lemma NE_intT_forget: "NE (intT σ)"
proof-
  obtain a where a: "eintT σ a" using GE.NE_intT by blast
  show ?thesis
  proof(cases "unprot σ")
    case True
      thus ?thesis using a unfolding intT_def by auto
  next
    case False note unprot = False
      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 = intF f al"
      have a: "eintT σ a" unfolding a_def σ intF_def using f al
      by (metis GE_arOf.simps GE_resOf.simps GE_wtFsym.simps GE.intF)
      show ?thesis proof (cases "protCl σ")
        case True
        define a where "a = eintF (Wit σ) []"
        have "eintT σ a" unfolding a_def
        by (metis True GE_arOf.simps GE_resOf.simps GE_wtFsym.simps intF list_all2_Nil)
        moreover have "eintP (Guard σ) [a]"
        unfolding a_def using GE_Wit[OF unprot] True by simp
        ultimately show ?thesis using unprot unfolding intT_def by auto
      next
        case False
        hence "eintP (Guard σ) [a]"
        using unprot GE_Guard_not_unprot_protCl[OF f _ _ al] unfolding σ a_def by simp
        thus ?thesis using unprot a unfolding intT_def by auto
      qed
    next
      case False
      define a where "a = eintF (Wit σ) []"
      have "eintT σ a" unfolding a_def
      by (metis False GE_arOf.simps GE_resOf.simps GE_wtFsym.simps intF list_all2_Nil)
      moreover have "eintP (Guard σ) [a]"
      unfolding a_def using GE_Wit[OF unprot] False by simp
      ultimately show ?thesis using unprot unfolding intT_def by auto
    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-
  have 0: "list_all2 eintT (arOf f) al"
  using al unfolding intT_def[abs_def] list_all2_length by metis
  hence "eintT (resOf f) (eintF (Oldf f) al)"
  by (metis GE_arOf.simps GE_resOf.simps GE_wtFsym.simps f al GE.intF)
  hence 1: "eintT (resOf f) (intF f al)" unfolding intF_def by simp
  show ?thesis  proof(cases "unprot (resOf f)")
    case True thus ?thesis unfolding intT_def by (simp add: 1)
  next
    case False note unprot = False
    have "eintP (Guard (resOf f)) [intF f al]"
    proof(cases "protCl (resOf f)")
      case False show ?thesis using GE_Guard_not_unprot_protCl[OF f unprot False 0] .
    next
      case True
      hence "list_all protCl (arOf f)" using protCl_fsym by simp
      hence "list_all (λ σ. ¬ unprot σ) (arOf f)"
      unfolding list_all_length unprot_def by auto
      hence 2: "list_all2 (eintP ∘ Guard) (arOf f) (map singl al)"
      using al unfolding intT_def[abs_def] list_all2_length list_all_length
      singl_def[abs_def] by auto
      show ?thesis using GE_Guard_protCl[OF f True 0 2] .
    qed
    thus ?thesis using unprot unfolding intT_def by (simp add: 1)
  qed
qed

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

end (* context ProblemIkTpartG_GEModel *)

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


context ProblemIkTpartG_GEModel begin

lemma wtE[simp]: "Ik.wtE ξ ⟹ GE.wtE ξ"
unfolding Ik.wtE_def GE.wtE_def intT_def by metis

lemma int_g[simp]: "GE.int ξ (gT T) = Ik.int ξ T"
proof (induct T)
  case (Fn f Tl)
  let ?ar = "arOf f" let ?r = "resOf f"
  have 0: "map (Ik.int ξ) Tl = map (GE.int ξ ∘ gT) Tl"
  apply(rule nth_equalityI) using Fn unfolding list_all_length by auto
  show ?case
  using [[unfold_abs_def = false]]
  unfolding Ik.int.simps GE.int.simps gT.simps unfolding intF_def
  using Fn by (simp add: 0)
qed auto

lemma map_int_g[simp]:
"map (Ik.int ξ) Tl = map (GE.int ξ ∘ gT) Tl"
apply(rule nth_equalityI) unfolding list_all_length by auto

lemma satA_gA[simp]: "GE.satA ξ (gA at) ⟷ Ik.satA ξ at"
by (cases at) (auto simp add: intP_def)

lemma satL_gL[simp]: "GE.satL ξ (gL l) ⟷ Ik.satL ξ l"
by (cases l) auto

lemma satC_map_gL[simp]: "GE.satC ξ (map gL c) ⟷ Ik.satC ξ c"
unfolding GE.satC_def Ik.satC_def by (induct c) auto

lemma wtE_not_grdLit_unprot[simp]: (* crucial: *)
assumes "Ik.wtE ξ" and "¬ unprot (tpOfV x)"
shows "¬ GE.satL ξ (grdLit x)"
using assms unfolding Ik.wtE_def intT_def grdLit_def by simp

lemma wtE_not_grdLit[simp]:
assumes "Ik.wtE ξ" and "prot (tpOfV x) ∨ protFw (tpOfV x)"
shows "¬ GE.satL ξ (grdLit x)"
apply(rule wtE_not_grdLit_unprot) using assms unfolding unprot_def by auto

lemma wtE_not_glitOfL[simp]:
assumes "Ik.wtE ξ"
shows "¬ GE.satC ξ (list (glitOfL l))"
using assms unfolding GE.satC_def list_ex_list[OF finite_glitOfL]
by (cases l, auto)

lemma wtE_not_glitOfC[simp]:
assumes "Ik.wtE ξ"
shows "¬ GE.satC ξ (list (glitOfC c))"
using wtE_not_glitOfL[OF assms]
unfolding GE.satC_def list_ex_list[OF finite_glitOfC] list_ex_list[OF finite_glitOfL]
unfolding glitOfC_def by auto

lemma satC_gC[simp]:
assumes "Ik.wtE ξ" and "GE.satC ξ (gC c)"
shows "Ik.satC ξ c"
using assms unfolding gC_def by simp

lemma satPB_gPB[simp]:
assumes "Ik.wtE ξ" and "GE.satPB ξ (gC ` Φ)"
shows "Ik.satPB ξ Φ"
using Ik.wt_Φ assms unfolding GE.satPB_def Ik.satPB_def by (auto simp add: Ik.wtPB_def)

lemma completeness: "Ik.SAT Φ"
unfolding Ik.SAT_def proof safe
  fix ξ assume ξ: "Ik.wtE ξ" hence "GE.wtE ξ" by simp
  hence "GE.satPB ξ gPB" by (rule GE.sat_Φ)
  hence "GE.satPB ξ (gC ` Φ)" unfolding gPB_def by simp
  thus "Ik.satPB ξ Φ" using ξ by simp
qed

lemma G_completeness: "Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP"
apply standard using completeness .

end (* context ProblemIkTpartG_GEModel *)

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

sublocale ProblemIkTpartG_GEModel < Ik? : Model
where intT = intT and intF = intF and intP = intP
using G_completeness .


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

(* An observation similar to the corresponding one for tags applies here.  *)

sublocale ProblemIkTpartG < GE? : Problem
where wtFsym = GE_wtFsym and wtPsym = GE_wtPsym
and arOf = GE_arOf and resOf = GE_resOf and parOf = GE_parOf
and Φ = gPB
apply standard
apply auto
done

sublocale ProblemIkTpartG < GE? : ProblemIk
where wtFsym = GE_wtFsym and wtPsym = GE_wtPsym
and arOf = GE_arOf and resOf = GE_resOf and parOf = GE_parOf
and Φ = gPB
proof
  fix σ eintT eintF eintP a  assume σ: "infTp σ"
  assume M: "Model GE_wtFsym GE_wtPsym GE_arOf GE_resOf GE_parOf gPB eintT eintF eintP"
  let ?GE_intT = "ProblemIkTpartG_GEModel.intT prot protFw eintT eintP"
  let ?GE_intF = "ProblemIkTpartG_GEModel.intF eintF"
  let ?GE_intP = "ProblemIkTpartG_GEModel.intP eintP"
  have 0: "ProblemIkTpartG_GEModel wtFsym wtPsym arOf resOf parOf
                                   Φ infTp prot protFw protCl eintT eintF eintP"
  using M unfolding ProblemIkTpartG_GEModel_def apply safe ..
  hence MM: "Ik.MModel ?GE_intT ?GE_intF ?GE_intP"
  by (rule ProblemIkTpartG_GEModel.G_completeness)
  have "infinite {a. ?GE_intT σ a}" using infTp[OF σ MM] .
  moreover have "{a. ?GE_intT σ a} ⊆ {a. eintT σ a}"
  using ProblemIkTpartG_GEModel.intT_def[OF 0] by auto
  ultimately show "infinite {a. eintT σ a}" using infinite_super by blast
qed


subsection‹The verification of the second monotonicity calculus criterion
for the guarded problem›

context ProblemIkTpartG begin

fun pol where
"pol _ (Oldp p) = Cext"
|
"pol _ (Guard σ) = Fext"

lemma pol_ct: "pol σ1 p = pol σ2 p"
by(cases p, auto)

definition "grdOf c l x = grdLit x"
end

sublocale ProblemIkTpartG < GE?: ProblemIkPol
where wtFsym = GE_wtFsym and wtPsym = GE_wtPsym
and arOf = GE_arOf and resOf = GE_resOf and parOf = GE_parOf
and Φ = gPB and pol = pol and grdOf = grdOf ..

context ProblemIkTpartG begin

lemma nv2_nv[simp]: "GE.nv2T (gT T) = GE.nvT T"
apply (induct T) by auto

lemma nv2L_nvL[simp]: "GE.nv2L (gL l) = GE.nvL l"
proof(cases l)
  case (Pos at) thus ?thesis by (cases at, simp_all)
next
  case (Neg at) thus ?thesis by (cases at, auto)
qed

lemma nv2L:
assumes "l ∈ set c" and mc: "GE.mcalc σ c"
shows "infTp σ ∨ (∀ x ∈ GE.nv2L (gL l). tpOfV x ≠ σ)"
using assms mc nv2L_nvL unfolding GE.mcalc_iff GE.nvC_def apply simp
using nv2L_nvL[of l]
by (metis empty_subsetI equalityI nv2L_nvL)

(* The guarding literals are guarded: *)
lemma isGuard_grdLit[simp]: "GE.isGuard x (grdLit x)"
unfolding grdLit_def by auto

lemma nv2L_grdLit[simp]: "GE.nv2L (grdLit x) = {}"
unfolding grdLit_def by auto

lemma mcalc_mcalc2: "GE.mcalc σ c ⟹ GE.mcalc2 σ (gC c)"
using nv2L unfolding GE.mcalc2_iff gC_def glitOfC_def grdOf_def by auto

lemma nv2L_wax[simp]: "l' ∈ set (wax σ) ⟹ GE.nv2L l' = {}"
unfolding wax_def by auto

lemma nv2L_Wax:
assumes "c' ∈ Wax" and "l' ∈ set c'"
shows "GE.nv2L l' = {}"
using assms unfolding Wax_def by auto

lemma nv2L_cOfFax[simp]: "GE.nv2L (Pos (cOfFax σ)) = {}"
unfolding cOfFax_def by auto

lemma nv2L_hOfFax[simp]:
assumes "at ∈ set (hOfFax σ)"
shows "GE.nv2L (Neg at) = {}"
using assms unfolding hOfFax_def by auto

lemma nv2L_fax[simp]: "l ∈ set (fax σ) ⟹ GE.nv2L l = {}"
unfolding fax_def by auto

lemma nv2L_faxCD[simp]: "l ∈ set (faxCD σ) ⟹ GE.nv2L l = {}"
unfolding faxCD_def by auto

lemma nv2L_Fax:
assumes "c' ∈ Fax" and "l' ∈ set c'"
shows "GE.nv2L l' = {}"
using assms unfolding Fax_def by auto

lemma grdOf:
assumes c': "c' ∈ gPB" and l': "l' ∈ set c'"
and x: "x ∈ GE.nv2L l'" and i: "¬ infTp (tpOfV x)"
shows "grdOf c' l' x ∈ set c' ∧ GE.isGuard x (grdOf c' l' x)"
proof(cases "c' ∈ Fax ∪ Wax")
  case True thus ?thesis using x l' nv2L_Wax nv2L_Fax by force
next
  case False then obtain c where c': "c' = gC c" and c: "c ∈ Φ"
  using c' unfolding gPB_def by auto
  show ?thesis
  proof(cases "l' ∈ glitOfC c")
    case True then obtain l where l: "l ∈ set c" and l': "l' ∈ glitOfL l"
    unfolding glitOfC_def by auto
    then obtain x1 where "l' = grdLit x1" using l' by (cases l rule: lit.exhaust) auto
    hence "GE.nv2L l' = {}" by simp
    thus ?thesis using x by simp
  next
    let ?σ = "tpOfV x"
    case False then obtain l where l: "l ∈ set c" and l': "l' = gL l"
    using l' unfolding c' gC_def by auto
    hence x: "x ∈ GE.nvL l" using x by simp
    hence "x ∈ GE.nvC c" using l unfolding GE.nvC_def by auto
    hence "¬ GE.mcalc ?σ c" using i unfolding GE.mcalc_iff by auto
    hence tp: "prot ?σ ∨ protFw ?σ" using unprot_mcalc[OF _ c] unfolding unprot_def by auto
    moreover obtain at where l_at: "l = Pos at" using x by(cases l, auto)
    moreover have "x ∈ varsA at" using x unfolding l_at by auto
    ultimately have "grdLit x ∈ glitOfL l" using x unfolding l_at by force
    thus ?thesis using l x unfolding grdOf_def c' gC_def glitOfC_def by auto
  qed
qed

lemma mcalc2:
assumes c': "c' ∈ gPB"
shows "GE.mcalc2 σ c'"
proof(cases "c' ∈ Fax ∪ Wax")
  case True thus ?thesis using nv2L_Wax nv2L_Fax
  unfolding GE.mcalc2_iff by fastforce
next
  case False hence c': "c' ∈ gPB" using c' unfolding gPB_def by auto
  show ?thesis unfolding GE.mcalc2_iff using grdOf[OF c'] by auto
qed


end (* context ProblemIkTpartG *)


sublocale ProblemIkTpartG < GE?: ProblemIkPolMcalc2C
where wtFsym = GE_wtFsym and wtPsym = GE_wtPsym
and arOf = GE_arOf and resOf = GE_resOf and parOf = GE_parOf
and Φ = gPB and pol = pol and grdOf = grdOf
apply standard using grdOf mcalc2
apply (auto simp: pol_ct)
done

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

context ProblemIkTpartG begin

theorem G_monotonic:
"MonotProblem GE_wtFsym GE_wtPsym GE_arOf GE_resOf GE_parOf gPB" ..

end (* context ProblemIkTpartG *)


(* Also in sublocale form: *)

sublocale ProblemIkTpartG < GE?: MonotProblem
where wtFsym = GE_wtFsym and wtPsym = GE_wtPsym
and arOf = GE_arOf and resOf = GE_resOf and parOf = GE_parOf
and Φ = gPB
using G_monotonic .



end