Theory Implicit_Exhaustive_Factorization

theory Implicit_Exhaustive_Factorization
  imports
    Exhaustive_Factorization
    Exhaustive_Resolution
begin

section ‹Function for implicit full factorization›

context simulation_SCLFOL_ground_ordered_resolution begin

definition iefac where
  "iefac ℱ C = (if C |∈| ℱ then efac C else C)"

lemma iefac_mempty[simp]:
  fixes ℱ :: "'f gclause fset"
  shows "iefac ℱ {#} = {#}"
  by (metis efac_mempty iefac_def)

lemma fset_mset_iefac[simp]: 
  fixes ℱ :: "'f gclause fset" and C :: "'f gclause"
  shows "fset_mset (iefac ℱ C) = fset_mset C"
proof (cases "C |∈| ℱ")
  case True
  hence "iefac ℱ C = efac C"
    unfolding iefac_def by simp
  thus ?thesis
    by auto
next
  case False
  hence "iefac ℱ C = C"
    unfolding iefac_def by simp
  thus ?thesis by simp
qed

lemma atms_of_cls_iefac[simp]:
  fixes ℱ :: "'f gclause fset" and C :: "'f gclause"
  shows "atms_of_cls (iefac ℱ C) = atms_of_cls C"
  by (simp add: atms_of_cls_def)

lemma iefac_le:
  fixes ℱ :: "'f gclause fset" and C :: "'f gclause"
  shows "iefac ℱ C ≼⇩c C"
  by (metis efac_subset iefac_def reflclp_iff subset_implies_reflclp_multp)

lemma true_cls_iefac_iff[simp]:
  fixes ℐ :: "'f gterm set" and ℱ :: "'f gclause fset" and C :: "'f gclause"
  shows "ℐ ⊫ iefac ℱ C ⟷ ℐ ⊫ C"
  by (metis iefac_def true_cls_efac_iff)

(*
ifac |`| (N |∪| U⇩e⇩r) |⊆| (N |∪| U⇩e⇩r |∪| U⇩e⇩f) = (ifac |`| (N |∪| U⇩e⇩r)) |∪| N |∪| U⇩e⇩r
*)
lemma funion_funion_eq_funion_funion_fimage_iefac_if:
  assumes U⇩e⇩f_eq: "U⇩e⇩f = iefac ℱ |`| {|C |∈| N |∪| U⇩e⇩r. iefac ℱ C ≠ C|}"
  shows "N |∪| U⇩e⇩r |∪| U⇩e⇩f = N |∪| U⇩e⇩r |∪| (iefac ℱ |`| (N |∪| U⇩e⇩r))"
proof (intro fsubset_antisym fsubsetI)
  fix C :: "'f gterm clause"
  assume "C |∈| N |∪| U⇩e⇩r |∪| U⇩e⇩f"
  hence "C |∈| N |∪| U⇩e⇩r ∨ C |∈| U⇩e⇩f"
    by simp
  thus "C |∈| N |∪| U⇩e⇩r |∪| (iefac ℱ |`| (N |∪| U⇩e⇩r))"
  proof (elim disjE)
    assume "C |∈| N |∪| U⇩e⇩r"
    thus ?thesis
      by simp
  next
    assume "C |∈| U⇩e⇩f"
    hence "C |∈| iefac ℱ |`| {|C |∈| N |∪| U⇩e⇩r. iefac ℱ C ≠ C|}"
      using U⇩e⇩f_eq by argo
    then obtain C⇩0 :: "'f gterm clause" where
      "C⇩0 |∈| N |∪| U⇩e⇩r" and "iefac ℱ C⇩0 ≠ C⇩0" and "C = iefac ℱ C⇩0"
      by auto
    thus ?thesis
      by simp
  qed
next
  fix C :: "'f gterm clause"
  assume "C |∈| N |∪| U⇩e⇩r |∪| (iefac ℱ |`| (N |∪| U⇩e⇩r))"
  hence "C |∈| N |∪| U⇩e⇩r ∨ C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
    by simp
  thus "C |∈| N |∪| U⇩e⇩r |∪| U⇩e⇩f"
  proof (elim disjE)
    assume "C |∈| N |∪| U⇩e⇩r"
    thus ?thesis
      by simp
  next
    assume "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)"
    then obtain C⇩0 :: "'f gterm clause" where
      "C⇩0 |∈| N |∪| U⇩e⇩r" and "C = iefac ℱ C⇩0"
      by auto

    show ?thesis
    proof (cases "iefac ℱ C⇩0 = C⇩0")
      case True
      hence "C = C⇩0"
        using ‹C = iefac ℱ C⇩0› by argo
      thus ?thesis
        using ‹C⇩0 |∈| N |∪| U⇩e⇩r› by simp
    next
      case False
      hence "C |∈| U⇩e⇩f"
        unfolding U⇩e⇩f_eq
        using ‹C⇩0 |∈| N |∪| U⇩e⇩r› ‹C = iefac ℱ C⇩0› by simp
      thus ?thesis
        by simp
    qed
  qed
