theory Prop_Logic_Multiset imports Nested_Multisets_Ordinals.Multiset_More Prop_Normalisation Entailment_Definition.Partial_Herbrand_Interpretation begin section ‹Link with Multiset Version› subsection ‹Transformation to Multiset› fun mset_of_conj :: "'a propo ⇒ 'a literal multiset" where "mset_of_conj (FOr φ ψ) = mset_of_conj φ + mset_of_conj ψ" | "mset_of_conj (FVar v) = {# Pos v #}" | "mset_of_conj (FNot (FVar v)) = {# Neg v #}" | "mset_of_conj FF = {#}" fun mset_of_formula :: "'a propo ⇒ 'a literal multiset set" where "mset_of_formula (FAnd φ ψ) = mset_of_formula φ ∪ mset_of_formula ψ" | "mset_of_formula (FOr φ ψ) = {mset_of_conj (FOr φ ψ)}" | "mset_of_formula (FVar ψ) = {mset_of_conj (FVar ψ)}" | "mset_of_formula (FNot ψ) = {mset_of_conj (FNot ψ)}" | "mset_of_formula FF = {{#}}" | "mset_of_formula FT = {}" subsection ‹Equisatisfiability of the two Versions› lemma is_conj_with_TF_FNot: "is_conj_with_TF (FNot φ) ⟷ (∃v. φ = FVar v ∨ φ = FF ∨ φ = FT)" unfolding is_conj_with_TF_def apply (rule iffI) apply (induction "FNot φ" rule: super_grouped_by.induct) apply (induction "FNot φ" rule: grouped_by.induct) apply simp apply (cases φ; simp) apply auto done lemma grouped_by_COr_FNot: "grouped_by COr (FNot φ) ⟷ (∃v. φ = FVar v ∨ φ = FF ∨ φ = FT)" unfolding is_conj_with_TF_def apply (rule iffI) apply (induction "FNot φ" rule: grouped_by.induct) apply simp apply (cases φ; simp) apply auto done lemma shows no_T_F_FF[simp]: "¬no_T_F FF" and no_T_F_FT[simp]: "¬no_T_F FT" unfolding no_T_F_def all_subformula_st_def by auto lemma grouped_by_CAnd_FAnd: "grouped_by CAnd (FAnd φ1 φ2) ⟷ grouped_by CAnd φ1 ∧ grouped_by CAnd φ2" apply (rule iffI) apply (induction "FAnd φ1 φ2" rule: grouped_by.induct) using connected_is_group[of CAnd φ1 φ2] by auto lemma grouped_by_COr_FOr: "grouped_by COr (FOr φ1 φ2) ⟷ grouped_by COr φ1 ∧ grouped_by COr φ2" apply (rule iffI) apply (induction "FOr φ1 φ2" rule: grouped_by.induct) using connected_is_group[of COr φ1 φ2] by auto lemma grouped_by_COr_FAnd[simp]: "¬ grouped_by COr (FAnd φ1 φ2)" apply clarify apply (induction "FAnd φ1 φ2" rule: grouped_by.induct) apply auto done lemma grouped_by_COr_FEq[simp]: "¬ grouped_by COr (FEq φ1 φ2)" apply clarify apply (induction "FEq φ1 φ2" rule: grouped_by.induct) apply auto done lemma [simp]: "¬grouped_by COr (FImp φ ψ)" apply clarify by (induction "FImp φ ψ" rule: grouped_by.induct) simp_all lemma [simp]: "¬ is_conj_with_TF (FImp φ ψ)" unfolding is_conj_with_TF_def apply clarify by (induction "FImp φ ψ" rule: super_grouped_by.induct) simp_all lemma [simp]: "¬ is_conj_with_TF (FEq φ ψ)" unfolding is_conj_with_TF_def apply clarify by (induction "FEq φ ψ" rule: super_grouped_by.induct) simp_all lemma is_conj_with_TF_Fand: "is_conj_with_TF (FAnd φ1 φ2) ⟹ is_conj_with_TF φ1 ∧ is_conj_with_TF φ2" unfolding is_conj_with_TF_def apply (induction "FAnd φ1 φ2" rule: super_grouped_by.induct) apply (auto simp: grouped_by_CAnd_FAnd intro: grouped_is_super_grouped)[] apply auto[] done lemma is_conj_with_TF_FOr: "is_conj_with_TF (FOr φ1 φ2) ⟹ grouped_by COr φ1 ∧ grouped_by COr φ2" unfolding is_conj_with_TF_def apply (induction "FOr φ1 φ2" rule: super_grouped_by.induct) apply (auto simp: grouped_by_COr_FOr)[] apply auto[] done lemma grouped_by_COr_mset_of_formula: "grouped_by COr φ ⟹ mset_of_formula φ = (if φ = FT then {} else {mset_of_conj φ})" by (induction φ) (auto simp add: grouped_by_COr_FNot) text ‹When a formula is in CNF form, then there is equisatisfiability between the multiset version and the CNF form. Remark that the definition for the entailment are slightly different: @{term eval} uses a function assigning @{term True} or @{term False}, while @{term Partial_Herbrand_Interpretation.true_clss} uses a set where being in the list means entailment of a literal. › theorem cnf_eval_true_clss: fixes φ :: "'v propo" assumes "is_cnf φ" shows "eval A φ ⟷ Partial_Herbrand_Interpretation.true_clss ({Pos v|v. A v} ∪ {Neg v|v. ¬A v}) (mset_of_formula φ)" using assms proof (induction φ) case FF then show ?case by auto next case FT then show ?case by auto next case (FVar v) then show ?case by auto next case (FAnd φ ψ) then show ?case unfolding is_cnf_def by (auto simp: is_conj_with_TF_FNot dest: is_conj_with_TF_Fand dest!: is_conj_with_TF_FOr) next case (FOr φ ψ) then have [simp]: "mset_of_formula φ = {mset_of_conj φ}" "mset_of_formula ψ = {mset_of_conj ψ}" unfolding is_cnf_def by (auto dest!:is_conj_with_TF_FOr simp: grouped_by_COr_mset_of_formula split: if_splits) have "is_conj_with_TF φ" "is_conj_with_TF ψ" using FOr(3) unfolding is_cnf_def no_T_F_def by (metis grouped_is_super_grouped is_conj_with_TF_FOr is_conj_with_TF_def)+ then show ?case using FOr unfolding is_cnf_def by simp next case (FImp φ ψ) then show ?case unfolding is_cnf_def by auto next case (FEq φ ψ) then show ?case unfolding is_cnf_def by auto next case (FNot φ) then show ?case unfolding is_cnf_def by (auto simp: is_conj_with_TF_FNot) qed function formula_of_mset :: "'a clause ⇒ 'a propo" where ‹formula_of_mset φ = (if φ = {#} then FF else let v = (SOME v. v ∈# φ); v' = (if is_pos v then FVar (atm_of v) else FNot (FVar (atm_of v))) in if remove1_mset v φ = {#} then v' else FOr v' (formula_of_mset (remove1_mset v φ)))› by auto termination apply (relation ‹measure size›) apply (auto simp: size_mset_remove1_mset_le_iff) by (meson multiset_nonemptyE someI_ex) lemma formula_of_mset_empty[simp]: ‹formula_of_mset {#} = FF› by (auto simp: Let_def) lemma formula_of_mset_empty_iff[iff]: ‹formula_of_mset φ = FF ⟷ φ = {#}› by (induction φ) (auto simp: Let_def) declare formula_of_mset.simps[simp del] function formula_of_msets :: "'a literal multiset set ⇒ 'a propo" where ‹formula_of_msets φs = (if φs = {} ∨ infinite φs then FT else let v = (SOME v. v ∈ φs); v' = formula_of_mset v in if φs - {v} = {} then v' else FAnd v' (formula_of_msets (φs - {v})))› by auto termination apply (relation ‹measure card›) apply (auto simp: some_in_eq) by (metis all_not_in_conv card_gt_0_iff diff_less lessI) declare formula_of_msets.simps[simp del] lemma remove1_mset_empty_iff: ‹remove1_mset v φ = {#} ⟷ (φ = {#} ∨ φ = {#v#})› using remove1_mset_eqE by force definition fun_of_set where ‹fun_of_set A x = (if Pos x ∈ A then True else if Neg x ∈ A then False else undefined)› lemma grouped_by_COr_formula_of_mset: ‹grouped_by COr (formula_of_mset φ)› proof (induction ‹size φ› arbitrary: φ) case 0 then show ?case by (subst formula_of_mset.simps) (auto simp: Let_def) next case (Suc n) note IH = this(1) and s = this(2) then have ‹n = size (remove1_mset (SOME v. v ∈# φ) φ)› if ‹φ ≠ {#}› using that by (auto simp: size_Diff_singleton_if some_in_eq) then show ?case using IH[of ‹remove1_mset (SOME v. v ∈# φ) φ›] by(subst formula_of_mset.simps) (auto simp: Let_def grouped_by_COr_FOr) qed lemma no_T_F_formula_of_mset: ‹no_T_F (formula_of_mset φ)› if ‹formula_of_mset φ ≠ FF› for φ using that proof (induction ‹size φ› arbitrary: φ) case 0 then show ?case by (subst formula_of_mset.simps) (auto simp: Let_def no_T_F_def all_subformula_st_def) next case (Suc n) note IH = this(1) and s = this(2) and FF = this(3) then have ‹n = size (remove1_mset (SOME v. v ∈# φ) φ)› if ‹φ ≠ {#}› using that by (auto simp: size_Diff_singleton_if some_in_eq) moreover have ‹no_T_F (FVar (atm_of (SOME v. v ∈# φ)))› by (auto simp: no_T_F_def) ultimately show ?case using IH[of ‹remove1_mset (SOME v. v ∈# φ) φ›] FF by(subst formula_of_mset.simps) (auto simp: Let_def grouped_by_COr_FOr) qed lemma mset_of_conj_formula_of_mset[simp]: ‹mset_of_conj(formula_of_mset φ) = φ› for φ proof (induction ‹size φ› arbitrary: φ) case 0 then show ?case by (subst formula_of_mset.simps) (auto simp: Let_def no_T_F_def all_subformula_st_def) next case (Suc n) note IH = this(1) and s = this(2) then have ‹n = size (remove1_mset (SOME v. v ∈# φ) φ)› if ‹φ ≠ {#}› using that by (auto simp: size_Diff_singleton_if some_in_eq) moreover have ‹no_T_F (FVar (atm_of (SOME v. v ∈# φ)))› by (auto simp: no_T_F_def) ultimately show ?case using IH[of ‹remove1_mset (SOME v. v ∈# φ) φ›] by(subst formula_of_mset.simps) (auto simp: some_in_eq Let_def grouped_by_COr_FOr remove1_mset_empty_iff) qed lemma mset_of_formula_formula_of_mset [simp]: ‹mset_of_formula (formula_of_mset φ) = {φ}› for φ proof (induction ‹size φ› arbitrary: φ) case 0 then show ?case by (subst formula_of_mset.simps) (auto simp: Let_def no_T_F_def all_subformula_st_def) next case (Suc n) note IH = this(1) and s = this(2) then have ‹n = size (remove1_mset (SOME v. v ∈# φ) φ)› if ‹φ ≠ {#}› using that by (auto simp: size_Diff_singleton_if some_in_eq) moreover have ‹no_T_F (FVar (atm_of (SOME v. v ∈# φ)))› by (auto simp: no_T_F_def) ultimately show ?case using IH[of ‹remove1_mset (SOME v. v ∈# φ) φ›] by(subst formula_of_mset.simps) (auto simp: some_in_eq Let_def grouped_by_COr_FOr remove1_mset_empty_iff) qed lemma formula_of_mset_is_cnf: ‹is_cnf (formula_of_mset φ)› by (auto simp: is_cnf_def is_conj_with_TF_def grouped_by_COr_formula_of_mset no_T_F_formula_of_mset intro!: grouped_is_super_grouped) lemma eval_clss_iff: assumes ‹consistent_interp A› and ‹total_over_set A UNIV› shows ‹eval (fun_of_set A) (formula_of_mset φ) ⟷ Partial_Herbrand_Interpretation.true_clss A {φ}› apply (subst cnf_eval_true_clss[OF formula_of_mset_is_cnf]) using assms apply (auto simp add: true_cls_def fun_of_set_def consistent_interp_def total_over_set_def) apply (case_tac L) by (fastforce simp add: true_cls_def fun_of_set_def consistent_interp_def total_over_set_def)+ lemma is_conj_with_TF_Fand_iff: "is_conj_with_TF (FAnd φ1 φ2) ⟷ is_conj_with_TF φ1 ∧ is_conj_with_TF φ2 " unfolding is_conj_with_TF_def by (subst super_grouped_by.simps) auto lemma is_CNF_Fand: ‹is_cnf (FAnd φ ψ) ⟷ (is_cnf φ ∧ no_T_F φ) ∧ is_cnf ψ ∧ no_T_F ψ› by (auto simp: is_cnf_def is_conj_with_TF_Fand_iff) lemma no_T_F_formula_of_mset_iff: ‹no_T_F (formula_of_mset φ) ⟷ φ ≠ {#}› proof (induction ‹size φ› arbitrary: φ) case 0 then show ?case by (subst formula_of_mset.simps) (auto simp: Let_def no_T_F_def all_subformula_st_def) next case (Suc n) note IH = this(1) and s = this(2) then have ‹n = size (remove1_mset (SOME v. v ∈# φ) φ)› if ‹φ ≠ {#}› using that by (auto simp: size_Diff_singleton_if some_in_eq) moreover have ‹no_T_F (FVar (atm_of (SOME v. v ∈# φ)))› by (auto simp: no_T_F_def) ultimately show ?case using IH[of ‹remove1_mset (SOME v. v ∈# φ) φ›] by(subst formula_of_mset.simps) (auto simp: some_in_eq Let_def grouped_by_COr_FOr remove1_mset_empty_iff) qed lemma no_T_F_formula_of_msets: assumes ‹finite φ› and ‹{#} ∉ φ› and ‹φ ≠ {}› shows ‹no_T_F (formula_of_msets (φ))› using assms apply (induction ‹card φ› arbitrary: φ) subgoal by (subst formula_of_msets.simps) (auto simp: no_T_F_def all_subformula_st_def)[] subgoal apply (subst formula_of_msets.simps) apply (auto split: simp: Let_def formula_of_mset_is_cnf is_CNF_Fand no_T_F_formula_of_mset_iff some_in_eq) apply (metis (mono_tags, lifting) some_eq_ex) done done lemma is_cnf_formula_of_msets: assumes ‹finite φ› and ‹{#} ∉ φ› shows ‹is_cnf (formula_of_msets φ)› using assms apply (induction ‹card φ› arbitrary: φ) subgoal by (subst formula_of_msets.simps) (auto simp: is_cnf_def is_conj_with_TF_def)[] subgoal apply (subst formula_of_msets.simps) apply (auto split: simp: Let_def formula_of_mset_is_cnf is_CNF_Fand no_T_F_formula_of_mset_iff some_in_eq intro: no_T_F_formula_of_msets) apply (metis (mono_tags, lifting) some_eq_ex) done done lemma mset_of_formula_formula_of_msets: assumes ‹finite φ› shows ‹mset_of_formula (formula_of_msets φ) = φ› using assms apply (induction ‹card φ› arbitrary: φ) subgoal by (subst formula_of_msets.simps) (auto simp: is_cnf_def is_conj_with_TF_def)[] subgoal apply (subst formula_of_msets.simps) apply (auto split: simp: Let_def formula_of_mset_is_cnf is_CNF_Fand no_T_F_formula_of_mset_iff some_in_eq intro: no_T_F_formula_of_msets) done done lemma assumes ‹consistent_interp A› and ‹total_over_set A UNIV› and ‹finite φ› and ‹{#} ∉ φ› shows ‹eval (fun_of_set A) (formula_of_msets φ) ⟷ Partial_Herbrand_Interpretation.true_clss A φ› apply (subst cnf_eval_true_clss[OF is_cnf_formula_of_msets[OF assms(3-4)]]) using assms(3) unfolding mset_of_formula_formula_of_msets[OF assms(3)] by (induction φ) (use eval_clss_iff[OF assms(1,2)] in ‹simp_all add: cnf_eval_true_clss formula_of_mset_is_cnf›) end