Session Sort_Encodings

Theory Preliminaries

section‹Preliminaries›
theory Preliminaries
imports "HOL-Cardinals.Cardinals"
        "HOL-Library.Countable_Set_Type"
begin


subsection ‹Miscelanea›

text‹A fixed countable universe for interpreting countable models:›

datatype univ = UU nat

lemma infinite_univ[simp]: "infinite (UNIV :: univ set)"
unfolding infinite_iff_card_of_nat card_of_ordLeq[symmetric]
unfolding inj_on_def by auto

lemma countable_univ[simp]: "countable (UNIV :: univ set)"
unfolding countable_card_of_nat apply(rule surj_imp_ordLeq[of _ UU])
by (metis subset_UNIV surj_def univ.exhaust)


text‹Picking an element from a nonempty set (Hilbert choice for sets):›

definition "pick X  SOME x. x  X"

lemma pick[simp]: "x  X  pick X  X"
unfolding pick_def by (metis someI_ex)

lemma pick_NE[simp]: "X  {}  pick X  X" by auto

definition sappend (infix "@@" 60) where
"Al @@ Bl = {al @ bl | al bl. al  Al  bl  Bl}"

lemma sappend_NE[simp]: "A @@ B  {}  A  {}  B  {}"
unfolding sappend_def by auto

abbreviation fst3 :: "'a * 'b * 'c  'a" where "fst3 abc  fst abc"
abbreviation "snd3 abc  fst (snd abc)"
abbreviation "trd3 abc  snd (snd abc)"

hide_const int

abbreviation "any  undefined"

text‹Non-emptyness of predicates:›

abbreviation (input) "NE φ   a. φ a"

lemma NE_NE: "NE NE"
apply(rule exI[of _ "λ a. True"]) by auto

lemma length_Suc_0:
"length al = Suc 0  ( a. al = [a])"
by (metis (lifting) length_0_conv length_Suc_conv)


subsection‹List combinators›

lemmas list_all2_length = list_all2_conv_all_nth
lemmas list_eq_iff = list_eq_iff_nth_eq
lemmas list_all_iff
lemmas list_all_length

definition "singl a = [a]"

lemma length_singl[simp]: "length (singl a) = Suc 0"
unfolding singl_def by simp

lemma hd_singl[simp]: "hd (singl a) = a"
unfolding singl_def by simp

lemma hd_o_singl[simp]: "hd o singl = id"
unfolding comp_def fun_eq_iff by simp

lemma singl_hd[simp]: "length al = Suc 0  singl (hd al) = al"
unfolding singl_def by (cases al, auto)

lemma singl_inj[simp]: "singl a = singl b  a = b"
unfolding singl_def by simp

(* The list of a finite set: *)
definition "list A  SOME al. distinct al  set al = A"

lemma distinct_set_list:
"finite A  distinct (list A)  set (list A) = A"
unfolding list_def apply(rule someI_ex) using finite_distinct_list by auto

lemmas distinct_list[simp] = distinct_set_list[THEN conjunct1]
lemmas set_list[simp] = distinct_set_list[THEN conjunct2]

lemma set_list_set[simp]: "set (list (set xl)) = set xl" by auto

lemma length_list[simp]: "finite A  length (list A) = card A"
by (metis distinct_card distinct_set_list)

lemma list_all_mp[elim]:
assumes "list_all (λ a. φ a  ψ a) al" and "list_all φ al"
shows "list_all ψ al"
using assms unfolding list_all_iff by auto

lemma list_all_map:
"list_all φ (map f al) = list_all (φ o f) al"
by (metis (no_types) length_map list_all_length nth_map o_def)

lemma list_Emp[simp]: "list {} = []"
by (metis set_empty2 set_list_set)

lemma distinct_set_eq_Singl[simp]: "distinct al  set al = {a}  al = [a]"
apply(cases al, simp)
by (metis (lifting) List.set_simps distinct.simps
           distinct_singleton empty_not_insert insert_eq_iff set_empty2)

lemma list_Singl[simp]: "list {b} = [b]"
unfolding list_def apply(rule some_equality) by auto

lemma list_insert:
assumes A: "finite A" and b: "b  A"
shows
" al1 al2.
   A = set (al1 @ al2)  distinct (al1 @ [b] @ al2) 
   list (insert b A) = al1 @ [b] @ al2"
proof-
  have "b  set (list (insert b A))" using A by auto
  then obtain al1 al2 where 0: "list (insert b A) = al1 @ [b] @ al2"
  by (metis append_Cons eq_Nil_appendI split_list_last)
  hence 1: "distinct (al1 @ [b] @ al2)" using A
  by (metis distinct_set_list finite_insert)
  hence "b  set (al1 @ al2)" by simp
  moreover have "insert b A = insert b (set (al1 @ al2))"
  using 0 set_list[OF finite.insertI[OF A, of b]] by auto
  ultimately have "A = set (al1 @ al2)" using b by auto
  thus ?thesis using 0 1 by auto
qed

lemma list_all_list[simp]:
assumes "finite A" shows "list_all φ (list A)  ( a  A. φ a)"
using assms unfolding list_all_iff by simp

lemma list_ex_list[simp]:
"finite A  list_ex φ (list A) = (aA. φ a)"
unfolding list_ex_iff by simp

text‹list update:›

fun lupd where
"lupd Nil Nil F = F"
|
"lupd (a # al) (b # bl) F = lupd al bl (F(a := b))"
|
"lupd _ _ F = any"