qed


lemma clauses_for_iefac_are_unproductive:
  "∀C |∈| N |-| iefac ℱ |`| N. ∀U. ord_res.production U C = {}"
proof (intro ballI allI)
  fix C U
  assume "C |∈| N |-| iefac ℱ |`| N"
  hence "C |∈| N" and "C |∉| iefac ℱ |`| N"
    by simp_all
  hence "iefac ℱ C ≠ C"
    by (metis fimage_iff)
  hence "efac C ≠ C"
    by (metis iefac_def)
  hence "∄L. is_pos L ∧ ord_res.is_strictly_maximal_lit L C"
    using nex_strictly_maximal_pos_lit_if_neq_efac by metis
  thus "ord_res.production U C = {}"
    using unproductive_if_nex_strictly_maximal_pos_lit by metis
qed

lemma clauses_for_iefac_have_smaller_entailing_clause:
  "∀C |∈| N |-| iefac ℱ |`| N. ∃D |∈| iefac ℱ |`| N. D ≺⇩c C ∧ {D} ⊫e {C}"
proof (intro ballI allI)
  fix C
  assume "C |∈| N |-| iefac ℱ |`| N"
  hence "C |∈| N" and "C |∉| iefac ℱ |`| N"
    by simp_all
  hence "iefac ℱ C ≠ C"
    by (metis fimage_iff)
  hence "efac C ≠ C"
    by (metis iefac_def)

  show "∃D |∈| iefac ℱ |`| N. D ≺⇩c C ∧ {D} ⊫e {C}"
  proof (intro bexI conjI)
    show "efac C ≺⇩c C" and "{efac C} ⊫e {C}"
      using efac_properties_if_not_ident[OF ‹efac C ≠ C›] by simp_all
  next
    show "efac C |∈| iefac ℱ |`| N"
      using ‹C |∈| N› ‹iefac ℱ C ≠ C› by (metis fimageI iefac_def)
  qed
qed

