Theory Partial_And_Total_Herbrand_Interpretation

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