Theory MLSSmf_to_MLSS

theory MLSSmf_to_MLSS
  imports MLSS_Extras MLSS_Decision_Proc.MLSS_Semantics
          MLSSmf_Defs Var_Fun_Composite MLSSmf_to_MLSS_Auxiliary MLSSmf_HF_Extras
begin

fun P_plus :: "'a set ⇒ 'a set set" where
  "P_plus s = Pow s - {{}}"
notation P_plus (‹P⇧+›)

lemma P_plus_finite[intro]: "finite S ⟹ finite (P⇧+ S)"
  unfolding P_plus.simps by blast

lemma mem_P_plus_finite[intro]: "finite S ⟹ s ∈ P⇧+ S ⟹ finite s"
  unfolding P_plus.simps
  by (meson Diff_subset PowD finite_subset in_mono)

lemma mem_P_plus_not_empty[intro]: "finite S ⟹ s ∈ P⇧+ S ⟹ s ≠ {}"
  unfolding P_plus.simps by blast

lemma pow_P_plus_finite[intro]: "finite S ⟹ finite {s. s ⊆ P⇧+ S}"
  unfolding P_plus.simps by blast

lemma pow_of_p_Plus_finite[intro]: "finite V ⟹ finite (Pow (P⇧+ V))"
  using vars_finite pow_P_plus_finite by auto

lemma mem_P_plus_subset[intro]: "α ∈ P⇧+ V ⟹ α ⊆ V"
  by simp

fun ℒ :: "'v set ⇒ 'v ⇒ 'v set set" where
  "ℒ V x = {α ∈ P⇧+ V. x ∈ α}"

lemma ℒ_subset_P_plus:
  "ℒ V x ⊆ P⇧+ V"
  by fastforce

lemma ℒ_finite[intro]: "finite V ⟹ finite (ℒ V x)"
  using pow_of_p_Plus_finite by auto

lemma mem_ℒ_finite[intro]:
  assumes "x ∈ V"
    and "finite V"
      and "α ∈ ℒ V x"
    shows "finite α"
  apply (rule mem_P_plus_finite[where ?S = "V"])
  using ‹finite V› apply blast
  using assms by simp

lemma mem_ℒ_non_empty[intro]:
  assumes "x ∈ V"
      and "α ∈ ℒ V x"
    shows "α ≠ {}"
proof -
  from assms have "x ∈ α" by simp
  then show ?thesis by blast
qed

locale normalized_MLSSmf_clause =
    fixes 𝒞 :: "('v, 'f) MLSSmf_clause"
  assumes norm_𝒞: "norm_clause 𝒞"
begin

definition "V ≡ vars⇩m 𝒞"
definition "V_list ≡ var_list_clause 𝒞"
definition "V_set_list ≡ filter ((≠) {}) (map set (subseqs V_list))"
definition "all_V_set_lists ≡ subseqs V_set_list"
definition "F ≡ funs⇩m 𝒞"
definition "F_list ≡ fun_list_clause 𝒞"
declare V_def V_list_def V_set_list_def F_def F_list_def [simp]

lemma set_V_list: "set V_list = V"
  unfolding V_list_def V_def
  using set_var_list_clause by fast

lemma distinct_V_list: "distinct V_list"
  unfolding V_list_def by simp

lemma finite_V[intro]: "finite V"
  using V_def by auto

fun var_set_to_list :: "'v set ⇒ 'v list" where
  "var_set_to_list α = filter (λx. x ∈ α) V_list"

lemma set_var_set_to_list[intro]: "α ⊆ V ⟹ set (var_set_to_list α) = α"
  using V_def V_list_def by auto

lemma distinct_var_set_to_list[intro]: "distinct (var_set_to_list α)"
  using V_list_def by simp

lemma set_V_set_list: "set V_set_list = P⇧+ V"
proof -
  have "set (filter ((≠) {}) (map set (subseqs V_list))) = set (map set (subseqs V_list)) - {{}}"
    by auto
  moreover
  have "P⇧+ V = Pow V - {{}}" by simp
  moreover
  have "set (map set (subseqs V_list)) = Pow V"
    unfolding V_list_def V_def
    by (simp add: subseqs_powset)
  ultimately
  show ?thesis unfolding V_set_list_def by argo
qed

lemma distinct_V_set_list: "distinct V_set_list"
  unfolding V_set_list_def
  using distinct_V_list
  by (simp add: distinct_set_subseqs)

lemma set_all_V_set_lists: "set (map set all_V_set_lists) = Pow (P⇧+ V)"
  unfolding all_V_set_lists_def
  using set_V_set_list
  by (simp add: subseqs_powset)

lemma distinct_all_V_set_lists: "distinct all_V_set_lists"
  unfolding all_V_set_lists_def
  using distinct_V_set_list distinct_subseqs by blast

lemma set_F_list: "set F_list = F"
  unfolding F_list_def F_def using set_fun_list_clause by fast

fun var_set_set_to_var_set_list :: "'v set set ⇒ 'v set list" where
  "var_set_set_to_var_set_list l = filter (λα. α ∈ l) V_set_list"

lemma var_set_set_to_var_set_list_in_set_all_V_set_lists:
  "var_set_set_to_var_set_list l ∈ set all_V_set_lists"
  unfolding all_V_set_lists_def
  using filter_subseq by auto

lemma set_var_set_set_to_var_set_list[intro]: "l ⊆ P⇧+ V ⟹ set (var_set_set_to_var_set_list l) = l"
  using set_V_set_list by auto 

lemma distinct_var_set_set_to_var_set_list[intro]: "distinct (var_set_set_to_var_set_list l)"
  using distinct_V_set_list by auto

section ‹Step 1 and 2: Generate new variables and add the corresponding conditions into the MLSS-formulae›

text ‹v_α = ⋂{x∈α} \ ⋃{y∉α}›

fun restriction_on_InterOfVars :: "'v list ⇒ ('v, 'f) Composite pset_atom set" where
  "restriction_on_InterOfVars [] = {}"