lemma is_least_false_clause_with_iefac_conv:
  "is_least_false_clause (N |∪| U⇩e⇩r |∪| iefac ℱ |`| (N |∪| U⇩e⇩r)) =
    is_least_false_clause (iefac ℱ |`| (N |∪| U⇩e⇩r))"
  using is_least_false_clause_funion_cancel_right_strong[OF clauses_for_iefac_are_unproductive
    clauses_for_iefac_have_smaller_entailing_clause]
  by (simp add: sup_commute)

lemma MAGIC4:
  fixes N ℱ ℱ' U⇩e⇩r U⇩e⇩r'
  defines
    "N1 ≡ iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    "N2 ≡ iefac ℱ' |`| (N |∪| U⇩e⇩r')"
  assumes
    subsets_agree: "{|x |∈| N1. x ≺⇩c C|} = {|x |∈| N2. x ≺⇩c C|}" and
    "is_least_false_clause N1 D" and
    "is_least_false_clause N2 E" and
    "C ≺⇩c D"
  shows "C ≼⇩c E"
proof -
  have "¬ E ≺⇩c C"
  proof (rule notI)
    assume "E ≺⇩c C"

    have "is_least_false_clause N2 E ⟷ is_least_false_clause {|x |∈| N2. x ≼⇩c E|} E"
    proof (rule is_least_false_clause_swap_swap_compatible_fsets)
      show "{|x |∈| N2. (≺⇩c)⇧=⇧= x E|} = {|x |∈| {|x |∈| N2. (≺⇩c)⇧=⇧= x E|}. (≺⇩c)⇧=⇧= x E|}"
        using ‹E ≺⇩c C› by force
    qed

    also have "… ⟷ is_least_false_clause {|x |∈| N1. x ≼⇩c E|} E"
    proof (rule is_least_false_clause_swap_swap_compatible_fsets)
      show "{|x |∈| {|x |∈| N2. (≺⇩c)⇧=⇧= x E|}. (≺⇩c)⇧=⇧= x E|} =
        {|x |∈| {|x |∈| N1. (≺⇩c)⇧=⇧= x E|}. (≺⇩c)⇧=⇧= x E|}"
        using subsets_agree ‹E ≺⇩c C› by fastforce
    qed

    also have "… ⟷ is_least_false_clause N1 E"
    proof (rule is_least_false_clause_swap_swap_compatible_fsets)
      show "{|x |∈| {|x |∈| N1. (≺⇩c)⇧=⇧= x E|}. (≺⇩c)⇧=⇧= x E|} = {|x |∈| N1. (≺⇩c)⇧=⇧= x E|}"
        using ‹E ≺⇩c C› by fastforce
    qed

    finally have "is_least_false_clause N1 E"
      using ‹is_least_false_clause N2 E› by argo

    hence "D = E"
      using ‹is_least_false_clause N1 D›
      by (metis Uniq_is_least_false_clause the1_equality')

    thus False
      using ‹E ≺⇩c C› ‹C ≺⇩c D› by order
  qed
  thus "C ≼⇩c E"
    by order
qed

lemma atms_of_clss_fimage_iefac[simp]:
  "atms_of_clss (iefac ℱ |`| N) = atms_of_clss N"
proof -
  have "atms_of_clss (iefac ℱ |`| N) = ffUnion (atms_of_cls |`| iefac ℱ |`| N)"
    unfolding atms_of_clss_def ..

  also have "… = ffUnion ((atms_of_cls ∘ iefac ℱ) |`| N)"
    by simp

  also have "… = ffUnion (atms_of_cls |`| N)"
    unfolding comp_def atms_of_cls_iefac ..

  also have "… = atms_of_clss N"
    unfolding atms_of_clss_def ..

  finally show ?thesis .
qed

lemma atm_of_in_atms_of_clssI:
  assumes L_in: "L ∈# C" and C_in: "C |∈| iefac ℱ |`| N"
  shows "atm_of L |∈| atms_of_clss N"
proof -
  have "atm_of L |∈| atms_of_cls C"
    unfolding atms_of_cls_def
    using L_in by simp

  hence "atm_of L |∈| atms_of_clss (iefac ℱ |`| N)"
    unfolding atms_of_clss_def
    using C_in by (metis fmember_ffUnion_iff)

  thus "atm_of L |∈| atms_of_clss N"
    by simp
qed

lemma clause_almost_almost_definedI:
  fixes Γ D K
  assumes
    D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    D_max_lit: "ord_res.is_maximal_lit K D" and
    no_undef_atm: "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ)"
  shows "trail_defined_cls Γ {#L ∈# D. L ≠ K ∧ L ≠ - K#}"
  unfolding trail_defined_cls_def
proof (intro ballI)
  have "K ∈# D" and lit_in_D_le_K: "⋀L. L ∈# D ⟹ L ≼⇩l K"
    using D_max_lit
    unfolding atomize_imp atomize_all atomize_conj linorder_lit.is_maximal_in_mset_iff
    using linorder_lit.leI by blast

  fix L :: "'f gterm literal"
  assume "L ∈# {#L ∈# D. L ≠ K ∧ L ≠ - K#}"

  hence "L ∈# D" and "L ≠ K" and "L ≠ - K"
    by simp_all

  have "atm_of L |∈| atms_of_clss (N |∪| U⇩e⇩r)"
    using ‹L ∈# D› D_in by (metis atm_of_in_atms_of_clssI)

  hence "atm_of L ≺⇩t atm_of K ⟹ atm_of L |∈| trail_atms Γ"
    using no_undef_atm by metis

  moreover have "atm_of L ≺⇩t atm_of K"
    using lit_in_D_le_K[OF ‹L ∈# D›] ‹L ≠ K› ‹L ≠ - K›
    by (cases L; cases K) simp_all

  ultimately show "trail_defined_lit Γ L"
    using trail_defined_lit_iff_trail_defined_atm by auto
qed

lemma clause_almost_definedI:
  fixes Γ D K
  assumes
    D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    D_max_lit: "ord_res.is_maximal_lit K D" and
    no_undef_atm: "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≺⇩t atm_of K ∧ A |∉| trail_atms Γ)" and
    K_defined: "trail_defined_lit Γ K"
  shows "trail_defined_cls Γ {#Ka ∈# D. Ka ≠ K#}"
  using clause_almost_almost_definedI[OF D_in D_max_lit no_undef_atm]
  using K_defined
  unfolding trail_defined_cls_def trail_defined_lit_def
  by (metis (mono_tags, lifting) mem_Collect_eq set_mset_filter uminus_lit_swap)

lemma eres_not_in_known_clauses_if_trail_false_cls:
  fixes
    ℱ :: "'f gclause fset" and
    Γ :: "('f gliteral × 'f gclause option) list"
  assumes
    Γ_consistent: "trail_consistent Γ" and
    clauses_lt_E_true: "∀C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r). C ≺⇩c E ⟶ trail_true_cls Γ C" and
    "eres D E ≺⇩c E" and
    "trail_false_cls Γ (eres D E)"
  shows "eres D E |∉| N |∪| U⇩e⇩r"
proof (rule notI)
  have "iefac ℱ (eres D E) ≼⇩c eres D E"
    using iefac_le by metis
  hence "iefac ℱ (eres D E) ≺⇩c E"
    using ‹eres D E ≺⇩c E› by order

  moreover assume "eres D E |∈| N |∪| U⇩e⇩r"

  ultimately have "trail_true_cls Γ (iefac ℱ (eres D E))"
    using clauses_lt_E_true[rule_format, of "iefac ℱ (eres D E)"]
    by (simp add: iefac_def linorder_lit.is_maximal_in_mset_iff)

  hence "trail_true_cls Γ (eres D E)"
    unfolding trail_true_cls_def
    by (metis fset_fset_mset fset_mset_iefac)

  thus False
    using Γ_consistent ‹trail_false_cls Γ (eres D E)›
    by (metis not_trail_true_cls_and_trail_false_cls)
qed

lemma no_undefined_atom_le_max_lit_of_false_clause:
  assumes
    Γ_lower_set: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
    D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    D_false: "trail_false_cls Γ D" and
    D_max_lit: "linorder_lit.is_maximal_in_mset D L"
  shows "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≼⇩t atm_of L ∧ A |∉| trail_atms Γ)"
proof -
  have "trail_false_lit Γ L"
    using D_false D_max_lit
    unfolding trail_false_cls_def linorder_lit.is_maximal_in_mset_iff by simp

  hence "trail_defined_lit Γ L"
    unfolding trail_false_lit_def trail_defined_lit_def by argo

  hence "atm_of L |∈| trail_atms Γ"
    unfolding trail_defined_lit_iff_trail_defined_atm .

  thus ?thesis
    using Γ_lower_set
    using linorder_trm.not_in_lower_setI by blast
qed

lemma trail_defined_if_no_undef_atom_le_max_lit:
  assumes
    C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    C_max_lit: "linorder_lit.is_maximal_in_mset C K" and
    no_undef_atom_le_K:
      "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≼⇩t atm_of K ∧ A |∉| trail_atms Γ)"
  shows "trail_defined_cls Γ C"
proof -

  have "⋀x. x ∈# C ⟹ atm_of x ≼⇩t atm_of K"
    using C_in C_max_lit
    unfolding linorder_lit.is_maximal_in_mset_iff
    by (metis linorder_trm.le_cases linorder_trm.le_less_linear literal.exhaust_sel
        ord_res.less_lit_simps(1) ord_res.less_lit_simps(2) ord_res.less_lit_simps(3)
        ord_res.less_lit_simps(4))

  hence "⋀x. x ∈# C ⟹ trail_defined_lit Γ x"
    using C_in no_undef_atom_le_K
    by (meson atm_of_in_atms_of_clssI trail_defined_lit_iff_trail_defined_atm)

  thus "trail_defined_cls Γ C"
    unfolding trail_defined_cls_def
    by metis
qed

lemma no_undef_atom_le_max_lit_if_lt_false_clause:
  assumes
    Γ_lower_set: "linorder_trm.is_lower_fset (trail_atms Γ) (atms_of_clss (N |∪| U⇩e⇩r))" and
    D_in: "D |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    D_false: "trail_false_cls Γ D" and
    D_max_lit: "linorder_lit.is_maximal_in_mset D L" and
    C_in: "C |∈| iefac ℱ |`| (N |∪| U⇩e⇩r)" and
    C_max_lit: "linorder_lit.is_maximal_in_mset C K" and
    C_lt: "C ≺⇩c D"
  shows "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≼⇩t atm_of K ∧ A |∉| trail_atms Γ)"
proof -
  have "K ≼⇩l L"
    using C_lt C_max_lit D_max_lit
    using linorder_cls.less_imp_not_less linorder_lit.multp_if_maximal_less_that_maximal
      linorder_lit.nle_le by blast

  hence "atm_of K ≼⇩t atm_of L"
    by (cases K; cases L) simp_all

  thus "¬ (∃A|∈|atms_of_clss (N |∪| U⇩e⇩r). A ≼⇩t atm_of K ∧ A |∉| trail_atms Γ)"
    using no_undefined_atom_le_max_lit_of_false_clause[OF assms(1,2,3,4)]
    by fastforce
qed

lemma bex_trail_false_cls_simp:
  fixes ℱ N Γ
  shows "fBex (iefac ℱ |`| N) (trail_false_cls Γ) ⟷ fBex N (trail_false_cls Γ)"
proof (rule iffI ; elim bexE)
  fix C :: "'f gclause"
  assume C_in: "C |∈| iefac ℱ |`| N" and C_false: "trail_false_cls Γ C"
  thus "fBex N (trail_false_cls Γ)"
    by (smt (verit, ccfv_SIG) fimage_iff iefac_def set_mset_efac trail_false_cls_def)
next
  fix C :: "'f gclause"
  assume "C |∈| N" and "trail_false_cls Γ C"
  thus "fBex (iefac ℱ |`| N) (trail_false_cls Γ)"
    by (metis fimageI iefac_def set_mset_efac trail_false_cls_def)
qed

end

end