Theory Place_Realisation

theory Place_Realisation
  imports Place_Framework MLSS_Decision_Proc.MLSS_Realisation Proper_Venn_Regions
begin

lemma u_exists:
  assumes "finite (S :: 'a set)"
    shows "∃(u :: 'a ⇒ hf). (∀x ∈ S. ∀y ∈ S. x ≠ y ⟶ u x ≠ u y) ∧ (∀x ∈ S. hcard (u x) ≥ n)"
proof -
  from ‹finite S› have "∃f. inj_on f S ∧ f ` S = {0 ..< card S}"
  proof (induction S)
    case empty
    then show ?case by simp
  next
    case (insert x S)
    from insert.IH obtain f where "inj_on f S" "f ` S = {0 ..< card S}" by blast
    then have range_f_on_S: "y ∈ S ⟹ f y < card S" for y
      by fastforce
    let ?f = "(λx. if x ∈ S then f x else card S)"
    have "?f y ≠ ?f z" if "y ∈ insert x S" "z ∈ insert x S" "y ≠ z" for y z
    proof -
      from that consider "y ∈ S ∧ z ∈ S" | "y ∈ S ∧ z = x" | "y = x ∧ z ∈ S" | "y = x ∧ z = x"
        by fast
      then show ?thesis
      proof (cases)
        case 1
        then have "?f y = f y" "?f z = f z" by simp+
        moreover
        from ‹inj_on f S› ‹y ≠ z› 1 have "f y ≠ f z"
          by (simp add: inj_on_contraD)
        ultimately
        show ?thesis by presburger
      next
        case 2
        then have "?f y = f y" by simp
        with range_f_on_S have "?f y < card S"
          using 2 by presburger
        moreover
        from 2 ‹x ∉ S› have "?f z = card S" by argo
        ultimately
        show ?thesis by force
      next
        case 3
        then have "?f z = f z" by simp
        with range_f_on_S have "?f z < card S"
          using 3 by presburger
        moreover
        from 3 ‹x ∉ S› have "?f y = card S" by argo
        ultimately
        show ?thesis by force
      next
        case 4
        with ‹y ≠ z› have False by blast
        then show ?thesis by blast
      qed
    qed
    then have "inj_on ?f (insert x S)"
      using inj_on_def by blast
    moreover
    have "?f ` (insert x S) = {0 ..< card (insert x S)}"
    proof (standard; standard)
      fix c assume "c ∈ ?f ` (insert x S)"
      then obtain y where "y ∈ insert x S" "c = ?f y" by blast
      then have "c < Suc (card S)"
        apply (cases "y ∈ S")
        using range_f_on_S
         apply fastforce
        by auto
      also have "... = card (insert x S)"
        using ‹x ∉ S› ‹finite S› by simp
      finally show "c ∈ {0 ..< card (insert x S)}" by simp
    next
      fix c assume "c ∈ {0 ..< card (insert x S)}"
      then have "c ≤ card S"
        using ‹x ∉ S› ‹finite S› by auto

      have "∃y ∈ S. ?f y = c" if "c < card S"
      proof -
        from that have "c ∈ {0 ..< card S}" by simp
        with ‹f ` S = {0 ..< card S}›
        obtain y where "y ∈ S" "f y = c"
          using image_iff[where ?z = c and ?f = f and ?A = S]
          by blast
        moreover
        from ‹y ∈ S› have "f y = ?f y" by auto
        ultimately
        show ?thesis by auto
      qed
      then have "c < card S ⟹ ∃y ∈ insert x S. ?f y = c" by blast
      moreover
      from ‹x ∉ S› have "?f x = card S" by argo
      then have "c = card S ⟹ ∃y ∈ insert x S. ?f y = c" by blast
      ultimately
      show "c ∈ ?f ` (insert x S)"
        using ‹c ≤ card S› by fastforce
    qed
    ultimately
    show ?case by blast
  qed
  then obtain f' where "inj_on f' S" "f' ` S = {0 ..< card S}" by blast
  let ?f = "λx. f' x + n"
  from ‹inj_on f' S› have f_inj: "?f x ≠ ?f y" if "x ∈ S" "y ∈ S" "x ≠ y" for x y
    by (simp add: inj_on_eq_iff that)
  from ‹f' ` S = {0 ..< card S}› have f_ge_n: "?f x ∉ {0 ..< n}" if "x ∈ S" for x
    using that by auto

  let ?u = "λx. HF (Abs_hf ` {0 ..< n}) ◃ Abs_hf (?f x)"
  have "?u x ≠ ?u y" if "x ∈ S" "y ∈ S" "x ≠ y" for x y
  proof -
    from f_inj that have "?f x ≠ ?f y" by blast
    then have "Abs_hf (?f x) ≠ Abs_hf (?f y)"
      by (simp add: Abs_hf_inject)
    moreover
    from f_ge_n ‹x ∈ S› have "Abs_hf (?f x) ∉ Abs_hf ` {0 ..< n}"
      using Abs_hf_inject by fastforce
    then have "Abs_hf (?f x) ∉ HF (Abs_hf ` {0 ..< n})" by simp
    moreover
    from f_ge_n ‹y ∈ S› have "Abs_hf (?f y) ∉ Abs_hf ` {0 ..< n}"
      using Abs_hf_inject by fastforce
    then have "Abs_hf (?f y) ∉ HF (Abs_hf ` {0 ..< n})" by simp
    ultimately
    show "?u x ≠ ?u y"
      by (metis hmem_hinsert)
  qed
  then have "∀x∈S. ∀y∈S. x ≠ y ⟶ ?u x ≠ ?u y" by blast
  moreover
  have "hcard (?u x) ≥ n" if "x ∈ S" for x
  proof -
    from f_ge_n ‹x ∈ S› have "Abs_hf (?f x) ∉ Abs_hf ` {0 ..< n}"
      using Abs_hf_inject by fastforce
    then have "Abs_hf (?f x) ∉ HF (Abs_hf ` {0 ..< n})" by simp
    then have "hcard (?u x) = Suc (hcard (HF (Abs_hf ` {0..<n})))"
      by (simp add: hcard_hinsert_if)
    also have "... = Suc (card (Abs_hf ` {0 ..< n}))"
      using hcard_def by auto
    also have "... = Suc (card {0 ..< n})"
      using Abs_hf_inject card_image injD inj_on_def by metis
    also have "... = Suc n" by auto
    finally show "hcard (?u x) ≥ n" by auto
  qed
  ultimately
  show ?thesis by meson