| "restriction_on_InterOfVars [x] = {Var (InterOfVars [x]) =⇩s Var (Solo x)}"
| "restriction_on_InterOfVars (x # xs) =
   {Var (InterOfVarsAux (x # xs)) =⇩s Var (Solo x) -⇩s Var (InterOfVars xs),
    Var (InterOfVars (x # xs)) =⇩s Var (Solo x) -⇩s Var (InterOfVarsAux (x # xs))} ∪
   restriction_on_InterOfVars xs"

lemma restriction_on_InterOfVar_finite: "finite (restriction_on_InterOfVars xs)"
  by (induction xs rule: restriction_on_InterOfVars.induct) auto

lemma restriction_on_InterOfVar_normalized: "normalized_MLSS_clause (AT ` restriction_on_InterOfVars xs)"
proof
  have "normalized_MLSS_literal lt" if "lt ∈ AT ` restriction_on_InterOfVars xs" for lt
    using that
    apply (induction xs rule: restriction_on_InterOfVars.induct)
      apply simp_all
      apply (meson normalized_MLSS_literal.eq)
     apply (meson normalized_MLSS_literal.diff)
    done
  then show "∀lt∈AT ` restriction_on_InterOfVars xs. normalized_MLSS_literal lt"
    by blast
  from restriction_on_InterOfVar_finite show "finite (AT ` restriction_on_InterOfVars xs)"
    by auto
qed

lemma eval_InterOfVars:
  assumes "∀a ∈ restriction_on_InterOfVars vs. I⇩s⇩a M a"
      and "vs ≠ []"
    shows "M (InterOfVars vs) = ⨅HF ((M ∘ Solo) ` set vs)"
  using assms
proof (induction vs rule: restriction_on_InterOfVars.induct)
  case (2 x)
  then have "I⇩s⇩a M (Var (InterOfVars [x]) =⇩s Var (Solo x))" by simp
  then have "M (InterOfVars [x]) = M (Solo x)" by simp
  moreover
  have "⨅HF ((M ∘ Solo) ` set [x]) = M (Solo x)"
    using HInter_singleton by auto
  ultimately
  show ?case by argo
next
  case (3 y x xs)
  then have IH: "M (InterOfVars (x # xs)) = ⨅HF ((M ∘ Solo) ` set (x # xs))"
    by fastforce
  from "3.prems"(1) have "M (InterOfVars (y # x # xs)) = M (Solo y) ⊓ M (InterOfVars (x # xs))"
    by auto
  also have "... = M (Solo y) ⊓ ⨅HF ((M ∘ Solo) ` set (x # xs))"
    using IH by presburger
  also have "... = ⨅ (HF ((M ∘ Solo) ` set (x # xs)) ◃ M (Solo y))"
    using HInter_def by force
  also have "... = ⨅HF ((M ∘ Solo) ` (insert y (set (x # xs))))"
    using hinsert_def by auto
  also have "... = ⨅ (HF ((M ∘ Solo) ` set (y # x # xs)))"
    by simp
  finally show ?case .
qed blast

fun restriction_on_UnionOfVars :: "'v list ⇒ ('v, 'f) Composite pset_atom set" where
  "restriction_on_UnionOfVars [] = {Var (UnionOfVars []) =⇩s ∅ 0}"
| "restriction_on_UnionOfVars (x # xs) =
   insert (Var (UnionOfVars (x # xs)) =⇩s Var (Solo x) ⊔⇩s Var (UnionOfVars xs))
   (restriction_on_UnionOfVars xs)"

lemma restriction_on_UnionOfVar_finite: "finite (restriction_on_UnionOfVars xs)"
  by (induction xs) auto

lemma restriction_on_UnionOfVar_normalized: "normalized_MLSS_clause (AT ` restriction_on_UnionOfVars xs)"
proof
  have "normalized_MLSS_literal lt" if "lt ∈ AT ` restriction_on_UnionOfVars xs" for lt
    using that
    apply (induction xs rule: restriction_on_UnionOfVars.induct)
     apply simp_all
     apply (meson normalized_MLSS_literal.eq_empty)
    apply (meson normalized_MLSS_literal.union)
    done
  then show "∀lt∈AT ` restriction_on_UnionOfVars xs. normalized_MLSS_literal lt"
    by blast
  from restriction_on_UnionOfVar_finite show "finite (AT ` restriction_on_UnionOfVars xs)"
    by auto
qed

lemma eval_UnionOfVar:
  assumes "∀a ∈ restriction_on_UnionOfVars vs. I⇩s⇩a M a"
    shows "M (UnionOfVars vs) = ⨆HF ((M ∘ Solo) ` set vs)"
  using assms
proof (induction vs rule: restriction_on_UnionOfVars.induct)
  case (2 x xs)
  then have IH: "M (UnionOfVars xs) = ⨆HF ((M ∘ Solo) ` set xs)"
    by fastforce
  from "2.prems" have "M (UnionOfVars (x # xs)) = M (Solo x) ⊔ M (UnionOfVars xs)"
    by simp
  also have "... = M (Solo x) ⊔ ⨆HF ((M ∘ Solo) ` set xs)"
    using IH by presburger
  also have "... = ⨆ (HF ((M ∘ Solo) ` set xs) ◃ M (Solo x))"
    using HInter_def by force
  also have "... = ⨆HF ((M ∘ Solo) ` (insert x (set xs)))"
    using hinsert_def by auto
  also have "... = ⨆ (HF ((M ∘ Solo) ` set (x # xs)))"
    by simp
  finally show ?case .
qed auto

fun restriction_on_v :: "'v set ⇒ ('v, 'f) Composite pset_atom" where
  "restriction_on_v α =
   Var v⇘α⇙ =⇩s Var (InterOfVars (var_set_to_list α)) -⇩s Var (UnionOfVars (var_set_to_list (V - α)))"

lemma v_α_in_vars_restriction_on_v: "v⇘α⇙ ∈ vars (restriction_on_v α)"
  by simp

definition introduce_v :: "('v, 'f) Composite pset_fm set" where
  "introduce_v ≡ AT `
    (restriction_on_v ` (P⇧+ V) ∪
    ⋃ ((restriction_on_InterOfVars ∘ var_set_to_list) ` (P⇧+ V)) ∪
    ⋃ ((restriction_on_UnionOfVars ∘ var_set_to_list) ` (Pow V)))"

lemma introduce_v_finite: "finite introduce_v"
proof -
  have "finite (P⇧+ V)" by blast
  then have "finite (restriction_on_v ` (P⇧+ V))" by blast
  moreover
  from restriction_on_InterOfVar_finite ‹finite (P⇧+ V)›
  have "finite (⋃ ((restriction_on_InterOfVars ∘ var_set_to_list) ` (P⇧+ V)))"
    by auto
  moreover
  from restriction_on_UnionOfVar_finite finite_V
  have "finite (⋃ ((restriction_on_UnionOfVars ∘ var_set_to_list) ` (Pow V)))"
    by force
  ultimately
  show ?thesis unfolding introduce_v_def by auto
qed

lemma introduce_v_normalized: "normalized_MLSS_clause introduce_v"
proof
  have "∀lt ∈ AT ` (restriction_on_v ` P⇧+ V). normalized_MLSS_literal lt"
    by auto (meson normalized_MLSS_literal.diff)
  moreover
  from restriction_on_InterOfVar_normalized
  have "∀α ∈ P⇧+ V. ∀lt ∈ AT ` (restriction_on_InterOfVars ∘ var_set_to_list) α. normalized_MLSS_literal lt"
    using normalized_MLSS_clause.norm_𝒞 by fastforce
  then have "∀lt ∈ AT ` ⋃ ((restriction_on_InterOfVars ∘ var_set_to_list) ` P⇧+ V). normalized_MLSS_literal lt"
    by blast
  moreover
  from restriction_on_UnionOfVar_normalized
  have "∀α ∈ Pow V. ∀lt ∈ AT ` (restriction_on_UnionOfVars ∘ var_set_to_list) α. normalized_MLSS_literal lt"
    using normalized_MLSS_clause.norm_𝒞 by fastforce
  then have "∀lt ∈ AT ` ⋃ ((restriction_on_UnionOfVars ∘ var_set_to_list) ` Pow V). normalized_MLSS_literal lt"
    by blast
  ultimately
  show "∀lt ∈ introduce_v. normalized_MLSS_literal lt"
    unfolding introduce_v_def
    by (metis UnE image_Un)

  from introduce_v_finite show "finite introduce_v" by blast
qed

lemma v_α_in_vars_introduce_v:
  "α ∈ P⇧+ V ⟹ ∃a ∈ introduce_v. v⇘α⇙ ∈ vars a"
proof -
  assume "α ∈ P⇧+ V"
  then have "AT (restriction_on_v α) ∈ introduce_v"
    unfolding introduce_v_def by force
  moreover
  from v_α_in_vars_restriction_on_v have "v⇘α⇙ ∈ vars (restriction_on_v α)" by fast
  then have "v⇘α⇙ ∈ vars (AT (restriction_on_v α))" by simp
  ultimately
  have "AT (restriction_on_v α) ∈ introduce_v ∧ v⇘α⇙ ∈ vars (AT (restriction_on_v α))"
    by fastforce
  then show "∃a ∈ introduce_v. v⇘α⇙ ∈ vars a" by blast
qed

lemma eval_v:
  assumes "α ∈ P⇧+ V"
      and M_model: "∀fm ∈ introduce_v. interp I⇩s⇩a M fm"
    shows "M v⇘α⇙ = ⨅HF ((M ∘ Solo) ` α) - ⨆HF ((M ∘ Solo) ` (V - α))"
proof -
  from ‹α ∈ P⇧+ V› have "set (var_set_to_list α) = α"
    by (meson mem_P_plus_subset set_var_set_to_list)
  have "V - α ⊆ V" by blast
  with set_var_set_to_list have "set (var_set_to_list (V - α)) = V - α" by presburger
  from ‹α ∈ P⇧+ V› have "α ≠ {}" by simp
  with ‹set (var_set_to_list α) = α› have "var_set_to_list α ≠ []" by fastforce

  from ‹α ∈ P⇧+ V› have "AT (restriction_on_v α) ∈ introduce_v" unfolding introduce_v_def by auto
  with M_model have "I⇩s⇩a M (restriction_on_v α)" by fastforce
  then have "M v⇘α⇙ = M (InterOfVars (var_set_to_list α)) - M (UnionOfVars (var_set_to_list (V - α)))"
    by simp
  moreover
  from ‹α ∈ P⇧+ V› have "AT ` (restriction_on_InterOfVars (var_set_to_list α)) ⊆ introduce_v"
    unfolding introduce_v_def by auto
  with M_model have "∀a∈restriction_on_InterOfVars (var_set_to_list α). interp I⇩s⇩a M (AT a)"
    by blast
  then have "∀a∈restriction_on_InterOfVars (var_set_to_list α). I⇩s⇩a M a" by auto
  with eval_InterOfVars[where ?vs = "var_set_to_list α" and ?M = M] M_model
  have "M (InterOfVars (var_set_to_list α)) = ⨅HF ((M ∘ Solo) ` set (var_set_to_list α))"
    using ‹var_set_to_list α ≠ []› by blast
  with ‹set (var_set_to_list α) = α› have "M (InterOfVars (var_set_to_list α)) = ⨅HF ((M ∘ Solo) ` α)"
    by presburger
  moreover
  from ‹α ∈ P⇧+ V› have "V - α ∈ Pow V" by blast
  then have "AT ` (restriction_on_UnionOfVars (var_set_to_list (V - α))) ⊆ introduce_v"
    unfolding introduce_v_def
    by (smt (verit) UN_absorb comp_eq_dest_lhs image_Un sup.absorb_iff2 sup_assoc sup_commute)
  with M_model have "∀a∈restriction_on_UnionOfVars (var_set_to_list (V - α)). interp I⇩s⇩a M (AT a)"
    by blast
  then have "∀a∈(restriction_on_UnionOfVars (var_set_to_list (V - α))). I⇩s⇩a M a" by auto
  with eval_UnionOfVar[where ?vs = "var_set_to_list (V - α)" and ?M = M] M_model
  have "M (UnionOfVars (var_set_to_list (V - α))) = ⨆HF ((M ∘ Solo) ` set (var_set_to_list (V - α)))"
    by blast
  with ‹set (var_set_to_list (V - α)) = V - α›
  have "M (UnionOfVars (var_set_to_list (V - α))) = ⨆HF ((M ∘ Solo) ` (V - α))"
    by presburger
  ultimately
  show ?thesis by argo
qed

lemma v_subset_Inter_of_values:
  assumes "α ≠ {}"
      and "α ⊆ V"
      and "∀fm∈introduce_v. interp I⇩s⇩a M fm"
    shows "M (v⇘α⇙) ≤ ⨅HF (M ` (Solo ` α))"
proof -
  from assms have "α ∈ P⇧+ V" by auto
  with eval_v assms have "M (v⇘α⇙) = ⨅HF ((M ∘ Solo) ` α) - ⨆HF ((M ∘ Solo) ` (V - α))"
    by blast
  then have "M (v⇘α⇙) ≤ ⨅HF ((M ∘ Solo) ` α)" by auto
  then show ?thesis
    by (simp add: image_comp)
qed

fun restriction_on_UnionOfVennRegions :: "'v set list ⇒ ('v, 'f) Composite pset_atom set" where
  "restriction_on_UnionOfVennRegions [] = {Var (UnionOfVennRegions []) =⇩s ∅ 0}"
| "restriction_on_UnionOfVennRegions (α # αs) =
   insert (Var (UnionOfVennRegions (α # αs)) =⇩s (Var v⇘α⇙) ⊔⇩s (Var (UnionOfVennRegions αs)))
   (restriction_on_UnionOfVennRegions αs)"

definition "introduce_UnionOfVennRegions ≡ AT ` ⋃ (restriction_on_UnionOfVennRegions ` set all_V_set_lists)"

lemma introduce_UnionOfVennRegions_normalized: "normalized_MLSS_clause introduce_UnionOfVennRegions"
proof
  have "normalized_MLSS_literal lt" if "lt ∈ AT ` restriction_on_UnionOfVennRegions αs" for lt αs
    using that
    apply (induction αs rule: restriction_on_UnionOfVennRegions.induct)
     apply simp_all
     apply (meson normalized_MLSS_literal.eq_empty)
    apply (meson normalized_MLSS_literal.union)
    done
  then show "∀lt∈introduce_UnionOfVennRegions. normalized_MLSS_literal lt"
    unfolding introduce_UnionOfVennRegions_def
    by blast

  have "finite (restriction_on_UnionOfVennRegions αs)" for αs
    by (induction αs) auto
  moreover
  have "finite (set all_V_set_lists)" by blast
  ultimately
  have "finite (⋃ (restriction_on_UnionOfVennRegions ` set all_V_set_lists))"
    by simp
  then show "finite introduce_UnionOfVennRegions"
    unfolding introduce_UnionOfVennRegions_def by blast
qed

lemma eval_UnionOfVennRegions:
  assumes "∀a ∈ restriction_on_UnionOfVennRegions αs. I⇩s⇩a M a"
    shows "M (UnionOfVennRegions αs) = ⨆HF ((M ∘ VennRegion) ` set αs)"
  using assms
proof (induction αs rule: restriction_on_UnionOfVennRegions.induct)
  case (2 α αs)
  then have IH: "M (UnionOfVennRegions αs) = ⨆HF ((M ∘ VennRegion) ` set αs)"
    by fastforce
  from "2.prems" have "I⇩s⇩a M (Var (UnionOfVennRegions (α # αs)) =⇩s (Var v⇘α⇙) ⊔⇩s (Var (UnionOfVennRegions αs)))"
    by auto
  then have "M (UnionOfVennRegions (α # αs)) = M v⇘α⇙ ⊔ M (UnionOfVennRegions αs)"
    by simp
  also have "... = M v⇘α⇙ ⊔ ⨆HF ((M ∘ VennRegion) ` set αs)"
    using IH by presburger
  also have "... = ⨆ (HF ((M ∘ VennRegion) ` set αs) ◃ M v⇘α⇙)"
    using HInter_def by force
  also have "... = ⨆HF ((M ∘ VennRegion) ` (insert α (set αs)))"
    using hinsert_def by auto
  also have "... = ⨆HF ((M ∘ VennRegion) ` set (α # αs))"
    by simp
  finally show ?case .
qed auto

text ‹⋃{v_α | α ∈ l} = ⋃{v_β | β ∈ m} ==> w_{f,l} = w_{f, m}›
fun restriction_on_FunOfUnionOfVennRegions :: "'v set list ⇒ 'v set list ⇒ 'f ⇒ ('v, 'f) Composite pset_fm list" where
  "restriction_on_FunOfUnionOfVennRegions l m f = [
    AF (Var (UnionOfVennRegions l) =⇩s Var (UnionOfVennRegions m)),
    AT (Var w⇘f⇙⇘set l⇙ =⇩s Var w⇘f⇙⇘set m⇙)]"

lemma restriction_on_FunOfUnionOfVennRegions_normalized:
  "∀lt ∈ set (restriction_on_FunOfUnionOfVennRegions l m f). normalized_MLSS_literal lt"
  apply simp_all
   apply (meson normalized_MLSS_literal.neq)
  apply (meson normalized_MLSS_literal.eq)
  done

fun choices_from_lists :: "'a list list ⇒ 'a list list" where
  "choices_from_lists [] = [[]]" |
  "choices_from_lists (xs # xss) = [x # ys. x ← xs, ys ← choices_from_lists xss]"

lemma choices_from_lists_complete:
  "∀choice ∈ set (choices_from_lists xss). ∀xs ∈ set xss. ∃x ∈ set xs. x ∈ set choice"
  by (induction xss) auto

lemma choices_from_lists_sound:
  "∀choice ∈ set (choices_from_lists xss). ∀x ∈ set choice. ∃xs ∈ set xss. x ∈ set xs"
  by (induction xss) auto

lemma valid_choice:
  assumes "∀x ∈ set xs. f (g x) ∈ set (g x)"
    shows "map f (map g xs) ∈ set (choices_from_lists (map g xs))"
  using assms by (induction xs) auto

definition introduce_w :: "('v, 'f) Composite pset_fm set set" where
  "introduce_w ≡ set (map set (choices_from_lists (map
     (λ(l, m, f). restriction_on_FunOfUnionOfVennRegions l m f)
     (List.product all_V_set_lists (List.product all_V_set_lists F_list)))))"

lemma introduce_w_finite: "finite introduce_w ∧ (∀fms ∈ introduce_w. finite fms)"
  unfolding introduce_w_def by auto

lemma introduce_w_normalized: "∀clause ∈ introduce_w. normalized_MLSS_clause clause"
proof
  let ?fms_before_norm = "(map
     (λ(l, m, f). restriction_on_FunOfUnionOfVennRegions l m f)
     (List.product all_V_set_lists (List.product all_V_set_lists F_list)))"

  fix clause assume "clause ∈ introduce_w"
  then obtain choice where choice:
    "choice ∈ set (choices_from_lists ?fms_before_norm)" "clause = set choice"
    unfolding introduce_w_def by auto
  then have "normalized_MLSS_literal lt" if "lt ∈ set choice" for lt
    using that choices_from_lists_sound
    using restriction_on_FunOfUnionOfVennRegions_normalized
    by fastforce
  moreover
  from choice have "finite clause" by blast
  ultimately
  show "normalized_MLSS_clause clause"
    using ‹clause = set choice›
    by unfold_locales blast+
qed

lemma eval_w:
  assumes M_w: "∃fms ∈ introduce_w. ∀fm ∈ fms. interp I⇩s⇩a M fm"
      and M_UnV: "∀fm ∈ introduce_UnionOfVennRegions. interp I⇩s⇩a M fm"
    shows "∀l ⊆ P⇧+ V. ∀m ⊆ P⇧+ V. ∀f ∈ F.
           ⨆HF ((M ∘ VennRegion) ` l) = ⨆HF ((M ∘ VennRegion) ` m) ⟶
           M w⇘f⇙⇘l⇙ = M w⇘f⇙⇘m⇙"
proof -
  let ?fms_before_norm = "map
     (λ(l, m, f). restriction_on_FunOfUnionOfVennRegions l m f)
     (List.product all_V_set_lists (List.product all_V_set_lists F_list))"
  from M_w obtain fms where "fms ∈ introduce_w" "∀fm ∈ fms. interp I⇩s⇩a M fm"
    by blast
  from ‹fms ∈ introduce_w› obtain clause where "fms = set clause" "clause ∈ set (choices_from_lists ?fms_before_norm)"
    unfolding introduce_w_def by auto
  with choices_from_lists_complete
  have "∀restriction_on_w ∈ set ?fms_before_norm. ∃fm ∈ set restriction_on_w. fm ∈ set clause"
    by blast
  with ‹fms = set clause› have "∀restriction_on_w ∈ set ?fms_before_norm. ∃fm ∈ set restriction_on_w. fm ∈ fms"
    by blast
  with ‹∀fm ∈ fms. interp I⇩s⇩a M fm› have restriction_on_w_all_hold:
    "∀restriction_on_w ∈ set ?fms_before_norm. ∃fm ∈ set restriction_on_w. interp I⇩s⇩a M fm"
    by fast

  from set_all_V_set_lists have "restriction_on_UnionOfVennRegions (var_set_set_to_var_set_list l) ⊆
                                 ⋃ (restriction_on_UnionOfVennRegions ` set all_V_set_lists)"
    if "l ⊆ P⇧+ V" for l
    using that set_var_set_set_to_var_set_list var_set_set_to_var_set_list_in_set_all_V_set_lists
    by (meson Union_upper image_iff)
  with M_UnV have "∀a∈restriction_on_UnionOfVennRegions (var_set_set_to_var_set_list l). I⇩s⇩a M a"
    if "l ⊆ P⇧+ V" for l
    using that unfolding introduce_UnionOfVennRegions_def
    using var_set_set_to_var_set_list_in_set_all_V_set_lists by auto
  with eval_UnionOfVennRegions[of "var_set_set_to_var_set_list l" for l]
  have eval_UnV: "M (UnionOfVennRegions (var_set_set_to_var_set_list l)) = ⨆HF ((M ∘ VennRegion) ` l)"
    if "l ⊆ P⇧+ V" for l
    using that set_var_set_set_to_var_set_list by metis
  
  {fix l m f assume lmf: "l ⊆ P⇧+ V" "m ⊆ P⇧+ V" "f ∈ F"
    let ?l = "var_set_set_to_var_set_list l"
    let ?m = "var_set_set_to_var_set_list m"
    have "(?l, ?m, f) ∈ set (List.product all_V_set_lists (List.product all_V_set_lists F_list))"
      using lmf set_F_list var_set_set_to_var_set_list_in_set_all_V_set_lists
      by simp
    then have "restriction_on_FunOfUnionOfVennRegions ?l ?m f ∈ set ?fms_before_norm"
      by force
    with restriction_on_w_all_hold
    have "∃fm ∈ set (restriction_on_FunOfUnionOfVennRegions ?l ?m f). interp I⇩s⇩a M fm"
      by blast
    then have "interp I⇩s⇩a M (AF (Var (UnionOfVennRegions ?l) =⇩s Var (UnionOfVennRegions ?m))) ∨
               interp I⇩s⇩a M (AT (Var w⇘f⇙⇘l⇙ =⇩s Var w⇘f⇙⇘m⇙))"
      using lmf set_var_set_set_to_var_set_list by auto
    then have "M (UnionOfVennRegions ?l) ≠ M (UnionOfVennRegions ?m) ∨ M w⇘f⇙⇘l⇙ = M w⇘f⇙⇘m⇙"
      by auto
    then have "M (UnionOfVennRegions ?l) = M (UnionOfVennRegions ?m) ⟶ M w⇘f⇙⇘l⇙ = M w⇘f⇙⇘m⇙"
      by blast
    with eval_UnV lmf
    have "⨆HF ((M ∘ VennRegion) ` l) = ⨆HF ((M ∘ VennRegion) ` m) ⟶  M w⇘f⇙⇘l⇙ = M w⇘f⇙⇘m⇙"
      by presburger
  }
  then show ?thesis by blast
qed

lemma lt_in_clause_in_introduce_w_E:
  assumes "∃clause ∈ introduce_w. lt ∈ clause"
  shows "∃l' m' f. l' ∈ set all_V_set_lists ∧ m' ∈ set all_V_set_lists ∧ f ∈ set F_list ∧
                   lt ∈ set (restriction_on_FunOfUnionOfVennRegions l' m' f)"
proof -
  let ?xss = "map
    (λ(l, m, f). restriction_on_FunOfUnionOfVennRegions l m f)
    (List.product all_V_set_lists (List.product all_V_set_lists F_list))"
  from assms obtain clause where "clause ∈ introduce_w" "lt ∈ clause"
    by blast
  with choices_from_lists_sound obtain fms where "fms ∈ set ?xss" "lt ∈ set fms"
    unfolding introduce_w_def by force
  then show ?thesis by fastforce
qed

section ‹Step 3: reduce each literal into MLSS›

fun reduce_atom :: "('v, 'f) MLSSmf_atom ⇒ ('v, 'f) Composite pset_atom set" where
  "reduce_atom (Var⇩m x ∈⇩m Var⇩m y) = {
     Var (MemAux x) =⇩s Single (Var (Solo x)),
     Var (Solo y) =⇩s Var (Solo y) ⊔⇩s Var (MemAux x)}" |
  "reduce_atom (Var⇩m x =⇩m App f (Var⇩m y)) = {Var (Solo x) =⇩s Var w⇘f⇙⇘ℒ V y⇙}" |
  "reduce_atom (Var⇩m x =⇩m Var⇩m y ⊔⇩m Var⇩m z) = {Var (Solo x) =⇩s Var (Solo y) ⊔⇩s Var (Solo z)}" |
  "reduce_atom (Var⇩m x =⇩m Var⇩m y -⇩m Var⇩m z) = {Var (Solo x) =⇩s Var (Solo y) -⇩s Var (Solo z)}" |
  "reduce_atom (Var⇩m x =⇩m Single⇩m (Var⇩m y)) = {Var (Solo x) =⇩s Single (Var (Solo y))}" |
  "reduce_atom (Var⇩m x =⇩m Var⇩m y) = {Var (Solo x) =⇩s Var (Solo y)}" |
  "reduce_atom (Var⇩m x =⇩m ∅⇩m n) = {Var (Solo x) =⇩s ∅ n}" |
  "reduce_atom (inc(f)) = {Var w⇘f⇙⇘m⇙ =⇩s Var w⇘f⇙⇘m⇙ ⊔⇩s Var w⇘f⇙⇘l⇙ |l m.
                             l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V ∧ l ⊆ m}" |
  "reduce_atom (dec(f)) = {Var w⇘f⇙⇘l⇙ =⇩s Var w⇘f⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘m⇙ |l m.
                             l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V ∧ l ⊆ m}" |
  "reduce_atom (add(f)) = {Var w⇘f⇙⇘l∪m⇙ =⇩s Var w⇘f⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘m⇙ |l m.
                             l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V}" |
  "reduce_atom (mul(f)) =
     {Var (InterOfWAux f l m) =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var w⇘f⇙⇘m⇙ |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V} ∪
     {Var w⇘f⇙⇘l∩m⇙ =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var (InterOfWAux f l m) |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V}" |
  "reduce_atom (f ≼⇩m g) = {Var w⇘g⇙⇘l⇙ =⇩s Var w⇘g⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘l⇙ |l. l ⊆ P⇧+ V}" |
  "reduce_atom _ = {}"

lemma reduce_atom_finite: "finite (reduce_atom a)"
  apply (cases a rule: reduce_atom.cases)
                      apply (simp_all del: P_plus.simps)
proof (goal_cases)
  case (1 f)
  have "{Var w⇘f⇙⇘m⇙ =⇩s Var w⇘f⇙⇘m⇙ ⊔⇩s Var w⇘f⇙⇘l⇙ |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V ∧ l ⊆ m} ⊆
        (λ(l, m). Var w⇘f⇙⇘m⇙ =⇩s Var w⇘f⇙⇘m⇙ ⊔⇩s Var w⇘f⇙⇘l⇙) ` ((Pow (P⇧+ V)) × (Pow (P⇧+ V)))"
    by force
  moreover
  from pow_of_p_Plus_finite have "finite ((Pow (P⇧+ V)) × (Pow (P⇧+ V)))"
    by blast
  then have "finite ((λ(l, m). Var w⇘f⇙⇘m⇙ =⇩s Var w⇘f⇙⇘m⇙ ⊔⇩s Var w⇘f⇙⇘l⇙) ` ((Pow (P⇧+ V)) × (Pow (P⇧+ V))))"
    by blast
  ultimately
  show ?case by fastforce
next
  case (2 f)
  have "{Var w⇘f⇙⇘l⇙ =⇩s Var w⇘f⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘m⇙ |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V ∧ l ⊆ m} ⊆
        (λ(l, m). Var w⇘f⇙⇘m⇙ =⇩s Var w⇘f⇙⇘m⇙ ⊔⇩s Var w⇘f⇙⇘l⇙) ` ((Pow (P⇧+ V)) × (Pow (P⇧+ V)))"
    by force
  moreover
  from pow_of_p_Plus_finite have "finite ((Pow (P⇧+ V)) × (Pow (P⇧+ V)))"
    by blast
  then have "finite ((λ(l, m). Var w⇘f⇙⇘l⇙ =⇩s Var w⇘f⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘m⇙) ` ((Pow (P⇧+ V)) × (Pow (P⇧+ V))))"
    by blast
  ultimately
  show ?case by fastforce
