Theory Syntactic_Description

theory Syntactic_Description
imports Place_Framework Proper_Venn_Regions "HereditarilyFinite.Rank"
begin

locale satisfiable_normalized_MLSS_clause = ATOM I⇩s⇩a +
  normalized_MLSS_clause 𝒞 +
  proper_Venn_regions V 𝒜
  for 𝒞 :: "'a pset_fm set" and 𝒜 :: "'a ⇒ hf" +
  assumes 𝒜_sat_𝒞: "∀lt ∈ 𝒞. I 𝒜 lt"
begin

―‹The collection of the non-empty proper regions of the Venn diagram of V under 𝒜›

definition Σ :: "hf set" where
  "Σ ≡ proper_Venn_regions.proper_Venn_region V 𝒜 ` (P⇧+ V) - {0}"
declare Σ_def [simp]

lemma mem_Σ_not_empty: "σ ∈ Σ ⟹ σ ≠ 0" by simp

fun associated_place :: "hf ⇒ ('a ⇒ bool)"  (‹π⇘_⇙›) where
  "π⇘σ⇙ x ⟷ x ∈ V ∧ σ ≤ 𝒜 x"

definition PI :: "('a ⇒ bool) set" where
  "PI ≡ associated_place ` Σ"
declare PI_def [simp]

fun containing_region :: "'a ⇒ hf" (‹σ⇘_⇙›) where
  "σ⇘x⇙ = HF {𝒜 x}"

lemma containing_region_in_Σ:
  assumes "x ∈ W"
    shows "σ⇘x⇙ ∈ Σ"
