theory Partial_And_Total_Herbrand_Interpretation imports Partial_Herbrand_Interpretation Ordered_Resolution_Prover.Herbrand_Interpretation begin section ‹Bridging of total and partial Herbrand interpretation› text ‹This theory has mostly be written as a sanity check between the two entailment notion.› definition partial_model_of :: ‹'a interp ⇒ 'a partial_interp› where ‹partial_model_of I = Pos ` I ∪ Neg ` {x. x ∉ I}› definition total_model_of :: ‹'a partial_interp ⇒ 'a interp› where ‹total_model_of I = {x. Pos x ∈ I}› lemma total_over_set_partial_model_of: ‹total_over_set (partial_model_of I) UNIV› unfolding total_over_set_def by (auto simp: partial_model_of_def) lemma consistent_interp_partial_model_of: ‹consistent_interp (partial_model_of I)› unfolding consistent_interp_def by (auto simp: partial_model_of_def) lemma consistent_interp_alt_def: ‹consistent_interp I ⟷ (∀L. ¬(Pos L ∈ I ∧ Neg L ∈ I))› unfolding consistent_interp_def by (metis literal.exhaust uminus_Neg uminus_of_uminus_id) context fixes I :: ‹'a partial_interp› assumes cons: ‹consistent_interp I› begin lemma partial_implies_total_true_cls_total_model_of: assumes ‹Partial_Herbrand_Interpretation.true_cls I C› shows ‹Herbrand_Interpretation.true_cls (total_model_of I) C› using assms cons apply - unfolding total_model_of_def Partial_Herbrand_Interpretation.true_cls_def Herbrand_Interpretation.true_cls_def consistent_interp_alt_def by (rule bexE, assumption) (case_tac x; auto) lemma total_implies_partial_true_cls_total_model_of: assumes ‹Herbrand_Interpretation.true_cls (total_model_of I) C› and ‹total_over_set I (atms_of C)› shows ‹Partial_Herbrand_Interpretation.true_cls I C› using assms cons unfolding total_model_of_def Partial_Herbrand_Interpretation.true_cls_def Herbrand_Interpretation.true_cls_def consistent_interp_alt_def total_over_m_def total_over_set_def by (auto simp: atms_of_def dest: multi_member_split) lemma partial_implies_total_true_clss_total_model_of: assumes ‹Partial_Herbrand_Interpretation.true_clss I C› shows ‹Herbrand_Interpretation.true_clss (total_model_of I) C› using assms cons unfolding Partial_Herbrand_Interpretation.true_clss_def Herbrand_Interpretation.true_clss_def by (auto simp: partial_implies_total_true_cls_total_model_of) lemma total_implies_partial_true_clss_total_model_of: assumes ‹Herbrand_Interpretation.true_clss (total_model_of I) C› and ‹total_over_m I C› shows ‹Partial_Herbrand_Interpretation.true_clss I C› using assms cons mk_disjoint_insert unfolding Partial_Herbrand_Interpretation.true_clss_def Herbrand_Interpretation.true_clss_def total_over_set_def by (fastforce simp: total_implies_partial_true_cls_total_model_of dest: multi_member_split) end lemma total_implies_partial_true_cls_partial_model_of: assumes ‹Herbrand_Interpretation.true_cls I C› shows ‹Partial_Herbrand_Interpretation.true_cls (partial_model_of I) C› using assms apply - unfolding partial_model_of_def Partial_Herbrand_Interpretation.true_cls_def Herbrand_Interpretation.true_cls_def consistent_interp_alt_def by (rule bexE, assumption) (case_tac x; auto) lemma total_implies_partial_true_clss_partial_model_of: assumes ‹Herbrand_Interpretation.true_clss I C› shows ‹Partial_Herbrand_Interpretation.true_clss (partial_model_of I) C› using assms unfolding Partial_Herbrand_Interpretation.true_clss_def Herbrand_Interpretation.true_clss_def by (auto simp: total_implies_partial_true_cls_partial_model_of) lemma partial_total_satisfiable_iff: ‹Partial_Herbrand_Interpretation.satisfiable N ⟷ Herbrand_Interpretation.satisfiable N› by (meson consistent_interp_partial_model_of partial_implies_total_true_clss_total_model_of satisfiable_carac total_implies_partial_true_clss_partial_model_of) end