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