Theory ORD_RES_4

theory ORD_RES_4
  imports
    ORD_RES
    Implicit_Exhaustive_Factorization
    Exhaustive_Resolution
begin

section ‹ORD-RES-4 (implicit factorization)›

context simulation_SCLFOL_ground_ordered_resolution begin

inductive ord_res_4 where
  factoring: "
    NN = iefac ℱ |`| (N |∪| U⇩e⇩r) ⟹
    is_least_false_clause NN C ⟹
    linorder_lit.is_maximal_in_mset C L ⟹
    is_pos L ⟹
    ℱ' = finsert C ℱ ⟹
    ord_res_4 N (U⇩e⇩r, ℱ) (U⇩e⇩r, ℱ')" |

  resolution: "
    NN = iefac ℱ |`| (N |∪| U⇩e⇩r) ⟹
    is_least_false_clause NN C ⟹
    linorder_lit.is_maximal_in_mset C L ⟹
    is_neg L ⟹
    D |∈| NN ⟹
    D ≺⇩c C ⟹
    ord_res.production (fset NN) D = {atm_of L} ⟹
    U⇩e⇩r' = finsert (eres D C) U⇩e⇩r ⟹
    ord_res_4 N (U⇩e⇩r, ℱ) (U⇩e⇩r', ℱ)"

inductive ord_res_4_step where
  "ord_res_4 N s s' ⟹ ord_res_4_step (N, s) (N, s')"

inductive ord_res_4_final where
  "ord_res_final (iefac ℱ |`| (N |∪| U⇩e⇩r)) ⟹ ord_res_4_final (N, U⇩e⇩r, ℱ)"

sublocale ord_res_4_semantics: semantics where
  step = ord_res_4_step and
  final = ord_res_4_final
proof unfold_locales
  fix S4 :: "'f gterm clause fset × 'f gterm clause fset × 'f gterm clause fset"

  obtain N U⇩e⇩r ℱ :: "'f gterm clause fset" where
    S4_def: "S4 = (N, (U⇩e⇩r, ℱ))"
    by (metis prod.exhaust)

  assume "ord_res_4_final S4"
  hence "{#} |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) ∨ ¬ ex_false_clause (fset (iefac ℱ |`| (N |∪| U⇩e⇩r)))"
    by (simp add: S4_def ord_res_4_final.simps ord_res_final_def)
  thus "finished ord_res_4_step S4"
  proof (elim disjE)
    assume "{#} |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
    hence "is_least_false_clause (iefac ℱ |`| (N |∪| U⇩e⇩r)) {#}"
      using is_least_false_clause_mempty by metis
    hence "∄C L. is_least_false_clause (iefac ℱ |`| (N |∪| U⇩e⇩r)) C ∧ linorder_lit.is_maximal_in_mset C L"
      by (metis Uniq_D Uniq_is_least_false_clause bot_fset.rep_eq fBex_fempty
          linorder_lit.is_maximal_in_mset_iff set_mset_empty)
    hence "∄x. ord_res_4 N (U⇩e⇩r, ℱ) x"
      by (auto simp: S4_def elim: ord_res_4.cases)
    thus ?thesis
      by (simp add: S4_def finished_def ord_res_4_step.simps)
  next
    assume "¬ ex_false_clause (fset (iefac ℱ |`| (N |∪| U⇩e⇩r)))"
    hence "∄C. is_least_false_clause (iefac ℱ |`| (N |∪| U⇩e⇩r)) C"
      unfolding ex_false_clause_def is_least_false_clause_def
      by (metis (no_types, lifting) linorder_cls.is_least_in_fset_ffilterD(1)
          linorder_cls.is_least_in_fset_ffilterD(2))
    hence "∄x. ord_res_4 N (U⇩e⇩r, ℱ) x"
      by (auto simp: S4_def elim: ord_res_4.cases)
    thus ?thesis
      by (simp add: S4_def finished_def ord_res_4_step.simps)
  qed
qed

lemma right_unique_ord_res_4: "right_unique (ord_res_4 N)"
proof (rule right_uniqueI)
  fix s s' s'' :: "'f gterm clause fset × 'f gterm clause fset"
  assume step1: "ord_res_4 N s s'" and step2: "ord_res_4 N s s''"
  show "s' = s''"
    using step1
  proof (cases N s s' rule: ord_res_4.cases)
    case hyps1: (factoring NN1 ℱ1 U⇩e⇩r1 C1 L1 ℱ1')
    show ?thesis
      using step2
    proof (cases N s s'' rule: ord_res_4.cases)
      case (factoring NN2 ℱ2 U⇩e⇩r2 C2 L2 ℱ2')
      with hyps1 show ?thesis
        by (metis Uniq_D Uniq_is_least_false_clause prod.inject)
    next
      case (resolution NN2 ℱ2 U⇩e⇩r2 C2 L2 D2 U⇩e⇩r2')
      with hyps1 have False
        by (metis Pair_inject Uniq_is_least_false_clause linorder_lit.Uniq_is_maximal_in_mset
          the1_equality')
      thus ?thesis ..
    qed
  next
    case hyps1: (resolution NN1 ℱ1 U⇩e⇩r1 C1 L1 D1 U⇩e⇩r1')
    show ?thesis
      using step2
    proof (cases N s s'' rule: ord_res_4.cases)
      case (factoring NN ℱ U⇩e⇩r C L ℱ')
      with hyps1 have False
        by (metis Pair_inject Uniq_is_least_false_clause linorder_lit.Uniq_is_maximal_in_mset
          the1_equality')
      thus ?thesis ..
    next
      case (resolution NN ℱ U⇩e⇩r C L D U⇩e⇩r')
      with hyps1 show ?thesis
        by (metis (mono_tags, lifting) Uniq_D Uniq_is_least_false_clause
          ord_res.less_trm_iff_less_cls_if_mem_production insertI1 linorder_cls.neq_iff
          linorder_lit.Uniq_is_maximal_in_mset prod.inject)
    qed
  qed
qed

lemma right_unique_ord_res_4_step: "right_unique ord_res_4_step"
proof (rule right_uniqueI)
  fix x y z
  show "ord_res_4_step x y ⟹ ord_res_4_step x z ⟹ y = z"
    using right_unique_ord_res_4[THEN right_uniqueD]
    by (elim ord_res_4_step.cases) (metis prod.inject)
qed

lemma ex_ord_res_4_if_not_final:
  assumes "¬ ord_res_4_final S"
  shows "∃S'. ord_res_4_step S S'"
proof -
  from assms obtain N U⇩e⇩r ℱ where
    S_def: "S = (N, (U⇩e⇩r, ℱ))" and
    "{#} |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    "ex_false_clause (fset (iefac ℱ |`| (N |∪| U⇩e⇩r)))"
    by (metis ord_res_4_final.intros ord_res_final_def surj_pair)

  obtain C where C_least_false: "is_least_false_clause (iefac ℱ |`| (N |∪| U⇩e⇩r)) C"
    using ‹ex_false_clause (fset (iefac ℱ |`| (N |∪| U⇩e⇩r)))›
      obtains_least_false_clause_if_ex_false_clause
    by metis

  hence "C ≠ {#}"
    using ‹{#} |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)›
    unfolding is_least_false_clause_def linorder_cls.is_least_in_ffilter_iff
    by metis

  then obtain L where C_max: "linorder_lit.is_maximal_in_mset C L"
    using linorder_lit.ex_maximal_in_mset by metis

  show ?thesis
  proof (cases L)
    case (Pos A)
    thus ?thesis
      using ord_res_4.factoring[OF refl C_least_false C_max] S_def is_pos_def
      by (metis ord_res_4_step.intros)
  next
    case (Neg A)
    then obtain D where
      "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
      "D ≺⇩c C" and
      "ord_res.is_strictly_maximal_lit (Pos A) D" and
      "ord_res.production (fset (iefac ℱ |`| (N |∪| U⇩e⇩r))) D = {A}"
      using bex_smaller_productive_clause_if_least_false_clause_has_negative_max_lit
      using C_least_false C_max by metis

    thus ?thesis
      using ord_res_4.resolution[OF refl C_least_false C_max]
      by (metis Neg S_def literal.disc(2) literal.sel(2) ord_res_4_step.simps)
  qed
qed

corollary ord_res_4_step_safe: "ord_res_4_final S ∨ (∃S'. ord_res_4_step S S')"
  using ex_ord_res_4_if_not_final by metis

end

end