Theory Proper_Venn_Regions

theory Proper_Venn_Regions
  imports MLSSmf_Semantics MLSSmf_to_MLSS MLSSmf_HF_Extras
begin

locale proper_Venn_regions =
    fixes V :: "'a set"
      and 𝒜 :: "'a ⇒ hf"
  assumes finite_V: "finite V"
begin

fun proper_Venn_region :: "'a set ⇒ hf" where
  "proper_Venn_region α = ⨅HF (𝒜 ` α) - ⨆HF (𝒜 ` (V - α))"

lemma proper_Venn_region_nonempty_iff[iff]:
  "c ❙∈ proper_Venn_region α ∧ α ⊆ V ⟷ α = {x ∈ V. c ❙∈ 𝒜 x} ∧ α ≠ {}"
proof(standard, goal_cases)
  case 1
  then have "c ❙∈ proper_Venn_region α" "α ⊆ V" by blast+
  show ?case
  proof(standard, standard, goal_cases)
    case 1
    then show ?case
    proof
      fix x assume "x ∈ α"
      have "c ❙∈ ⨅HF (𝒜 ` α)"
        using ‹c ❙∈ proper_Venn_region α› by auto
      then have "c ❙∈ 𝒜 x"
        using ‹x ∈ α›
        by (metis (mono_tags, opaque_lifting) HInter_hempty HInter_iff hempty_iff hmem_HF_iff imageI)
      then show "x ∈ {x ∈ V. c ❙∈ 𝒜 x}"
        using ‹α ⊆ V› ‹x ∈ α› by blast
    qed
  next
    case 2
    then show ?case
    proof
      fix x assume "x ∈ {x ∈ V. c ❙∈ 𝒜 x}"
      then have "x ∈ V" "c ❙∈ 𝒜 x" by blast+
      show "x ∈ α"
      proof (rule ccontr)
        assume "x ∉ α"
        then have "x ∈ V - α"
          using ‹α ⊆ V› ‹x ∈ V› by blast
        then have "c ❙∈ ⨆HF (𝒜 ` (V - α))"
          using ‹c ❙∈ 𝒜 x› finite_V by auto
        then have "c ❙∉ proper_Venn_region α" by simp
        then show False
          using ‹c ❙∈ proper_Venn_region α› by blast
      qed
    qed
  next
    case 3
    then show ?case
    proof (rule ccontr)
      assume "¬ α ≠ {}"
      then have "α = {}" by fast
      then have "proper_Venn_region α = 0"
        using Zero_hf_def by auto
      then show False
        using ‹c ❙∈ proper_Venn_region α› by simp
    qed
  qed