qed

locale place_realization =
  adequate_place_framework 𝒞 PI atp for 𝒞 PI atp +
    fixes u :: "('a ⇒ bool) ⇒ hf"
  assumes u_distinct: "⟦π1 ∈ PI - Range atp; π2 ∈ PI - Range atp; π1 ≠ π2⟧ ⟹ u π1 ≠ u π2"
      and hcard_u_not_in_range_atp: "π ∈ PI - Range atp ⟹ hcard (u π) ≥ card PI"
begin

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

definition "membership ≡ place_membership 𝒞 PI"
declare membership_def [simp]

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

lemma u_distinct':
  "⟦π1 ∈ PI - Range atp; π2 ∈ PI - Range atp; π1 ≠ π2⟧ ⟹ u π1 ≠ u π2"
  using u_distinct by simp

interpretation realisation G_PI "PI - Range atp" "Range atp" u "{(π, π) |π. π ∈ PI}"
proof -
  have "(PI - Range atp) ∩ Range atp = {}"
    by (simp add: inf_commute)
  moreover
  have "verts G_PI = (PI - Range atp) ∪ Range atp"
    using range_atp by auto 
  moreover
  have "¬ t →⇘G_PI⇙ p" if "p ∈ PI - Range atp" for p t
  proof -
    have "(t, p) ∉ membership"
    proof (rule ccontr)
      assume "¬ (t, p) ∉ membership"
      then have "(t, p) ∈ membership" by blast
      then have t: "t ∈ PI" and p: "p ∈ PI" and "∃x y. AT (Var x =s Single (Var y)) ∈ 𝒞 ∧ t y ∧ p x"
        by auto
      then obtain x y where xy: "AT (Var x =s Single (Var y)) ∈ 𝒞" "t y" "p x" by blast
      with C5_1 range_atp single_valued_atp obtain π
        where C5_1_1: "π ∈ PI" "(y, π) ∈ atp" "π x"
          and C5_1_2: "π' ∈ PI ∧ π' x ⟹ π' = π" for π'
        by blast
      show False
      proof (cases "(y, p) ∈ atp")
        case True
        from xy have "y ∈ W" by fastforce
        with ‹p ∈ PI - Range atp› ‹(y, p) ∈ atp› show ?thesis by blast
      next
        case False
        with C5_1_2 xy p show ?thesis
          using C5_1 by fast
      qed
    qed
    moreover
    have "arcs_ends G_PI = membership"
      unfolding arcs_ends_def arc_to_ends_def by simp
    ultimately
    show ?thesis by blast
  qed
  moreover
  from C6 have "dag G_PI" by auto
  ultimately
  show "realisation G_PI (PI - Range atp) (Range atp)"
    unfolding realisation_def
    by (meson realisation_axioms.intro)
qed

function place_realise :: "('a ⇒ bool) ⇒ hf" where
  "π ∈ PI - Range atp ⟹ place_realise π = HF {u π}"
| "π ∈ Range atp ⟹ place_realise π = HF {⨆HF (place_realise ` parents G_PI π)}"
| "π ∉ PI ⟹ place_realise π = 0"
  using B_T_partition_verts range_atp by blast+
termination
  apply (relation "measure (λt. card (ancestors G_PI t))")
   apply (simp_all add: card_ancestors_strict_mono del: G_PI_def)
  done

lemma place_realise_singleton:
  assumes "π ∈ PI"
    shows "hcard (place_realise π) = 1"
  using assms
proof (cases π rule: place_realise.cases)
  case (1 π)
  have "finite {u π}" by blast
  then have "hcard (HF {u π}) = 1"
    using hcard_def by auto
  with 1 show ?thesis by simp
next
  case (2 π)
  then have "hcard (HF {⨆HF (place_realise ` parents G_PI π)}) = 1"
    using hcard_def by auto
  with 2 show ?thesis by simp
next
  case (3 π)
  with assms show ?thesis by fast
qed

lemma place_realise_nonempty:
  assumes "π ∈ PI"
    shows "place_realise π ≠ 0"
  using assms place_realise_singleton hcard_1E by fastforce

