Theory MLSSmf_to_MLSS_Soundness

theory MLSSmf_to_MLSS_Soundness
  imports MLSSmf_to_MLSS MLSSmf_Semantics Proper_Venn_Regions MLSSmf_HF_Extras
begin

locale satisfiable_normalized_MLSSmf_clause =
  normalized_MLSSmf_clause š’ž for š’ž :: "('v, 'f) MLSSmf_clause" +
    fixes Mv :: "'v ā‡’ hf"
      and Mf :: "'f ā‡’ hf ā‡’ hf"
  assumes model_for_š’ž: "Icl Mv Mf š’ž"
begin

interpretation proper_Venn_regions V Mv
  using finite_V by unfold_locales

function ā„³ :: "('v, 'f) Composite ā‡’ hf" where
  "ā„³ (Solo x)  = Mv x"
| "ā„³ (vā‡˜Ī±ā‡™)    = proper_Venn_region Ī±"
| "ā„³ (UnionOfVennRegions xss) = ā؆HF ((ā„³ āˆ˜ VennRegion) ` set xss)"
| "ā„³ (wā‡˜fā‡™ā‡˜lā‡™) = (Mf f) (ā„³ (UnionOfVennRegions (var_set_set_to_var_set_list l)))"
| "ā„³ (UnionOfVars xs) = ā؆HF (Mv ` set xs)"
| "ā„³ (InterOfVars xs) = ā؅HF (Mv ` set xs)"
| "ā„³ (MemAux x) = HF {Mv x}"
| "ā„³ (InterOfWAux f l m) = ā„³ wā‡˜fā‡™ā‡˜lā‡™ - ā„³ wā‡˜fā‡™ā‡˜mā‡™"
| "ā„³ (InterOfVarsAux xs) = Mv (hd xs) - ā„³ (InterOfVars (tl xs))"
  by pat_completeness auto
termination
  apply (relation "measure (Ī»comp. case comp of
                    InterOfVarsAux _ ā‡’ Suc 0
                  | UnionOfVennRegions _ ā‡’ Suc 0
                  | wā‡˜_ā‡™ā‡˜_ā‡™ ā‡’ Suc (Suc 0)
                  | InterOfWAux _ _ _ ā‡’ Suc (Suc (Suc 0))
                  | _ ā‡’ 0)")
       apply auto
  done

lemma soundness_restriction_on_InterOfVars:
  assumes "set xs āˆˆ P+ V"
    shows "āˆ€a āˆˆ restriction_on_InterOfVars xs. Isa ā„³ a"
proof (induction xs rule: restriction_on_InterOfVars.induct)
  case (2 x)
  {fix a assume "a āˆˆ restriction_on_InterOfVars [x]"
    then have "a = Var (InterOfVars [x]) =s Var (Solo x)" by simp
    then have "Isa ā„³ a" by (simp add: HInter_singleton)
  }
  then show ?case by blast
