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); ∃T∈set 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); ∃T∈set 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