next
  case 2
  then have "α = {x ∈ V. c ❙∈ 𝒜 x}" "α ≠ {}" by simp+
  then have "α ⊆ V" by blast
  moreover
  from 2 finite_V have "finite α" by force
  then have "finite (𝒜 ` α)" by blast
  then have "finite (𝒜 ` (V - α))"
    using finite_V by fast
  from ‹α ≠ {}› have "𝒜 ` α ≠ {}" by blast
  from 2 have "∀x ∈ α. c ❙∈ 𝒜 x" by simp
  then have "∀x ∈ 𝒜 ` α. c ❙∈ x" by blast
  then have "c ❙∈ ⨅HF (𝒜 ` α)"
    using ‹finite (𝒜 ` α)› ‹𝒜 ` α ≠ {}›
    by (metis HInter_iff hfset_0 hfset_HF hmem_HF_iff)
  moreover
  have "c ❙∉ ⨆HF (𝒜 ` (V - α))"
  proof
    assume "c ❙∈ ⨆HF (𝒜 ` (V - α))"
    then obtain x where "c ❙∈ x" "x ∈ 𝒜 ` (V - α)" by auto
    then have "x ∈ 𝒜 ` (V) - 𝒜 ` α"
      using 2 by fastforce
    then have "x ∉ 𝒜 ` α" by blast
    then show False
      using ‹c ❙∈ x› 2 ‹x ∈ 𝒜 ` (V - α)› by blast 
  qed
  ultimately show ?case by auto
qed

lemma proper_Venn_region_strongly_injective:
  assumes "proper_Venn_region α ⊓ proper_Venn_region β ≠ 0"
      and "α ⊆ V"
      and "β ⊆ V"
    shows "α = β"
proof -
  from ‹proper_Venn_region α ⊓ proper_Venn_region β ≠ 0›
  obtain c where c: "c ❙∈ proper_Venn_region α" "c ❙∈ proper_Venn_region β"
    by blast
  then have "α = {x ∈ V. c ❙∈ 𝒜 x}" "β = {x ∈ V. c ❙∈ 𝒜 x}"
    using ‹α ⊆ V› ‹β ⊆ V›
    using proper_Venn_region_nonempty_iff by (metis (mono_tags, lifting))+
  then show "α = β" by presburger
qed

lemma proper_Venn_region_disjoint:
  "α ≠ β ⟹ α ⊆ V ⟹ β ⊆ V ⟹ proper_Venn_region α ⊓ proper_Venn_region β = 0"
  using proper_Venn_region_strongly_injective by meson

lemma HUnion_proper_Venn_region_union:
  assumes "l ⊆ P⇧+ V"
      and "m ⊆ P⇧+ V"
    shows "⨆HF (proper_Venn_region ` (l ∪ m)) = ⨆HF (proper_Venn_region ` l) ⊔ ⨆HF(proper_Venn_region ` m)"
  by (metis HUnion_hunion P_plus_finite assms(1) assms(2) finite_V finite_imageI finite_subset image_Un union_hunion)

lemma HUnion_proper_Venn_region_inter:
  assumes "l ⊆ P⇧+ V"
      and "m ⊆ P⇧+ V"
    shows "⨆HF (proper_Venn_region ` (l ∩ m)) = ⨆HF (proper_Venn_region ` l) ⊓ ⨆HF(proper_Venn_region ` m)"
proof -
  from ‹l ⊆ P⇧+ V› have "finite l"
    using finite_V P_plus_finite by (metis finite_subset)
  from ‹m ⊆ P⇧+ V› have "finite m"
    using finite_V P_plus_finite by (metis finite_subset)
  
  have "⨆HF (proper_Venn_region ` (l ∩ m)) ≤ ⨆HF (proper_Venn_region ` l) ⊓ ⨆HF (proper_Venn_region ` m)"
    using proper_Venn_region_disjoint ‹finite l› ‹finite m›
    by auto
  moreover
  have "c ❙∈ ⨆HF (proper_Venn_region ` (l ∩ m))" if "c ❙∈ ⨆HF (proper_Venn_region ` l) ⊓ ⨆HF (proper_Venn_region ` m)" for c
  proof -
    from that have "c ❙∈ ⨆HF (proper_Venn_region ` l)" "c ❙∈ ⨆HF (proper_Venn_region ` m)" by blast+
    then obtain α β where "α ∈ l" "β ∈ m" and c_mem: "c ❙∈ proper_Venn_region α" "c ❙∈ proper_Venn_region β" by auto
    with ‹l ⊆ P⇧+ V› ‹m ⊆ P⇧+ V› finite_V have "α ⊆ V" "β ⊆ V" by auto
    with proper_Venn_region_strongly_injective c_mem have "α = β" by blast
    with ‹α ∈ l› ‹β ∈ m› have "α ∈ l ∩ m" by blast
    with c_mem show ?thesis
      using HUnion_iff ‹finite l› hmem_def by auto 
  qed
  then have "⨆HF (proper_Venn_region ` l) ⊓ ⨆HF (proper_Venn_region ` m) ≤ ⨆HF (proper_Venn_region ` (l ∩ m))" by blast
  ultimately show ?thesis by order
qed