next
  case (3 f)
  have "{Var w⇘f⇙⇘l ∪ m⇙ =⇩s Var w⇘f⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘m⇙ |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V} =
        (λ(l, m). Var w⇘f⇙⇘l ∪ m⇙ =⇩s Var w⇘f⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘m⇙) ` ((Pow (P⇧+ V)) × (Pow (P⇧+ V)))"
    by force
  moreover
  from pow_of_p_Plus_finite have "finite ((Pow (P⇧+ V)) × (Pow (P⇧+ V)))"
    by blast
  then have "finite ((λ(l, m). Var w⇘f⇙⇘l ∪ m⇙ =⇩s Var w⇘f⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘m⇙) ` ((Pow (P⇧+ V)) × (Pow (P⇧+ V))))"
    by blast
  ultimately
  show ?case by fastforce
next
  case (4 f)
  have "{Var (InterOfWAux f l m) =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var w⇘f⇙⇘m⇙ |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V} =
        (λ(l, m). Var (InterOfWAux f l m) =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var w⇘f⇙⇘m⇙) ` ((Pow (P⇧+ V)) × (Pow (P⇧+ V)))"
    by force
  moreover
  from pow_of_p_Plus_finite have "finite ((Pow (P⇧+ V)) × (Pow (P⇧+ V)))"
    by blast
  then have "finite ((λ(l, m). Var (InterOfWAux f l m) =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var w⇘f⇙⇘m⇙) ` ((Pow (P⇧+ V)) × (Pow (P⇧+ V))))"
    by blast
  ultimately
  have 1: "finite {Var (InterOfWAux f l m) =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var w⇘f⇙⇘m⇙ |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V}"
    by argo

  have "{Var w⇘f⇙⇘l ∩ m⇙ =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var (InterOfWAux f l m) |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V} =
        (λ(l, m). Var w⇘f⇙⇘l ∩ m⇙ =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var (InterOfWAux f l m)) ` ((Pow (P⇧+ V)) × (Pow (P⇧+ V)))"
    by force
  moreover
  from pow_of_p_Plus_finite have "finite ((Pow (P⇧+ V)) × (Pow (P⇧+ V)))"
    by blast
  then have "finite ((λ(l, m). Var w⇘f⇙⇘l ∩ m⇙ =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var (InterOfWAux f l m)) ` ((Pow (P⇧+ V)) × (Pow (P⇧+ V))))"
    by blast
  ultimately
  have 2: "finite {Var w⇘f⇙⇘l ∩ m⇙ =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var (InterOfWAux f l m) |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V}"
    by argo
  from 1 2 show ?case by blast