lemma place_realise_elem_hcard_in_range_atp:
  assumes "π ∈ Range atp"
    shows "∃a. place_realise π = HF {a} ∧ hcard a < card PI"
proof -
  from assms obtain a where a: "a = ⨆HF (place_realise ` parents G_PI π)" "place_realise π = HF {a}"
    by simp

  from assms have "π ∈ PI"
    by (metis B_T_partition_verts(2) UnCI verts_G_PI) 
  moreover
  have "π ∉ parents G_PI π"
    using membership_irreflexive by fastforce
  moreover
  have "parents G_PI π ⊆ PI" by auto
  ultimately
  have "parents G_PI π ⊂ PI"
    by blast
  then have "card (parents G_PI π) < card PI"
    using finite_PI by (simp add: psubset_card_mono)
  moreover
  from hcard_Hunion_singletons[where ?s = "parents G_PI π" and ?f = place_realise]
  have "hcard (⨆HF (place_realise ` parents G_PI π)) ≤ card (parents G_PI π)"
    using place_realise_singleton ‹parents G_PI π ⊆ PI› by blast
  ultimately
  have "hcard (⨆HF (place_realise ` parents G_PI π)) < card PI"
    by linarith
  with a show ?thesis by blast
qed

lemma place_realise_elem_hcard_not_in_range_atp:
  assumes "π ∈ PI - Range atp"
    shows "∃a. place_realise π = HF {a} ∧ hcard a ≥ card PI"
  using assms hcard_u_not_in_range_atp by auto

lemma place_in_range_at_eq_if_parents_eq:
  assumes "π1 ∈ Range atp"
      and "π2 ∈ Range atp"
      and parents_eq: "parents G_PI π1 = parents G_PI π2"
    shows "π1 = π2"
proof (cases "parents G_PI π1 = {}")
  case True
  then have "π1 ∉ Range membership" using arcs_ends_G_PI by force
  with ‹π1 ∈ Range atp› have "π1 ∈ Range atp - Range (place_membership 𝒞 PI)"
    by fastforce
  moreover
  from True parents_eq have "parents G_PI π2 = {}" by argo
  then have "π2 ∉ Range membership" using arcs_ends_G_PI by force
  with ‹π2 ∈ Range atp› have "π2 ∈ Range atp - Range (place_membership 𝒞 PI)"
    by fastforce
  ultimately
  show ?thesis using C7 by blast