next
  case (3 y x xs)
  {fix a assume "a āˆˆ restriction_on_InterOfVars (y # x # xs) - restriction_on_InterOfVars (x # xs)"
    then consider "a = Var (InterOfVarsAux (y # x # xs)) =s Var (Solo y) -s Var (InterOfVars (x # xs))"
                | "a = Var (InterOfVars (y # x # xs)) =s Var (Solo y) -s Var (InterOfVarsAux (y # x # xs))"
      by fastforce
    then have "Isa ā„³ a"
    proof (cases)
      case 1
      then show ?thesis by simp
    next
      case 2
      have "ā؅HF (insert (Mv y) (insert (Mv x) (Mv ` set xs))) =
            ā؅ (HF ((insert (Mv x) (Mv ` set xs))) ā—ƒ Mv y)"
        using HF_insert_hinsert by auto
      also have "... = Mv y āŠ“ ā؅HF (insert (Mv x) (Mv ` set xs))"
        by (simp add: HF_nonempty)
      also have "... = Mv y - (Mv y - ā؅HF (insert (Mv x) (Mv ` set xs)))"
        by blast
      finally show ?thesis using 2 by simp
    qed
  }
  with "3.IH" show ?case by blast
qed simp

lemma soundness_restriction_on_UnionOfVars:
  assumes "set xs āˆˆ Pow V"
    shows "āˆ€a āˆˆ restriction_on_UnionOfVars xs. Isa ā„³ a"
proof (induction xs rule: restriction_on_UnionOfVars.induct)
  case 1
  then show ?case by auto
next
  case (2 x xs)
  {fix a assume "a āˆˆ restriction_on_UnionOfVars (x # xs) - restriction_on_UnionOfVars xs"
    then have a: "a = Var (UnionOfVars (x # xs)) =s Var (Solo x) āŠ”s Var (UnionOfVars xs)"
      by fastforce
    have "ā؆HF (insert (Mv x) (Mv ` set xs)) = ā؆ (HF (Mv ` set xs) ā—ƒ Mv x)"
      by (simp add: HF_insert_hinsert)
    also have "... = Mv x āŠ” ā؆HF (Mv ` set xs)" by auto
    finally have "Isa ā„³ a"
      using a by simp
  }
  with "2.IH" show ?case by blast
qed

lemma soundness_introduce_v:
  "āˆ€fml āˆˆ introduce_v. interp Isa ā„³ fml"
proof -
  {fix Ī± assume "Ī± āˆˆ P+ V"
    have "ā„³ vā‡˜Ī±ā‡™ = ā؅HF (Mv ` Ī±) - ā؆HF (Mv ` (V - Ī±))"
      by simp
    also have "... = ā؅HF ((ā„³ āˆ˜ Solo) ` Ī±) - ā؆HF ((ā„³ āˆ˜ Solo) ` (V - Ī±))"
      by simp
    finally have "Isa ā„³ (restriction_on_v Ī±)"
      apply (simp add: set_V_list)
      using ā€¹Ī± āˆˆ P+ Vā€ŗ
      by (metis Int_def inf.absorb2 mem_P_plus_subset set_diff_eq)
  }
  then have "āˆ€Ī± āˆˆ P+ V. interp Isa ā„³ (AT (restriction_on_v Ī±))"
    by simp
  moreover
  from soundness_restriction_on_InterOfVars
  have "āˆ€a āˆˆ (restriction_on_InterOfVars āˆ˜ var_set_to_list) Ī±. Isa ā„³ a" if "Ī± āˆˆ P+ V" for Ī±
    by (metis comp_apply mem_P_plus_subset set_var_set_to_list that)
  then have "āˆ€lt āˆˆ AT ` ā‹ƒ ((restriction_on_InterOfVars āˆ˜ var_set_to_list) ` P+ V). interp Isa ā„³ lt"
    by fastforce
  moreover
  from soundness_restriction_on_UnionOfVars
  have "āˆ€a āˆˆ (restriction_on_UnionOfVars āˆ˜ var_set_to_list) Ī±. Isa ā„³ a" if "Ī± āˆˆ Pow V" for Ī±
    by (metis Pow_iff comp_apply set_var_set_to_list that)
  then have "āˆ€lt āˆˆ AT ` ā‹ƒ ((restriction_on_UnionOfVars āˆ˜ var_set_to_list) ` Pow V). interp Isa ā„³ lt"
    by fastforce
  ultimately
  show ?thesis
    unfolding introduce_v_def by blast
qed

lemma soundness_restriction_on_UnionOfVennRegions:
  assumes "set Ī±s āˆˆ Pow (Pow V)"
    shows "āˆ€a āˆˆ restriction_on_UnionOfVennRegions Ī±s. Isa ā„³ a"
proof (induction Ī±s rule: restriction_on_UnionOfVennRegions.induct)
  case 1
  then show ?case by auto
next
  case (2 Ī± Ī±s)
  {fix a assume "a āˆˆ restriction_on_UnionOfVennRegions (Ī± # Ī±s) - restriction_on_UnionOfVennRegions Ī±s"
    then have a: "a = Var (UnionOfVennRegions (Ī± # Ī±s)) =s Var vā‡˜Ī±ā‡™ āŠ”s Var (UnionOfVennRegions Ī±s)"
      by fastforce
    have "ā؆HF ((ā„³ āˆ˜ VennRegion) ` set (Ī± # Ī±s)) = ā؆HF (insert (ā„³ vā‡˜Ī±ā‡™) ((ā„³ āˆ˜ VennRegion) ` set Ī±s))"
      by simp
    also have "... = ā؆ (HF ((ā„³ āˆ˜ VennRegion) ` set Ī±s) ā—ƒ ā„³ vā‡˜Ī±ā‡™)"
      by (simp add: HF_insert_hinsert)
    also have "... = ā„³ vā‡˜Ī±ā‡™ āŠ” ā؆HF ((ā„³ āˆ˜ VennRegion) ` set Ī±s)"
      by blast
    finally have "Isa ā„³ a" using a by simp
  }
  with "2.IH" show ?case by blast
qed

lemma soundness_introduce_UnionOfVennRegions:
  "āˆ€lt āˆˆ introduce_UnionOfVennRegions. interp Isa ā„³ lt"
proof
  fix lt assume "lt āˆˆ introduce_UnionOfVennRegions"
  then obtain Ī±s where "Ī±s āˆˆ set all_V_set_lists" "lt āˆˆ AT ` restriction_on_UnionOfVennRegions Ī±s"
    unfolding introduce_UnionOfVennRegions_def by blast
  with soundness_restriction_on_UnionOfVennRegions
  show "interp Isa ā„³ lt"
    using set_all_V_set_lists by fastforce
qed

lemma soundness_restriction_on_FunOfUnionOfVennRegions:
  assumes l'_l: "l' = var_set_set_to_var_set_list l"
      and m'_m: "m' = var_set_set_to_var_set_list m"
    shows "āˆƒlt āˆˆ set (restriction_on_FunOfUnionOfVennRegions l' m' f). interp Isa ā„³ lt"
proof (cases "ā„³ (UnionOfVennRegions l') = ā„³ (UnionOfVennRegions m')")
  case True
  then have "ā„³ wā‡˜fā‡™ā‡˜lā‡™ = ā„³ wā‡˜fā‡™ā‡˜mā‡™"
    using l'_l m'_m by auto
  then have "interp Isa ā„³ (AT (Var wā‡˜fā‡™ā‡˜set l'ā‡™ =s Var wā‡˜fā‡™ā‡˜set m'ā‡™))"
    using l'_l m'_m by auto
  then show ?thesis by simp
next
  case False
  then have "interp Isa ā„³ (AF (Var (UnionOfVennRegions l') =s Var (UnionOfVennRegions m')))"
    by fastforce
  then show ?thesis by simp
qed

lemma soundness_introduce_w:
  "āˆƒclause āˆˆ introduce_w. āˆ€lt āˆˆ clause. interp Isa ā„³ lt"
proof -
  let ?f = "Ī»lts. if interp Isa ā„³ (lts ! 0) then lts ! 0 else lts ! 1"
  let ?g = "Ī»(l, m, f). restriction_on_FunOfUnionOfVennRegions l m f"
  let ?xs = "List.product all_V_set_lists (List.product all_V_set_lists F_list)"
  have "āˆ€(l', m', f) āˆˆ set ?xs. ?f (?g (l', m', f)) āˆˆ set (?g (l', m', f))"
    by fastforce
  with valid_choice[where ?f = ?f and ?g = ?g and ?xs = ?xs]
  have "map ?f (map ?g ?xs) āˆˆ set (choices_from_lists (map ?g ?xs))"
    by fast
  then have "set (map ?f (map ?g ?xs)) āˆˆ introduce_w"
    unfolding introduce_w_def
    using mem_set_map[where ?x = "map ?f (map ?g ?xs)" and ?f = set]
    by blast
  moreover
  have "{x āˆˆ set V_set_list. x āˆˆ set l'} = set l'" if "l' āˆˆ set all_V_set_lists" for l'
    using that set_V_set_list set_all_V_set_lists by auto
  then have "interp Isa ā„³ (?f (restriction_on_FunOfUnionOfVennRegions l' m' f))"
    if "l' āˆˆ set all_V_set_lists" "m' āˆˆ set all_V_set_lists" for l' m' f
    using that by auto
  then have "āˆ€lt āˆˆ set (map ?f (map ?g ?xs)). interp Isa ā„³ lt"
    by force
  ultimately
  show ?thesis by blast
qed

lemma soundness_reduce_literal:
  assumes "lt āˆˆ set š’ž"
    shows "āˆ€fml āˆˆ reduce_literal lt. interp Isa ā„³ fml"
proof -
  from norm_š’ž ā€¹lt āˆˆ set š’žā€ŗ have "norm_literal lt" by auto
  then show ?thesis
  proof (cases rule: norm_literal.cases)
    case (inc f)
    show ?thesis
    proof
      fix fml assume "fml āˆˆ reduce_literal lt"
      then have "fml āˆˆ reduce_literal (ATm (inc(f)))"
        using inc by blast
      then obtain l m where lm: "l āŠ† P+ V" "m āŠ† P+ V" "l āŠ† m"
                        and fml: "fml = AT (Var wā‡˜fā‡™ā‡˜mā‡™ =s Var wā‡˜fā‡™ā‡˜mā‡™ āŠ”s Var wā‡˜fā‡™ā‡˜lā‡™)"
        by auto
      from model_for_š’ž ā€¹lt āˆˆ set š’žā€ŗ inc have "Ia Mv Mf (inc(f))" by fastforce
      then have "āˆ€s t. s ā‰¤ t āŸ¶ (Mf f) s ā‰¤ (Mf f) t" by simp
      moreover
      from lm have "ā؆HF ((ā„³ āˆ˜ VennRegion) ` l) ā‰¤ ā؆HF ((ā„³ āˆ˜ VennRegion) ` m)"
        by (metis HUnion_proper_Venn_region_inter ā„³.simps(2) comp_apply image_cong inf.absorb_iff2)
      ultimately
      have "Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` l)) ā‰¤ Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` m))"
        by blast
      then have "Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` m)) =
                 Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` m)) āŠ” Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` l))"
        by blast
      with fml lm show "interp Isa ā„³ fml"
        by (auto simp only: interp.simps Isa.simps Ist.simps ā„³.simps set_var_set_set_to_var_set_list)
    qed
  next
    case (dec f)
    show ?thesis
    proof
      fix fml assume "fml āˆˆ reduce_literal lt"
      then have "fml āˆˆ reduce_literal (ATm (dec(f)))"
        using dec by blast
      then obtain l m where lm: "l āŠ† P+ V" "m āŠ† P+ V" "l āŠ† m"
                        and fml: "fml = AT (Var wā‡˜fā‡™ā‡˜lā‡™ =s Var wā‡˜fā‡™ā‡˜lā‡™ āŠ”s Var wā‡˜fā‡™ā‡˜mā‡™)"
        by auto
      from model_for_š’ž ā€¹lt āˆˆ set š’žā€ŗ dec have "Ia Mv Mf (dec(f))" by fastforce
      then have "āˆ€s t. s ā‰¤ t āŸ¶ (Mf f) t ā‰¤ (Mf f) s" by simp
      moreover
      from lm have "ā؆HF ((ā„³ āˆ˜ VennRegion) ` l) ā‰¤ ā؆HF ((ā„³ āˆ˜ VennRegion) ` m)"
        by (metis HUnion_proper_Venn_region_inter ā„³.simps(2) comp_apply image_cong inf.absorb_iff2)
      ultimately
      have "Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` m)) ā‰¤ Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` l))"
        by blast
      then have "Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` l)) =
                 Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` l)) āŠ” Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` m))"
        by blast
      with fml lm show "interp Isa ā„³ fml"
        by (auto simp only: interp.simps Isa.simps Ist.simps ā„³.simps set_var_set_set_to_var_set_list)
    qed
  next
    case (add f)
    show ?thesis
    proof
      fix fml assume "fml āˆˆ reduce_literal lt"
      then have "fml āˆˆ reduce_literal (ATm (add(f)))"
        using add by blast
      then obtain l m where lm: "l āŠ† P+ V" "m āŠ† P+ V"
                        and fml: "fml = AT (Var wā‡˜fā‡™ā‡˜lāˆŖmā‡™ =s Var wā‡˜fā‡™ā‡˜lā‡™ āŠ”s Var wā‡˜fā‡™ā‡˜mā‡™)"
        by auto
      from model_for_š’ž ā€¹lt āˆˆ set š’žā€ŗ add have "Ia Mv Mf (add(f))" by fastforce
      then have "āˆ€s t. (Mf f) (s āŠ” t) = (Mf f) s āŠ” (Mf f) t" by simp
      moreover
      have "ā؆HF ((ā„³ āˆ˜ VennRegion) ` (l āˆŖ m)) = ā؆HF ((ā„³ āˆ˜ VennRegion) ` l) āŠ” ā؆HF ((ā„³ āˆ˜ VennRegion) ` m)"
        using HUnion_proper_Venn_region_union ā„³.simps(2) lm(1) lm(2) by auto
      ultimately
      have "Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` (l āˆŖ m))) =
            Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` l)) āŠ” Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` m))"
        by auto
      with fml lm show "interp Isa ā„³ fml"
        using set_var_set_set_to_var_set_list
        apply (simp only: interp.simps Isa.simps Ist.simps ā„³.simps)
        by (metis le_sup_iff)
    qed
  next
    case (mul f)
    with model_for_š’ž ā€¹lt āˆˆ set š’žā€ŗ have "Ia Mv Mf (mul(f))" by fastforce
    then have f_mul: "āˆ€s t. (Mf f) (s āŠ“ t) = (Mf f) s āŠ“ (Mf f) t" by simp
    have InterOfWAux: "Isa ā„³ (Var (InterOfWAux f l m) =s Var wā‡˜fā‡™ā‡˜lā‡™ -s Var wā‡˜fā‡™ā‡˜mā‡™)" for l m
      by auto
    {fix l m assume "l āŠ† P+ V" "m āŠ† P+ V"
      then have "ā؆HF ((ā„³ āˆ˜ VennRegion) ` (l āˆ© m)) = ā؆HF ((ā„³ āˆ˜ VennRegion) ` l) āŠ“ ā؆HF ((ā„³ āˆ˜ VennRegion) ` m)"
        using HUnion_proper_Venn_region_inter by force
      then have "ā„³ (UnionOfVennRegions (var_set_set_to_var_set_list (l āˆ© m))) =
                 ā„³ (UnionOfVennRegions (var_set_set_to_var_set_list l)) āŠ“
                 ā„³ (UnionOfVennRegions (var_set_set_to_var_set_list m))"
        using set_var_set_set_to_var_set_list ā€¹l āŠ† P+ Vā€ŗ ā€¹m āŠ† P+ Vā€ŗ
        by (metis ā„³.simps(3) inf.absorb_iff2 inf_left_commute)
      with f_mul have "ā„³ wā‡˜fā‡™ā‡˜lāˆ©mā‡™ = ā„³ wā‡˜fā‡™ā‡˜lā‡™ āŠ“ ā„³ wā‡˜fā‡™ā‡˜mā‡™"
        by auto
      moreover
      from InterOfWAux have "ā„³ (InterOfWAux f l m) = ā„³ wā‡˜fā‡™ā‡˜lā‡™ - ā„³ wā‡˜fā‡™ā‡˜mā‡™"
        by simp
      ultimately
      have "ā„³ wā‡˜fā‡™ā‡˜lāˆ©mā‡™ = ā„³ wā‡˜fā‡™ā‡˜lā‡™ - ā„³ (InterOfWAux f l m)"
        by auto
      then have "Isa ā„³ (Var wā‡˜fā‡™ā‡˜lāˆ©mā‡™ =s Var wā‡˜fā‡™ā‡˜lā‡™ -s Var (InterOfWAux f l m))"
        by auto
    }
    with InterOfWAux show ?thesis
      using mul by auto
  next
    case (le f g)
    show ?thesis
    proof
      fix fml assume "fml āˆˆ reduce_literal lt"
      then have "fml āˆˆ reduce_literal (ATm (f ā‰¼m g))"
        using le by blast
      then obtain l where l: "l āŠ† P+ V"
                      and fml: "fml = AT (Var wā‡˜gā‡™ā‡˜lā‡™ =s Var wā‡˜gā‡™ā‡˜lā‡™ āŠ”s Var wā‡˜fā‡™ā‡˜lā‡™)"
        by auto
      from model_for_š’ž ā€¹lt āˆˆ set š’žā€ŗ le have "Ia Mv Mf (f ā‰¼m g)" by fastforce
      then have "āˆ€s. (Mf f) s ā‰¤ (Mf g) s" by simp
      then have "Mf f (ā؆HF ((ā„³ āˆ˜ VennRegion) ` l)) ā‰¤ Mf g (ā؆HF ((ā„³ āˆ˜ VennRegion) ` l))"
        by auto
      with fml l show "interp Isa ā„³ fml"
        using set_var_set_set_to_var_set_list
        by (auto simp only: interp.simps Isa.simps Ist.simps ā„³.simps)
    qed
  next
    case (eq_empty x n)
    with ā€¹lt āˆˆ set š’žā€ŗ model_for_š’ž have "Mv x = 0" by auto
    show ?thesis
    proof
      fix fml assume "fml āˆˆ reduce_literal lt"
      with eq_empty have "fml = AT (Var (Solo x) =s āˆ… n)"
        by simp
      with ā€¹Mv x = 0ā€ŗ show "interp Isa ā„³ fml" by auto
    qed
  next
    case (eq x y)
    with ā€¹lt āˆˆ set š’žā€ŗ model_for_š’ž have "Mv x = Mv y" by auto
    show ?thesis
    proof
      fix fml assume "fml āˆˆ reduce_literal lt"
      with eq have "fml = AT (Var (Solo x) =s Var (Solo y))"
        by simp
      with ā€¹Mv x = Mv yā€ŗ show "interp Isa ā„³ fml" by auto
    qed
  next
    case (neq x y)
    with ā€¹lt āˆˆ set š’žā€ŗ model_for_š’ž have "Mv x ā‰  Mv y" by auto
    show ?thesis
    proof
      fix fml assume "fml āˆˆ reduce_literal lt"
      with neq have "fml = AF (Var (Solo x) =s Var (Solo y))"
        by simp
      with ā€¹Mv x ā‰  Mv yā€ŗ show "interp Isa ā„³ fml" by auto
    qed
  next
    case (union x y z)
    with ā€¹lt āˆˆ set š’žā€ŗ model_for_š’ž have "Mv x = Mv y āŠ” Mv z" by fastforce
    then have "interp Isa ā„³ (AT (Var (Solo x) =s Var (Solo y) āŠ”s Var (Solo z)))" by simp
    with union show ?thesis by auto
  next
    case (diff x y z)
    with ā€¹lt āˆˆ set š’žā€ŗ model_for_š’ž have "Mv x = Mv y - Mv z" by fastforce
    then have "interp Isa ā„³ (AT (Var (Solo x) =s Var (Solo y) -s Var (Solo z)))" by simp
    with diff show ?thesis by auto
  next
    case (single x y)
    with ā€¹lt āˆˆ set š’žā€ŗ model_for_š’ž have "Mv x = HF {Mv y}" by fastforce
    then have "interp Isa ā„³ (AT (Var (Solo x) =s Single (Var (Solo y))))" by simp
    with single show ?thesis by auto
  next
    case (app x f y)
    with ā€¹lt āˆˆ set š’žā€ŗ model_for_š’ž
    have "Mv x = (Mf f) (Mv y)" by fastforce
    moreover
    from app ā€¹lt āˆˆ set š’žā€ŗ have "y āˆˆ V"
      unfolding V_def by force
    with variable_as_composition_of_proper_Venn_regions
    have "Mv y = ā؆HF (proper_Venn_region ` ā„’ V y)"
      by presburger
    then have "Mv y = ā؆HF ((ā„³ āˆ˜ VennRegion) ` ā„’ V y)"
      by simp
    ultimately
    have "ā„³ (Solo x) = ā„³ wā‡˜fā‡™ā‡˜ā„’ V yā‡™"
      using ā„³.simps set_var_set_set_to_var_set_list ā„’_subset_P_plus
      by metis
    with app show ?thesis by simp
  qed
qed

lemma soundness_reduce_cl:
  "āˆ€fml āˆˆ reduce_clause. interp Isa ā„³ fml"
  unfolding reduce_clause_def
  using soundness_reduce_literal
  by fastforce

lemma ā„³_is_model_for_reduced_dnf: "is_model_for_reduced_dnf ā„³"
  unfolding is_model_for_reduced_dnf_def
  unfolding reduced_dnf_def
  using soundness_introduce_v soundness_introduce_w soundness_introduce_UnionOfVennRegions soundness_reduce_cl
  by (metis (no_types, lifting) Un_iff imageI)

end

lemma MLSSmf_to_MLSS_soundness:
  assumes š’ž_norm: "norm_clause š’ž"
      and š’ž_has_model: "āˆƒMv Mf. Icl Mv Mf š’ž"
    shows "āˆƒM. normalized_MLSSmf_clause.is_model_for_reduced_dnf š’ž M"
proof -
  from š’ž_has_model obtain Mv Mf where "Icl Mv Mf š’ž" by blast
  with š’ž_norm
  interpret satisfiable_normalized_MLSSmf_clause š’ž Mv Mf
    by unfold_locales
  from ā„³_is_model_for_reduced_dnf show ?thesis by auto
qed

end