Theory ORD_RES_9

theory ORD_RES_9
  imports
    ORD_RES_8
begin

section ‹ORD-RES-9 (factorize when propagating)›

context simulation_SCLFOL_ground_ordered_resolution begin

inductive ord_res_9 where
  decide_neg: "
    ¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C) ⟹
    linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
      ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A ⟹
    ¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)) ⟹
    Γ' = (Neg A, None) # Γ ⟹
    ord_res_9 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r, ℱ, Γ')" |

  propagate: "
    ¬ (∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C) ⟹
    linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
      ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A ⟹
    linorder_cls.is_least_in_fset {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r).
      clause_could_propagate Γ C (Pos A)|} C ⟹
    Γ' = (Pos A, Some (efac C)) # Γ ⟹
    ℱ' = (if linorder_lit.is_greatest_in_mset C (Pos A) then ℱ else finsert C ℱ) ⟹
    ord_res_9 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r, ℱ', Γ')" |

  resolution: "
    linorder_cls.is_least_in_fset {|D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ D|} D ⟹
    linorder_lit.is_maximal_in_mset D (Neg A) ⟹
    map_of Γ (Pos A) = Some (Some C) ⟹
    U⇩e⇩r' = finsert (eres C D) U⇩e⇩r ⟹
    Γ' = dropWhile (λLn. ∀K.
      linorder_lit.is_maximal_in_mset (eres C D) K ⟶ atm_of K ≼⇩t atm_of (fst Ln)) Γ ⟹
    ord_res_9 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r', ℱ, Γ')"

lemma right_unique_ord_res_9:
  fixes N :: "'f gclause fset"
  shows "right_unique (ord_res_9 N)"