next
  case (5 f g)
  have "{Var w⇘g⇙⇘l⇙ =⇩s Var w⇘g⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘l⇙ |l. l ⊆ P⇧+ V} =
        (λl. Var w⇘g⇙⇘l⇙ =⇩s Var w⇘g⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘l⇙) ` Pow (P⇧+ V)"
    by blast
  with pow_of_p_Plus_finite show ?case by auto
qed

fun reduce_literal :: "('v, 'f) MLSSmf_literal ⇒ ('v, 'f) Composite pset_fm set" where
  "reduce_literal (AT⇩m a) = AT ` (reduce_atom a)" |
  "reduce_literal (AF⇩m a) = AF ` (reduce_atom a)"

lemma reduce_literal_finite: "finite (reduce_literal lt)"
  by (cases lt) (simp add: reduce_atom_finite)+

lemma reduce_literal_normalized:
  assumes "lt ∈ set 𝒞"
    shows "normalized_MLSS_clause (reduce_literal lt)"
proof -
  from assms norm_𝒞 have "norm_literal lt" by blast
  then show ?thesis
  proof (cases lt rule: norm_literal.cases)
    case (inc f)
    then have "reduce_literal lt =
      AT ` {Var w⇘f⇙⇘m⇙ =⇩s Var w⇘f⇙⇘m⇙ ⊔⇩s Var w⇘f⇙⇘l⇙ |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V ∧ l ⊆ m}"
      by simp
    then show ?thesis
      apply unfold_locales
      using normalized_MLSS_literal.union
       apply force
      by (meson reduce_literal_finite)
  next
    case (dec f)
    then have "reduce_literal lt =
      AT ` {Var w⇘f⇙⇘l⇙ =⇩s Var w⇘f⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘m⇙ |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V ∧ l ⊆ m}"
      by simp
    then show ?thesis
      apply unfold_locales
      using normalized_MLSS_literal.union
       apply force
      by (meson reduce_literal_finite)
  next
    case (add f)
    then have "reduce_literal lt =
      AT ` {Var w⇘f⇙⇘l∪m⇙ =⇩s Var w⇘f⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘m⇙ |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V}"
      by simp
    then show ?thesis
      apply unfold_locales
      using normalized_MLSS_literal.union
       apply force
      by (meson reduce_literal_finite)
  next
    case (mul f)
    then have "reduce_literal lt = AT ` (
      {Var (InterOfWAux f l m) =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var w⇘f⇙⇘m⇙ |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V} ∪
      {Var w⇘f⇙⇘l∩m⇙ =⇩s Var w⇘f⇙⇘l⇙ -⇩s Var (InterOfWAux f l m) |l m. l ⊆ P⇧+ V ∧ m ⊆ P⇧+ V})"
      by simp
    then show ?thesis
      apply unfold_locales
      using normalized_MLSS_literal.diff
       apply force
      by (meson reduce_literal_finite)
  next
    case (le f g)
    then have "reduce_literal lt =
      AT ` {Var w⇘g⇙⇘l⇙ =⇩s Var w⇘g⇙⇘l⇙ ⊔⇩s Var w⇘f⇙⇘l⇙ |l. l ⊆ P⇧+ V}"
      by simp
    then show ?thesis
      apply unfold_locales
      using normalized_MLSS_literal.union
       apply force
      by (meson reduce_literal_finite)
  next
    case (eq_empty x n)
    then have "reduce_literal lt = AT ` {Var (Solo x) =⇩s ∅ n}"
      by simp
    then show ?thesis 
      apply unfold_locales
      using normalized_MLSS_literal.eq_empty
       apply force
      by (meson reduce_literal_finite)
  next
    case (eq x y)
    then have "reduce_literal lt = AT ` {Var (Solo x) =⇩s Var (Solo y)}"
      by simp
    then show ?thesis 
      apply unfold_locales
      using normalized_MLSS_literal.eq
       apply force
      by (meson reduce_literal_finite)
  next
    case (neq x y)
    then have "reduce_literal lt = AF ` {Var (Solo x) =⇩s Var (Solo y)}"
      by simp
    then show ?thesis 
      apply unfold_locales
      using normalized_MLSS_literal.neq
       apply force
      by (meson reduce_literal_finite)
  next
    case (union x y z)
    then show ?thesis
      apply simp
      using normalized_MLSS_literal.union
      by (metis finite.emptyI finite.insertI normalized_MLSS_clause.intro singletonD)
  next
    case (diff x y z)
    then show ?thesis
      apply simp
      using normalized_MLSS_literal.diff
      by (metis finite.emptyI finite.insertI normalized_MLSS_clause.intro singletonD)
  next
    case (single x y)
    then show ?thesis
      apply simp
      using normalized_MLSS_literal.singleton
      by (metis finite.emptyI finite.insertI normalized_MLSS_clause.intro singletonD)
  next
    case (app x f y)
    then show ?thesis
      apply simp
      using normalized_MLSS_literal.eq
      using normalized_MLSS_clause_def by fastforce
  qed