proof -
  from ‹x ∈ W› obtain y where y: "AT (Var y =⇩s Single (Var x)) ∈ 𝒞"
    using memW_E by blast
  then have "y ∈ V" by fastforce

  from y 𝒜_sat_𝒞 have "𝒜 y = HF {𝒜 x}" by auto
  then have "𝒜 y = σ⇘x⇙" by simp
  moreover
  from variable_as_composition_of_proper_Venn_regions ‹y ∈ V› have "𝒜 y = ⨆HF (proper_Venn_region ` ℒ V y)"
    by presburger
  ultimately
  have "σ⇘x⇙ = ⨆HF (proper_Venn_region ` ℒ V y)" by argo
  then have "∃α ∈ P⇧+ V. 𝒜 y = proper_Venn_region α"
  proof -
    let ?l = "{α ∈ ℒ V y. proper_Venn_region α ≠ 0}"

    have "?l ≠ {}"
    proof (rule ccontr)
      assume "¬ ?l ≠ {}"
      then have "⨆HF (proper_Venn_region ` ℒ V y) = 0"
        using HUnion_empty[where ?f = proper_Venn_region and ?S = "ℒ V y"]
        by blast
      with ‹𝒜 y = HF {𝒜 x}› ‹𝒜 y = ⨆HF (proper_Venn_region ` ℒ V y)› show False
        by (metis Int_lower1 equals0I finite_Int finite_V finite_imageI finite_insert hemptyE hmem_HF_iff insert_not_empty subset_empty) 
    qed
    then obtain α where "α ∈ ?l" by blast
    moreover
    have "β = α" if "β ∈ ?l" for β
    proof (rule ccontr)
      assume "β ≠ α"

      from ‹α ∈ ?l› ‹y ∈ V›
      have "proper_Venn_region α ≤ 𝒜 y"
        by (metis (mono_tags, lifting) ℒ.elims mem_Collect_eq mem_P_plus_subset proper_Venn_region_subset_variable_iff)
      with ‹α ∈ ?l› have "proper_Venn_region α = 𝒜 y"
        using ‹𝒜 y = HF {𝒜 x}›
        using singleton_nonempty_subset[where ?s = "𝒜 y" and ?c = "𝒜 x" and ?t = "proper_Venn_region α"]
        by fastforce

      from ‹β ∈ ?l› ‹y ∈ V›
      have "proper_Venn_region β ≤ 𝒜 y"
        by (metis (mono_tags, lifting) ℒ.elims mem_Collect_eq mem_P_plus_subset proper_Venn_region_subset_variable_iff)
      with ‹β ∈ ?l› have "proper_Venn_region β = 𝒜 y"
        using ‹𝒜 y = HF {𝒜 x}›
        using singleton_nonempty_subset[where ?s = "𝒜 y" and ?c = "𝒜 x" and ?t = "proper_Venn_region β"]
        by fastforce

      from ‹β ≠ α› ‹proper_Venn_region α = 𝒜 y› ‹proper_Venn_region β = 𝒜 y› ‹𝒜 y = HF {𝒜 x}› ‹x ∈ W›
      show False using proper_Venn_region_strongly_injective[where ?α = α and ?β = β]
        using calculation that by auto
    qed
    ultimately
    have "?l = {α}" by blast

    have Ly_minus_l: "ℒ V y - ?l = {α ∈ ℒ V y. proper_Venn_region α = 0}" by auto

    have "?l ⊆ ℒ V y" by blast
    then have "?l ∪ (ℒ V y - ?l) = ℒ V y" by blast
    then have "⨆HF (proper_Venn_region ` ℒ V y) = ⨆HF (proper_Venn_region ` (?l ∪ (ℒ V y - ?l)))" by argo
    also have "... = ⨆HF (proper_Venn_region ` (?l ∪ {α ∈ ℒ V y. proper_Venn_region α = 0}))"
      using Ly_minus_l by argo
    also have "... = ⨆HF (proper_Venn_region ` ?l) ⊔ ⨆HF (proper_Venn_region ` {α ∈ ℒ V y. proper_Venn_region α = 0})"
      using HUnion_proper_Venn_region_union[where ?l = ?l and ?m = "{α ∈ ℒ V y. proper_Venn_region α = 0}"]
      using finite_V ‹y ∈ V›
      by auto
    also have "... = ⨆HF (proper_Venn_region ` ?l)"
      using finite_V ‹y ∈ V› by auto
    also have "... = ⨆HF (proper_Venn_region ` {α})"
      using ‹?l = {α}› by argo
    also have "... = proper_Venn_region α" by fastforce
    finally have "⨆HF (proper_Venn_region ` ℒ V y) = proper_Venn_region α" .

    with ‹𝒜 y = ⨆HF (proper_Venn_region ` (ℒ V y))› ‹α ∈ ?l› show ?thesis by auto
  qed
  moreover
  from ‹𝒜 y = HF {𝒜 x}› ‹𝒜 y = σ⇘x⇙› have "σ⇘x⇙ ≠ 0"
    by (metis finite.emptyI finite_insert hfset_0 hfset_HF insert_not_empty)
  ultimately
  show ?thesis
    by (metis Diff_iff Σ_def ‹𝒜 y = σ⇘x⇙› empty_iff imageI insert_iff)
qed

fun at⇩p_f :: "'a ⇒ ('a ⇒ bool)" where
  "at⇩p_f w = π⇘σ⇘w⇙⇙"

lemma range_at⇩p_f: "w ∈ W ⟹ at⇩p_f w ∈ PI"
  using at⇩p_f.simps containing_region_in_Σ PI_def by blast

lemma π_σ_α:
  assumes "π ∈ PI"
    shows "∃α ∈ P⇧+ V. π = (λx. x ∈ α) ∧ π = π⇘proper_Venn_region α⇙ ∧ proper_Venn_region α ≠ 0"
proof -
  from ‹π ∈ PI› obtain α where α:
    "π = π⇘proper_Venn_region α⇙" "proper_Venn_region α ≠ 0" "α ∈ P⇧+ V"
    by auto
  have "π x ⟷ x ∈ α" for x
  proof (cases "x ∈ V")
    case True
    with α proper_Venn_region_subset_variable_iff
    have "x ∈ α ⟷ proper_Venn_region α ≤ 𝒜 x" by simp
    with ‹π = π⇘proper_Venn_region α⇙› True
    show ?thesis by simp
  next
    case False
    with ‹π = π⇘(proper_Venn_region α)⇙› have "¬ π x" by auto
    from False ‹α ∈ P⇧+ V› have "x ∉ α" by auto
    from ‹¬ π x› ‹x ∉ α› show ?thesis by blast
  qed
  with α show ?thesis by blast
qed

lemma π_σ_α':
  assumes "σ ∈ Σ"
  shows "∃α ∈ P⇧+ V. π⇘σ⇙ = (λx. x ∈ α) ∧ σ = proper_Venn_region α"
proof -
  from ‹σ ∈ Σ› obtain α where α: "α ∈ P⇧+ V" "σ = proper_Venn_region α" "proper_Venn_region α ≠ 0"
    by auto
  have "π⇘σ⇙ x ⟷ x ∈ α" for x
  proof (cases "x ∈ V")
    case True
    with α proper_Venn_region_subset_variable_iff
    have "x ∈ α ⟷ proper_Venn_region α ≤ 𝒜 x" by simp
    with ‹σ = proper_Venn_region α› True
    show ?thesis by simp
  next
    case False
    with ‹σ = proper_Venn_region α› have "¬ π⇘σ⇙ x" by auto
    from False ‹α ∈ P⇧+ V› have "x ∉ α" by auto
    from ‹¬ π⇘σ⇙ x› ‹x ∉ α› show ?thesis by blast
  qed
  with α show ?thesis by blast
qed

lemma realise_same_implies_eq_under_all_π:
  assumes "x ∈ V"
      and "y ∈ V"
      and "𝒜 x = 𝒜 y"
      and "π ∈ PI"
    shows "π x ⟷ π y"
  by (metis π_σ_α assms associated_place.elims(2) associated_place.elims(3))

definition "rel_PI ≡ place_membership 𝒞 PI"
declare rel_PI_def [simp]

definition "G_PI ≡ place_mem_graph 𝒞 PI"
declare G_PI_def [simp]

lemma arcs_G_PI[simp]: "arcs G_PI = rel_PI" by simp
lemma arcs_ends_G_PI[simp]: "arcs_ends G_PI = rel_PI"
  unfolding arcs_ends_def arc_to_ends_def by auto
lemma verts_G_PI[simp]: "verts G_PI = PI" by simp

lemma rel_PI_head_tail:
  assumes "e ∈ rel_PI"
    shows "e = (tail G_PI e, head G_PI e)"
proof -
  from assms arcs_ends_G_PI have "e ∈ arcs_ends G_PI" 
    by blast
  then show ?thesis
    unfolding arcs_ends_def arc_to_ends_def
    by simp
qed

lemma place_membership_irreflexive: "(π, π) ∉ rel_PI"
proof (rule ccontr)
  assume "¬ (π, π) ∉ rel_PI"
  then have "(π, π) ∈ rel_PI" by blast
  then obtain x y where xy: "AT (Var x =⇩s Single (Var y)) ∈ 𝒞" "π x" "π y" by auto
  with 𝒜_sat_𝒞 have "𝒜 x = HF {𝒜 y}" by fastforce
  then have "𝒜 x ⊓ 𝒜 y = 0" by (simp add: hmem_not_refl)

  from ‹(π, π) ∈ rel_PI› have "π ∈ PI" by auto
  then obtain σ where σ: "π = π⇘σ⇙" "σ ∈ Σ" by auto
  then obtain α where α: "σ = proper_Venn_region α" "α ∈ P⇧+ V" by auto
  with σ xy ‹𝒜 x ⊓ 𝒜 y = 0›
  show False
    by (metis Σ_def DiffD2 associated_place.elims(2) insertCI le_inf_iff less_eq_hempty)
qed

interpretation pre_digraph G_PI .

lemma rel_PI_implies_rank_lt:
  assumes π_lt: "(π⇘σ⇙, π⇘σ'⇙) ∈ rel_PI"
      and "σ ∈ Σ"
      and "σ' ∈ Σ"
    shows "rank σ < rank σ'"
proof -
  from ‹σ' ∈ Σ› have "σ' ≠ 0" by auto

  from π_lt obtain x y where xy: "AT (Var x =⇩s Single (Var y)) ∈ 𝒞"
                         and "π⇘σ⇙ y" and "π⇘σ'⇙ x"
    by auto
  with 𝒜_sat_𝒞 have "𝒜 x = HF {𝒜 y}" by auto
  with ‹π⇘σ'⇙ x› ‹σ' ≠ 0› have "σ' = 𝒜 x"
    by (metis associated_place.simps singleton_nonempty_subset)
  then have "rank σ' = rank (𝒜 x)" by blast
  moreover
  from ‹π⇘σ⇙ y› have "σ ≤ 𝒜 y" by simp
  then have "rank σ ≤ rank (𝒜 y)"
    by (simp add: rank_mono) 
  moreover
  from ‹𝒜 x = HF {𝒜 y}› have "rank (𝒜 y) < rank (𝒜 x)"
    by (simp add: rank_lt)
  ultimately
  show ?thesis by order
qed

lemma awalk_in_G_PI_rank_lt:
  assumes "awalk π⇘σ⇙ p π⇘σ'⇙"
      and "σ ≠ σ'"
      and "σ ∈ Σ"
      and "σ' ∈ Σ"
    shows "rank σ < rank σ'"
  using assms unfolding awalk_def
proof (induction "π⇘σ⇙" p "π⇘σ'⇙" arbitrary: σ σ' rule: cas.induct)
  case 1
  then have "π⇘σ⇙ = π⇘σ'⇙" using cas.simps(1) by blast
  then have "σ = σ'"
    by (smt (verit) "1.prems"(3) "1.prems"(4) Collect_mem_eq π_σ_α')
  with ‹σ ≠ σ'› have False by blast
  then show ?case ..
next
  case (2 e es)
  then have e_es_in_arcs: "set (e # es) ⊆ arcs G_PI"
                 and cas_e_es: "cas π⇘σ⇙ (e # es) π⇘σ'⇙"
    by argo+
  from e_es_in_arcs have "e ∈ rel_PI"
    by (metis arcs_G_PI in_mono list.set_intros(1))
  then obtain π⇩1 π⇩2 where "e = (π⇩1, π⇩2)" "π⇩1 ∈ PI" "π⇩2 ∈ PI" by auto
  then have e_π12: "π⇩1 = tail G_PI e" "π⇩2 = head G_PI e" by simp+
  with cas_e_es have "π⇩1 = π⇘σ⇙" by (meson pre_digraph.cas.simps(2))
  from ‹π⇩2 ∈ PI› obtain σ'' where "σ'' ∈ Σ" "π⇩2 = π⇘σ''⇙" by auto
  with cas_e_es e_π12 have "cas π⇘σ''⇙ es π⇘σ'⇙"
    by (metis cas.simps(2))

  from ‹π⇩1 = π⇘σ⇙› ‹π⇩2 = π⇘σ''⇙› ‹e = (π⇩1, π⇩2)› have "e = (π⇘σ⇙, π⇘σ''⇙)"
    by simp
  with ‹e ∈ rel_PI› rel_PI_implies_rank_lt have "rank σ < rank σ''"
    using ‹σ ∈ Σ› ‹σ'' ∈ Σ› by blast

  show ?case
  proof (cases "σ'' = σ'")
    case True
    with ‹rank σ < rank σ''› show ?thesis by blast
  next
    case False
    with "2.hyps" have "rank σ'' < rank σ'"
      using "2.prems"(1) "2.prems"(4) ‹π⇩2 = π⇘σ''⇙› ‹π⇩2 ∈ PI› ‹σ'' ∈ Σ› ‹cas π⇘σ''⇙ es π⇘σ'⇙› e_π12(2)
      by (metis insert_subset list.simps(15) verts_G_PI)
    with ‹rank σ < rank σ''› show ?thesis by order
  qed
qed

lemma all_places_same_implies_assignment_equal:
  assumes "x ∈ V"
      and "y ∈ V"
      and π_eq: "∀π ∈ PI. π x ⟷ π y"
    shows "𝒜 x = 𝒜 y"
proof -
  let ?ℒ_x' = "{α ∈ ℒ V x. proper_Venn_region α ≠ 0}"
  let ?ℒ_y' = "{α ∈ ℒ V y. proper_Venn_region α ≠ 0}"

  have proper_Venn_region_ℒ_x': "proper_Venn_region ` ?ℒ_x' = {s ∈ proper_Venn_region ` ℒ V x. s ≠ 0}"
    by fast
  have proper_Venn_region_ℒ_y': "proper_Venn_region ` ?ℒ_y' = {s ∈ proper_Venn_region ` ℒ V y. s ≠ 0}"
    by fast

  from finite_V have "finite (ℒ V x)" by blast
  then have "finite (proper_Venn_region ` ℒ V x)" by blast
  from finite_V have "finite (ℒ V y)" by blast
  then have "finite (proper_Venn_region ` ℒ V y)" by blast

  have π_eq': "π⇘proper_Venn_region α⇙ x = π⇘proper_Venn_region α⇙ y"
    if "α ∈ ?ℒ_x' ∨ α ∈ ?ℒ_y'" for α
  proof -
    from that have "x ∈ α ∨ y ∈ α" by fastforce
    from that have "α ∈ P⇧+ V" by fastforce
    with that have "π⇘proper_Venn_region α⇙ ∈ PI" by fastforce
    with π_eq show ?thesis by fast
  qed

  have "?ℒ_x' = ?ℒ_y'"
  proof (standard; standard)
    fix α assume "α ∈ ?ℒ_x'"
    then have "x ∈ α" by fastforce
    with ‹α ∈ ?ℒ_x'› ‹x ∈ V› have "π⇘proper_Venn_region α⇙ x"
      using proper_Venn_region_subset_variable_iff by auto
    with π_eq' ‹α ∈ ?ℒ_x'› have "π⇘proper_Venn_region α⇙ y" by blast
    with ‹α ∈ ?ℒ_x'› ‹y ∈ V› have "y ∈ α"
      using proper_Venn_region_subset_variable_iff by auto
    with ‹α ∈ ?ℒ_x'› show "α ∈ ?ℒ_y'" by fastforce
  next
    fix α assume "α ∈ ?ℒ_y'"
    then have "y ∈ α" by fastforce
    with ‹α ∈ ?ℒ_y'› ‹y ∈ V› have "π⇘proper_Venn_region α⇙ y"
      using proper_Venn_region_subset_variable_iff by auto
    with π_eq' ‹α ∈ ?ℒ_y'› have "π⇘proper_Venn_region α⇙ x" by blast
    with ‹α ∈ ?ℒ_y'› ‹x ∈ V› have "x ∈ α"
      using proper_Venn_region_subset_variable_iff by auto
    with ‹α ∈ ?ℒ_y'› show "α ∈ ?ℒ_x'" by fastforce
  qed

  from ‹x ∈ V› have "𝒜 x = ⨆HF (proper_Venn_region ` ℒ V x)"
    using variable_as_composition_of_proper_Venn_regions by presburger
  also have "... = ⨆HF (proper_Venn_region ` ?ℒ_x')"
    using Hunion_nonempty[where ?S = "proper_Venn_region ` ℒ V x"]
    using ‹finite (proper_Venn_region ` ℒ V x)› proper_Venn_region_ℒ_x'
    by argo
  also have "... = ⨆HF (proper_Venn_region ` ?ℒ_y')"
    using ‹?ℒ_x' = ?ℒ_y'› by argo
  also have "... = ⨆HF (proper_Venn_region ` ℒ V y)"
    using Hunion_nonempty[where ?S = "proper_Venn_region ` ℒ V y"]
    using ‹finite (proper_Venn_region ` ℒ V y)› proper_Venn_region_ℒ_y'
    by argo
  also have "... = 𝒜 y"
    using ‹y ∈ V› variable_as_composition_of_proper_Venn_regions
    by presburger
  finally show "𝒜 x = 𝒜 y" .
qed

definition "at⇩p ≡ {(y, at⇩p_f y)|y. y ∈ W}"
declare at⇩p_def [simp]

(* Lemma 27 *)
theorem syntactic_description_is_adequate:
  "adequate_place_framework 𝒞 PI at⇩p"
proof (unfold_locales, goal_cases)
  case 1
  then show ?case
  proof
    fix π assume "π ∈ PI"
    then obtain σ where "π = π⇘σ⇙" "σ ∈ Σ" by auto
    then obtain α where "σ = proper_Venn_region α" "α ∈ P⇧+ V" by auto
    with ‹σ ∈ Σ› have "σ ≠ 0" "proper_Venn_region α ≠ 0" by auto
    from ‹α ∈ P⇧+ V› have "α ⊆ V" by simp

    from proper_Venn_region_subset_variable_iff
    have α_σ: "x ∈ α ⟷ σ ≤ 𝒜 x" if "x ∈ V" for x
      using ‹α ⊆ V› ‹x ∈ V› ‹proper_Venn_region α ≠ 0› ‹σ = proper_Venn_region α›
      by presburger

    from ‹π = π⇘σ⇙› ‹σ = proper_Venn_region α› have "π = (λx. x ∈ V ∧ proper_Venn_region α ≤ 𝒜 x)"
      by (meson associated_place.elims(2) associated_place.elims(3))
    also have "... = (λx. x ∈ α)"
      using α_σ ‹α ⊆ V› ‹σ = proper_Venn_region α› by (metis rev_contra_hsubsetD)
    also have "... ∈ places V"
      unfolding places_def using ‹α ⊆ V› by blast
    finally show "π ∈ places V" .
  qed
next
  case 2
  then show ?case using at⇩p_f.simps by auto
next
  case 3
  then show ?case using range_at⇩p_f by fastforce
next
  case 4
  then show ?case by (simp add: single_valued_def)
next
  case (5 π)
  from place_membership_irreflexive show ?case by auto
next
  case (6 e)
  obtain π π' where "e = (π, π')" by fastforce
  with 6 have "π ∈ PI" by simp
  with ‹e = (π, π')› show ?case by simp
next
  case (7 e)
  obtain π π' where "e = (π, π')" by fastforce
  with 7 have "π' ∈ PI" by simp
  with ‹e = (π, π')› show ?case by simp
next
  case 8
  from finite_V have "finite Σ" by auto
  then show ?case by auto
next
  case 9
  from finite_V have "finite PI" by auto
  then have "finite (PI × PI)" by auto
  moreover
  have "rel_PI ⊆ PI × PI" by auto
  ultimately
  have "finite rel_PI" by (simp add: finite_subset) 
  then show ?case by auto
next
  case (10 e)
  then have "e ∈ rel_PI" by force
  with place_membership_irreflexive have "fst e ≠ snd e"
    by (metis prod.collapse)
  with rel_PI_head_tail show ?case by auto
next
  case (11 e⇩1 e⇩2)
  then show ?case
    unfolding arc_to_ends_def by simp
next
  case 12
  show ?case
  proof (rule ccontr)
    assume "¬(∄c. pre_digraph.cycle (place_mem_graph 𝒞 PI) c)"
    then obtain c where "cycle c"
      by fastforce
    then obtain e es π where e_es: "c = e # es" "awalk π (e # es) π"
      by (metis awalk_def cas.elims(2) cycle_def)
    then obtain π' where "e = (π, π')"
      by (metis arcs_G_PI awalk_def cas.simps(2) insert_subset list.simps(15) rel_PI_head_tail) 
    then show False
    proof (cases "es = []")
      case True
      with e_es have "e = (π, π)"
        by (metis arcs_G_PI awalk_def cas.simps(1) cas.simps(2) list.set_intros(1) rel_PI_head_tail subset_code(1))
      then have "(π, π) ∈ rel_PI"
        by (metis arcs_G_PI e_es(2) insert_subset list.simps(15) pre_digraph.awalk_def)
      with place_membership_irreflexive show False by blast
    next
      case False
      with e_es ‹cycle c› ‹e = (π, π')› have "π' ≠ π"
        by (metis arcs_G_PI awalk_def list.set_intros(1) place_membership_irreflexive subset_code(1))
      from e_es ‹e = (π, π')› have "π ∈ PI" "π' ∈ PI"
        unfolding awalk_def by simp+
      then obtain σ σ' where σ_σ': "π = π⇘σ⇙" "π' = π⇘σ'⇙" "σ ∈ Σ" "σ' ∈ Σ" by auto
      from e_es ‹e = (π, π')› have "awalk π' es π"
        unfolding awalk_def
        by (metis Pair_inject ‹π' ∈ PI› arcs_G_PI cas.simps(2) insert_subset list.simps(15) rel_PI_head_tail verts_G_PI)
      with awalk_in_G_PI_rank_lt have "rank σ' < rank σ"
        using ‹π' ≠ π› σ_σ' by blast
      moreover
      from rel_PI_implies_rank_lt have "rank σ < rank σ'"
        using ‹e = (π, π')› σ_σ'
        by (metis e_es arcs_G_PI e_es(1) list.set_intros(1) pre_digraph.awalk_def subset_code(1))
      ultimately
      show False by simp
    qed
  qed
next
  case (13 x)
  with 𝒜_sat_𝒞 have "𝒜 x = 0" by fastforce
  from 13 have "x ∈ V" by force
  have "¬ π x" if "π ∈ PI" for π
  proof -
    from that obtain σ where "σ ∈ Σ" "π = π⇘σ⇙" by auto
    then have "π x ⟷ x ∈ V ∧ σ ≤ 𝒜 x" "σ ≠ 0" by simp+
    with ‹x ∈ V› have "π x ⟷ σ ≤ 𝒜 x" by argo
    with ‹σ ≠ 0› ‹𝒜 x = 0› show "¬ π x" by simp
  qed
  then show ?case unfolding PI_def by blast
next
  case (14 x y)
  with 𝒜_sat_𝒞 have "𝒜 x = 𝒜 y" by fastforce
  from ‹AT (Var x =⇩s Var y) ∈ 𝒞› have "x ∈ V" "y ∈ V" by force+
  have "π x = π y" if "π ∈ PI" for π
  proof -
    from that obtain σ where "σ ∈ Σ" "π = π⇘σ⇙" by auto
    then have "π x ⟷ x ∈ V ∧ σ ≤ 𝒜 x" "π y ⟷ y ∈ V ∧ σ ≤ 𝒜 y" by simp+
    with ‹x ∈ V› ‹y ∈ V› have "π x ⟷ σ ≤ 𝒜 x" "π y ⟷ σ ≤ 𝒜 y" by argo+
    with ‹𝒜 x = 𝒜 y› show "π x = π y" by simp
  qed
  then show ?case unfolding PI_def by blast
next
  case (15 x y z)
  with 𝒜_sat_𝒞 have "𝒜 x = 𝒜 y ⊔ 𝒜 z" by fastforce
  from 15 have "x ∈ V" "y ∈ V" "z ∈ V" by force+
  have "π x ⟷ π y ∨ π z" if "π ∈ PI" for π
  proof -
    from that π_σ_α obtain α where α:
      "α ∈ P⇧+ V" "π = π⇘proper_Venn_region α⇙" "π = (λv. v ∈ α)" "proper_Venn_region α ≠ 0"
      by blast
    have "π y ∨ π z" if "π x"
    proof -
      from ‹π x› α have "x ∈ α" by metis
      from ‹π x› α have "proper_Venn_region α ≤ 𝒜 x" by simp
      with ‹proper_Venn_region α ≠ 0› have "𝒜 x ≠ 0" by fastforce
      {assume "y ∉ α" "z ∉ α"
        from ‹y ∉ α› ‹y ∈ V› have "𝒜 y ⊓ proper_Venn_region α = 0"
          using finite_V by fastforce
        moreover
        from ‹z ∉ α› ‹z ∈ V› have "𝒜 z ⊓ proper_Venn_region α = 0"
          using finite_V by fastforce
        ultimately
        have "𝒜 x ⊓ proper_Venn_region α = 0"
          using ‹𝒜 x = 𝒜 y ⊔ 𝒜 z› by simp
        from ‹x ∈ α› have "proper_Venn_region α ≤ 𝒜 x"
          using α by (meson associated_place.elims(2))
        with ‹𝒜 x ≠ 0› ‹𝒜 x ⊓ proper_Venn_region α = 0›
        have "proper_Venn_region α = 0" by blast
        with ‹proper_Venn_region α ≠ 0› have False by blast}
      then have "y ∈ α ∨ z ∈ α" by blast
      then show "π y ∨ π z" by (simp add: ‹π = (λv. v ∈ α)›) 
    qed
    have "π x" if "π y ∨ π z"
    proof -
      from ‹π y ∨ π z› α have "proper_Venn_region α ≤ 𝒜 y ∨ proper_Venn_region α ≤ 𝒜 z"
        by auto
      with ‹𝒜 x = 𝒜 y ⊔ 𝒜 z› have "proper_Venn_region α ≤ 𝒜 x" by auto
      with α ‹x ∈ V› show "π x" by simp
    qed
    from ‹π x ⟹ π y ∨ π z› ‹π y ∨ π z ⟹ π x› 
    show ?thesis by blast
  qed
  then show ?case unfolding PI_def by blast
next
  case (16 x y z)
  with 𝒜_sat_𝒞 have "𝒜 x = 𝒜 y - 𝒜 z" by fastforce
  from ‹AT (Var x =⇩s Var y -⇩s Var z) ∈ 𝒞› have "x ∈ V" "y ∈ V" "z ∈ V" by force+
  have "π x ⟷ π y ∧ ¬ π z" if "π ∈ PI" for π
  proof -
    from that π_σ_α obtain α where α:
      "α ∈ P⇧+ V" "π = π⇘proper_Venn_region α⇙" "π = (λv. v ∈ α)" "proper_Venn_region α ≠ 0"
      by blast
    with finite_V have "finite α" by blast
    have "π x" if "π y" "¬ π z"
    proof -
      have "proper_Venn_region α ≤ 𝒜 y"
        by (metis α(2) associated_place.elims(2) ‹π y›)
      moreover
      from ‹¬ π z› ‹z ∈ V› have "z ∈ V - α"
        using α by (metis DiffI) 
      then have "𝒜 z ≤ ⨆HF (𝒜 ` (V - α))"
        by (meson finite_Diff finite_V finite_imageI image_eqI mem_hsubset_HUnion)
      then have "𝒜 z ⊓ proper_Venn_region α = 0"
        by (simp add: hinter_hdiff_hempty)
      ultimately
      have "proper_Venn_region α ≤ 𝒜 y - 𝒜 z" by blast
      with ‹𝒜 x = 𝒜 y - 𝒜 z› have "proper_Venn_region α ≤ 𝒜 x" by argo
      with α ‹x ∈ V› show ?thesis by auto
    qed
    have "π y ∧ ¬ π z" if "π x"
    proof -
      from ‹π x› α have "proper_Venn_region α ≤ 𝒜 x"
        by auto
      with ‹𝒜 x = 𝒜 y - 𝒜 z› have "proper_Venn_region α ≤ 𝒜 y" "¬ proper_Venn_region α ≤ 𝒜 z"
        apply simp_all
         apply auto[1]
        by (metis (no_types, lifting) α(4) hdiff_iff hdisjoint_iff inf.orderE proper_Venn_region.elims rev_hsubsetD)
      with α ‹y ∈ V› ‹z ∈ V› show "π y ∧ ¬ π z" by simp
    qed
    from ‹π x ⟹ π y ∧ ¬ π z› ‹π y ⟹ ¬ π z ⟹ π x› 
    show ?thesis by blast
  qed
  then show ?case unfolding PI_def by blast
next
  case (17 x y)
  with 𝒜_sat_𝒞 have "𝒜 x ≠ 𝒜 y" by fastforce
  from 17 have "x ∈ V" "y ∈ V" by fastforce+
  with ‹𝒜 x ≠ 𝒜 y› all_places_same_implies_assignment_equal
  show ?case by metis
next
  case (18 x y)
  then have "y ∈ W" by fastforce
  from 18 have "x ∈ V" "y ∈ V" by fastforce+
  from 18 𝒜_sat_𝒞 have "𝒜 x = HF{𝒜 y}" by fastforce
  then have "σ⇘y⇙ ≤ 𝒜 x" by simp
  with ‹x ∈ V› have "at⇩p_f y x" by (simp only: at⇩p_f.simps) simp
  moreover
  {fix π assume "π ∈ PI" "π x"
    then obtain σ where "π = π⇘σ⇙" "σ ≤ 𝒜 x" "σ ≠ 0" by fastforce
    with ‹𝒜 x = HF{𝒜 y}› have "σ = HF{𝒜 y}" by fastforce
    with ‹π = π⇘σ⇙› have "π = at⇩p_f y" by simp
  }
  then have "∀π'∈PI. π' ≠ at⇩p_f y ⟶ ¬ π' x"
    by blast
  ultimately
  show ?case using ‹y ∈ W› by simp
next
  case (19 y z)
  then obtain π where "π = at⇩p_f z" "π = at⇩p_f y" by simp
  then have "at⇩p_f z = at⇩p_f y" by blast
  from ‹y ∈ W› obtain x where x: "AT (Var x =⇩s Single (Var y)) ∈ 𝒞"
    using memW_E by blast
  with 𝒜_sat_𝒞 have "𝒜 x = HF{𝒜 y}" by fastforce
  from 19 x have "x ∈ V" "y ∈ V" by fastforce+
  from 19 have "z ∈ V" using W_subset_V by blast

  from ‹𝒜 x = HF{𝒜 y}› have "σ⇘y⇙ ≤ 𝒜 x" by simp
  with ‹x ∈ V› have "at⇩p_f y x" by auto
  with ‹at⇩p_f z = at⇩p_f y› have "at⇩p_f z x" by argo
  then have "σ⇘z⇙ ≤ 𝒜 x" by simp
  with ‹𝒜 x = HF{𝒜 y}› have "σ⇘z⇙ = HF{𝒜 y}" by force
  then have "𝒜 z = 𝒜 y"
    by (metis finite.emptyI finite_insert hfset_HF containing_region.elims singleton_insert_inj_eq)

  {fix π assume "π ∈ PI"
    then obtain σ where "π = π⇘σ⇙" "σ ≠ 0" by auto
    with ‹y ∈ V› have "π y ⟷ σ ≤ 𝒜 y" by fastforce
    also have "... ⟷ σ ≤ 𝒜 z"
      using ‹𝒜 z = 𝒜 y› by auto
    also have "... ⟷ π z"
      using ‹π = π⇘σ⇙› ‹z ∈ V› by simp
    finally have "π y = π z" .
  }
  then show ?case by blast
next
  case (20 y y')
  then have "y ∈ V" "y' ∈ V" by (metis W_subset_V subsetD)+
  with ‹∀π∈PI. π y' = π y› all_places_same_implies_assignment_equal
  have "𝒜 y = 𝒜 y'" by presburger
  then have "at⇩p_f y = at⇩p_f y'" by simp
  with ‹y ∈ W› ‹y' ∈ W› show ?case by simp
next
  case (21 π⇩1 π⇩2)
  have "π = π⇘HF {0}⇙" if "π ∈ Range at⇩p - Range (place_membership 𝒞 PI)" for π
  proof -
    from that obtain y where y: "y ∈ W" "at⇩p_f y = π"
    by (simp only: at⇩p_def) blast
    with range_at⇩p_f have "π ∈ PI" by blast
    from ‹y ∈ W› obtain x where lt_in_𝒞:
      "AT (Var x =⇩s Single (Var y)) ∈ 𝒞"
      using memW_E by presburger
    with 𝒜_sat_𝒞 have "𝒜 x = HF {𝒜 y}" by fastforce
    then have "σ⇘y⇙ ≤ 𝒜 x" by simp
    with lt_in_𝒞 have "at⇩p_f y x" by force
    with ‹at⇩p_f y = π› have "π x" by blast
  
    have "∀π ∈ PI. ¬ π y"
    proof (rule ccontr)
      assume "¬ (∀π∈PI. ¬ π y)"
      then obtain π' where "π' ∈ PI" "π' y" by blast
      with ‹AT (Var x =⇩s Single (Var y)) ∈ 𝒞› ‹π x›
      have "(π', π) ∈ place_membership 𝒞 PI"
        using ‹π ∈ PI›
        by (simp only: place_membership.simps) blast
      then have "π ∈ Range (place_membership 𝒞 PI)" by blast
      with that show False by blast
    qed
    have "∀α ∈ ℒ V y. proper_Venn_region α = 0"
    proof (rule ccontr)
      assume "¬ (∀α ∈ ℒ V y. proper_Venn_region α = 0)"
      then obtain α where α: "α ∈ ℒ V y" "proper_Venn_region α ≠ 0" by blast
      then have "proper_Venn_region α ≤ 𝒜 y"
        using variable_as_composition_of_proper_Venn_regions ℒ_finite finite_V
        by (smt (verit, ccfv_threshold) W_subset_V finite_imageI image_eqI mem_hsubset_HUnion subset_iff y(1))
      then have "π⇘proper_Venn_region α⇙ y"
        using W_subset_V ‹y ∈ W› by auto
      with ‹∀π ∈ PI. ¬ π y› show False
        using α by auto
    qed
    then have "⨆HF (proper_Venn_region ` ℒ V y) = 0"
      by fastforce
    with variable_as_composition_of_proper_Venn_regions[of y]
    have "𝒜 y = 0"
      using ‹y ∈ W› W_subset_V by auto
    with ‹𝒜 x = HF {𝒜 y}› have "𝒜 x = HF {0}" by argo

    from ‹π ∈ PI› obtain σ where "σ ∈ Σ" "π = π⇘σ⇙" by auto
    with ‹π x› have "σ ≠ 0" "σ ≤ 𝒜 x" by simp+
    with ‹𝒜 x = HF {0}› have "σ = HF {0}" by fastforce
    with ‹π = π⇘σ⇙› show "π = π⇘HF {0}⇙" by blast
  qed
  with 21 show ?case by blast
qed

end

end