lemma set_lupd:
assumes "a  set al  F1 a = F2 a"
shows "lupd al bl F1 a = lupd al bl F2 a"
using assms apply(induct arbitrary: F1 F2 rule: list_induct2') by auto

lemma lupd_map:
assumes "length al = length bl" and "a1  set al  G a1 = F (H a1)"
shows "lupd al (map F bl) G a1 = F (lupd al bl H a1)"
using assms apply (induct arbitrary: F G H rule: list_induct2) by auto

lemma nth_map2[simp]:
assumes "length bl = length al" and "i < length al"
shows "(map2 f al bl) ! i = f (al!i) (bl!i)"
using assms by auto

lemma list_all2_Nil_iff:
assumes "list_all2 R xs ys"
shows "xs = []  ys = []"
using assms by (cases xs, cases ys) auto

lemma list_all2_NilL[simp]:
"list_all2 R [] ys  ys = []"
using list_all2_Nil_iff by auto

lemma list_all2_NilR[simp]:
"list_all2 R xs []  xs = []"
using list_all2_Nil_iff by auto

lemma list_all2_ConsL:
assumes "list_all2 R (x # xs') ys"
shows " y ys'. ys = y # ys'  R x y  list_all2 R xs' ys'"
using assms by(cases ys) auto

lemma list_all2_elimL[elim, consumes 2, case_names Cons]:
assumes xs: "xs = x # xs'" and h: "list_all2 R xs ys"
and Cons: " y ys'. ys = y # ys'; R x y; list_all2 R xs' ys'  phi"
shows phi
using list_all2_ConsL assms by metis

lemma list_all2_elimL2[elim, consumes 1, case_names Cons]:
assumes h: "list_all2 R (x # xs') ys"
and Cons: " y ys'. ys = y # ys'; R x y; list_all2 R xs' ys'  phi"
shows phi
using list_all2_ConsL assms by metis

lemma list_all2_ConsR:
assumes "list_all2 R xs (y # ys')"
shows " x xs'. xs = x # xs'  R x y  list_all2 R xs' ys'"
using assms by(cases xs) auto

lemma list_all2_elimR[elim, consumes 2, case_names Cons]:
assumes ys: "ys = y # ys'" and h: "list_all2 R xs ys"
and Cons: " x xs'. xs = x # xs'; R x y; list_all2 R xs' ys'  phi"
shows phi
using list_all2_ConsR assms by metis

lemma list_all2_elimR2[elim, consumes 1, case_names Cons]:
assumes h: "list_all2 R xs (y # ys')"
and Cons: " x xs'. xs = x # xs'; R x y; list_all2 R xs' ys'  phi"
shows phi
using list_all2_ConsR assms by metis

lemma ex_list_all2:
assumes "x. x  set xs  y. f x y"
shows " ys. list_all2 f xs ys"
using assms apply(induct xs)
apply fastforce
by (metis set_simps insertCI list_all2_Cons)

lemma list_all2_cong[fundef_cong]:
assumes "xs1 = ys1" and "xs2 = ys2"
and " i . i < length xs2  R (xs1!i) (xs2!i)  R' (ys1!i) (ys2!i)"
shows "list_all2 R xs1 xs2  list_all2 R' ys1 ys2"
by (metis assms list_all2_length)

lemma list_all2_o: "list_all2 (P o f) al bl = list_all2 P (map f al) bl"
unfolding list_all2_map1 comp_def ..

lemma set_size_list:
assumes "x  set xs"
shows "f x  size_list f xs"
by (metis assms size_list_estimation' order_eq_refl)

lemma nth_size_list:
assumes "i < length xs"
shows "f (xs!i)  size_list f xs"
by (metis assms nth_mem set_size_list)

lemma list_all2_list_all[simp]:
"list_all2 (λ x. f) xs ys 
 length xs = length ys  list_all f ys"
by (metis list_all2_length list_all_length)

lemma list_all2_list_allR[simp]:
"list_all2 (λ x y. f x) xs ys 
 length xs = length ys  list_all f xs"
by (metis (lifting) list_all2_length list_all_length)

lemma list_all2_list_all_2[simp]:
"list_all2 f xs xs  list_all (λ x. f x x) xs"
by (auto simp add: list_all2_iff list_all_iff zip_same)

lemma list_all2_map_map:
"list_all2 φ (map f Tl) (map g Tl) =
 list_all (λT. φ (f T) (g T)) Tl"
unfolding list_all2_map1 list_all2_map2 list_all2_list_all_2 ..

lemma length_map2[simp]:
assumes "length ys = length xs"
shows "length (map2 f xs ys) = length xs"
using assms by auto

lemma listAll2_map2I[intro?]:
assumes "length xs = length ys"
and " i. i < length xs  R (xs!i) (f (xs!i) (ys!i))"
shows "list_all2 R xs (map2 f xs ys)"
apply(rule list_all2I) using assms unfolding set_zip by auto

(*
lemma listAll2_map2I[intro?]:
assumes "length xs = length ys" and "⋀ x y. R x (f x y)"
shows "list_all2 R xs (map2 f xs ys)"
apply(rule list_all2I) using assms unfolding set_zip map2_def by auto
*)

lemma set_incl_pred:
"A  B  ( a. A a  B a)"
by (metis predicate1D predicate1I)

lemma set_incl_pred2:
"A  B  ( a1 a2. A a1 a2  B a1 a2)"
by (metis predicate2I rev_predicate2D)

lemma set_incl_pred3:
"A  B  ( a1 a2 a3. A a1 a2 a3  B a1 a2 a3)" (is "_  ?R")
proof-
  have "A  B  ( a1. A a1  B a1)" by (metis le_funD le_funI)
  also have "...  ?R" apply(rule iff_allI)
  unfolding set_incl_pred2 ..
  finally show ?thesis .
qed

lemma set_incl_pred4:
"A  B  ( a1 a2 a3 a4. A a1 a2 a3 a4  B a1 a2 a3 a4)" (is "_  ?R")
proof-
  have "A  B  ( a1. A a1  B a1)" by (metis le_funD le_funI)
  also have "...  ?R" apply(rule iff_allI)
  unfolding set_incl_pred3 ..
  finally show ?thesis .
qed

lemma list_all_mono:
assumes "phi  chi"
shows "list_all phi  list_all chi"
using assms unfolding set_incl_pred list_all_iff by auto

lemma list_all2_mono:
assumes "phi  chi"
shows "list_all2 phi  list_all2 chi"
using assms by (metis (full_types) list_all2_mono set_incl_pred2)


subsection‹Variables›

text‹The type of variables:›

datatype var = Variable nat

lemma card_of_var: "|UNIV::var set| =o natLeq"
proof-
  have "|UNIV::var set| =o |UNIV::nat set|"
  apply(rule ordIso_symmetric,rule card_of_ordIsoI)
  unfolding bij_betw_def inj_on_def surj_def using var.exhaust by auto
  also have "|UNIV::nat set| =o natLeq" by(rule card_of_nat)
  finally show ?thesis .
qed

lemma infinite_var[simp]: "infinite (UNIV :: var set)"
using card_of_var by (rule ordIso_natLeq_infinite1)

lemma countable_var: "countable (UNIV :: var set)"
proof-
  have 0: "(UNIV :: var set)  {}" by simp
  show ?thesis unfolding countable_card_of_nat unfolding card_of_ordLeq2[symmetric, OF 0]
  apply(rule exI[of _ Variable]) unfolding image_def apply auto by (case_tac x, auto)
qed


(* FIXME: Move into Countable_Set *)
lemma countable_infinite:
assumes A: "countable A" and B: "infinite B"
shows "|A| ≤o |B|"
proof-
  have "|A| ≤o natLeq" using A unfolding countable_card_le_natLeq .
  also have "natLeq ≤o |B|" by (metis B infinite_iff_natLeq_ordLeq)
  finally show ?thesis .
qed

(* Partitioning V in two infinite disjoint sets *)
definition "part12_pred V V1_V2 
 V = fst V1_V2  snd V1_V2  fst V1_V2  snd V1_V2 = {} 
 infinite (fst V1_V2)  infinite (snd V1_V2)"

definition "part12 V  SOME V1_V2. part12_pred V V1_V2"
definition "part1 = fst o part12"  definition "part2 = snd o part12"

lemma part12_pred:
assumes "infinite (V::'a set)"  shows " V1_V2. part12_pred V V1_V2"
proof-
  obtain f :: "nat  'a" where f: "inj f" and r: "range f  V"
  using assms by (metis infinite_iff_countable_subset)
  let ?u = "λ k::nat. 2 * k"  let ?v = "λ k::nat. Suc (2 * k)"
  let ?A = "?u ` UNIV"  let ?B = "?v ` UNIV"
  have 0: "inj ?u  inj ?v" unfolding inj_on_def by auto
  hence 1: "infinite ?A  infinite ?B" using finite_imageD by auto
  let ?V1 = "f ` ?A"  let ?V2 = "V - ?V1"
  have "V = ?V1  ?V2  ?V1  ?V2 = {}" using r by blast
  moreover have "infinite ?V1" using 1 f
  by (metis finite_imageD subset_inj_on top_greatest)
  moreover
  {have "infinite (f ` ?B)" using 1 f
   by (metis finite_imageD subset_inj_on top_greatest)
   moreover have "f ` ?B  ?V2" using r f by (auto simp: inj_eq) arith
   ultimately have "infinite ?V2" by (metis infinite_super)
  }
  ultimately show ?thesis unfolding part12_pred_def
  by (intro exI[of _ "(?V1,?V2)"]) auto
qed

lemma part12: assumes "infinite V"  shows "part12_pred V (part12 V)"
using part12_pred[OF assms] unfolding part12_def by(rule someI_ex)

lemma part1_Un_part2: "infinite V  part1 V  part2 V = V"
using part12 unfolding part1_def part2_def part12_pred_def by auto

lemma part1_Int_part2: "infinite V  part1 V  part2 V = {}"
using part12 unfolding part1_def part2_def part12_pred_def by auto

lemma infinite_part1: "infinite V  infinite (part1 V)"
using part12 unfolding part1_def part12_pred_def by auto

lemma part1_su: "infinite V  part1 V  V"
using part1_Un_part2 by auto

lemma infinite_part2: "infinite V  infinite (part2 V)"
using part12 unfolding part2_def part12_pred_def by auto

lemma part2_su: "infinite V  part2 V  V"
using part1_Un_part2 by auto



end

Theory TermsAndClauses

section‹Syntax of Terms and Clauses›
theory TermsAndClauses
imports Preliminaries
begin

text
‹These are used for both unsorted and many-sorted FOL, the difference being that,
for the latter, the signature will fix a variable typing.›

text‹Terms:›

datatype 'fsym trm =
  Var var |
  Fn 'fsym "'fsym trm list"

text‹Atomic formulas (atoms):›

datatype ('fsym, 'psym) atm =
  Eq "'fsym trm" "'fsym trm" |
  Pr 'psym "'fsym trm list"

text‹Literals:›

datatype ('fsym, 'psym) lit =
  Pos "('fsym, 'psym) atm" |
  Neg "('fsym, 'psym) atm"

text‹Clauses:›

type_synonym ('fsym, 'psym) cls = "('fsym, 'psym) lit list"

text‹Problems:›

type_synonym ('fsym, 'psym) prob = "('fsym, 'psym) cls set"

lemma trm_induct[case_names Var Fn, induct type: trm]:
assumes " x. φ (Var x)"
and " f Tl. list_all φ Tl  φ (Fn f Tl)"
shows "φ T"
using assms unfolding list_all_iff by (rule trm.induct) metis

fun vars where
"vars (Var x) = {x}"
|
"vars (Fn f Tl) =  (vars ` (set Tl))"

fun varsA where
"varsA (Eq T1 T2) = vars T1  vars T2"
|
"varsA (Pr p Tl) =  (set (map vars Tl))"

fun varsL where
"varsL (Pos at) = varsA at"
|
"varsL (Neg at) = varsA at"

definition "varsC c =  (set (map varsL c))"

definition "varsPB Φ =  {varsC c | c. c  Φ}"

text‹Substitution:›

fun subst where
"subst π (Var x) = π x"
|
"subst π (Fn f Tl) = Fn f (map (subst π) Tl)"

fun substA where
"substA π (Eq T1 T2) = Eq (subst π T1) (subst π T2)"
|
"substA π (Pr p Tl) = Pr p (map (subst π) Tl)"

fun substL where
"substL π (Pos at) = Pos (substA π at)"
|
"substL π (Neg at) = Neg (substA π at)"

definition "substC π c = map (substL π) c"

definition "substPB π Φ = {substC π c | c. c  Φ}"

lemma subst_cong:
assumes " x. x  vars T  π1 x = π2 x"
shows "subst π1 T = subst π2 T"
using assms by (induct T, auto simp add: list_all_iff)

lemma substA_congA:
assumes " x. x  varsA at  π1 x = π2 x"
shows "substA π1 at = substA π2 at"
using assms subst_cong[of _ π1 π2]
by (cases at, fastforce+)

lemma substL_congL:
assumes " x. x  varsL l  π1 x = π2 x"
shows "substL π1 l = substL π2 l"
using assms substA_congA[of _ π1 π2] by (cases l, auto)

lemma substC_congC:
assumes " x. x  varsC c  π1 x = π2 x"
shows "substC π1 c = substC π2 c"
using substL_congL[of _ π1 π2] assms unfolding substC_def varsC_def
by (induct c, auto)

lemma substPB_congPB:
assumes " x. x  varsPB Φ  π1 x = π2 x"
shows "substPB π1 Φ = substPB π2 Φ"
using substC_congC[of _ π1 π2] assms unfolding substPB_def varsPB_def
by simp_all (metis (lifting) substC_congC) 

lemma vars_subst:
"vars (subst π T) = ( x  vars T. vars (π x))"
by (induct T) (auto simp add: list_all_iff)

lemma varsA_substA:
"varsA (substA π at) = ( x  varsA at. vars (π x))"
using vars_subst[of π] by (cases at, auto)

lemma varsL_substL:
"varsL (substL π l) = ( x  varsL l. vars (π x))"
using varsA_substA[of π] by (cases l, auto)

lemma varsC_substC:
"varsC (substC π c) = ( x  varsC c. vars (π x))"
apply(induct c) unfolding substC_def varsC_def
  apply fastforce
  unfolding substC_def varsC_def map_map set_map
  unfolding comp_def varsL_substL by blast

lemma varsPB_Un[simp]: "varsPB (Φ1  Φ2) = varsPB Φ1  varsPB Φ2"
unfolding varsPB_def by auto

lemma varsC_append[simp]: "varsC (c1 @ c2) = varsC c1  varsC c2"
unfolding varsC_def by auto

lemma varsPB_sappend_incl[simp]:
"varsPB (Φ1 @@ Φ2)   varsPB Φ1  varsPB Φ2"
by (unfold varsPB_def sappend_def, fastforce)

lemma varsPB_sappend[simp]:
assumes 1: "Φ1  {}" and 2: "Φ2  {}"
shows "varsPB (Φ1 @@ Φ2) = varsPB Φ1  varsPB Φ2"
proof safe
  fix x
  {assume "x  varsPB Φ1"
   then obtain c1 c2 where "x  varsC c1" and "c1  Φ1" and "c2  Φ2"
   using 2 unfolding varsPB_def by auto
   thus "x  varsPB (Φ1 @@ Φ2)" unfolding sappend_def varsPB_def by fastforce
  }
  {assume "x  varsPB Φ2"
   then obtain c1 c2 where "x  varsC c2" and "c1  Φ1" and "c2  Φ2"
   using 1 unfolding varsPB_def by auto
   thus "x  varsPB (Φ1 @@ Φ2)" unfolding sappend_def varsPB_def by fastforce
  }
qed(unfold varsPB_def sappend_def, fastforce)

lemma varsPB_substPB:
"varsPB (substPB π Φ) = ( x  varsPB Φ. vars (π x))" (is "_ = ?K")
proof safe
  fix x assume "x  varsPB (substPB π Φ)"
  then obtain c where "c  Φ" and "x  varsC (substC π c)"
  unfolding varsPB_def substPB_def by auto
  thus "x  ?K" unfolding varsC_substC varsPB_def by auto
next
  fix x y assume "y  varsPB Φ" and x: "x  vars (π y)"
  then obtain c where c: "c  Φ" and "y  varsC c" unfolding varsPB_def by auto
  hence "x  varsC (substC π c)" using x unfolding varsC_substC by auto
  thus "x  varsPB (substPB π Φ)" using c unfolding varsPB_def substPB_def by auto
qed

lemma subst_o:
"subst (subst π1 o π2) T = subst π1 (subst π2 T)"
apply(induct T) by (auto simp add: list_all_iff)

lemma o_subst:
"subst π1 o subst π2 = subst (subst π1 o π2)"
apply(rule ext) apply(subst comp_def) unfolding subst_o[symmetric] ..

lemma substA_o:
"substA (subst π1 o π2) at = substA π1 (substA π2 at)"
using subst_o[of π1 π2] by (cases at, auto)

lemma o_substA:
"substA π1 o substA π2 = substA (subst π1 o π2)"
apply(rule ext) apply(subst comp_def) unfolding substA_o[symmetric] ..

lemma substL_o:
"substL (subst π1 o π2) l = substL π1 (substL π2 l)"
using substA_o[of π1 π2] by (cases l, auto)

lemma o_substL:
"substL π1 o substL π2 = substL (subst π1 o π2)"
apply(rule ext) apply(subst comp_def) unfolding substL_o[symmetric] ..

lemma substC_o:
"substC (subst π1 o π2) c = substC π1 (substC π2 c)"
using substL_o[of π1 π2] unfolding substC_def by (induct c, auto)

lemma o_substC:
"substC π1 o substC π2 = substC (subst π1 o π2)"
apply(rule ext) apply(subst comp_def) unfolding substC_o[symmetric] ..

lemma substPB_o:
"substPB (subst π1 o π2) Φ = substPB π1 (substPB π2 Φ)"
using substC_o[of π1 π2] unfolding substPB_def by auto

lemma o_substPB:
"substPB π1 o substPB π2 = substPB (subst π1 o π2)"
apply(rule ext) apply(subst comp_def) unfolding substPB_o[symmetric] ..

lemma finite_vars: "finite (vars T)"
by(induct T, auto simp add: list_all_iff)

lemma finite_varsA: "finite (varsA at)"
using finite_vars by (cases at, auto)

lemma finite_varsL: "finite (varsL l)"
using finite_varsA by (cases l, auto)

lemma finite_varsC: "finite (varsC c)"
using finite_varsL unfolding varsC_def by (induct c, auto)

lemma finite_varsPB: "finite Φ  finite (varsPB Φ)"
using finite_varsC unfolding varsPB_def by (auto intro!: finite_Union)

end

Theory Sig

section ‹Many-Typed (Many-Sorted) First-Order Logic›
theory Sig imports Preliminaries
begin

text‹In this formalization, we call ``types" what the first-order logic community usually calls ``sorts".› 


subsection‹Signatures› 

locale Signature =
fixes
    wtFsym :: "'fsym  bool"
and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf :: "'fsym  'tp"
and parOf :: "'psym  'tp list"
assumes
    countable_tp: "countable (UNIV :: 'tp set)"
and countable_wtFsym: "countable {f::'fsym. wtFsym f}"
and countable_wtPsym: "countable {p::'psym. wtPsym p}"
begin

text‹Partitioning of the variables in countable sets for each type:›

definition tpOfV_pred :: "(var  'tp)  bool" where
"tpOfV_pred f   σ. infinite (f -` {σ})"

definition "tpOfV  SOME f. tpOfV_pred f"

lemma infinite_fst_vimage:
"infinite ((fst :: 'a × nat  'a) -` {a})" (is "infinite (?f -` {a})")
proof-
  have "?f -` {a} = {(a,n::nat) | n . True}" (is "_ = ?A") by auto
  moreover
  {have 0: "?A = range (Pair a)" by auto
   have "infinite ?A" unfolding 0 apply(rule range_inj_infinite)
   unfolding inj_on_def by auto
  }
  ultimately show ?thesis by auto
qed

lemma tpOfV_pred: " f. tpOfV_pred f"
proof-
  define Ut Uv where "Ut = (UNIV :: 'tp set)" and "Uv = (UNIV :: var set)"
  define Unt where "Unt = (UNIV :: nat set)"
  define U2 where "U2 = (UNIV :: ('tp × nat) set)"
  have U2: "U2  Ut × Unt" unfolding Ut_def Unt_def U2_def UNIV_Times_UNIV .
  have "|U2| =o |Unt × Ut|" unfolding U2 by (metis card_of_Times_commute)
  also have "|Unt × Ut| =o |Unt|"
  apply(rule card_of_Times_infinite_simps(1)) unfolding Ut_def Unt_def
  apply (metis nat_not_finite)
  apply (metis UNIV_not_empty)
  by (metis countable_card_of_nat countable_tp)
  also have "|Unt| =o |Uv|" apply(rule ordIso_symmetric)
  unfolding Unt_def Uv_def using card_of_var card_of_nat[THEN ordIso_symmetric]
  by(rule ordIso_transitive)
  finally have "|U2| =o |Uv|" .
  hence "|Uv| =o |U2|" by(rule ordIso_symmetric)
  then obtain g where g: "bij_betw g Uv U2" unfolding card_of_ordIso[symmetric] by blast
  show ?thesis apply(rule exI[of _ "fst o g"]) unfolding tpOfV_pred_def apply safe
  unfolding vimage_comp [symmetric] apply (drule finite_vimageD)
  using g unfolding bij_betw_def Uv_def U2_def by (auto simp: infinite_fst_vimage)
qed

lemma tpOfV_pred_tpOfV: "tpOfV_pred tpOfV"
using tpOfV_pred unfolding tpOfV_def by (rule someI_ex)

lemma tpOfV: "infinite (tpOfV -` {σ})"
using tpOfV_pred_tpOfV unfolding tpOfV_pred_def by auto

definition "tpart1 V   σ. part1 (V  tpOfV -` {σ})"
definition "tpart2 V   σ. part2 (V  tpOfV -` {σ})"
definition "tinfinite V   σ. infinite (V  tpOfV -` {σ})"

lemma tinfinite_var[simp,intro]: "tinfinite (UNIV :: var set)"
unfolding tinfinite_def using tpOfV by auto

lemma tinifnite_singl[simp]:
assumes "tinfinite V"  shows "tinfinite (V - {x})"
unfolding tinfinite_def proof safe
  fix σ assume 0: "finite ((V - {x})  tpOfV -` {σ})"
  have "finite ((V  tpOfV -` {σ}) - {x})" apply(rule finite_subset[OF _ 0]) by auto
  thus False using assms unfolding tinfinite_def by auto
qed

lemma tpart1_Un_tpart2[simp]:
assumes "tinfinite V" shows "tpart1 V  tpart2 V = V"
using assms part1_Un_part2 unfolding tinfinite_def tpart1_def tpart2_def
unfolding UN_Un_distrib[symmetric] by blast

lemma tpart1_Int_tpart2[simp]:
assumes "tinfinite V" shows "tpart1 V  tpart2 V = {}"
using assms part1_Int_part2 unfolding tinfinite_def tpart1_def tpart2_def
unfolding Int_UN_distrib2 apply auto apply (case_tac "xa = xb", auto)
using part1_su part2_su by blast (* fixme: clean proof *)

lemma tpart1_su:
assumes "tinfinite V"  shows "tpart1 V  V"
using assms unfolding tinfinite_def tpart1_def
using part1_su by (auto intro: UN_least)

lemma tpart1_in:
assumes "tinfinite V" and "x  tpart1 V" shows "x  V"
using assms tpart1_su by auto

lemma tinfinite_tpart1[simp]:
assumes "tinfinite V"
shows "tinfinite (tpart1 V)"
unfolding tinfinite_def tpart1_def proof safe
  fix σ assume
  "finite ((σ'. part1 (V  tpOfV -` {σ'}))  tpOfV -` {σ})" (is "finite ?A")
  moreover have "?A = part1 (V  tpOfV -` {σ})"
  using assms part1_su unfolding tinfinite_def by auto
  moreover have "infinite ..."
  using assms infinite_part1 unfolding tinfinite_def by auto
  ultimately show False by auto
qed

lemma tinfinite_tpart2[simp]:
assumes "tinfinite V"
shows "tinfinite (tpart2 V)"
unfolding tinfinite_def tpart2_def proof safe
  fix σ assume
  "finite ((σ'. part2 (V  tpOfV -` {σ'}))  tpOfV -` {σ})" (is "finite ?A")
  moreover have "?A = part2 (V  tpOfV -` {σ})"
  using assms part2_su unfolding tinfinite_def by auto
  moreover have "infinite ..."
  using assms infinite_part2 unfolding tinfinite_def by auto
  ultimately show False by auto
qed

lemma tpart2_su:
assumes "tinfinite V"  shows "tpart2 V  V"
using assms unfolding tinfinite_def tpart2_def
using part2_su by (auto intro: UN_least)

lemma tpart2_in:
assumes "tinfinite V" and "x  tpart2 V" shows "x  V"
using assms tpart2_su by auto

text‹Typed-pick: picking a variable of a given type›

definition "tpick σ V  pick (V  tpOfV -` {σ})"

lemma tinfinite_ex: "tinfinite V   x  V. tpOfV x = σ"
unfolding tinfinite_def using infinite_imp_nonempty by auto

lemma tpick: assumes "tinfinite V" shows "tpick σ V  V  tpOfV -` {σ}"
proof-
  obtain x where "x  V  tpOfV x = σ"
  using tinfinite_ex[OF assms] by auto
  hence "x  V  tpOfV -` {σ}" by blast
  thus ?thesis unfolding tpick_def by (rule pick)
qed

lemma tpick_in[simp]: "tinfinite V  tpick σ V  V"
and tpOfV_tpick[simp]: "tinfinite V  tpOfV (tpick σ V) = σ"
using tpick by auto

lemma finite_tinfinite:
assumes "finite V"
shows "tinfinite (UNIV - V)"
using assms infinite_var unfolding tinfinite_def
by (metis Diff_Int2 Diff_Int_distrib2 Int_UNIV_left finite_Diff2 tpOfV)

(* get variable terms for the given types: *)
fun getVars where
"getVars [] = []"
|
"getVars (σ # σl) =
 (let xl = getVars σl in (tpick σ (UNIV - set xl)) # xl)"

lemma distinct_getVars: "distinct (getVars σl)"
using tpick_in[OF finite_tinfinite] by (induct σl, auto simp: Let_def)

lemma length_getVars[simp]: "length (getVars σl) = length σl"
by(induct σl, auto simp: Let_def)

lemma map_tpOfV_getVars[simp]: "map tpOfV (getVars σl) = σl"
using tpOfV_tpick[OF finite_tinfinite] by (induct σl, auto simp: Let_def)

lemma tpOfV_getVars_nth[simp]:
assumes "i < length σl"  shows "tpOfV (getVars σl ! i) = σl ! i"
using assms using map_tpOfV_getVars by (metis length_getVars nth_map)


end (* context Signature *)


end

Theory M

theory M
imports TermsAndClauses Sig
begin  


subsection‹Well-typed (well-formed) terms, clauses, literals and problems›

context Signature begin

text‹The type of a term›
fun tpOf where
"tpOf (Var x) = tpOfV x"
|
"tpOf (Fn f Tl) = resOf f"

(* Well-typed terms *)
fun wt where
"wt (Var x)  True"
|
"wt (Fn f Tl) 
 wtFsym f  list_all wt Tl  arOf f = map tpOf Tl"

(* Well-typed atoms (atomic formulas) *)
fun wtA where
"wtA (Eq T1 T2)  wt T1  wt T2  tpOf T1 = tpOf T2"
|
"wtA (Pr p Tl) 
 wtPsym p  list_all wt Tl  parOf p = map tpOf Tl"

(* Well-typed literals *)
fun wtL where
"wtL (Pos a)  wtA a"
|
"wtL (Neg a)  wtA a"

(* Well-typed clauses *)
definition "wtC  list_all wtL"

lemma wtC_append[simp]: "wtC (c1 @ c2)  wtC c1  wtC c2"
unfolding wtC_def by simp

(* Well-typed problems *)
definition "wtPB Φ   c  Φ. wtC c"

lemma wtPB_Un[simp]: "wtPB (Φ1  Φ2)  wtPB Φ1  wtPB Φ2"
unfolding wtPB_def by auto

lemma wtPB_UN[simp]: "wtPB ( i  I. Φ i)  ( i  I. wtPB (Φ i))"
unfolding wtPB_def by auto

lemma wtPB_sappend[simp]:
assumes "wtPB Φ1" and "wtPB Φ2"  shows "wtPB (Φ1 @@ Φ2)"
using assms unfolding wtPB_def sappend_def by auto

(* Well-typed substitutions *)
definition "wtSB π   x. wt (π x)  tpOf (π x) = tpOfV x"

lemma wtSB_wt[simp]: "wtSB π  wt (π x)"
unfolding wtSB_def by auto

lemma wtSB_tpOf[simp]: "wtSB π  tpOf (π x) = tpOfV x"
unfolding wtSB_def by auto

lemma wt_tpOf_subst:
assumes "wtSB π" and "wt T"
shows "wt (subst π T)  tpOf (subst π T) = tpOf T"
using assms apply(induct T) by (auto simp add: list_all_iff)

lemmas wt_subst[simp] = wt_tpOf_subst[THEN conjunct1]
lemmas tpOf_subst[simp] = wt_tpOf_subst[THEN conjunct2]

lemma wtSB_o:
assumes 1: "wtSB π1" and 2: "wtSB π2"
shows "wtSB (subst π1 o π2)"
using 2 unfolding wtSB_def using 1 by auto

(* Getting variable terms for given types: *)
definition "getTvars σl  map Var (getVars σl)"

lemma length_getTvars[simp]: "length (getTvars σl) = length σl"
unfolding getTvars_def by auto

lemma wt_getTvars[simp]: "list_all wt (getTvars σl)"
unfolding list_all_length getTvars_def by simp

lemma wt_nth_getTvars[simp]:
"i < length σl  wt (getTvars σl ! i)"
unfolding getTvars_def by auto

lemma map_tpOf_getTvars[simp]: "map tpOf (getTvars σl) = σl"
unfolding getTvars_def unfolding list_eq_iff by auto

lemma tpOf_nth_getTvars[simp]:
"i < length σl  tpOf (getTvars σl ! i) = σl ! i"
unfolding getTvars_def by auto

end (* context Signature *)


subsection ‹Structures›

text‹We split a structre into a ``type structure'' that interprets the types 
and the rest of the structure that interprets the function and relation symbols.›

text‹Type structures:›

locale Tstruct =
fixes intT :: "'tp  'univ  bool"
assumes NE_intT: "NE (intT σ)"

text‹Environment:›

type_synonym ('tp,'univ) env = "'tp  var  'univ"

text‹Structures:›

locale Struct = Signature wtFsym wtPsym arOf resOf parOf +
                Tstruct intT
for wtFsym and wtPsym
and arOf :: "'fsym  'tp list"
and resOf :: "'fsym  'tp"
and parOf :: "'psym  'tp list"
and intT :: "'tp  'univ  bool"
+
fixes
    intF :: "'fsym  'univ list  'univ"
and intP :: "'psym  'univ list  bool"
assumes
intF: "wtFsym f; list_all2 intT (arOf f) al  intT (resOf f) (intF f al)"
and
dummy: "intP = intP"
begin

text‹Well-typed environment:›

definition "wtE ξ   x. intT (tpOfV x) (ξ x)"

lemma wtTE_intT[simp]: "wtE ξ  intT (tpOfV x) (ξ x)"
unfolding wtE_def dom_def by auto

(* Picking an element from the domain of a given type: *)
definition "pickT σ  SOME a. intT σ a"

lemma pickT[simp]: "intT σ (pickT σ)"
unfolding pickT_def apply(rule someI_ex) using NE_intT by auto

text‹Picking a well-typed environment:›

definition
"pickE (xl::var list) al 
 SOME ξ. wtE ξ  ( i < length xl. ξ (xl!i) = al!i)"

lemma ex_pickE:
assumes "length xl = length al"
and "distinct xl" and " i. i < length xl  intT (tpOfV (xl!i)) (al!i)"
shows " ξ. wtE ξ  ( i < length xl. ξ (xl!i) = al!i)"
using assms
proof(induct rule: list_induct2)
  case Nil show ?case apply(rule exI[of _ "λ x. pickT (tpOfV x)"])
  unfolding wtE_def by auto
next
  case (Cons x xl a al)
  then obtain ξ where 1: "wtE ξ" and 2: " i < length xl. ξ (xl!i) = al!i" by force
  define ξ' where "ξ' x' = (if x = x' then a else ξ x')" for x'
  show ?case
  proof(rule exI[of _ ξ'], unfold wtE_def, safe)
    fix x' show "intT (tpOfV x') (ξ' x')"
    using 1 Cons.prems(2)[of 0] unfolding ξ'_def by auto
  next
    fix i assume i: "i < length (x # xl)"
    thus "ξ' ((x # xl) ! i) = (a # al) ! i"
    proof(cases i)
      case (Suc j) hence j: "j < length xl" using i by auto
      have "¬ x = (x # xl) ! i" using Suc i Cons.prems(1) by auto
      thus ?thesis using Suc using j Cons.prems(1) Cons.hyps 2 unfolding ξ'_def by auto
    qed(insert Cons.prems(1) Cons.hyps 2, unfold ξ'_def, simp)
  qed
qed

lemma wtE_pickE_pickE:
assumes "length xl = length al"
and "distinct xl" and " i. i < length xl  intT (tpOfV (xl!i)) (al!i)"
shows "wtE (pickE xl al)  ( i. i < length xl  pickE xl al (xl!i) = al!i)"
proof-
  let ?phi = "λ ξ. wtE ξ  ( i < length xl. ξ (xl!i) = al!i)"
  show ?thesis unfolding pickE_def apply(rule someI_ex[of ?phi])
  using ex_pickE[OF assms] by simp
qed

lemmas wtE_pickE[simp] = wtE_pickE_pickE[THEN conjunct1]

lemma pickE[simp]:
assumes "length xl = length al"
and "distinct xl" and " i. i < length xl  intT (tpOfV (xl!i)) (al!i)"
and "i < length xl"
shows "pickE xl al (xl!i) = al!i"
using assms wtE_pickE_pickE by auto

definition "pickAnyE  pickE [] []"

lemma wtE_pickAnyE[simp]: "wtE pickAnyE"
unfolding pickAnyE_def by (rule wtE_pickE) auto

(* Interpretation of terms: *)
fun int where
"int ξ (Var x) = ξ x"
|
"int ξ (Fn f Tl) = intF f (map (int ξ) Tl)"

(* Satisfaction of atoms: *)
fun satA where
"satA ξ (Eq T1 T2)  int ξ T1 = int ξ T2"
|
"satA ξ (Pr p Tl)  intP p (map (int ξ) Tl)"

(* Satisfaction literals: *)
fun satL where
"satL ξ (Pos a)  satA ξ a"
|
"satL ξ (Neg a)  ¬ satA ξ a"

(* Satisfaction of clauses: *)
definition "satC ξ  list_ex (satL ξ)"

lemma satC_append[simp]: "satC ξ (c1 @ c2)  satC ξ c1  satC ξ c2"
unfolding satC_def by auto

lemma satC_iff_set: "satC ξ c  ( l  set c. satL ξ l)"
unfolding satC_def Bex_set[symmetric] ..

(* satisfaction of problems *)
definition "satPB ξ Φ   c  Φ. satC ξ c"

lemma satPB_Un[simp]: "satPB ξ (Φ1  Φ2)  satPB ξ Φ1  satPB ξ Φ2"
unfolding satPB_def by auto

lemma satPB_UN[simp]: "satPB ξ ( i  I. Φ i)  ( i  I. satPB ξ (Φ i))"
unfolding satPB_def by auto

lemma satPB_sappend[simp]: "satPB ξ (Φ1 @@ Φ2)  satPB ξ Φ1  satPB ξ Φ2"
unfolding satPB_def sappend_def by (fastforce simp: satC_append)

definition "SAT Φ   ξ. wtE ξ  satPB ξ Φ"

lemma SAT_UN[simp]: "SAT ( i  I. Φ i)  ( i  I. SAT (Φ i))"
unfolding SAT_def by auto

text‹Soundness of typing w.r.t. interpretation:›

lemma wt_int:
assumes wtE: "wtE ξ" and wt: "wt T"
shows "intT (tpOf T) (int ξ T)"
using wt apply(induct T) using wtE
by (auto intro!: intF simp add: list_all2_map_map)

lemma int_cong:
assumes "x. x  vars T  ξ1 x = ξ2 x"
shows "int ξ1 T = int ξ2 T"
using assms proof(induct T)
  case (Fn f Tl)
  hence 1: "map (int ξ1) Tl = map (int ξ2) Tl"
  unfolding list_all_iff by (auto intro: map_ext)
  show ?case apply simp by (metis 1)
qed auto

lemma satA_cong:
assumes "x. x  varsA at  ξ1 x = ξ2 x"
shows "satA ξ1 at  satA ξ2 at"
using assms int_cong[of _ ξ1 ξ2]
apply(cases at) apply(fastforce intro!: int_cong[of _ ξ1 ξ2])
apply simp by (metis (hide_lams, mono_tags) map_eq_conv)

lemma satL_cong:
assumes " x. x  varsL l  ξ1 x = ξ2 x"
shows "satL ξ1 l  satL ξ2 l"
using assms satA_cong[of _ ξ1 ξ2] by (cases l, auto)

lemma satC_cong:
assumes " x. x  varsC c  ξ1 x = ξ2 x"
shows "satC ξ1 c  satC ξ2 c"
using assms satL_cong[of _ ξ1 ξ2] unfolding satC_def varsC_def
apply (induct c) by (fastforce intro!: satL_cong[of _ ξ1 ξ2])+

lemma satPB_cong:
assumes " x. x  varsPB Φ  ξ1 x = ξ2 x"
shows "satPB ξ1 Φ  satPB ξ2 Φ"
by (force simp: satPB_def varsPB_def intro!: satC_cong ball_cong assms)

lemma int_o:
"int (int ξ o ρ) T = int ξ (subst ρ T)"
apply(induct T) apply simp_all unfolding list_all_iff o_def
using map_ext by (metis (lifting, no_types))

lemmas int_subst = int_o[symmetric]

lemma int_o_subst:
"int ξ o subst ρ = int (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding int_o[symmetric] ..

lemma satA_o:
"satA (int ξ o ρ) at = satA ξ (substA ρ at)"
by (cases at, simp_all add: int_o_subst int_o[of ξ ρ])

lemmas satA_subst = satA_o[symmetric]

lemma satA_o_subst:
"satA ξ o substA ρ = satA (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding satA_o[symmetric] ..

lemma satL_o:
"satL (int ξ o ρ) l = satL ξ (substL ρ l)"
using satA_o[of ξ ρ] by (cases l, simp_all)

lemmas satL_subst = satL_o[symmetric]

lemma satL_o_subst:
"satL ξ o substL ρ = satL (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding satL_o[symmetric] ..

lemma satC_o:
"satC (int ξ o ρ) c = satC ξ (substC ρ c)"
using satL_o[of ξ ρ] unfolding satC_def substC_def by (induct c, auto)

lemmas satC_subst = satC_o[symmetric]

lemma satC_o_subst:
"satC ξ o substC ρ = satC (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding satC_o[symmetric] ..

lemma satPB_o:
"satPB (int ξ o ρ) Φ = satPB ξ (substPB ρ Φ)"
using satC_o[of ξ ρ] unfolding satPB_def substPB_def by auto

lemmas satPB_subst = satPB_o[symmetric]

lemma satPB_o_subst:
"satPB ξ o substPB ρ = satPB (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding satPB_o[symmetric] ..

lemma wtE_o:
assumes 1: "wtE ξ" and 2: "wtSB ρ"
shows "wtE (int ξ o ρ)"
unfolding wtE_def proof
  fix x have 0: "tpOfV x = tpOf (ρ x)" using 2 by auto
  show "intT (tpOfV x) ((int ξ  ρ) x)" apply(subst 0) unfolding comp_def
  apply(rule wt_int[OF 1]) using 2 by auto
qed

(* fixme: unify compE and int ξ o ρ, since they are the same *)
definition "compE ρ ξ x  int ξ (ρ x)"

lemma wtE_compE:
assumes "wtSB ρ" and "wtE ξ"  shows "wtE (compE ρ ξ)"
unfolding wtE_def using assms wt_int
unfolding wtSB_def compE_def by fastforce

lemma compE_upd: "compE (ρ (x := T)) ξ = (compE ρ ξ) (x := int ξ T)"
unfolding compE_def[abs_def] by auto

end (* context Struct *)


context Signature begin

(* The function symbols of: *)

fun fsyms where
"fsyms (Var x) = {}"
|
"fsyms (Fn f Tl) = {f}   (set (map fsyms Tl))"

fun fsymsA where
"fsymsA (Eq T1 T2) = fsyms T1  fsyms T2"
|
"fsymsA (Pr p Tl) =  (set (map fsyms Tl))"

fun fsymsL where
"fsymsL (Pos at) = fsymsA at"
|
"fsymsL (Neg at) = fsymsA at"

definition "fsymsC c =  (set (map fsymsL c))"

definition "fsymsPB Φ =  {fsymsC c | c. c  Φ}"

lemma fsyms_int_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: " f. f  fsyms T  intF1 f = intF2 f"
shows "Struct.int intF1 ξ T = Struct.int intF2 ξ T"
using 0 proof(induct T)
  case (Fn f Tl)
  hence 1: "map (Struct.int intF1 ξ) Tl = map (Struct.int intF2 ξ) Tl"
  unfolding list_all_iff map_ext by auto
  show ?case 
  using Fn Struct.int.simps[OF S1, of ξ] Struct.int.simps[OF S2, of ξ] apply simp
  using 1 by metis
qed (auto simp: Struct.int.simps[OF S1, of ξ] Struct.int.simps[OF S2, of ξ])

lemma fsyms_satA_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: " f. f  fsymsA at  intF1 f = intF2 f"
shows "Struct.satA intF1 intP ξ at  Struct.satA intF2 intP ξ at"
using 0 fsyms_int_cong[OF S1 S2]
apply(cases at)
apply(fastforce intro!: fsyms_int_cong[OF S1 S2, of _ ξ]
                simp: Struct.satA.simps[OF S1, of ξ] Struct.satA.simps[OF S2, of ξ])
apply (simp add: Struct.satA.simps[OF S1, of ξ] Struct.satA.simps[OF S2, of ξ])
by (metis (hide_lams, mono_tags) map_eq_conv)

lemma fsyms_satL_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: " f. f  fsymsL l  intF1 f = intF2 f"
shows "Struct.satL intF1 intP ξ l  Struct.satL intF2 intP ξ l"
using 0 fsyms_satA_cong[OF S1 S2]
by (cases l, auto simp: Struct.satL.simps[OF S1, of ξ] Struct.satL.simps[OF S2, of ξ])

lemma fsyms_satC_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: " f. f  fsymsC c  intF1 f = intF2 f"
shows "Struct.satC intF1 intP ξ c  Struct.satC intF2 intP ξ c"
using 0 fsyms_satL_cong[OF S1 S2]
unfolding Struct.satC_def[OF S1] Struct.satC_def[OF S2] fsymsC_def
apply (induct c) by (fastforce intro!: fsyms_satL_cong[OF S1 S2])+

lemma fsyms_satPB_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: " f. f  fsymsPB Φ  intF1 f = intF2 f"
shows "Struct.satPB intF1 intP ξ Φ  Struct.satPB intF2 intP ξ Φ"
by (force simp: Struct.satPB_def[OF S1] Struct.satPB_def[OF S2] fsymsPB_def
          intro!: fsyms_satC_cong[OF S1 S2] ball_cong 0)

lemma fsymsPB_Un[simp]: "fsymsPB (Φ1  Φ2) = fsymsPB Φ1  fsymsPB Φ2"
unfolding fsymsPB_def by auto

lemma fsymsC_append[simp]: "fsymsC (c1 @ c2) = fsymsC c1  fsymsC c2"
unfolding fsymsC_def by auto

lemma fsymsPB_sappend_incl[simp]:
"fsymsPB (Φ1 @@ Φ2)   fsymsPB Φ1  fsymsPB Φ2"
by (unfold fsymsPB_def sappend_def, fastforce)

lemma fsymsPB_sappend[simp]:
assumes 1: "Φ1  {}" and 2: "Φ2  {}"
shows "fsymsPB (Φ1 @@ Φ2) = fsymsPB Φ1  fsymsPB Φ2"
proof safe
  fix x
  {assume "x  fsymsPB Φ1"
   then obtain c1 c2 where "x  fsymsC c1" and "c1  Φ1" and "c2  Φ2"
   using 2 unfolding fsymsPB_def by auto
   thus "x  fsymsPB (Φ1 @@ Φ2)" unfolding sappend_def fsymsPB_def by fastforce
  }
  {assume "x  fsymsPB Φ2"
   then obtain c1 c2 where "x  fsymsC c2" and "c1  Φ1" and "c2  Φ2"
   using 1 unfolding fsymsPB_def by auto
   thus "x  fsymsPB (Φ1 @@ Φ2)" unfolding sappend_def fsymsPB_def by fastforce
  }
qed(unfold fsymsPB_def sappend_def, fastforce)

lemma Struct_upd:
assumes "Struct wtFsym wtPsym arOf resOf intT intF intP"
and " al. list_all2 intT (arOf ef) al  intT (resOf ef) (EF al)"
shows "Struct wtFsym wtPsym arOf resOf intT (intF (ef := EF)) intP"
apply standard using assms
unfolding Struct_def Struct_axioms_def Tstruct_def by auto

end (* context Signature *)


subsection‹Problems›

text‹A problem is a potentially infinitary formula in clausal form, i.e., 
a potentially infinite conjunction of clauses.›

locale Problem = Signature wtFsym wtPsym arOf resOf parOf
for wtFsym wtPsym
and arOf :: "'fsym  'tp list"
and resOf :: "'fsym  'tp"
and parOf :: "'psym  'tp list"
+
fixes Φ :: "('fsym, 'psym) prob"
assumes wt_Φ: "wtPB Φ"


subsection‹Models of a problem›

text‹Model of a problem:›

locale Model = Problem + Struct +
assumes SAT: "SAT Φ"
begin
lemma sat_Φ: "wtE ξ  satPB ξ Φ"
using SAT unfolding SAT_def by auto
end


end

Theory CM

(* Countable version of MFOL structures: *)
theory CM
imports M
begin

(* Countable Versions of the locales from M
that assume a fixed countable carrier univ
instead of an arbitrary one 'univ: *)
locale Tstruct = M.Tstruct intT
for intT :: "'tp  univ  bool"

locale Struct = M.Struct wtFsym wtPsym arOf resOf parOf intT intF intP
for wtFsym and wtPsym
and arOf :: "'fsym  'tp list"
and resOf and parOf :: "'psym  'tp list"
and intT :: "'tp  univ  bool"
and intF and intP

locale Model = M.Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP
for wtFsym and wtPsym
and arOf :: "'fsym  'tp list"
and resOf and parOf :: "'psym  'tp list" and Φ
and intT :: "'tp  univ  bool"
and intF and intP

sublocale Struct < Tstruct ..
sublocale Model < Struct ..


end

Theory Mono

section‹Monotonicity›
theory Mono imports CM begin


subsection‹Fullness and infiniteness›

text‹In a structure, a full type is one that contains all elements of univ (the fixed countable universe):›

definition (in Tstruct) "full σ   d. intT σ d"

locale FullStruct = F? : Struct +
assumes full: "full σ"
begin
lemma full2[simp]: "intT σ d"
using full unfolding full_def by simp

lemma full_True: "intT = (λ σ D. True)"
apply(intro ext) by auto
end

locale FullModel =
F? : Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP +
F? : FullStruct wtFsym wtPsym arOf resOf parOf intT intF intP
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ and intT and intF and intP

text‹An infinite structure is one with all carriers infinite:›

locale InfStruct = I? : Struct +
assumes inf: "infinite {a. intT σ a}"

locale InfModel =
I? : Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP +
I? : InfStruct wtFsym wtPsym arOf resOf parOf intT intF intP
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ and intT and intF and intP

context Problem begin
abbreviation "SStruct  Struct wtFsym wtPsym arOf resOf"
abbreviation "FFullStruct  FullStruct wtFsym wtPsym arOf resOf"
abbreviation "IInfStruct  InfStruct wtFsym wtPsym arOf resOf"

abbreviation "MModel  Model wtFsym wtPsym arOf resOf parOf Φ"
abbreviation "FFullModel  FullModel wtFsym wtPsym arOf resOf parOf Φ"
abbreviation "IInfModel  InfModel wtFsym wtPsym arOf resOf parOf Φ"
end

text‹Problem that deduces some infiniteness constraints:›

locale ProblemIk = Ik? : Problem wtFsym wtPsym arOf resOf parOf Φ
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ
+
fixes infTp :: "'tp  bool"
(* infTp assumes that Φ implies infiniteness on the infTp-marked types,
i.e., any model of Φ is infinite on these types: *)
assumes infTp:
" σ intT intF intP (a::univ). infTp σ; MModel intT intF intP  infinite {a. intT σ a}"

locale ModelIk =
Ik? : ProblemIk wtFsym wtPsym arOf resOf parOf Φ infTp +
Ik? : Model wtFsym wtPsym arOf resOf parOf Φ intT intF intP
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ and infTp and intT and intF and intP
begin
lemma infTp_infinite[simp]: "infTp σ  infinite {a. intT σ a}"
apply(rule ProblemIk.infTp[of wtFsym wtPsym arOf resOf parOf Φ infTp])
apply unfold_locales by simp
end


subsection‹Monotonicity›

context Problem begin
(* Monotonicity: *)
definition
"monot 
 ( intT intF intP. MModel intT intF intP)
 
 ( intTI intFI intPI. IInfModel intTI intFI intPI)"
end

locale MonotProblem = Problem +
assumes monot: monot

locale MonotProblemIk =
MonotProblem wtFsym wtPsym arOf resOf parOf Φ +
ProblemIk wtFsym wtPsym arOf resOf parOf Φ infTp
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list" and resOf and parOf and Φ and infTp

context MonotProblem
begin

definition "MI_pred K  IInfModel (fst3 K) (snd3 K) (trd3 K)"

definition "MI  SOME K. MI_pred K"

lemma MI_pred:
assumes "MModel intT intF intP"
shows " K. MI_pred K"
proof-
  obtain T F R where "MI_pred (T,F,R)"
  using monot assms unfolding monot_def MI_pred_def by auto
  thus ?thesis by blast
qed

lemma MI_pred_MI:
assumes "MModel intT intF intP"
shows "MI_pred MI"
using MI_pred[OF assms] unfolding MI_def by (rule someI_ex)

definition "intTI  fst3 MI"
definition "intFI  snd3 MI"
definition "intPI  trd3 MI"

lemma InfModel_intTI_intFI_intPI:
assumes "MModel intT intF intP"
shows "IInfModel intTI intFI intPI"
using MI_pred_MI[OF assms]
unfolding MI_pred_def intFI_def intPI_def intTI_def .

end (* context MonotProblem *)

locale MonotModel = M? : MonotProblem + M? : Model

context MonotModel begin

lemma InfModelI: "IInfModel intTI intFI intPI"
apply(rule MonotProblem.InfModel_intTI_intFI_intPI)
apply standard
done

end

(* Trivial fact: Any monotonic problem that has a model also has an infinite model: *)
sublocale MonotModel < InfModel where
intT = intTI and intF = intFI and intP = intPI
using InfModelI .


context InfModel begin

definition "toFull σ  SOME F. bij_betw F {a::univ. intT σ a} (UNIV::univ set)"
definition "fromFull σ  inv_into {a::univ. intT σ a} (toFull σ)"

definition "intTF σ a  True"
definition "intFF f al  toFull (resOf f) (intF f (map2 fromFull (arOf f) al))"
definition "intPF p al  intP p (map2 fromFull (parOf p) al)"

lemma intTF: "intTF σ a"
unfolding intTF_def by auto

lemma ex_toFull: " F. bij_betw F {a::univ. intT σ a} (UNIV::univ set)"
by (metis inf card_of_ordIso card_of_UNIV countable_univ UnE
          countable_infinite not_ordLeq_ordLess ordLeq_ordLess_Un_ordIso)

lemma toFull: "bij_betw (toFull σ) {a. intT σ a} UNIV"
by (metis (lifting) ex_toFull someI_ex toFull_def)

lemma toFull_fromFull[simp]: "toFull σ (fromFull σ a) = a"
by (metis UNIV_I bij_betw_inv_into_right fromFull_def toFull)

lemma fromFull_toFull[simp]: "intT σ a  fromFull σ (toFull σ a) = a"
by (metis CollectI bij_betw_inv_into_left toFull fromFull_def)

lemma fromFull_inj[simp]: "fromFull σ a = fromFull σ b  a = b"
by (metis toFull_fromFull)

lemma toFull_inj[simp]:
assumes "intT σ a" and "intT σ b"
shows "toFull σ a = toFull σ b  a = b"
by (metis assms fromFull_toFull)

lemma fromFull[simp]: "intT σ (fromFull σ a)"
unfolding fromFull_def
apply(rule inv_into_into[of a "toFull σ" "{a. intT σ a}", simplified])
using toFull unfolding bij_betw_def by auto

lemma toFull_iff_fromFull:
assumes "intT σ a"
shows "toFull σ a = b  a = fromFull σ b"
by (metis assms fromFull_toFull toFull_fromFull)

lemma Tstruct: "Tstruct intTF"
apply(unfold_locales) unfolding intTF_def by simp

lemma FullStruct: "FullStruct wtFsym wtPsym arOf resOf intTF intFF intPF"
apply (unfold_locales) unfolding intTF_def Tstruct.full_def[OF Tstruct] by auto

end (* locale InfModel *)

sublocale InfModel < FullStruct
where intT = intTF and intF = intFF and intP = intPF
using FullStruct .


context InfModel begin

definition "kE ξ  λ x. fromFull (tpOfV x) (ξ x)"

lemma kE[simp]: "kE ξ x = fromFull (tpOfV x) (ξ x)"
unfolding kE_def by simp

lemma wtE[simp]: "F.wtE ξ"
unfolding F.wtE_def by simp

lemma kE_wtE[simp]: "I.wtE (kE ξ)"
unfolding I.wtE_def kE_def by simp

lemma kE_int_toFull:
assumes ξ: "I.wtE (kE ξ)" and T: "wt T"
shows "toFull (tpOf T) (I.int (kE ξ) T) = F.int ξ T"
using T proof(induct T)
  case (Fn f Tl)
  have 0: "map (I.int (kE ξ)) Tl =
           map2 fromFull (arOf f) (map (F.int ξ) Tl)"
  (is "map ?F Tl = map2 fromFull (arOf f) (map ?H Tl)"
   is "?L = ?R")
  proof(rule nth_equalityI)
    have l: "length Tl = length (arOf f)" using Fn by simp
    thus "length ?L = length ?R" by simp
    fix i assume "i < length ?L"  hence i: "i < length Tl" by simp
    let ?toFull = "toFull (arOf f!i)"   let ?fromFull = "fromFull (arOf f!i)"
    have tp: "tpOf (Tl ! i) = arOf f ! i" using Fn(2) i unfolding list_all_length by auto
    have wt: "wt (Tl!i)" using Fn i by (auto simp: list_all_iff)
    have "intT (arOf f!i) (?F (Tl!i))" using I.wt_int[OF ξ wt] unfolding tp .
    moreover have "?toFull (?F (Tl!i)) = ?H (Tl!i)"
      using Fn tp i by (auto simp: list_all_iff kE_def)
    ultimately have "?F (Tl!i) = fromFull (arOf f!i) (?H (Tl!i))"
      using toFull_iff_fromFull by blast
    thus "?L!i = ?R!i" using l i by simp
  qed
  show ?case unfolding I.int.simps F.int.simps tpOf.simps unfolding intFF_def 0 ..
qed simp

lemma kE_int[simp]:
assumes ξ: "I.wtE (kE ξ)" and T: "wt T"
shows "I.int (kE ξ) T = fromFull (tpOf T) (F.int ξ T)"
using kE_int_toFull[OF assms]
unfolding toFull_iff_fromFull[OF I.wt_int[OF ξ T]] .

lemma map_kE_int[simp]:
  assumes ξ: "I.wtE (kE ξ)" and T: "list_all wt Tl"
  shows "map (I.int (kE ξ)) Tl = map2 fromFull (map tpOf Tl) (map (F.int ξ) Tl)"
  apply(rule nth_equalityI)
   apply (metis (lifting) length_map length_map2)
  by (metis T ξ kE_int length_map list_all_length nth_map nth_map2)

lemma kE_satA[simp]:
assumes at: "wtA at" and ξ: "I.wtE (kE ξ)"
shows "I.satA (kE ξ) at  F.satA ξ at"
using assms by (cases at, auto simp add: intPF_def)

lemma kE_satL[simp]:
assumes l: "wtL l" and ξ: "I.wtE (kE ξ)"
shows "I.satL (kE ξ) l  F.satL ξ l"
using assms by (cases l, auto)

lemma kE_satC[simp]:
assumes c: "wtC c" and ξ: "I.wtE (kE ξ)"
shows "I.satC (kE ξ) c  F.satC ξ c"
unfolding I.satC_def F.satC_def
using assms by(induct c, auto simp add: wtC_def)

lemma kE_satPB:
assumes ξ: "I.wtE (kE ξ)"  shows "F.satPB ξ Φ"
using I.sat_Φ[OF assms]
using wt_Φ assms unfolding I.satPB_def F.satPB_def
by (auto simp add: wtPB_def)

lemma F_SAT: "F.SAT Φ"
unfolding F.SAT_def using kE_satPB kE_wtE by auto

lemma FullModel: "FullModel wtFsym wtPsym arOf resOf parOf Φ intTF intFF intPF"
apply (unfold_locales) using F_SAT .

end (* context InfModel *)

sublocale InfModel < FullModel where
intT = intTF and intF = intFF and intP = intPF
using FullModel .


context MonotProblem begin

definition "intTF  InfModel.intTF"
definition "intFF  InfModel.intFF arOf resOf intTI intFI"
definition "intPF  InfModel.intPF parOf intTI intPI"

text‹Strengthening of the infiniteness condition for monotonicity,
replacing infininetess by fullness:›

theorem FullModel_intTF_intFF_intPF:
assumes "MModel intT intF intP"
shows "FFullModel intTF intFF intPF"
unfolding intTF_def intFF_def intPF_def
apply(rule InfModel.FullModel) using InfModel_intTI_intFI_intPI[OF assms] .

end (* context MonotProblem *)

sublocale MonotModel < FullModel where
intT = intTF and intF = intFF and intP = intPF
using FullModel .

end

Theory Mcalc

section‹The First Monotonicity Calculus›
theory Mcalc
imports Mono
begin

context ProblemIk begin

subsection‹Naked variables›

fun nvT where
"nvT (Var x) = {x}"
|
"nvT (Fn f Tl) = {}"

fun nvA where
"nvA (Eq T1 T2) = nvT T1  nvT T2"
|
"nvA (Pr p Tl) = {}"

fun nvL where
"nvL (Pos at) = nvA at"
|
"nvL (Neg at) = {}"

definition "nvC c   (set (map nvL c))"

definition "nvPB   c  Φ. nvC c"

lemma nvT_vars[simp]: "x  nvT T  x  vars T"
by (induct T) (auto split: if_splits)

lemma nvA_varsA[simp]: "x  nvA at  x  varsA at"
by (cases at, auto)

lemma nvL_varsL[simp]: "x  nvL l  x  varsL l"
by (cases l, auto)

lemma nvC_varsC[simp]: "x  nvC c  x  varsC c"
unfolding varsC_def nvC_def by(induct c, auto)

lemma nvPB_varsPB[simp]: "x  nvPB  x  varsPB Φ"
unfolding varsPB_def nvPB_def by auto


subsection‹The calculus›

inductive mcalc (infix "" 40) where
 [simp]: "infTp σ  σ  c"
|[simp]: "( x  nvC c. tpOfV x  σ)  σ  c"

lemma mcalc_iff: "σ  c  infTp σ  ( x  nvC c. tpOfV x  σ)"
unfolding mcalc.simps by simp

end (* context ProblemIk *)

locale ProblemIkMcalc = ProblemIk wtFsym wtPsym arOf resOf parOf Φ infTp
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ and infTp
+ assumes mcalc: " σ c. c  Φ  σ  c"

locale ModelIkMcalc =
ModelIk wtFsym wtPsym arOf resOf parOf Φ infTp intT intF intP +
ProblemIkMcalc wtFsym wtPsym arOf resOf parOf Φ infTp
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ and infTp and intT and intF and intP

subsection‹Extension of a structure to an infinite structure
by adding indistinguishable elements›

context ModelIkMcalc begin

text‹The projection from univ to a structure:›

definition proj where "proj σ a  if intT σ a then a else pickT σ"

lemma intT_proj[simp]: "intT σ (proj σ a)"
unfolding proj_def using pickT by auto

lemma proj_id[simp]: "intT σ a  proj σ a = a"
unfolding proj_def by auto

lemma surj_proj:
assumes "intT σ a"   shows " b. proj σ b = a"
using assms by (intro exI[of _ a]) simp

definition "I_intT σ (a::univ)  infTp σ  intT σ a"
definition "I_intF f al  intF f (map2 proj (arOf f) al)"
definition "I_intP p al  intP p (map2 proj (parOf p) al)"

lemma not_infTp_I_intT[simp]: "¬ infTp σ  I_intT σ a" unfolding I_intT_def by simp

lemma infTp_I_intT[simp]: "infTp σ  I_intT σ a = intT σ a" unfolding I_intT_def by simp

lemma NE_I_intT: "NE (I_intT σ)"
using NE_intT by (cases "infTp σ", auto)

lemma I_intF:
assumes f: "wtFsym f" and al: "list_all2 I_intT (arOf f) al"
shows "I_intT (resOf f) (I_intF f al)"
unfolding I_intT_def I_intF_def apply safe apply(rule intF[OF f])
using al unfolding list_all2_length by auto

lemma Tstruct_I_intT: "Tstruct I_intT"
by standard (rule NE_I_intT)

lemma inf_I_intT: "infinite {a. I_intT σ a}"
by (cases "infTp σ", auto)

lemma InfStruct: "IInfStruct I_intT I_intF I_intP"
apply standard using NE_I_intT I_intF Tstruct_I_intT inf_I_intT by auto

end (* context ModelIkMcalc *)

sublocale ModelIkMcalc < InfStruct where
intT = I_intT and intF = I_intF and intP = I_intP
using InfStruct .

subsection‹The soundness of the calculus›

text‹In what follows, ``Ik'' stands for the original
(augmented with infiniteness-knowledge)
and ``I'' for the infinite structure constructed from it
through the above sublocale statement.›


context ModelIkMcalc begin

text‹The environment translation along the projection:›
definition "transE ξ  λ x. proj (tpOfV x) (ξ x)"

lemma transE[simp]: "transE ξ x = proj (tpOfV x) (ξ x)"
unfolding transE_def by simp

lemma wtE_transE[simp]: "I.wtE ξ  Ik.wtE (transE ξ)"
unfolding Ik.wtE_def I.wtE_def transE_def by auto

abbreviation "Ik_intT  intT"
abbreviation "Ik_intF  intF"
abbreviation "Ik_intP  intP"

lemma Ik_intT_int:
assumes wt: "Ik.wt T" and ξ: "I.wtE ξ"
and snv: " σ. infTp σ  ( x  nvT T. tpOfV x  σ)"
shows "Ik_intT (tpOf T) (I.int ξ T)"
proof(cases " x. T = Var x")
  case True then obtain x where T: "T = Var x" by auto
  show ?thesis proof(cases "infTp (tpOf T)")
    case True thus ?thesis using T using wtE_transE[OF ξ]
    by (metis I.wt_int I_intT_def ξ wt)
  next
    case False hence " x  nvT T. tpOfV x  tpOf T" using snv by auto
    hence "Ik.full (tpOf T)" using T by (cases T, simp_all)
    thus ?thesis unfolding Ik.full_def by simp
  qed
next
  case False hence nonVar: "¬ ( x. T = Var x)" by (cases T, auto)
  thus ?thesis using nonVar wt apply(induct T, force)
  unfolding I_intF_def tpOf.simps int.simps
  apply(rule Ik.intF, simp) apply(rule listAll2_map2I) by auto
qed

lemma int_transE_proj:
  assumes wt: "Ik.wt T"
  shows "Ik.int (transE ξ) T = proj (tpOf T) (I.int ξ T)"
  using wt proof (induct T)
  case (Fn f Tl)
  have 0: "Ik_intT (resOf f) (I_intF f (map (int ξ) Tl))" (is "Ik_intT  ?a")
    unfolding I_intF_def apply(rule Ik.intF)
    using Fn unfolding list_all2_length list_all_iff by auto
  have 1: "proj  ?a = ?a" using proj_id[OF 0] .
  show ?case
    using [[unfold_abs_def = false]]
    unfolding Ik.int.simps int.simps tpOf.simps 1
    unfolding I_intF_def apply(rule arg_cong[of _ _ "intF f"])
  proof (rule nth_equalityI)
    have l[simp]: "length (arOf f) = length Tl" using Fn by simp
    fix i assume "i < length (map (Ik.int (transE ξ)) Tl)"
    hence i[simp]: "i < length Tl" by simp
    have 0: "arOf f ! i = tpOf (Tl ! i)" using Fn by simp
    have [simp]: "Ik.int (transE ξ) (Tl ! i) = proj (arOf f ! i) (I.int ξ (Tl ! i))"
      unfolding 0 using Fn by (auto simp: list_all_length transE_def)
    show "map (Ik.int (transE ξ)) Tl ! i =
          map2 proj (arOf f) (map (I.int ξ) Tl) ! i"
      using Fn unfolding list_all_length by simp
  qed(use Fn in simp)
qed simp

lemma int_transE_snv[simp]:
assumes wt: "Ik.wt T" and ξ: "I.wtE ξ" and snv: " σ. infTp σ  ( x  nvT T. tpOfV x  σ)"
shows "Ik.int (transE ξ) T = I.int ξ T"
unfolding int_transE_proj[OF wt] apply(rule proj_id)
using Ik_intT_int[OF wt ξ snv] .

lemma int_transE_Fn:
assumes wt: "list_all wt Tl" and f: "wtFsym f" and ξ: "I.wtE ξ"
and ar: "arOf f = map tpOf Tl"
shows "Ik.int (transE ξ) (Fn f Tl) = I.int ξ (Fn f Tl)"
apply(rule int_transE_snv) using assms by auto

lemma intP_transE[simp]:
assumes wt: "list_all wt Tl" and p: "wtPsym p" and ar: "parOf p = map tpOf Tl"
shows "Ik_intP p (map (Ik.int (transE ξ)) Tl) = I_intP p (map (I.int ξ) Tl)"
unfolding I_intP_def apply(rule arg_cong[of _ _ "Ik_intP p"])
apply(rule nth_equalityI) using assms
using int_transE_proj unfolding list_all_length by auto

lemma satA_snvA_transE[simp]:
assumes wtA: "Ik.wtA at" and ξ: "I.wtE ξ"
and pA: " σ. infTp σ  ( x  nvA at. tpOfV x  σ)"
shows "Ik.satA (transE ξ) at  I.satA ξ at"
using assms apply (cases at, simp_all add: ball_Un) by (metis int_transE_snv)

(* The next contrapositive twist is crucial for proving satL_transE: *)
lemma satA_transE[simp]:
assumes wtA: "Ik.wtA at" and "I.satA ξ at"
shows "Ik.satA (transE ξ) at"
using assms apply(cases at) using int_transE_proj by auto

lemma satL_snvL_transE[simp]:
assumes wtL: "Ik.wtL l" and ξ: "I.wtE ξ"
and pL: " σ. infTp σ  ( x  nvL l. tpOfV x  σ)" and "Ik.satL (transE ξ) l"
shows "I.satL ξ l"
using assms by (cases l) auto

lemma satC_snvC_transE[simp]:
assumes wtC: "Ik.wtC c" and ξ: "I.wtE ξ"
and pC: " σ. σ  c" and "Ik.satC (transE ξ) c"
shows "I.satC ξ c"
using assms unfolding Ik.mcalc_iff Ik.satC_def satC_def Ik.wtC_def nvC_def
unfolding list_all_iff list_ex_iff apply simp by (metis nth_mem satL_snvL_transE)

lemma satPB_snvPB_transE[simp]:
assumes ξ: "I.wtE ξ"  shows "I.satPB ξ Φ"
using Ik.wt_Φ Ik.sat_Φ[OF wtE_transE[OF ξ]]
using mcalc ξ unfolding Ik.satPB_def satPB_def Ik.wtPB_def nvPB_def by auto

lemma I_SAT: "I.SAT Φ" unfolding I.SAT_def by auto

lemma InfModel: "IInfModel I_intT I_intF I_intP"
by standard (rule I_SAT)

end (* context ModelIkMcalc *)

sublocale ModelIkMcalc < inf?: InfModel where
intT = I_intT and intF = I_intF and intP = I_intP
using InfModel .

context ProblemIkMcalc begin

abbreviation "MModelIkMcalc  ModelIkMcalc wtFsym wtPsym arOf resOf parOf Φ infTp"

theorem monot: monot
unfolding monot_def proof safe
  fix intT intF intP assume "MModel intT intF intP"
  hence M: "MModelIkMcalc intT intF intP"
  unfolding ModelIkMcalc_def ModelIk_def apply safe ..
  show " intTI intFI intPI. IInfModel intTI intFI intPI"
  using ModelIkMcalc.InfModel[OF M] by auto
qed

end (* context ProblemIkMcalc *)

text‹Final theorem in sublocale form: Any problem that passes the
  monotonicity calculus is monotonic:›

sublocale ProblemIkMcalc < MonotProblem
by standard (rule monot)

end

Theory T_G_Prelim

(* Preliminaries on the tag and guard encodings  *)
theory T_G_Prelim
imports Mcalc
begin


(* Copy of ProblemIk, together with a partitioning of the types.
O stands for the original---this copy shall be used
as ``the original problem: *)

locale ProblemIkTpart =
Ik? : ProblemIk wtFsym wtPsym arOf resOf parOf Φ infTp
for wtFsym :: "'fsym  bool"
and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ and infTp +
fixes
    prot :: "'tp  bool" (* types aimed to be protected (with tags or guards) *)
and protFw :: "'tp  bool" (* types aimed to be protected in a featherweight fashion  *)
assumes
    tp_disj: " σ. ¬ prot σ  ¬ protFw σ"
and tp_mcalc: " σ. prot σ  protFw σ  ( c  Φ. σ  c)"
begin

(* The notion of being a result type of some operation symbol: *)
definition isRes where "isRes σ   f. wtFsym f  resOf f = σ"

(* Types meant to be left unprotected:
-- in the case of tags, terms of these type are not tagged;
-- in the case of guards, no guards are added for these types  *)
definition "unprot σ  ¬ prot σ  ¬ protFw σ"

lemma unprot_mcalc[simp]: "unprot σ; c  Φ  σ  c "
using tp_mcalc unfolding unprot_def by auto

end (* context ProblemIkTpart *)


(* Problem with type partition and model: *)
locale ModelIkTpart =
Ik? : ProblemIkTpart wtFsym wtPsym arOf resOf parOf Φ infTp prot protFw +
Ik? : Model wtFsym wtPsym arOf resOf parOf Φ 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 intT and intF and intP

end

Theory Mcalc2

section ‹The Second Monotonicity Calculus›
theory Mcalc2
imports Mono
begin



subsection‹Extension policies›

text‹Extension policy: copy, true or false extension:›

datatype epol = Cext | Text | Fext

text‹Problem with infinite knowledge and predicate-extension policy:›

locale ProblemIkPol = ProblemIk wtFsym wtPsym arOf resOf parOf Φ infTp
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ and infTp
+ fixes (* the predicate-extension policy *) pol :: "'tp  'psym  epol"
and (* guard of a variable occurring in a certain literal of a certain clause: *)
    grdOf ::
"('fsym, 'psym) cls  ('fsym, 'psym) lit  var  ('fsym, 'psym) lit"


context ProblemIkPol begin

subsection‹Naked variables›

fun nv2T where
"nv2T (Var x) = {x}"
|
"nv2T (Fn f Tl) = {}"

fun nv2L where
"nv2L (Pos (Eq T1 T2)) = nv2T T1  nv2T T2"
|
"nv2L (Neg (Eq T1 T2)) = {}"
|
"nv2L (Pos (Pr p Tl)) = {x   (set (map nv2T Tl)) . pol (tpOfV x) p = Fext}"
|
"nv2L (Neg (Pr p Tl)) = {x   (set (map nv2T Tl)) . pol (tpOfV x) p = Text}"

definition "nv2C c   (set (map nv2L c))"

lemma in_nv2T: "x  nv2T T  T = Var x"
apply(cases T)
  apply (metis equals0D nv2T.simps singleton_iff)
  by simp

lemma nv2T_vars[simp]: "x  nv2T T  x  vars T"
by (induct T, auto split: if_splits)

lemma nv2L_varsL[simp]:
assumes "x  nv2L l" shows "x  varsL l"
proof (cases l)
  case (Pos at)
  show ?thesis proof(cases at)
    case (Pr p Tl) thus ?thesis using assms unfolding Pos
    apply(cases "pol (tpOfV x) p", simp_all) by (metis nv2T_vars)
  qed(insert assms, unfold Pos, auto)
next
  case (Neg at)
  show ?thesis proof(cases at)
    case (Pr p Tl) thus ?thesis using assms unfolding Neg
    apply(cases "pol (tpOfV x) p", simp_all) by (metis nv2T_vars)
  qed(insert assms, unfold Neg, auto)
qed

lemma nv2C_varsC[simp]: "x  nv2C c  x  varsC c"
unfolding varsC_def nv2C_def by (induct c, auto)

subsection‹The calculus›

text‹The notion of a literal being a guard for a (typed) variable:›

fun isGuard :: "var  ('fsym,'psym) lit  bool" where
"isGuard x (Pos (Eq T1 T2))  False"
|
"isGuard x (Neg (Eq T1 T2)) 
 (T1 = Var x  ( f Tl. T2 = Fn f Tl)) 
 (T2 = Var x  ( f Tl. T1 = Fn f Tl))"
|
"isGuard x (Pos (Pr p Tl))  x   (set (map nv2T Tl))  pol (tpOfV x) p = Text"
|
"isGuard x (Neg (Pr p Tl))  x   (set (map nv2T Tl))  pol (tpOfV x) p = Fext"


text‹The monotonicity calculus from the Classen et. al. paper, applied
to non-infinite types only: it checks that any variable in any literal of any clause
is indeed guarded by its guard:›

inductive mcalc2 (infix "⊢2" 40) where
 [simp]: "infTp σ  σ ⊢2 c"
|[simp]: "( l x. l  set c; x  nv2L l; tpOfV x = σ
          isGuard x (grdOf c l x))  σ ⊢2 c"

lemma mcalc2_iff:
"σ ⊢2 c 
 infTp σ  ( l x. l  set c  x  nv2L l  tpOfV x = σ  isGuard x (grdOf c l x))"
unfolding mcalc2.simps by auto

end (* context ProblemIk *)

locale ProblemIkPolMcalc2 = ProblemIkPol wtFsym wtPsym arOf resOf parOf Φ infTp pol grdOf
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ and infTp and pol and grdOf
+ assumes
(* well-definednedd of the guard: *)
    grdOf: " c l x. c  Φ; l  set c; x  nv2L l; ¬ infTp (tpOfV x)
                      grdOf c l x  set c"
and mcalc2: " σ c. c  Φ  σ ⊢2 c"
begin
lemma wtL_grdOf[simp]:
assumes "c  Φ" and "l  set c" and "x  nv2L l" and "¬ infTp (tpOfV x)"
shows "wtL (grdOf c l x)"
using grdOf[OF assms] by (metis assms list_all_iff wtC_def wtPB_def wt_Φ)
end

locale ModelIkPolMcalc2 =
ModelIk wtFsym wtPsym arOf resOf parOf Φ infTp intT intF intP +
ProblemIkPolMcalc2 wtFsym wtPsym arOf resOf parOf Φ infTp pol grdOf
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ and infTp pol and grdOf and intT and intF and intP


end

Theory Mcalc2C

(* A particular case of the second calculus, with policy constant on types: *)
theory Mcalc2C
imports Mcalc2
begin

subsection‹Constant policy on types›

text‹Currently our soundness proof only covers the case of the calculus
having different extension policies for different predicates, but not
for differnt types versus the same predicate. This is sufficient for our purpose
of proving soundness of the guard encodings.›

locale ProblemIkPolMcalc2C =
ProblemIkPolMcalc2 wtFsym wtPsym arOf resOf parOf Φ infTp pol grdOf
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ and infTp and pol and grdOf
+ assumes pol_ct: "pol σ1 P = pol σ2 P"

context ProblemIkPolMcalc2C begin

definition "polC  pol any"

lemma pol_polC: "pol σ P = polC P"
unfolding polC_def using pol_ct by auto

lemma nv2L_simps[simp]:
"nv2L (Pos (Pr p Tl)) = (case polC p of Fext   (set (map nv2T Tl)) |_  {})"
"nv2L (Neg (Pr p Tl)) = (case polC p of Text   (set (map nv2T Tl)) |_  {})"
by (auto split: epol.splits simp: pol_polC)

declare nv2L.simps(3,4)[simp del]

lemma isGuard_simps[simp]:
"isGuard x (Pos (Pr p Tl))  x   (set (map nv2T Tl))  polC p = Text"
"isGuard x (Neg (Pr p Tl))  x   (set (map nv2T Tl))  polC p = Fext"
by (auto simp: pol_polC)

declare isGuard.simps(3,4)[simp del]


end (* context  ProblemIkPolMcalc2 *)


locale ModelIkPolMcalc2C =
ModelIk wtFsym wtPsym arOf resOf parOf Φ infTp intT intF intP +
ProblemIkPolMcalc2C wtFsym wtPsym arOf resOf parOf Φ infTp pol grdOf
for wtFsym :: "'fsym  bool" and wtPsym :: "'psym  bool"
and arOf :: "'fsym  'tp list"
and resOf and parOf and Φ and infTp pol and grdOf and intT and intF and intP


subsection‹Extension of a structure to an infinte structure
by adding indistinguishable elements›

context ModelIkPolMcalc2C begin

(* The projection from univ to a structure: *)
definition proj where "proj σ a  if intT σ a then a else pickT σ"

lemma intT_proj[simp]: "intT σ (proj σ a)"
unfolding proj_def using pickT by auto

lemma proj_id[simp]: "intT σ a  proj σ a = a"
unfolding proj_def by auto

lemma map_proj_id[simp]:
assumes "list_all2 intT σl al"
shows "map2 proj σl al = al"
apply(rule nth_equalityI)
using assms unfolding list_all2_length by auto

lemma surj_proj:
assumes "intT σ a"   shows " b. proj σ b = a"
using assms by (intro exI[of _ a]) simp

definition "I_intT σ (a::univ)  infTp σ  intT σ a"
definition "I_intF f al  intF f (map2 proj (arOf f) al)"
definition
"I_intP p al 
 case polC p of
   Cext  intP p (map2 proj (parOf p) al)
  |Text  if list_all2 intT (parOf p) al then intP p al else True
  |Fext  if list_all2 intT (parOf p) al then intP p al else False"

lemma not_infTp_I_intT[simp]: "¬ infTp σ  I_intT σ a"
unfolding I_intT_def by simp

lemma infTp_I_intT[simp]: "infTp σ  I_intT σ a = intT σ a"
unfolding I_intT_def by simp

lemma NE_I_intT: "NE (I_intT σ)"
using NE_intT by (cases "infTp σ", auto)

lemma I_intP_Cext[simp]:
"polC p = Cext  I_intP p al = intP p (map2 proj (parOf p) al)"
unfolding I_intP_def by simp

lemma I_intP_Text_imp[simp]:
assumes "polC p = Text" and "intP p al"
shows "I_intP p al"
using assms unfolding I_intP_def by auto

lemma I_intP_Fext_imp[simp]:
assumes "polC p = Fext" and "¬ intP p al"
shows "¬ I_intP p al"
using assms unfolding I_intP_def by (cases "list_all2 intT (parOf p) al", auto)

lemma I_intP_intT[simp]:
assumes "list_all2 intT (parOf p) al"
shows "I_intP p al = intP p al"
using assms unfolding I_intP_def by (cases "polC p") auto

lemma I_intP_Text_not_intT[simp]:
assumes "polC p = Text" and "¬ list_all2 intT (parOf p) al"
shows "I_intP p al"
using assms unfolding I_intP_def by auto

lemma I_intP_Fext_not_intT[simp]:
assumes "polC p = Fext" and "¬ list_all2 intT (parOf p) al"
shows "¬ I_intP p al"
using assms unfolding I_intP_def by auto

lemma I_intF:
assumes f: "wtFsym f" and al: "list_all2 I_intT (arOf f) al"
shows "I_intT (resOf f) (I_intF f al)"
unfolding I_intT_def I_intF_def apply safe apply(rule intF[OF f])
using al unfolding list_all2_length by auto

lemma Tstruct_I_intT: "Tstruct I_intT"
by standard (rule NE_I_intT)

lemma inf_I_intT: "infinite {a. I_intT σ a}"
by (cases "infTp σ", auto)

lemma InfStruct: "IInfStruct I_intT I_intF I_intP"
apply standard using NE_I_intT I_intF Tstruct_I_intT inf_I_intT by auto

end (* context ModelIkPolMcalc2C *)

sublocale ModelIkPolMcalc2C < InfStruct where
intT = I_intT and intF = I_intF and intP = I_intP
using InfStruct .

subsection‹The soundness of the calculus›

(* In what follows, ``Ik" stands for the original
(augmented with infiniteness-knowledge)
and ``I" for the infinite structure constructed from it
through the above sublocale statement. *)

context ModelIkPolMcalc2C begin
(* The environment translation along the projection: *)
definition "transE ξ  λ x. proj (tpOfV x) (ξ x)"

lemma transE[simp]: "transE ξ x = proj (tpOfV x) (ξ x)"
unfolding transE_def by simp

lemma wtE_transE[simp]: "I.wtE ξ  Ik.wtE (transE ξ)"
unfolding Ik.wtE_def I.wtE_def transE_def by auto

abbreviation "Ik_intT  intT"
abbreviation "Ik_intF  intF"
abbreviation "Ik_intP  intP"

lemma Ik_intT_int:
assumes wt: "Ik.wt T" and ξ: "I.wtE ξ"
and nv2T: "infTp (Ik.tpOf T)  ( x  nv2T T. tpOfV x  Ik.tpOf T)"
shows "Ik_intT (Ik.tpOf T) (I.int ξ T)"
proof(cases " x. T = Var x")
  case True then obtain x where T: "T = Var x" by auto
  show ?thesis proof(cases "infTp (tpOf T)")
    case True thus ?thesis using T using wtE_transE[OF ξ]
    by (metis I.wt_int I_intT_def ξ wt)
  next
    case False hence " x  nv2T T. tpOfV x  tpOf T" using nv2T by auto
    hence "Ik.full (tpOf T)" using T by (cases T, simp_all)
    thus ?thesis unfolding Ik.full_def by simp
  qed
next
  case False hence nonVar: "¬ ( x. T = Var x)" by (cases T, auto)
  thus ?thesis using nonVar wt apply(induct T, force)
  unfolding I_intF_def tpOf.simps int.simps
  apply(rule Ik.intF, simp) apply(rule listAll2_map2I) by auto
qed

lemma int_transE_proj:
  assumes wt: "Ik.wt T"
  shows "Ik.int (transE ξ) T = proj (tpOf T) (I.int ξ T)"
  using wt proof (induct T)
  case (Fn f Tl)
  have 0: "Ik_intT (resOf f) (I_intF f (map (int ξ) Tl))" (is "Ik_intT  ?a")
    unfolding I_intF_def apply(rule Ik.intF)
    using Fn unfolding list_all2_length list_all_iff by auto
  have 1: "proj  ?a = ?a" using proj_id[OF 0] .
  show ?case
    using [[unfold_abs_def = false]]
    unfolding Ik.int.simps int.simps tpOf.simps 1
    unfolding I_intF_def apply(rule arg_cong[of _ _ "intF f"])
  proof (rule nth_equalityI)
    have l[simp]: "length (arOf f) = length Tl" using Fn by simp
    fix i assume "i < length (map (Ik.int (transE ξ)) Tl)"
    hence i[simp]: "i < length Tl" by simp
    have 0: "arOf f ! i = tpOf (Tl ! i)" using Fn by simp
    have [simp]: "Ik.int (transE ξ) (Tl ! i) = proj (arOf f ! i) (I.int ξ (Tl ! i))"
      unfolding 0 using Fn by (auto simp: list_all_length transE_def)
    show "map (Ik.int (transE ξ)) Tl ! i =
          map2 proj (arOf f) (map (I.int ξ) Tl) ! i"
      using Fn unfolding list_all_length by simp
  qed(insert Fn, simp)
qed simp

lemma int_transE_nv2T:
assumes wt: "Ik.wt T" and ξ: "I.wtE ξ"
and nv2T: "infTp (Ik.tpOf T)  ( x  nv2T T. tpOfV x  Ik.tpOf T)"
shows "Ik.int (transE ξ) T = I.int ξ T"
unfolding int_transE_proj[OF wt] apply(rule proj_id)
using Ik_intT_int[OF wt ξ nv2T] .

lemma isGuard_not_satL_intT:
assumes wtL: "Ik.wtL l"
and (* crucial hypothesis--the essence of guarding:*) ns: "¬ I.satL ξ l"
and g: "isGuard x l" and ξ: "I.wtE ξ"
shows "Ik_intT (tpOfV x) (ξ x)" (is "Ik_intT  (ξ x)")
(* "proj σ (ξ σ x) = ξ σ x" *)
(* "Ik.int (transE ξ) (Var σ x) = I.int ξ (Var σ x)" *)
proof(cases l)
  case (Pos at)  show ?thesis proof(cases at)
    case (Pr p Tl)
    then obtain T where Tin: "T  set Tl" and x: "x  nv2T T" and pol: "polC p = Text"
    using g unfolding Pos Pr by auto
    hence T: "T = Var x" by (simp add: in_nv2T)
    obtain i where i: "i < length Tl" and Ti: "T = Tl!i" using Tin
    by (metis in_set_conv_nth)
    hence 0 : "wt T" "parOf p ! i = " using wtL unfolding Pos Pr T
    apply (simp_all add: list_all_iff) by (metis T x in_nv2T tpOf.simps)
    have "list_all2 Ik_intT (parOf p) (map (I.int ξ) Tl)" (is ?phi)
    using ns unfolding Pos Pr using pol by (cases ?phi, auto)
    hence "Ik_intT  (I.int ξ T)"
    using ns 0 i Ti unfolding Pos Pr by (auto simp add: list_all2_length nth_map)
    thus ?thesis unfolding T by simp
  qed(insert g, unfold Pos, simp)
next
  case (Neg at)  show ?thesis proof(cases at)
    case (Eq T1 T2)
    hence 0: "T1 = Var x  T2 = Var x" using g unfolding Neg by auto
    hence wt1: "Ik.wt T1" "Ik.tpOf T1 = tpOfV x"
    and wt2: "Ik.wt T2" "Ik.tpOf T2 = tpOfV x"
    using wtL unfolding Neg Eq by auto
    have eq: "I.int ξ T1 = I.int ξ T2" using ns unfolding Neg Eq by simp
    show ?thesis proof(cases "T1 = Var x")
      case True note T1 = True obtain f Tl where "T2 = Fn f Tl"
      using g T1 Eq unfolding Neg by auto
      hence " σ. infTp σ  ( x  nv2T T2. tpOfV x  σ)" by auto
      hence 1: "I.int ξ T2 = Ik.int (transE ξ) T2" using int_transE_nv2T wt2 ξ by auto
      have "Ik_intT  (I.int ξ T1)" unfolding eq 1 using wt2 ξ Ik.wt_int by force
      thus ?thesis unfolding T1 by simp
    next
      case False then obtain f Tl where T2: "T2 = Var x" and "T1 = Fn f Tl"
      using Eq Neg g by auto
      hence " σ. infTp σ  ( x  nv2T T1. tpOfV x  σ)" by simp
      hence 1: "I.int ξ T1 = Ik.int (transE ξ) T1" using int_transE_nv2T wt1 ξ by auto
      have "Ik_intT  (I.int ξ T2)" unfolding eq[symmetric] 1
      using wt1 ξ Ik.wt_int by force
      thus ?thesis unfolding T2 by simp
    qed
  next
    case (Pr p Tl)
    then obtain T where Tin: "T  set Tl" and x: "x  nv2T T" and pol: "polC p = Fext"
    using g unfolding Neg Pr by auto
    hence T: "T = Var x" by (simp add: in_nv2T)
    obtain i where i: "i < length Tl" and Ti: "T = Tl!i" using Tin
    by (metis in_set_conv_nth)
    hence 0 : "wt T" "parOf p ! i = " using wtL unfolding Neg Pr T
    apply (simp_all add: list_all_iff) by (metis T x in_nv2T tpOf.simps)
    have "list_all2 Ik_intT (parOf p) (map (I.int ξ) Tl)" (is ?phi)
    using ns unfolding Neg Pr using pol by (cases ?phi, auto)
    hence "Ik_intT  (I.int ξ T)"
    using ns 0 i Ti unfolding Neg Pr by (auto simp add: list_all2_length nth_map)
    thus ?thesis unfolding T by simp
  qed
qed

lemma int_transE[simp]:
assumes wt: "Ik.wt T" and ξ: "I.wtE ξ" and
nv2T: " x. ¬ infTp (tpOfV x); x  nv2T T 
            l. Ik.wtL l  ¬ I.satL ξ l  isGuard x l"
shows "Ik.int (transE ξ) T = I.int ξ T"
proof(cases "infTp (Ik.tpOf T)  ( x  nv2T T. tpOfV x  Ik.tpOf T)")
  case True
  thus ?thesis using int_transE_nv2T[OF wt ξ] by auto
next
  define σ where "σ = Ik.tpOf T"
  case False then obtain x where i: "¬ infTp σ" and x: "x  nv2T T"
  unfolding σ_def by auto
  hence T: "T = Var x" by (simp add: in_nv2T)
  hence σ: "σ = tpOfV x" unfolding σ_def by simp
  obtain l where 0: "Ik.wtL l" "¬ I.satL ξ l" "isGuard x l"
  using nv2T[OF i[unfolded σ] x] by auto
  show ?thesis unfolding T using isGuard_not_satL_intT[OF 0 ξ] by simp
qed

lemma intT_int_transE[simp]:
assumes wt: "Ik.wt T" and ξ: "I.wtE ξ" and
nv2T: " x. ¬ infTp (tpOfV x); x  nv2T T 
            l. Ik.wtL l  ¬ I.satL ξ l  isGuard x l"
shows "Ik_intT (Ik.tpOf T) (I.int ξ T)"
proof-
  have 0: "I.int ξ T = Ik.int (transE ξ) T" using int_transE[OF assms] by simp
  show ?thesis unfolding 0 using Ik.wt_int[OF wtE_transE[OF ξ] wt] .
qed

lemma map_int_transE_nv2T[simp]:
assumes wt: "list_all Ik.wt Tl" and ξ: "I.wtE ξ" and
nv2T: " x. ¬ infTp (tpOfV x); Tset Tl. x  nv2T T 
            l. Ik.wtL l  ¬ I.satL ξ l  isGuard x l"
shows "map (Ik.int (transE ξ)) Tl = map (I.int ξ) Tl"
apply(rule nth_equalityI) using assms by (force simp: list_all_iff intro: int_transE)+

lemma list_all2_intT_int_transE_nv2T[simp]:
assumes wt: "list_all Ik.wt Tl" and ξ: "I.wtE ξ" and
nv2T: " x. ¬ infTp (tpOfV x); Tset Tl. x  nv2T T 
            l. Ik.wtL l  ¬ I.satL ξ l  isGuard x l"
shows "list_all2 Ik_intT (map Ik.tpOf Tl) (map (I.int ξ) Tl)"
unfolding list_all2_length using assms
unfolding list_all_iff apply simp_all by (metis intT_int_transE nth_mem)

lemma map_proj_transE[simp]:
assumes wt: "list_all wt Tl"
shows "map (Ik.int (transE ξ)) Tl =
       map2 proj (map tpOf Tl) (map (I.int ξ) Tl)"
apply(rule nth_equalityI) using assms
using int_transE_proj unfolding list_all_length by auto

lemma satL_transE[simp]:
assumes wtL: "Ik.wtL l" and ξ: "I.wtE ξ" and
nv2T:  " x. ¬ infTp (tpOfV x); x  nv2L l 
              l'. Ik.wtL l'  ¬ I.satL ξ l'  isGuard x l'"
and "Ik.satL (transE ξ) l"
shows "I.satL ξ l"
proof(cases l)
  case (Pos at) show ?thesis proof (cases at)
    case (Pr p Tl) show ?thesis using assms unfolding Pos Pr
    apply(cases "polC p")
      apply force
      apply(cases "list_all2 intT (map Ik.tpOf Tl) (map (I.int ξ) Tl)", force, force)
      by simp
  qed(insert assms, unfold Pos, simp)
next
  case (Neg at) show ?thesis proof (cases at)
    case (Pr p Tl) show ?thesis using assms unfolding Neg Pr
    apply(cases "polC p")
      apply force apply force
      by (cases "list_all2 intT (map Ik.tpOf Tl) (map (I.int ξ) Tl)", force, force)
  qed(insert assms int_transE_proj, unfold Neg, auto)
qed

lemma satPB_transE[simp]:
assumes ξ: "I.wtE ξ"  shows "I.satPB ξ Φ"
unfolding I.satPB_def proof safe
  fix c assume cin: "c  Φ"  let ?thesis = "I.satC ξ c"
  have mc: " σ. σ ⊢2 c" using mcalc2[OF cin] .
  have c: "Ik.satC (transE ξ) c"
  using sat_Φ wtE_transE[OF ξ] cin unfolding Ik.satPB_def by auto
  have wtC: "Ik.wtC c" using wt_Φ cin unfolding wtPB_def by auto
  obtain l where lin: "l  set c" and l: "Ik.satL (transE ξ) l"
  using c unfolding Ik.satC_iff_set by auto
  have wtL: "Ik.wtL l" using wtC unfolding wtC_def
  by (metis (lifting) lin list_all_iff)
  {assume "¬ ?thesis"
   hence 0: " l'. l'  set c  ¬ I.satL ξ l'" unfolding I.satC_iff_set by auto
   have "I.satL ξ l"
   proof (rule satL_transE[OF wtL ξ _ l])
     fix x let  = "tpOfV x"
     assume σ: "¬ infTp " and x: "x  nv2L l"
     hence g: "isGuard x (grdOf c l x)" using mc[of ] lin unfolding mcalc2_iff by simp
     show " l'. Ik.wtL l'  ¬ I.satL ξ l'  isGuard x l'"
     apply(rule exI[of _ "grdOf c l x"]) apply safe
     using g σ cin lin wtL_grdOf x 0 grdOf x by auto
   qed
   hence False using 0 lin by auto
   hence ?thesis by simp
  }
  thus ?thesis by auto
qed

lemma I_SAT: "I.SAT Φ"
unfolding I.SAT_def by simp

lemma InfModel: "IInfModel I_intT I_intF I_intP"
  by standard (rule I_SAT)

end (* context ModelIkPolMcalc2C *)

sublocale ModelIkPolMcalc2C < inf?: InfModel where
intT = I_intT and intF = I_intF and intP = I_intP
using InfModel .

context ProblemIkPolMcalc2C begin

abbreviation
"MModelIkPolMcalc2C  ModelIkPolMcalc2C wtFsym wtPsym arOf resOf parOf Φ infTp pol grdOf"

theorem monot: monot
unfolding monot_def proof safe
  fix intT intF intP assume "MModel intT intF intP"
  hence M: "MModelIkPolMcalc2C intT intF intP"
  unfolding ModelIkPolMcalc2C_def ModelIk_def apply safe ..
  show " intTI intFI intPI. IInfModel intTI intFI intPI"
  using ModelIkPolMcalc2C.InfModel[OF M] by auto
qed

end (* context ProblemIkPolMcalc2 *)

text‹Final theorem in sublocale form: Any problem that passes the
  monotonicity calculus is monotonic:›
sublocale ProblemIkPolMcalc2C < MonotProblem
by standard (rule monot)

end

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 (hide_lams, 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

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 (hide_lams, 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

Theory U

section‹Untyped (Unsorted) First-Order Logic›
theory U
imports TermsAndClauses
begin

text‹Even though untyped FOL is a particular case of many-typed FOL, we find 
it convenient to represent it separately.›

subsection ‹Signatures›

locale Signature =
fixes
    wtFsym :: "'fsym  bool"
and wtPsym :: "'psym  bool"
and arOf :: "'fsym  nat"
and parOf :: "'psym  nat"
assumes countable_wtFsym: "countable {f::'fsym. wtFsym f}"
and countable_wtPsym: "countable {p::'psym. wtPsym p}"
begin

(* Well-typed terms *)
fun wt where
"wt (Var x)  True"
|
"wt (Fn f Tl)  wtFsym f  list_all wt Tl  arOf f = length Tl"

lemma wt_induct[elim, consumes 1, case_names Var Fn, induct pred: wt]:
assumes T: "wt T"
and Var: " x. φ (Var x)"
and Fn:
" f Tl.
   wtFsym f; list_all wt Tl; arOf f = length Tl; list_all φ Tl
  φ (Fn f Tl)"
shows "φ T"
proof-
  have "wt T  φ T"
  apply (induct T) using Var Fn by (auto simp: list_all_iff)
  thus ?thesis using T by auto
qed

(* Well-typed substitutions *)
definition "wtSB π   x. wt (π x)"

lemma wtSB_wt[simp]: "wtSB π  wt (π x)"
unfolding wtSB_def by auto

lemma wt_subst[simp]:
assumes "wtSB π" and "wt T"
shows "wt (subst π T)"
using assms by (induct T) (auto simp: list_all_length)


lemma wtSB_o:
assumes 1: "wtSB π1" and 2: "wtSB π2"
shows "wtSB (subst π1 o π2)"
using 2 unfolding wtSB_def using 1 by auto


end (* context Signature *)


subsection ‹Structures›

(* Environment *)
type_synonym 'univ env = "var  'univ"

(* Structure *)
locale Struct = Signature wtFsym wtPsym arOf parOf
for wtFsym and wtPsym
and arOf :: "'fsym  nat"
and parOf :: "'psym  nat"
+
fixes
    D :: "'univ  bool"
and intF :: "'fsym  'univ list  'univ"
and intP :: "'psym  'univ list  bool"
assumes
NE_D: "NE D" and
intF: "wtFsym f; length al = arOf f; list_all D al  D (intF f al)"
and
dummy: "parOf = parOf  intF = intF  intP = intP"
begin

(* Well-typed environment *)
definition "wtE ξ   x. D (ξ x)"

lemma wtTE_D[simp]: "wtE ξ  D (ξ x)"
unfolding wtE_def by simp

(* Interpretation of terms: *)
fun int where
"int ξ (Var x) = ξ x"
|
"int ξ (Fn f Tl) = intF f (map (int ξ) Tl)"

(* Soundness of typing w.r.t. interpretation: *)
lemma wt_int:
assumes wtE: "wtE ξ" and wt_T: "wt T"
shows "D (int ξ T)"
using wt_T apply(induct T)
apply (metis int.simps(1) wtE wtE_def)
unfolding int.simps apply(rule intF)
unfolding list_all_map comp_def by auto

lemma int_cong:
assumes "x. x  vars T  ξ1 x = ξ2 x"
shows "int ξ1 T = int ξ2 T"
using assms apply(induct T) apply simp_all unfolding list_all_iff
using map_ext by metis

lemma int_o:
"int (int ξ o ρ) T = int ξ (subst ρ T)"
apply(induct T) apply simp_all  unfolding list_all_iff o_def 
using map_ext by (metis (lifting, no_types))

lemmas int_subst = int_o[symmetric]

lemma int_o_subst:
"int ξ o subst ρ = int (int ξ o ρ)"
apply(rule ext) apply(subst comp_def) unfolding int_o[symmetric] ..

lemma wtE_o:
assumes 1: "wtE ξ" and 2: "wtSB ρ"
shows "wtE (int ξ o ρ)"
unfolding wtE_def apply safe
unfolding comp_def apply(rule wt_int[OF 1]) using 2 by auto

end


context Signature begin

text‹Well-typed (i.e., well-formed) atoms, literals, caluses and problems:›

fun wtA where
"wtA (Eq T1 T2)  wt T1  wt T2"
|
"wtA (Pr p Tl)  wtPsym p  list_all wt Tl  parOf p = length Tl"

fun wtL where
"wtL (Pos a)  wtA a"
|
"wtL (Neg a)  wtA a"

definition "wtC  list_all wtL"

definition "wtPB Φ