qed

definition reduce_clause :: "('v, 'f) Composite pset_fm set" where
  "reduce_clause = ⋃ (reduce_literal ` set 𝒞)"

lemma reduce_clause_finite: "finite reduce_clause"
proof -
  have "finite (set 𝒞)" by simp
  have "∀lt ∈ set 𝒞. finite (reduce_literal lt)"
    using reduce_literal_finite by fast
  then have "finite reduce_clause"
    using ‹finite (set 𝒞)›
    unfolding reduce_clause_def by simp
  then show ?thesis by argo
qed

lemma reduce_clause_normalized: "normalized_MLSS_clause reduce_clause"
  using reduce_literal_normalized
  by (simp add: normalized_MLSS_clause_def reduce_clause_def)

section ‹Finalize: collect everything and get the final MLSS-formulae›

definition reduced_dnf :: "('v, 'f) Composite pset_fm set set" where
  "reduced_dnf ≡ (λfms. fms ∪ introduce_v ∪ introduce_UnionOfVennRegions ∪ reduce_clause) ` introduce_w"

lemma introduce_v_subset_reduced_fms: "∀fms ∈ reduced_dnf. introduce_v ⊆ fms"
  unfolding reduced_dnf_def by blast

lemma introduce_w_subset_reduced_fms: "∀fms ∈ reduced_dnf. ∃fms_w ∈ introduce_w. fms_w ⊆ fms"
  unfolding reduced_dnf_def by blast