text ‹⋃_{α∈L_y} v_α = y›
lemma variable_as_composition_of_proper_Venn_regions:
  assumes "y ∈ V"
    shows "⨆HF (proper_Venn_region ` ℒ V y) = 𝒜 y"
proof(standard; standard)
  fix c assume c: "c ❙∈ ⨆HF (proper_Venn_region ` (ℒ V y))"
  then obtain α where α: "α ∈ ℒ V y" "c ❙∈ proper_Venn_region α"
    by auto
  then have "y ∈ α" using ‹y ∈ V› by fastforce
  then have "𝒜 y ∈ 𝒜 ` α" by blast
  from finite_V ‹α ∈ ℒ V y› ‹y ∈ V› have "finite α" "α ≠ {}" by auto
  then have "finite (𝒜 ` α)" "𝒜 ` α ≠ {}" by simp+
  with ‹𝒜 y ∈ 𝒜 ` α› have "⨅(HF (𝒜 ` α)) ≤ 𝒜 y"
    by (metis HInter_iff hfset_0 hfset_HF hmem_HF_iff hsubsetI)
  then show "c ❙∈ 𝒜 y"
    using α by fastforce
next
  fix c assume "c ❙∈ 𝒜 y"
  let ?α = "{x ∈ V. c ❙∈ 𝒜 x}"
  from ‹c ❙∈ 𝒜 y› ‹y ∈ V› have "y ∈ ?α" by blast
  then have "?α ∈ ℒ V y" by auto
  then have "?α ≠ {}" by auto
  then have "c ❙∈ proper_Venn_region ?α"
    using proper_Venn_region_nonempty_iff
    by (metis (mono_tags, lifting))
  moreover
  from ‹?α ∈ ℒ V y› have "proper_Venn_region ?α ∈ proper_Venn_region ` ℒ V y" by fast
  moreover
  have "finite (ℒ V y)" using finite_V by simp
  ultimately
  show "c ❙∈ ⨆HF (proper_Venn_region ` (ℒ V y))"
    by (smt (verit, best) HUnion_iff finite_imageI hmem_HF_iff)
qed

lemma proper_Venn_region_subset_variable_iff:
  assumes "α ⊆ V"
      and "x ∈ V"
      and "proper_Venn_region α ≠ 0"
    shows "x ∈ α ⟷ proper_Venn_region α ≤ 𝒜 x"
proof
  assume "x ∈ α"
  then have "⨅HF (𝒜 ` α) ≤ 𝒜 x" using ‹α ⊆ V› finite_V
    by (smt (verit, ccfv_SIG) HInter_iff ball_imageD finite_imageI hemptyE hmem_HF_iff hsubsetI rev_finite_subset)
  then show "proper_Venn_region α ≤ 𝒜 x" by auto
next
  assume "proper_Venn_region α ≤ 𝒜 x"
  moreover
  from variable_as_composition_of_proper_Venn_regions ‹x ∈ V›
  have "𝒜 x = ⨆HF (proper_Venn_region ` ℒ V x)"
    by presburger
  ultimately
  have "proper_Venn_region α ≤ ⨆HF (proper_Venn_region ` ℒ V x)"
    by argo
  show "x ∈ α"
  proof (rule ccontr)
    assume "x ∉ α"
    then have "α ∉ ℒ V x" by simp
    moreover
    from ‹proper_Venn_region α ≤ ⨆HF (proper_Venn_region ` ℒ V x)› ‹proper_Venn_region α ≠ 0›
    have "proper_Venn_region α ⊓ ⨆HF (proper_Venn_region ` ℒ V x) ≠ 0" by fast
    then obtain β where "β ∈ ℒ V x" "proper_Venn_region α ⊓ proper_Venn_region β ≠ 0"
      by auto
    with proper_Venn_region_strongly_injective have "α = β"
      using ‹β ∈ ℒ V x› ‹α ⊆ V› by auto
    with ‹β ∈ ℒ V x› have "α ∈ ℒ V x" by blast
    ultimately
    show False by blast
  qed
qed

end

end