next
  case False  
  from assms range_atp have "π1 ∈ PI" "π2 ∈ PI" by blast+

  from ‹π1 ∈ Range atp› obtain y1 where "(y1, π1) ∈ atp" by blast
  then have "y1 ∈ W" using dom_atp by blast
  then obtain x1 where "AT (Var x1 =s Single (Var y1)) ∈ 𝒞"
    using memW_E by blast
  with C5_1 ‹(y1, π1) ∈ atp› have "π1 x1"
    by (metis single_valuedD single_valued_atp)

  from ‹π2 ∈ Range atp› obtain y2 where "(y2, π2) ∈ atp" by blast
  then have "y2 ∈ W" using dom_atp by blast
  then obtain x2 where "AT (Var x2 =s Single (Var y2)) ∈ 𝒞"
    using memW_E by blast
  with C5_1 ‹(y2, π2) ∈ atp› have "π2 x2"
    by (metis single_valuedD single_valued_atp)

  have "π y1 ⟷ π y2" if "π ∈ PI" for π
  proof
    assume "π y1"
    with ‹AT (Var x1 =s Single (Var y1)) ∈ 𝒞› ‹π1 x1› ‹π ∈ PI› ‹π1 ∈ PI›
    have "(π, π1) ∈ membership" by auto
    with parents_eq have "(π, π2) ∈ membership"
      using arcs_ends_G_PI by blast
    then obtain x2' y2' where "AT (Var x2' =s Single (Var y2')) ∈ 𝒞" "π y2'" "π2 x2'"
      by auto
    with C5_1 have "(y2', π2) ∈ atp"
      using ‹π2 ∈ PI› by fastforce
    from ‹AT (Var x2' =s Single (Var y2')) ∈ 𝒞› have "y2' ∈ W" by force
    from C5_2 ‹(y2, π2) ∈ atp› ‹(y2', π2) ∈ atp›
    have "∀π ∈ PI. π y2' = π y2"
      using ‹y2 ∈ W› ‹y2' ∈ W› by fast
    with ‹π y2'› show "π y2"
      using ‹π ∈ PI› by fast
  next
    assume "π y2"
    with ‹AT (Var x2 =s Single (Var y2)) ∈ 𝒞› ‹π2 x2› ‹π ∈ PI› ‹π2 ∈ PI›
    have "(π, π2) ∈ membership" by auto
    with parents_eq have "(π, π1) ∈ membership"
      using arcs_ends_G_PI by blast
    then obtain x1' y1' where "AT (Var x1' =s Single (Var y1')) ∈ 𝒞" "π y1'" "π1 x1'"
      by auto
    with C5_1 have "(y1', π1) ∈ atp"
      using ‹π1 ∈ PI› by fastforce
    from ‹AT (Var x1' =s Single (Var y1')) ∈ 𝒞› have "y1' ∈ W" by force
    from C5_2 ‹(y1, π1) ∈ atp› ‹(y1', π1) ∈ atp›
    have "∀π ∈ PI. π y1' = π y1"
      using ‹y1 ∈ W› ‹y1' ∈ W› by fast
    with ‹π y1'› show "π y1"
      using ‹π ∈ PI› by fast
  qed
  with C5_3 show ?thesis
    using ‹y1 ∈ W› ‹y2 ∈ W› ‹(y1, π1) ∈ atp› ‹(y2, π2) ∈ atp›
    by (metis single_valued_atp single_valued_def)
qed

lemma place_realise_pairwise_disjoint:
  assumes "π1 ∈ PI"
      and "π2 ∈ PI"
      and "π1 ≠ π2"
    shows "place_realise π1 ⊓ place_realise π2 = 0"
  using assms
proof (induction π1 arbitrary: π2 rule: place_realise.induct)
  case (1 π)
  then show ?case
  proof (cases "π2 ∈ Range atp")
    case True
      from ‹π2 ∈ Range atp› place_realise_elem_hcard_in_range_atp
      obtain a where π2_a: "place_realise π2 = HF {a}" and hcard_a: "hcard a < card PI"
        by blast      
      from ‹π ∈ PI - Range atp› hcard_u_not_in_range_atp
      obtain b where π_b: "place_realise π = HF {b}" and hcard_b: "card PI ≤ hcard b"
        by auto

      from hcard_a hcard_b have "hcard a ≠ hcard b" by linarith
      then have "HF {a} ⊓ HF {b} = 0" by fastforce
      with π2_a π_b show ?thesis by auto
  next
    case False
    with ‹π2 ∈ PI› have "π2 ∈ PI - Range atp" by blast
    with 1 u_distinct' ‹π ≠ π2› have "u π ≠ u π2" by presburger
    then have "HF {u π} ⊓ HF {u π2} = 0" by simp
    with ‹π ∈ PI - Range atp› ‹π2 ∈ PI - Range atp› show ?thesis
      by simp
  qed
next
  case (2 π)
  then show ?case
  proof (cases "π2 ∈ Range atp")
    case True
    have parents_not_empty: "parents G_PI π' ≠ {} ⟹ ⨆HF (place_realise ` parents G_PI π') ≠ 0" for π'
    proof -
      assume "parents G_PI π' ≠ {}"
      then obtain π'' where "π'' ∈ parents G_PI π'" by blast
      moreover
      have "finite (parents G_PI π')" by blast
      ultimately
      have "place_realise π'' ≤ ⨆HF (place_realise ` parents G_PI π')" by force
      moreover
      have "place_realise π'' ≠ 0"
        using place_realise_singleton ‹π'' ∈ parents G_PI π'›
        by fastforce
      ultimately
      show "⨆HF (place_realise ` parents G_PI π') ≠ 0" by force
    qed

    {assume "place_realise π ⊓ place_realise π2 ≠ 0"
      moreover
      from ‹π ∈ Range atp› have "place_realise π = HF {⨆HF (place_realise ` parents G_PI π)}" by auto
      moreover
      from ‹π2 ∈ Range atp› have "place_realise π2 = HF {⨆HF (place_realise ` parents G_PI π2)}" by auto
      ultimately
      have Hunion_place_realise_parents_eq: "⨆HF (place_realise ` parents G_PI π) = ⨆HF (place_realise ` parents G_PI π2)" by simp
      
      have "parents G_PI π = parents G_PI π2"
      proof(standard; standard)
        fix π' assume "π' ∈ parents G_PI π"
        then have "π' ∈ PI" by auto
        with place_realise_singleton obtain c where "c ∈ place_realise π'"
          by (metis hcard_0 hempty_iff zero_neq_one)
        have "finite (parents G_PI π)" by blast
        with ‹π' ∈ parents G_PI π› have "place_realise π' ≤ ⨆HF (place_realise ` parents G_PI π)"
          by force
        with ‹c ∈ place_realise π'› have "c ∈ ⨆HF (place_realise ` parents G_PI π)"
          by (simp add: less_eq_hf_def)
        with Hunion_place_realise_parents_eq have "c ∈ ⨆HF (place_realise ` parents G_PI π2)"
          by argo
        then obtain π'' where "π'' ∈ parents G_PI π2" "c ∈ place_realise π''" by auto
        with ‹c ∈ place_realise π'› have "place_realise π' ⊓ place_realise π'' ≠ 0" by blast
        with "2.IH" have "π' = π''"
          using ‹π' ∈ parents G_PI π› ‹π'' ∈ parents G_PI π2› ‹π' ∈ PI› by force
        with ‹π'' ∈ parents G_PI π2› show "π' ∈ parents G_PI π2" by blast
      next
        fix π'' assume "π'' ∈ parents G_PI π2"
        then have "π'' ∈ PI" by auto
        with place_realise_singleton obtain c where "c ∈ place_realise π''"
          by (metis hcard_0 hempty_iff zero_neq_one)
        have "finite (parents G_PI π2)" by blast
        with ‹π'' ∈ parents G_PI π2› have "place_realise π'' ≤ ⨆HF (place_realise ` parents G_PI π2)"
          by force
        with ‹c ∈ place_realise π''› have "c ∈ ⨆HF (place_realise ` parents G_PI π2)"
          by (simp add: less_eq_hf_def)
        with Hunion_place_realise_parents_eq have "c ∈ ⨆HF (place_realise ` parents G_PI π)"
          by argo
        then obtain π' where "π' ∈ parents G_PI π" "c ∈ place_realise π'" by auto
        with ‹c ∈ place_realise π''› have "place_realise π' ⊓ place_realise π'' ≠ 0" by blast
        with "2.IH" have "π' = π''"
          using ‹π' ∈ parents G_PI π› ‹π'' ∈ parents G_PI π2› ‹π'' ∈ PI› ‹c ∈ place_realise π'›
          by (metis hmem_hempty place_realise.simps(3))
        with ‹π' ∈ parents G_PI π› show "π'' ∈ parents G_PI π" by blast
      qed
    }
    with place_in_range_at_eq_if_parents_eq show ?thesis
      using 2 True by blast
    next
    case False
    with ‹π2 ∈ PI› have "π2 ∈ PI - Range atp" by blast

    from ‹π ∈ Range atp› place_realise_elem_hcard_in_range_atp
    obtain a where π_a: "place_realise π = HF {a}" and hcard_a: "hcard a < card PI"
      by blast
    from ‹π2 ∈ PI - Range atp› hcard_u_not_in_range_atp
    obtain b where π2_b: "place_realise π2 = HF {b}" and hcard_b: "card PI ≤ hcard b"
      by auto

    from hcard_a hcard_b have "hcard a ≠ hcard b" by linarith
    then have "HF {a} ⊓ HF {b} = 0" by fastforce
    with π_a π2_b show ?thesis by argo
  qed
next
  case (3 π)
  then show ?case by blast
qed

―‹Canonical assignments›
fun ℳ :: "'a ⇒ hf" where
  "ℳ x = ⨆HF (place_realise ` {π ∈ PI. π x})"

lemma var_empty_if_no_place_included_in_PI:
  assumes "∀π ∈ PI. ¬ π x"
    shows "ℳ x = 0"
  using assms by fastforce

lemma HUnion_place_realise_eq_iff_place_composition_same:
  assumes "S ⊆ PI"
      and "T ⊆ PI"
    shows "⨆HF (place_realise ` S) = ⨆HF (place_realise ` T) ⟷ S = T"
proof
  assume HUnion_eq: "⨆HF (place_realise ` S) = ⨆HF (place_realise ` T)"
  from assms finite_PI have "finite S" "finite T"
    by (simp add: finite_subset)+
  show "S = T"
  proof (standard; standard)
    fix π assume "π ∈ S"
    with place_realise_nonempty obtain c where "c ∈ place_realise π"
      using ‹S ⊆ PI› by blast
    with ‹π ∈ S› have "c ∈ ⨆HF (place_realise ` S)"
      using ‹finite S› by auto
    with HUnion_eq have "c ∈ ⨆HF (place_realise ` T)" by argo
    then obtain π' where "π' ∈ T" "c ∈ place_realise π'"
      by auto
    with ‹c ∈ place_realise π› place_realise_pairwise_disjoint place_realise_nonempty
    have "π = π'"
      using ‹π ∈ S› assms by blast
    with ‹π' ∈ T› show "π ∈ T"
      by argo
  next
    fix π assume "π ∈ T"
    with place_realise_nonempty obtain c where "c ∈ place_realise π"
      using ‹T ⊆ PI› by blast
    with ‹π ∈ T› have "c ∈ ⨆HF (place_realise ` T)"
      using ‹finite T› by auto
    with HUnion_eq have "c ∈ ⨆HF (place_realise ` S)" by argo
    then obtain π' where "π' ∈ S" "c ∈ place_realise π'"
      by auto
    with ‹c ∈ place_realise π› place_realise_pairwise_disjoint place_realise_nonempty
    have "π = π'"
      using ‹π ∈ T› assms by blast
    with ‹π' ∈ S› show "π ∈ S"
      by argo
  qed
next
  assume "S = T"
  then show "⨆HF (place_realise ` S) = ⨆HF (place_realise ` T)" by auto
qed

text ‹Lemma 29: canonical assignment is satisfying›
theorem ℳ_sat_𝒞: "∀lt ∈ 𝒞. interp Isa ℳ lt"
proof
  fix lt assume "lt ∈ 𝒞"
  with norm_𝒞 have "normalized_MLSS_literal lt" by blast
  then show "interp Isa ℳ lt"
  proof (cases lt)
    case (eq_empty x n)
      with C1_1 have "{π ∈ PI. π x} = {}"
        using ‹lt ∈ 𝒞› by auto
      with HUnion_place_realise_eq_iff_place_composition_same
      have "ℳ x = 0" by fastforce
      with ‹lt = AT (Var x =s ∅ n)› show ?thesis by auto
    next
    case (eq x y)
    with C1_2 have "{π ∈ PI. π x} = {π ∈ PI. π y}"
      using ‹lt ∈ 𝒞› by auto
    with HUnion_place_realise_eq_iff_place_composition_same
    have "ℳ x = ℳ y" by simp
    with ‹lt = AT (Var x =s Var y)› show ?thesis by auto
  next
    case (neq x y)
    with C4 have "{π ∈ PI. π x} ≠ {π ∈ PI. π y}"
      using ‹lt ∈ 𝒞› by auto
    with HUnion_place_realise_eq_iff_place_composition_same
    have "ℳ x ≠ ℳ y" by simp
    with ‹lt = AF (Var x =s Var y)› show ?thesis by auto
  next
    case (union x y z)
    with C2 have "{π ∈ PI. π x} = {π ∈ PI. π y} ∪ {π ∈ PI. π z}"
      using ‹lt ∈ 𝒞› by auto
    with HUnion_place_realise_eq_iff_place_composition_same
    have "⨆HF (place_realise ` {π ∈ PI. π x}) =
          ⨆HF (place_realise ` ({π ∈ PI. π y} ∪ {π ∈ PI. π z}))"
      by argo
    also have "... = ⨆HF (place_realise ` {π ∈ PI. π y}) ⊔ ⨆HF (place_realise ` {π ∈ PI. π z})"
      using finite_PI by (simp add: image_Un union_hunion)
    finally have "ℳ x = ℳ y ⊔ ℳ z" by fastforce
    with ‹lt = AT (Var x =s Var y ⊔s Var z)› show ?thesis by auto
  next
    case (diff x y z)
    with C3 have "{π ∈ PI. π x} = {π ∈ PI. π y} - {π ∈ PI. π z}"
      using ‹lt ∈ 𝒞› by fast
    with HUnion_place_realise_eq_iff_place_composition_same
    have "⨆HF (place_realise ` {π ∈ PI. π x}) =
          ⨆HF (place_realise ` ({π ∈ PI. π y} - {π ∈ PI. π z}))"
      by argo
    also have "... = ⨆HF (place_realise ` {π ∈ PI. π y}) - ⨆HF (place_realise ` {π ∈ PI. π z})"
      using HUnion_hdiff_if_image_pairwise_disjoint
      using finite_PI place_realise_pairwise_disjoint
      by (metis (mono_tags, lifting) Collect_mem_eq Collect_mono)
    finally have "ℳ x = ℳ y - ℳ z" by fastforce
    with ‹lt = AT (Var x =s Var y -s Var z)› show ?thesis by auto
  next
    case (singleton x y)
    with C5_1 obtain π0 where "(y, π0) ∈ atp" "π0 x" "(∀π'∈PI. π' ≠ π0 ⟶ ¬ π' x)" "π0 ∈ PI"
      using ‹lt ∈ 𝒞› range_atp by blast
    then have "{π ∈ PI. π x} = {π0}" by blast
    then have "ℳ x = place_realise π0" by fastforce
    also have "... = HF {⨆HF (place_realise ` parents G_PI π0)}"
      using ‹(y, π0) ∈ atp› by (simp add: Range.intros) 
    finally have "ℳ x = HF {⨆HF (place_realise ` parents G_PI π0)}" .
    moreover
    have "HF {ℳ y} = HF {⨆HF (place_realise ` {π ∈ PI. π y})}" by simp
    moreover
    have "{π ∈ PI. π y} = parents G_PI π0"
    proof (standard; standard)
      fix π assume "π ∈ {π ∈ PI. π y}"
      then have "π ∈ PI" "π y" by blast+
      with singleton ‹π0 x› ‹π0 ∈ PI› ‹lt ∈ 𝒞›
      have "(π, π0) ∈ membership" by auto
      then show "π ∈ parents G_PI π0"
        using arcs_ends_G_PI by blast
    next
      fix π assume "π ∈ parents G_PI π0"
      then have "π ∈ PI" by force
      from ‹π ∈ parents G_PI π0› have "(π, π0) ∈ membership"
        by fastforce
      then obtain x' y' where "AT (Var x' =s Single (Var y')) ∈ 𝒞" "π y'" "π0 x'"
        by auto
      with C5_1 have "(y', π0) ∈ atp" using ‹π0 ∈ PI› by fast

      from singleton ‹lt ∈ 𝒞› have "y ∈ W" by force
      from ‹AT (Var x' =s Single (Var y')) ∈ 𝒞› have "y' ∈ W" by force
      from ‹(y', π0) ∈ atp› ‹(y, π0) ∈ atp› C5_2 have "∀π ∈ PI. π y = π y'"
        using ‹y ∈ W› ‹y' ∈ W› by fast
      with ‹π y'› ‹π ∈ PI› have "π y" by fast
      moreover
      from ‹π ∈ parents G_PI π0› have "π ∈ PI" by fastforce
      ultimately
      show "π ∈ {π ∈ PI. π y}" by blast
    qed
    with HUnion_place_realise_eq_iff_place_composition_same
    have "⨆HF (place_realise ` parents G_PI π0) = ⨆HF (place_realise ` {π ∈ PI. π y})"
      by argo
    ultimately
    have "ℳ x = HF {ℳ y}" by argo
    with ‹lt = AT (Var x =s Single (Var y))› show ?thesis by simp
  qed
qed

text ‹Correspondence of proper Venn regions and realization of places, and singleton model property›

interpretation proper_Venn_regions V ℳ
  using finite_𝒞
  apply unfold_locales
  by (simp add: finite_vars_fm proper_Venn_regions_def)

lemma proper_Venn_region_place_composition:
  assumes "α ∈ P+ V"
    shows "proper_Venn_region α = ⨆HF (place_realise ` {π ∈ PI. ∀x. π x ⟷ x ∈ α})"
proof -
  from finite_𝒞 have "finite V" by (simp add: finite_vars_fm)
  from ‹α ∈ P+ V› ‹finite V› have "finite α" by blast
  from ‹α ∈ P+ V› have "α ≠ {}" by simp
  from ‹α ∈ P+ V› have "α ⊆ V" by simp

  from ‹finite α› ‹α ≠ {}›
  have "⨅HF (ℳ ` α) = ⨆HF (place_realise ` {π ∈ PI. ∀x ∈ α. π x})"
  proof (induction α)
    case (insert x α')
    then show ?case
    proof (cases "α' = {}")
      case True
      then have "⨅HF (ℳ ` insert x α') = ℳ x"
        using HInter_singleton by fastforce
      with True show ?thesis by force
    next
      case False
      with insert.IH have IH': "⨅HF (ℳ ` α') = ⨆HF (place_realise ` {π ∈ PI. ∀x ∈ α'. π x})"
        by blast
      from False have "ℳ ` α' ≠ {}" by blast
      with ‹finite α'› have "⨅HF (ℳ ` insert x α') = ℳ x ⊓ ⨅HF (ℳ ` α')"
        using HInter_hinsert[where ?A = "HF (ℳ ` α')" and ?a = "ℳ x"]
        using HF_nonempty[where ?S = "ℳ ` α'"]
        using HF_insert_hinsert[where ?S = "ℳ ` α'" and ?x = "ℳ x"]
        by auto
      also have "... = ℳ x ⊓ ⨆HF (place_realise ` {π ∈ PI. (∀x∈α'. π x)})"
        using IH' by argo
      also have "... = ⨆HF (place_realise ` {π ∈ PI. π x}) ⊓ ⨆HF (place_realise ` {π ∈ PI. ∀x ∈ α'. π x})"
        by auto
      also have "... = ⨆HF (place_realise ` ({π ∈ PI. π x} ∩ {π ∈ PI. ∀x ∈ α'. π x}))"
        using hinter_HUnion_if_image_pairwise_disjoint
        using finite_PI place_realise_pairwise_disjoint by force
      also have "... = ⨆HF (place_realise ` {π ∈ PI. ∀x ∈ insert x α'. π x})"
        by (smt (verit, del_insts) Collect_cong Collect_mem_eq IntI Int_iff insert_iff mem_Collect_eq)
      finally show ?thesis .
    qed
  qed blast
  moreover
  have "⨆HF (ℳ ` (V - α)) = ⨆HF (place_realise ` {π ∈ PI. ∃y ∈ V - α. π y})"
  proof (standard; standard)
    from finite_PI have "finite {π ∈ PI. ∃y ∈ V - α. π y}" by simp
    fix c assume "c ∈ ⨆HF (ℳ ` (V - α))"
    then obtain y where "y ∈ V - α" "c ∈ ℳ y" by auto
    then have "c ∈ ⨆HF (place_realise ` {π ∈ PI. π y})" by simp
    then obtain π where "π ∈ PI" "π y" "c ∈ place_realise π" by auto
    with ‹y ∈ V - α› have "π ∈ {π ∈ PI. ∃y ∈ V - α. π y}" by blast
    then have "place_realise π ≤ ⨆HF (place_realise ` {π ∈ PI. ∃y ∈ V - α. π y})"
      using mem_hsubset_HUnion[where ?S = "place_realise ` {π ∈ PI. ∃y ∈ V - α. π y}" and ?s = "place_realise π"]
      using ‹finite {π ∈ PI. ∃y ∈ V - α. π y}›
      by blast
    with ‹c ∈ place_realise π› show "c ∈ ⨆HF (place_realise ` {π ∈ PI. ∃y ∈ V - α. π y})"
      by fast
  next
    fix c assume "c ∈ ⨆HF (place_realise ` {π ∈ PI. ∃y ∈ V - α. π y})"
    then obtain π y where "π ∈ PI" "y ∈ V - α" "π y" "c ∈ place_realise π"
      by auto
    then have "π ∈ {π ∈ PI. π y}" by blast
    moreover
    from finite_PI have "finite {π ∈ PI. π y}" by simp
    ultimately
    have "c ∈ ℳ y" using ‹c ∈ place_realise π›
      using mem_hsubset_HUnion[where ?S = "place_realise ` {π ∈ PI. π y}" and ?s = "place_realise π"]
      by auto
    with ‹y ∈ V - α› show "c ∈ ⨆HF (ℳ ` (V - α))"
      using mem_hsubset_HUnion[where ?S = "ℳ ` (V - α)" and ?s = "ℳ y"]
      using finite_V by blast
  qed
  ultimately
  have "proper_Venn_region α = ⨆HF (place_realise ` {π ∈ PI. ∀x∈α. π x}) - ⨆HF (place_realise ` {π ∈ PI. ∃y∈⋃ (vars ` 𝒞) - α. π y})"
    by auto
  also have "... = ⨆HF (place_realise ` ({π ∈ PI. ∀x ∈ α. π x} - {π ∈ PI. ∃y ∈ V - α. π y}))"
    using HUnion_hdiff_if_image_pairwise_disjoint[where ?f = place_realise and ?U = PI
          and ?S = "{π ∈ PI. ∀x∈α. π x}" and ?T = "{π ∈ PI. ∃y∈⋃ (vars ` 𝒞) - α. π y}"]
    using place_realise_pairwise_disjoint
    by (simp add: finite_PI subsetI)
  moreover
  have "{π ∈ PI. ∀x ∈ α. π x} - {π ∈ PI. ∃y ∈ V - α. π y} = {π ∈ PI. (∀x ∈ α. π x) ∧ (∀y ∈ V - α. ¬ π y)}"
  proof (standard; standard)
    fix π assume "π ∈ {π ∈ PI. ∀x ∈ α. π x} - {π ∈ PI. ∃y ∈ V - α. π y}"
    then have "π ∈ {π ∈ PI. ∀x ∈ α. π x}" "π ∉ {π ∈ PI. ∃y ∈ V - α. π y}"
      by blast+
    from ‹π ∈ {π ∈ PI. ∀x ∈ α. π x}› have "π ∈ PI" "∀x ∈ α. π x" by blast+
    moreover
    from ‹π ∉ {π ∈ PI. ∃y ∈ V - α. π y}› ‹π ∈ PI› have "∀y ∈ V - α. ¬ π y" by blast
    ultimately
    show "π ∈ {π ∈ PI. (∀x ∈ α. π x) ∧ (∀y ∈ V - α. ¬ π y)}" by blast
  next
    fix π assume "π ∈ {π ∈ PI. (∀x ∈ α. π x) ∧ (∀y ∈ V - α. ¬ π y)}"
    then have "π ∈ {π ∈ PI. ∀x ∈ α. π x}" "π ∈ {π ∈ PI. ∀y ∈ V - α. ¬ π y}" by blast+
    then show "π ∈ {π ∈ PI. ∀x ∈ α. π x} - {π ∈ PI. ∃y ∈ V - α. π y}" by blast
  qed
  ultimately
  have 1: "proper_Venn_region α = ⨆HF (place_realise ` {π ∈ PI. (∀x ∈ α. π x) ∧ (∀y ∈ V - α. ¬ π y)})"
    by argo
  
  have "π x ⟷ x ∈ α" if "∀x ∈ α. π x" "∀y ∈ V - α. ¬ π y" and "π ∈ PI" for π x
  proof
    assume "π x"
    with ‹π ∈ PI› PI_subset_places_V places_domain have "x ∈ V"
      by fastforce
    moreover
    from ‹∀y ∈ V - α. ¬ π y› ‹π x› have "x ∉ V - α" by blast
    ultimately
    show "x ∈ α" by blast
  next
    assume "x ∈ α"
    with ‹∀x ∈ α. π x› show "π x" by blast
  qed
  moreover
  have "∀x ∈ α. π x" "∀y ∈ V - α. ¬ π y" if "∀x. π x ⟷ x ∈ α" for π
    using that by blast+
  ultimately
  have 2: "{π ∈ PI. (∀x ∈ α. π x) ∧ (∀y ∈ V - α. ¬ π y)} = {π ∈ PI. ∀x. π x ⟷ x ∈ α}"
    by blast

  from 1 2
  show "proper_Venn_region α = ⨆HF (place_realise ` {π ∈ PI. ∀x. π x ⟷ x ∈ α})"
    by argo    
qed

lemma place_corresponds_to_proper_Venn_region:
  assumes "α ∈ P+ V"
      and "(λx. x ∈ α) ∈ PI"
    shows "proper_Venn_region α = place_realise (λx. x ∈ α)"
proof -
  from proper_Venn_region_place_composition ‹α ∈ P+ V›
  have "proper_Venn_region α = ⨆HF (place_realise ` {π ∈ PI. ∀x. π x = (x ∈ α)})"
    by blast
  moreover
  from ‹(λx. x ∈ α) ∈ PI› have "{π ∈ PI. ∀x. π x = (x ∈ α)} = {λx. x ∈ α}" by blast
  ultimately
  have "proper_Venn_region α = ⨆HF (place_realise ` {λx. x ∈ α})"
    by argo
 then show ?thesis by auto
qed

lemma canonical_assignments_singleton:
  assumes "α ∈ P+ V"
    shows "hcard (proper_Venn_region α) ≤ 1"
proof (cases "(λx. x ∈ α) ∈ PI")
  case True
  with place_corresponds_to_proper_Venn_region ‹α ∈ P+ V›
  have "proper_Venn_region α = place_realise (λx. x ∈ α)" by blast
  with place_realise_singleton True show ?thesis by presburger
next
  case False
  have "¬ (∃π ∈ PI. (∀x. π x = (x ∈ α)))"
  proof (rule ccontr)
    assume "¬ ¬ (∃π∈PI. ∀x. π x = (x ∈ α))"
    then obtain π where "π ∈ PI" "π = (λx. x ∈ α)" by blast
    with False show False by blast
  qed
  then have "{π ∈ PI. ∀x. π x = (x ∈ α)} = {}" by blast
  with proper_Venn_region_place_composition ‹α ∈ P+ V›
  have "proper_Venn_region α = ⨆HF (place_realise ` {})" by presburger
  also have "... = 0" by auto
  finally show ?thesis by auto
qed

end

end