lemma reduce_clause_subset_reduced_fms: "∀fms ∈ reduced_dnf. reduce_clause ⊆ fms"
  unfolding reduced_dnf_def by blast

lemma introduce_UnionOfVennRegions_subset_reduced_fms:
  "∀fms ∈ reduced_dnf. introduce_UnionOfVennRegions ⊆ fms"
  unfolding reduced_dnf_def by blast

lemma reduced_dnf_normalized:
  "∀clause ∈ reduced_dnf. normalized_MLSS_clause clause"
proof
  fix clause assume "clause ∈ reduced_dnf"
  then obtain clause_w where "clause_w ∈ introduce_w" "clause = clause_w ∪ introduce_v ∪ introduce_UnionOfVennRegions ∪ reduce_clause"
    unfolding reduced_dnf_def by blast
  then show "normalized_MLSS_clause clause"
    using introduce_v_normalized introduce_UnionOfVennRegions_normalized reduce_clause_normalized introduce_w_normalized
    by (metis UnE finite_UnI normalized_MLSS_clause_def)
qed

lemma normalized_clause_contains_all_v_α:
  assumes "clause ∈ reduced_dnf"
    shows "∀α ∈ P⇧+ V. v⇘α⇙ ∈ ⋃ (vars ` clause)"
proof
  fix α assume "α ∈ P⇧+ V"
  with assms have "AT (restriction_on_v α) ∈ clause"
    unfolding reduced_dnf_def introduce_v_def
    by blast
  moreover
  from v_α_in_vars_restriction_on_v have "v⇘α⇙ ∈ vars (restriction_on_v α)"
    by blast
  ultimately
  show "v⇘α⇙ ∈ ⋃ (vars ` clause)"
    by force
qed

definition is_model_for_reduced_dnf :: "(('v, 'f) Composite ⇒ hf) ⇒ bool" where
  "is_model_for_reduced_dnf ℳ ≡ ∃clause ∈ reduced_dnf. ∀fm ∈ clause. interp I⇩s⇩a ℳ fm"

end

end