theory Model_Enumeration imports Entailment_Definition.Partial_Annotated_Herbrand_Interpretation Weidenbach_Book_Base.Wellfounded_More begin lemma Ex_sat_model: assumes ‹satisfiable (set_mset N)› shows ‹∃M. set M ⊨sm N ∧ distinct M ∧ consistent_interp (set M) ∧ atm_of ` set M ⊆ atms_of_mm N› proof - from assms obtain I where I_N: ‹I ⊨sm N› and consistent: ‹consistent_interp I› and ‹total_over_m I (set_mset N)› and atms_I_N: ‹atm_of ` I = atms_of_mm N› unfolding satisfiable_def_min by blast have ‹I ⊆ Pos ` (atms_of_mm N) ∪ Neg ` (atms_of_mm N)› using atms_I_N by (smt in_set_image_subsetD literal.exhaust_sel subsetI sup_ge1 sup_ge2) then have ‹finite I› using infinite_super by fastforce then obtain I' where I': ‹I = set I'› and dist: ‹distinct I'› using finite_distinct_list by force show ?thesis apply (rule exI[of _ I']) using I_N dist consistent atms_I_N by (auto simp: I') qed definition all_models where ‹all_models N = {M. set M ⊨sm N ∧ consistent_interp (set M) ∧ distinct M ∧ atm_of ` set M ⊆ atms_of_mm N}› lemma finite_all_models: ‹finite (all_models N)› proof - let ?n = ‹Pos ` (atms_of_mm N) ∪ Neg ` (atms_of_mm N)› have H: ‹all_models N ⊆ {M. set M ⊆ ?n ∧ length M ≤ card ?n}› unfolding all_models_def apply (auto dest: imageI[of _ _ atm_of]) apply (metis contra_subsetD image_eqI literal.exhaust_sel) by (smt atms_of_ms_finite card_mono distinct_card finite_Un finite_imageI finite_set_mset image_subset_iff literal.exhaust_sel subsetI sup_ge1 sup_ge2) show ?thesis apply (rule finite_subset) apply (rule H) apply (rule finite_lists_length_le) apply auto done qed inductive next_model where ‹set M ⊨sm N ⟹ distinct M ⟹ consistent_interp (set M) ⟹ atm_of ` set M ⊆ atms_of_mm N ⟹ next_model M N› lemma image_mset_uminus_eq_image_mset_uminus_literals[simp]: ‹image_mset uminus M' = image_mset uminus M ⟷ M = M'› for M :: ‹'v clause› by (auto simp:inj_image_mset_eq_iff inj_def) context fixes P :: ‹'v literal set ⇒ bool› begin inductive next_model_filtered :: ‹'v literal list option × 'v literal multiset multiset ⇒ 'v literal list option × 'v literal multiset multiset ⇒ bool› where ‹next_model M N ⟹ P (set M) ⟹ next_model_filtered (None, N) (Some M, N)› | ‹next_model M N ⟹ ¬P (set M) ⟹ next_model_filtered (None, N) (None, add_mset (image_mset uminus (mset M)) N)› lemma next_model_filtered_mono: ‹next_model_filtered a b ⟹ snd a ⊆# snd b› by (induction rule: next_model_filtered.induct) auto lemma rtranclp_next_model_filtered_mono: ‹next_model_filtered⇧*⇧* a b ⟹ snd a ⊆# snd b› by (induction rule: rtranclp_induct) (auto dest: next_model_filtered_mono) lemma next_filtered_same_atoms: ‹next_model_filtered a b ⟹ atms_of_mm (snd b) = atms_of_mm (snd a)› by (induction rule: next_model_filtered.induct) (auto simp: next_model.simps atms_of_def) lemma rtranclp_next_filtered_same_atoms: ‹next_model_filtered⇧*⇧* a b ⟹ atms_of_mm (snd b) = atms_of_mm (snd a)› by (induction rule: rtranclp_induct) (auto simp: next_filtered_same_atoms) lemma next_model_filtered_next_modelD: ‹next_model_filtered a b ⟹ M ∈# snd b - snd a ⟹ M = image_mset uminus (mset M') ⟹ next_model M' (snd a)› by (induction arbitrary: M M' rule: next_model_filtered.induct) (auto simp: next_model.simps distinct_mset_mset_distinct[symmetric] dest: mset_eq_setD simp del: distinct_mset_mset_distinct) lemma rtranclp_next_model_filtered_next_modelD: ‹next_model_filtered⇧*⇧* a b ⟹ M ∈# snd b - snd a ⟹ M = image_mset uminus (mset M') ⟹ next_model M' (snd a)› proof (induction arbitrary: M M' rule: rtranclp_induct) case base then show ?case by auto next case (step y z) note star = this(1) and step = this(2) and IH = this(3) and M_in = this(4) and M = this(5) consider ‹M ∈# snd y - snd a› | ‹M ∈# snd z - snd y› using step star M_in by (smt rtranclp_next_model_filtered_mono add_diff_cancel_right in_multiset_minus_notin_snd rtranclp.rtrancl_into_rtrancl subset_mset.diff_add) then show ?case proof cases case 1 show ?thesis by (rule IH[OF 1 M]) next case 2 then show ?thesis using step rtranclp_next_model_filtered_mono[OF star] rtranclp_next_filtered_same_atoms[OF star] unfolding subset_mset.le_iff_add by (force simp: next_model_filtered.simps M next_model.simps distinct_mset_mset_distinct[symmetric] dest: mset_eq_setD simp del: distinct_mset_mset_distinct) qed qed lemma rtranclp_next_model_filtered_next_false: ‹next_model_filtered⇧*⇧* a b ⟹ M ∈# snd b - snd a ⟹ M = image_mset uminus (mset M') ⟹ ¬P (uminus ` set_mset M)› proof (induction arbitrary: M M' rule: rtranclp_induct) case base then show ?case by auto next case (step y z) note star = this(1) and step = this(2) and IH = this(3) and M_in = this(4) and M = this(5) consider ‹M ∈# snd y - snd a› | ‹M ∈# snd z - snd y› using step star M_in by (smt rtranclp_next_model_filtered_mono add_diff_cancel_right in_multiset_minus_notin_snd rtranclp.rtrancl_into_rtrancl subset_mset.diff_add) then show ?case proof cases case 1 show ?thesis by (rule IH[OF 1 M]) next case 2 then show ?thesis using step rtranclp_next_model_filtered_mono[OF star] rtranclp_next_filtered_same_atoms[OF star] unfolding subset_mset.le_iff_add by (force simp: next_model_filtered.simps M next_model.simps distinct_mset_mset_distinct[symmetric] image_image dest: mset_eq_setD simp del: distinct_mset_mset_distinct) qed qed lemma next_model_decreasing: assumes ‹next_model M N› shows ‹(add_mset (image_mset uminus (mset M)) N, N) ∈ measure (λN. card (all_models N))› proof - have ‹M ∈ all_models N› using assms unfolding all_models_def by (auto simp: true_clss_def true_cls_mset_def next_model.simps) moreover { have ‹¬ set M ⊨ image_mset uminus (mset M)› using assms unfolding true_cls_def all_models_def by (auto simp: true_clss_def consistent_interp_def next_model.simps) then have ‹M ∉ all_models (add_mset (image_mset uminus (mset M)) N)› unfolding all_models_def by (auto elim!: simp: true_clss_def) } moreover { have ‹atm_of ` uminus ` set M ∪ atms_of_ms (set_mset N) = atms_of_ms (set_mset N)› using assms unfolding true_cls_def all_models_def by (auto simp: true_clss_def consistent_interp_def atms_of_def next_model.simps) then have ‹all_models (add_mset (image_mset uminus (mset M)) N) ⊆ all_models N› using assms unfolding all_models_def by (auto simp: atms_of_def) } ultimately have ‹all_models (add_mset (image_mset uminus (mset M)) N) ⊂ all_models N› by auto then show ?thesis by (auto simp: finite_all_models psubset_card_mono) qed lemma next_model_decreasing': assumes ‹next_model M N› shows ‹((P, add_mset (image_mset uminus (mset M)) N), P, N) ∈ measure (λ(P, N). card (all_models N))› using next_model_decreasing[OF assms] by auto lemma wf_next_model_filtered: ‹wf {(y, x). next_model_filtered x y}› proof - have ‹wf {(y, x). True ∧ next_model_filtered x y}› by (rule wfP_if_measure[of ‹λ_. True› next_model_filtered ‹λN. (if fst N = None then 1 else 0) + card (all_models (snd N))›]) (auto dest: next_model_decreasing simp: next_model_filtered.simps) then show ?thesis unfolding wfP_def by simp qed lemma no_step_next_model_filtered_unsat: assumes ‹no_step next_model_filtered (None, N)› shows ‹unsatisfiable (set_mset N)› by (metis Ex_sat_model Model_Enumeration.next_model_filtered.simps assms next_model.intros) lemma unsat_no_step_next_model_filtered: assumes ‹unsatisfiable (set_mset N)› shows ‹no_step next_model_filtered (None, N)› by (metis (no_types, lifting) next_model_filtered.simps assms next_model.cases satisfiable_carac' snd_conv) lemma full_next_model_filtered_no_distinct_model: assumes no_model: ‹full next_model_filtered (None, N) (None, N')› and filter_mono: ‹⋀M M'. set M ⊨sm N ⟹ consistent_interp (set M) ⟹ set M' ⊨sm N ⟹ distinct M ⟹ distinct M' ⟹ set M ⊆ set M' ⟹ P (set M) ⟷ P (set M')› shows ‹∄M. set M ⊨sm N ∧ P (set M) ∧ consistent_interp (set M) ∧ distinct M› proof clarify fix M assume M_N: ‹set M ⊨m N› and P_M: ‹P (set M)› and consistent: ‹consistent_interp (set M)› and dist_M: ‹distinct M› have st: ‹next_model_filtered⇧*⇧* (None, N) (None, N')› and ns: ‹no_step next_model_filtered (None, N')› using no_model unfolding full_def by blast+ define Ms where ‹Ms = N' - N› then have N'[simp]: ‹N' = N + Ms› using rtranclp_next_model_filtered_mono[OF st] by auto have ‹unsatisfiable (set_mset N')› using ns by (rule no_step_next_model_filtered_unsat) then have ‹¬set M ⊨m Ms› using consistent M_N by (auto simp: satisfiable_carac[symmetric]) then obtain M' where M'_MS: ‹M' ∈# Ms› and M_M': ‹¬set M ⊨ M'› by (auto simp: true_cls_mset_def) obtain M'' where [simp]: ‹M' = mset M''› using ex_mset[of M'] by auto let ?M'' = ‹map uminus M''› have ‹next_model ?M'' (snd (None :: 'v literal list option, N))› apply (rule rtranclp_next_model_filtered_next_modelD[OF st, of M']) using M'_MS by auto then have cons': ‹consistent_interp (set ?M'')› and M''_N: ‹set ?M'' ⊨sm N› and dist_M'': ‹distinct ?M''› unfolding next_model.simps by auto let ?I = ‹remdups (M @ ?M'')› have cons_I: ‹consistent_interp (set ?I)› using M_M' consistent cons' by (auto simp: consistent_interp_def true_cls_def) have ‹P (set ?I)› using filter_mono[of M ‹?I›] cons' M''_N M_N consistent dist_M'' dist_M P_M by auto then have ‹P (uminus ` (set M''))› using filter_mono[of ‹?M''› ?I] cons' M''_N M_N consistent dist_M'' dist_M P_M cons_I by auto then show False using rtranclp_next_model_filtered_next_false[OF st, of M' ?M''] M'_MS by auto qed lemma full_next_model_filtered_no_model: assumes no_model: ‹full next_model_filtered (None, N) (None, N')› and filter_mono: ‹⋀M M'. set M ⊨sm N ⟹ consistent_interp (set M) ⟹ set M' ⊨sm N ⟹ distinct M ⟹ distinct M' ⟹ set M ⊆ set M' ⟹ P (set M) ⟷ P (set M')› shows ‹∄M. set M ⊨sm N ∧ P (set M) ∧ consistent_interp (set M)› (is ‹∄M. ?P M›) proof - have H: ‹(∃M. ?P M) ⟷ (∃M. set M ⊨sm N ∧ P (set M) ∧ consistent_interp (set M) ∧ distinct M)› by (auto intro: exI[of _ ‹remdups _›]) show ?thesis apply (subst H) apply (rule full_next_model_filtered_no_distinct_model) apply (rule no_model) apply (rule filter_mono; assumption) done qed end lemma no_step_next_model_filtered_next_model_iff: ‹fst S = None ⟹ no_step (next_model_filtered P) S ⟷ (∄M. next_model M (snd S))› apply (cases S; auto simp: next_model_filtered.simps) by metis lemma Ex_next_model_iff_statisfiable: ‹(∃M. next_model M N) ⟷ satisfiable (set_mset N)› by (metis no_step_next_model_filtered_next_model_iff next_model.cases no_step_next_model_filtered_unsat prod.sel(1) prod.sel(2) satisfiable_carac') lemma unsat_no_step_next_model_filtered': assumes ‹unsatisfiable (set_mset (snd S)) ∨ fst S ≠ None› shows ‹no_step (next_model_filtered P) S› using assms apply cases apply (auto dest: unsat_no_step_next_model_filtered) apply (metis Ex_next_model_iff_statisfiable fst_conv next_model_filtered.simps no_step_next_model_filtered_next_model_iff) by (metis Pair_inject next_model_filtered.cases option.simps(3) prod.collapse) end