proof (rule right_uniqueI)
  fix x y z
  assume step1: "ord_res_9 N x y" and step2: "ord_res_9 N x z"
  show "y = z"
    using step1
  proof (cases N x y rule: ord_res_9.cases)
    case hyps1: (decide_neg ℱ U⇩e⇩r Γ A⇩1 Γ⇩1')
    show ?thesis
      using step2 unfolding ‹x = (U⇩e⇩r, ℱ, Γ)›
    proof (cases N "(U⇩e⇩r, ℱ, Γ)" z rule: ord_res_9.cases)
      case (decide_neg A Γ')
      with hyps1 show ?thesis
        by (metis (no_types, lifting) linorder_trm.dual_order.asym
            linorder_trm.is_least_in_fset_iff)
    next
      case (propagate A C Γ' ℱ')
      with hyps1 have False
        by (metis (no_types, lifting) linorder_cls.is_least_in_ffilter_iff
            linorder_trm.dual_order.asym linorder_trm.is_least_in_ffilter_iff)
      thus ?thesis ..
    next
      case (resolution D A C U⇩e⇩r' Γ')
      with hyps1 have False
        by (metis (no_types, lifting) linorder_cls.is_least_in_ffilter_iff)
      thus ?thesis ..
    qed
  next
    case hyps1: (propagate ℱ U⇩e⇩r Γ A⇩1 C⇩1 Γ⇩1' ℱ⇩1')
    show ?thesis
      using step2 unfolding ‹x = (U⇩e⇩r, ℱ, Γ)›
    proof (cases N "(U⇩e⇩r, ℱ, Γ)" z rule: ord_res_9.cases)
      case (decide_neg A Γ')
      with hyps1 have False
        by (metis (no_types, lifting) Uniq_D linorder_cls.is_least_in_ffilter_iff
            linorder_trm.Uniq_is_least_in_fset)
      thus ?thesis ..
    next
      case (propagate A C Γ' ℱ')
      with hyps1 show ?thesis
        by (metis (no_types, lifting) linorder_cls.dual_order.asym
            linorder_cls.is_least_in_ffilter_iff linorder_trm.dual_order.asym
            linorder_trm.is_least_in_fset_iff)
    next
      case (resolution D A C U⇩e⇩r' Γ')
      with hyps1 have False
        by (metis (no_types) linorder_cls.is_least_in_ffilter_iff)
      thus ?thesis ..
    qed
  next
    case hyps1: (resolution Γ ℱ U⇩e⇩r D⇩1 A⇩1 C⇩1 U⇩e⇩r⇩1' Γ⇩1')
    show ?thesis
      using step2 unfolding ‹x = (U⇩e⇩r, ℱ, Γ)›
    proof (cases N "(U⇩e⇩r, ℱ, Γ)" z rule: ord_res_9.cases)
      case (decide_neg A Γ')
      with hyps1 have False
        by (metis (no_types) linorder_cls.is_least_in_ffilter_iff)
      thus ?thesis ..
    next
      case (propagate A C Γ' ℱ')
      with hyps1 have False
        by (metis (no_types) linorder_cls.is_least_in_ffilter_iff)
      thus ?thesis ..
    next
      case hyps2: (resolution D A C U⇩e⇩r' Γ')
      have "D⇩1 = D"
        using hyps1 hyps2
        by (metis (no_types) Uniq_D linorder_cls.Uniq_is_least_in_fset)
      have "C⇩1 = C"
        using hyps1 hyps2
        unfolding ‹D⇩1 = D›
        by (metis (no_types) Uniq_D linorder_lit.Uniq_is_maximal_in_mset option.inject uminus_Neg)
      show ?thesis
        using hyps1 hyps2
        unfolding ‹D⇩1 = D› ‹C⇩1 = C›
        by argo
    qed
  qed
qed

lemma ord_res_9_is_one_or_two_ord_res_9_steps:
  fixes N s s'
  assumes step: "ord_res_9 N s s'"
  shows "ord_res_8 N s s' ∨ (ord_res_8 N OO ord_res_8 N) s s'"
  using step
proof (cases N s s' rule: ord_res_9.cases)
  case step_hyps: (decide_neg ℱ U⇩e⇩r Γ A Γ')
  show ?thesis
  proof (rule disjI1)
    show "ord_res_8 N s s'"
      using step_hyps ord_res_8.decide_neg by (simp only:)
  qed
next
  case step_hyps: (propagate ℱ U⇩e⇩r Γ A C Γ' ℱ')

  have
    C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    C_could_prop: "clause_could_propagate Γ C (Pos A)" and
    C_lt: "∀D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r).
        D ≠ C ⟶ clause_could_propagate Γ D (Pos A) ⟶ C ≺⇩c D"
    using step_hyps unfolding atomize_conj linorder_cls.is_least_in_ffilter_iff by argo

  hence C_max_lit: "ord_res.is_maximal_lit (Pos A) C"
    unfolding clause_could_propagate_def by argo

  show ?thesis
  proof (cases "ord_res.is_strictly_maximal_lit (Pos A) C")
    case True

    hence "efac C = C"
      using nex_strictly_maximal_pos_lit_if_neq_efac by force

    thus ?thesis
      using True step_hyps ord_res_8.propagate by simp
  next
    case False

    have "ℱ' = finsert C ℱ"
      using False step_hyps by simp

    have "efac C ≠ C"
      using False C_max_lit by (metis greatest_literal_in_efacI literal.disc(1))

    hence C_in': "C |∈| N |∪| U⇩e⇩r"
      using C_in
      by (smt (verit, ccfv_threshold) fimage_iff iefac_def ex1_efac_eq_factoring_chain
          factorizable_if_neq_efac)

    have "C |∉| ℱ"
      by (smt (verit, ccfv_threshold) C_in ‹efac C ≠ C› factorizable_if_neq_efac fimage_iff
          ex1_efac_eq_factoring_chain iefac_def)

    have fimage_iefac_ℱ'_eq:
      "iefac ℱ' |`| (N |∪| U⇩e⇩r) = finsert (efac C) ((iefac ℱ |`| (N |∪| U⇩e⇩r)) - {|C|})"
    proof (intro fsubset_antisym fsubsetI)
      fix x :: "'f gclause"
      assume "x |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
      then obtain x' where "x' |∈| N |∪| U⇩e⇩r" and "x = iefac ℱ' x'"
        by blast
      thus "x |∈| finsert (efac C) ((iefac ℱ |`| (N |∪| U⇩e⇩r)) |-| {|C|})"
      proof (cases "x' = C")
        case True
        hence "x = efac C"
          using ‹x = iefac ℱ' x'› by (simp add: ‹ℱ' = finsert C ℱ› iefac_def)
        thus ?thesis
          using ‹efac C ≠ C› by simp
      next
        case False
        hence "x = iefac ℱ x'"
          using ‹x = iefac ℱ' x'› by (auto simp add: ‹ℱ' = finsert C ℱ› iefac_def)
        then show ?thesis
          by (metis (no_types, lifting) False ‹x' |∈| N |∪| U⇩e⇩r› ex1_efac_eq_factoring_chain
              factorizable_if_neq_efac fimage_eqI finsertCI fminus_iff fsingletonE iefac_def)
      qed
    next
      fix x :: "'f gclause"
      assume x_in: "x |∈| finsert (efac C) (iefac ℱ |`| (N |∪| U⇩e⇩r) |-| {|C|})"
      hence "x = efac C ∨ x |∈| (iefac ℱ |`| (N |∪| U⇩e⇩r) |-| {|C|})"
        by blast
      thus "x |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
      proof (elim disjE)
        assume "x = efac C"
        hence "x = iefac ℱ' C"
          by (simp add: ‹ℱ' = finsert C ℱ› iefac_def)
        thus "x |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
          using ‹C |∈| N |∪| U⇩e⇩r› by blast
      next
        assume "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r) |-| {|C|}"
        hence "x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "x ≠ C"
          by simp_all
        then obtain x' where "x' |∈| N |∪| U⇩e⇩r" and "x = iefac ℱ x'"
          by auto
        moreover have "x' ≠ C"
          using ‹x ≠ C› ‹x = iefac ℱ x'›
          using ‹C |∉| ℱ› iefac_def by force
        ultimately show "x |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
          by (simp add: ‹ℱ' = finsert C ℱ› iefac_def)
      qed
    qed

    have first_step8: "ord_res_8 N (U⇩e⇩r, ℱ, Γ) (U⇩e⇩r, ℱ', Γ)"
      using False step_hyps ord_res_8.factorize by simp

    moreover have "ord_res_8 N (U⇩e⇩r, ℱ', Γ) (U⇩e⇩r, ℱ', Γ')"
    proof (rule ord_res_8.propagate)
      have "¬ trail_false_cls Γ C"
        using step_hyps using C_in by metis

      hence "¬ trail_false_cls Γ (efac C)"
        by (simp add: trail_false_cls_def)

      thus "¬ (∃C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C)"
        using step_hyps unfolding fimage_iefac_ℱ'_eq by blast
    next
      show "linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
          ∀A⇩1|∈|trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A"
        using step_hyps by argo
    next
      show "linorder_cls.is_least_in_fset {|C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r).
            clause_could_propagate Γ C (Pos A)|} (efac C)"
        unfolding linorder_cls.is_least_in_ffilter_iff
      proof (intro conjI ballI impI)
        show "efac C |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)"
          unfolding fimage_iefac_ℱ'_eq by simp
      next
        show "clause_could_propagate Γ (efac C) (Pos A)"
          using C_could_prop
          unfolding clause_could_propagate_def
          by (simp add: trail_false_cls_def greatest_literal_in_efacI
              linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset)
      next
        fix D :: "'f gterm literal multiset"
        assume
          "D |∈| iefac ℱ' |`| (N |∪| U⇩e⇩r)" and
          "D ≠ efac C" and
          "clause_could_propagate Γ D (Pos A)"
        thus "efac C ≺⇩c D"
          using C_lt
          by (metis (no_types, opaque_lifting) C_in efac_properties_if_not_ident(1)
              fimage_iefac_ℱ'_eq finsert_fminus finsert_iff linorder_cls.less_trans)
      qed
    next
      show "ord_res.is_strictly_maximal_lit (Pos A) (efac C)"
        using step_hyps
        by (simp add: clause_could_propagate_def greatest_literal_in_efacI
            linorder_cls.is_least_in_ffilter_iff)
    next
      show "Γ' = (Pos A, Some (efac C)) # Γ"
        using step_hyps by argo
    qed

    ultimately have "(ord_res_8 N OO ord_res_8 N) s s'"
      using step_hyps by blast

    thus ?thesis
      by argo
  qed
next
  case step_hyps: (resolution Γ ℱ U⇩e⇩r D A C U⇩e⇩r' Γ')
  show ?thesis
  proof (rule disjI1)
    show "ord_res_8 N s s'"
      using step_hyps ord_res_8.resolution by (simp only:)
  qed
qed

lemma ord_res_9_preserves_invars:
  assumes
    step: "ord_res_9 N s s'" and
    invars: "ord_res_8_invars N s"
  shows "ord_res_8_invars N s'"
  using invars ord_res_9_is_one_or_two_ord_res_9_steps
  by (metis local.step ord_res_8_preserves_invars relcomppE)

lemma rtranclp_ord_res_9_preserves_ord_res_8_invars:
  assumes
    step: "(ord_res_9 N)⇧*⇧* s s'" and
    invars: "ord_res_8_invars N s"
  shows "ord_res_8_invars N s'"
  using step invars ord_res_9_preserves_invars
  by (smt (verit, del_insts) rtranclp_induct)

lemma ex_ord_res_9_if_not_final:
  assumes
    not_final: "¬ ord_res_8_final (N, s)" and
    invars: "ord_res_8_invars N s"
  shows "∃s'. ord_res_9 N s s'"
proof -
  obtain U⇩e⇩r ℱ Γ where "s = (U⇩e⇩r, ℱ, Γ)"
    by (metis surj_pair)

  note invars' = invars[unfolded ‹s = (U⇩e⇩r, ℱ, Γ)› ord_res_8_invars_def]
  
  have
    undef_atm_or_false_cls: "
      (∃x |∈| atms_of_clss (N |∪| U⇩e⇩r). x |∉| trail_atms Γ) ∧
        ¬ (∃x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x)∨
      (∃x |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x)" and
    "{#} |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)"
    unfolding atomize_conj
    using not_final[unfolded ord_res_8_final.simps] ‹s = (U⇩e⇩r, ℱ, Γ)› by metis

  show ?thesis
    using undef_atm_or_false_cls
  proof (elim disjE conjE)
    assume
      ex_undef_atm: "∃x |∈| atms_of_clss (N |∪| U⇩e⇩r). x |∉| trail_atms Γ" and
      no_conflict: "¬ (∃x|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x)"

    moreover have "{|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r). ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} ≠ {||}"
    proof -
      obtain A⇩2 :: "'f gterm" where
        A⇩2_in: "A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r)" and
        A⇩2_undef: "A⇩2 |∉| trail_atms Γ"
        using ex_undef_atm by metis

      have "A⇩1 ≺⇩t A⇩2" if A⇩1_in: "A⇩1 |∈| trail_atms Γ" for A⇩1 :: "'f gterm"
      proof -
        have "A⇩1 ≠ A⇩2"
          using A⇩1_in A⇩2_undef by metis

        moreover have "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))"
          using invars'[unfolded trail_is_lower_set_def, simplified] by argo

        ultimately show ?thesis
          by (meson A⇩2_in A⇩2_undef linorder_trm.is_lower_set_iff linorder_trm.linorder_cases that)
      qed

      thus ?thesis
        using A⇩2_in
        by (smt (verit, ccfv_threshold) femptyE ffmember_filter)
    qed

    ultimately obtain A :: "'f gterm" where
      A_least: "linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
        ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A"
      using ex_undef_atm linorder_trm.ex_least_in_fset by presburger

    show "∃s'. ord_res_9 N s s'"
    proof (cases "∃C|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)")
      case True
      hence "{|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)|} ≠ {||}"
        by force

      then obtain C where
        C_least: "linorder_cls.is_least_in_fset
          {|C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). clause_could_propagate Γ C (Pos A)|} C"
        using linorder_cls.ex1_least_in_fset by meson

      show ?thesis
        unfolding ‹s = (U⇩e⇩r, ℱ, Γ)›
        using ord_res_9.propagate[OF no_conflict A_least C_least]
        by metis
    next
      case False
      thus ?thesis
        unfolding ‹s = (U⇩e⇩r, ℱ, Γ)›
        using ord_res_9.decide_neg[OF no_conflict A_least] by metis
    qed
  next
    assume "∃x|∈|iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ x"
    then obtain D :: "'f gclause" where
      D_least: "linorder_cls.is_least_in_fset
        (ffilter (trail_false_cls Γ) (iefac ℱ |`| (N |∪| U⇩e⇩r))) D"
      by (metis femptyE ffmember_filter linorder_cls.ex_least_in_fset)

    hence "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and "trail_false_cls Γ D"
      unfolding atomize_conj linorder_cls.is_least_in_ffilter_iff by argo

    moreover have "D ≠ {#}"
      using ‹D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)› ‹{#} |∉| iefac ℱ |`| (N |∪| U⇩e⇩r)› by metis

    ultimately obtain A where Neg_A_max: "linorder_lit.is_maximal_in_mset D (Neg A)"
      using invars' false_cls_is_mempty_or_has_neg_max_lit_def by metis

    hence "trail_false_lit Γ (Neg A)"
      using ‹trail_false_cls Γ D›
      by (metis linorder_lit.is_maximal_in_mset_iff trail_false_cls_def)

    hence "Pos A ∈ fst ` set Γ"
      unfolding trail_false_lit_def by simp

    hence "∃C. (Pos A, Some C) ∈ set Γ"
      using invars'[unfolded decided_literals_all_neg_def, simplified]
      by fastforce

    then obtain C :: "'f gclause" where
      "map_of Γ (Pos A) = Some (Some C)"
      by (metis invars' is_pos_def map_of_SomeD not_Some_eq decided_literals_all_neg_def
          weak_map_of_SomeI)

    thus "∃s'. ord_res_9 N s s'"
      unfolding ‹s = (U⇩e⇩r, ℱ, Γ)›
      using ord_res_9.resolution D_least Neg_A_max by blast
  qed
qed

lemma ord_res_9_safe_state_if_invars:
  fixes N s
  assumes invars: "ord_res_8_invars N s"
  shows "safe_state (constant_context ord_res_9) ord_res_8_final (N, s)"
  using safe_state_constant_context_if_invars[where
      ℛ = ord_res_9 and ℱ = ord_res_8_final and ℐ = ord_res_8_invars]
  using ord_res_9_preserves_invars ex_ord_res_9_if_not_final invars by metis

sublocale ord_res_9_semantics: semantics where
  step = "constant_context ord_res_9" and
  final = ord_res_8_final
proof unfold_locales
  fix S :: "'f gclause fset ×'f gclause fset × 'f gclause fset ×
    ('f gliteral × 'f gclause option) list"

  obtain
    N U⇩e⇩r ℱ :: "'f gterm clause fset" and
    Γ :: "('f gterm literal × 'f gterm literal multiset option) list" where
    S_def: "S = (N, U⇩e⇩r, ℱ, Γ)"
    by (metis prod.exhaust)

  assume "ord_res_8_final S"

  hence "∄x. ord_res_9 N (U⇩e⇩r, ℱ, Γ) x"
    unfolding S_def
  proof (cases "(N, U⇩e⇩r, ℱ, Γ)" rule: ord_res_8_final.cases)
    case model_found

    have "∄A. linorder_trm.is_least_in_fset {|A⇩2 |∈| atms_of_clss (N |∪| U⇩e⇩r).
      ∀A⇩1 |∈| trail_atms Γ. A⇩1 ≺⇩t A⇩2|} A"
      using ‹¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A |∉| trail_atms Γ)›
      using linorder_trm.is_least_in_ffilter_iff by fastforce

    moreover have "∄C. linorder_cls.is_least_in_fset
      (ffilter (trail_false_cls Γ) (iefac ℱ |`| (N |∪| U⇩e⇩r))) C"
      using ‹¬ fBex (iefac ℱ |`| (N |∪| U⇩e⇩r)) (trail_false_cls Γ)›
      by (metis linorder_cls.is_least_in_ffilter_iff)

    ultimately show ?thesis
      unfolding ord_res_9.simps by blast
  next
    case contradiction_found

    hence "∃C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). trail_false_cls Γ C"
      using trail_false_cls_mempty by metis

    moreover have "∄D A. linorder_cls.is_least_in_fset (ffilter (trail_false_cls Γ)
      (iefac ℱ |`| (N |∪| U⇩e⇩r))) D ∧ ord_res.is_maximal_lit (Neg A) D"
      by (metis empty_iff linorder_cls.is_least_in_ffilter_iff linorder_cls.leD
          linorder_lit.is_maximal_in_mset_iff local.contradiction_found(1) mempty_lesseq_cls
          set_mset_empty trail_false_cls_mempty)

    ultimately show ?thesis
      unfolding ord_res_9.simps by blast
  qed

  thus "finished (constant_context ord_res_9) S"
    by (simp add: S_def finished_def constant_context.simps)
qed

end

end