Theory Exhaustive_Factorization

theory Exhaustive_Factorization
  imports Background
begin

section ‹Function for full factorization›

context simulation_SCLFOL_ground_ordered_resolution begin

definition efac :: "'f gterm clause ⇒ 'f gterm clause" where
  "efac C = (THE C'. ord_res.ground_factoring⇧^*⇧^* C C' ∧ (∄C''. ord_res.ground_factoring C' C''))"

text ‹The function \<^const>‹efac› performs exhaustive factorization of its input clause.›

lemma ex1_efac_eq_factoring_chain:
  "∃!C'. efac C = C' ∧ ord_res.ground_factoring⇧^*⇧^* C C' ∧ (∄C''. ord_res.ground_factoring C' C'')"
proof -
  have "right_unique (λx y. ord_res.ground_factoring⇧^*⇧^* x y ∧ (∄z. ord_res.ground_factoring y z))"
    using ord_res.unique_ground_factoring right_unique_terminating_rtranclp right_unique_iff
    by blast

  moreover obtain C' where "ord_res.ground_factoring⇧^*⇧^* C C' ∧ (∄C''. ord_res.ground_factoring C' C'')"
    using ex_terminating_rtranclp[OF ord_res.termination_ground_factoring]
    by metis

  ultimately have "efac C = C'"
    by (simp add: efac_def right_unique_def the_equality)

  then show ?thesis
    using ‹ord_res.ground_factoring⇧^*⇧^* C C' ∧ (∄C''. ord_res.ground_factoring C' C'')› by blast
qed

lemma efac_eq_disj:
  "efac C = C ∨ (∃!C'. efac C = C' ∧ ord_res.ground_factoring⇧^*⇧^* C C' ∧ (∄C''. ord_res.ground_factoring C' C''))"
  using ex1_efac_eq_factoring_chain
  by (metis is_pos_def)

lemma member_mset_if_count_eq_Suc: "count X x = Suc n ⟹ x ∈# X"
  by (simp add: count_inI)

lemmas member_fsetE = mset_add

lemma ord_res_ground_factoring_iff: "ord_res.ground_factoring C C' ⟷
  (∃A. ord_res.is_maximal_lit (Pos A) C ∧ (∃n. count C (Pos A) = Suc (Suc n) ∧ C' = C - {#Pos A#}))"
proof (rule iffI)
  assume "ord_res.ground_factoring C C'"
  thus "∃A. ord_res.is_maximal_lit (Pos A) C ∧ (∃n. count C (Pos A) = Suc (Suc n) ∧ C' = C - {#Pos A#})"
  proof (cases C C' rule: ord_res.ground_factoring.cases)
    case (ground_factoringI A P')
    show ?thesis
    proof (intro exI conjI)
      show "ord_res.is_maximal_lit (Pos A) C"
        using ‹ord_res.is_maximal_lit (Pos A) C› .
    next
      show "count C (Pos A) = Suc (Suc (count P' (Pos A)))"
        unfolding ‹C = add_mset (Pos A) (add_mset (Pos A) P')› by simp
    next
      show "C' = remove1_mset (Pos A) C"
        unfolding ‹C = add_mset (Pos A) (add_mset (Pos A) P')› ‹C' = add_mset (Pos A) P'› by simp
    qed
  qed
next
  assume "∃A. ord_res.is_maximal_lit (Pos A) C ∧
    (∃n. count C (Pos A) = Suc (Suc n) ∧ C' = C - {#Pos A#})"
  then obtain A n where
    "ord_res.is_maximal_lit (Pos A) C" and
    "count C (Pos A) = Suc (Suc n)" and
    "C' = C - {#Pos A#}"
    by metis

  have "Pos A ∈# C"
    using ‹count C (Pos A) = Suc (Suc n)› member_mset_if_count_eq_Suc by metis
  then obtain C'' where "C = add_mset (Pos A) C''"
    by (auto elim: member_fsetE)
  with ‹count C (Pos A) = Suc (Suc n)› have "count C'' (Pos A) = Suc n"
    by simp
  hence "Pos A ∈# C''"
    using member_mset_if_count_eq_Suc by metis
  then obtain C''' where "C'' = add_mset (Pos A) C'''"
    by (auto elim: member_fsetE)

  show "ord_res.ground_factoring C C'"
  proof (rule ord_res.ground_factoringI)
    show "C = add_mset (Pos A) (add_mset (Pos A) C''')"
      using ‹C = add_mset (Pos A) C''› ‹C'' = add_mset (Pos A) C'''› by metis
  next
    show "ord_res.is_maximal_lit (Pos A) C"
      using ‹ord_res.is_maximal_lit (Pos A) C› .
  next
    show "C' = add_mset (Pos A) C'''"
      using ‹C' = C - {#Pos A#}› ‹C = add_mset (Pos A) C''› ‹C'' = add_mset (Pos A) C'''› by simp
  qed simp_all
qed

lemma tranclp_ord_res_ground_factoring_iff:
  "ord_res.ground_factoring⇧⁺⇧⁺ C C' ∧ (∄C''. ord_res.ground_factoring C' C'') ⟷
  (∃A. ord_res.is_maximal_lit (Pos A) C ∧ (∃n. count C (Pos A) = Suc (Suc n) ∧
    C' = C - replicate_mset (Suc n) (Pos A)))"
proof (intro iffI; elim exE conjE)
  assume "ord_res.ground_factoring⇧⁺⇧⁺ C C'" and "(∄C''. ord_res.ground_factoring C' C'')"
  then show "∃A. ord_res.is_maximal_lit (Pos A) C ∧ (∃n. count C (Pos A) = Suc (Suc n) ∧
    C' = C - replicate_mset (Suc n) (Pos A))"
  proof (induction C rule: converse_tranclp_induct)
    case (base C)
    from base.hyps obtain A n where
      "ord_res.is_maximal_lit (Pos A) C" and
      "count C (Pos A) = Suc (Suc n)" and
      "C' = remove1_mset (Pos A) C"
      unfolding ord_res_ground_factoring_iff by auto

    moreover have "n = 0"
    proof (rule ccontr)
      assume "n ≠ 0"
      then obtain C'' where "C' = add_mset (Pos A) (add_mset (Pos A) C'')"
        by (metis (no_types, lifting) Zero_not_Suc calculation(2,3) count_add_mset count_inI
            diff_Suc_1 insert_DiffM)
      hence "ord_res.ground_factoring C' (add_mset (Pos A) C'')"
        using ord_res.ground_factoringI
        by (metis calculation(1,3) linorder_lit.is_maximal_in_mset_iff more_than_one_mset_mset_diff
            union_single_eq_member)
      with base.prems show False
        by metis
    qed

    ultimately show ?case
      by (metis replicate_mset_0 replicate_mset_Suc)
  next
    case (step C C'')
    from step.IH step.prems obtain A n where
      "ord_res.is_maximal_lit (Pos A) C''" and
      "count C'' (Pos A) = Suc (Suc n)" and
      "C' = C'' - replicate_mset (Suc n) (Pos A)"
      by metis

    from step.hyps(1) obtain A' m where
      "ord_res.is_maximal_lit (Pos A') C" and
      "count C (Pos A') = Suc (Suc m)" and
      "C'' = remove1_mset (Pos A') C"
      unfolding ord_res_ground_factoring_iff by metis

    have "A' = A"
      using ‹ord_res.is_maximal_lit (Pos A) C''› ‹ord_res.is_maximal_lit (Pos A') C›
      by (metis ‹C'' = remove1_mset (Pos A') C› ‹count C (Pos A') = Suc (Suc m)›
          add_mset_remove_trivial_eq count_add_mset count_greater_zero_iff diff_Suc_1
          linorder_lit.antisym_conv3 linorder_lit.is_maximal_in_mset_iff literal.inject(1)
          zero_less_Suc)

    have "m = Suc n"
      using ‹count C'' (Pos A) = Suc (Suc n)› ‹count C (Pos A') = Suc (Suc m)›
      unfolding ‹C'' = remove1_mset (Pos A') C› ‹A' = A›
      by simp

    show ?case
    proof (intro exI conjI)
      show "ord_res.is_maximal_lit (Pos A) C"
        using ‹ord_res.is_maximal_lit (Pos A') C› ‹A' = A› by metis
    next
      show "count C (Pos A) = Suc (Suc m)"
        using ‹count C (Pos A') = Suc (Suc m)› ‹A' = A› by metis
    next
      show "C' = C - replicate_mset (Suc m) (Pos A)"
        unfolding ‹C' = C'' - replicate_mset (Suc n) (Pos A)› ‹C'' = remove1_mset (Pos A') C›
          ‹A' = A› ‹m = Suc n›
        by simp
    qed
  qed
next
  fix A n assume "ord_res.is_maximal_lit (Pos A) C"
  thus "count C (Pos A) = Suc (Suc n) ⟹ C' = C - replicate_mset (Suc n) (Pos A) ⟹
    ord_res.ground_factoring⇧⁺⇧⁺ C C' ∧ (∄C''. ord_res.ground_factoring C' C'')"
  proof (induction n arbitrary: C)
    case 0
    hence "(ord_res.is_maximal_lit (Pos A) C ∧
         (count C (Pos A) = Suc (Suc 0) ∧
              C' = remove1_mset (Pos A) C))"
      by (metis replicate_mset_0 replicate_mset_Suc)
    hence "ord_res.ground_factoring C C' ∧ (∄a. ord_res.ground_factoring C' a)"
      unfolding ord_res_ground_factoring_iff
      by (metis Zero_not_Suc add_mset_remove_trivial_eq count_add_mset count_inI
          linorder_lit.antisym_conv3 linorder_lit.is_maximal_in_mset_iff nat.inject)
    thus ?case
      by blast
  next
    case (Suc n)
    have "ord_res.ground_factoring⇧⁺⇧⁺ (C - {#Pos A#}) C' ∧ (∄a. ord_res.ground_factoring C' a)"
    proof (rule Suc.IH)
      show "count (remove1_mset (Pos A) C) (Pos A) = Suc (Suc n)"
        using Suc.prems by simp
    next
      show "C' = remove1_mset (Pos A) C - replicate_mset (Suc n) (Pos A)"
        using Suc.prems by simp
    next
      show "ord_res.is_maximal_lit (Pos A) (remove1_mset (Pos A) C)"
        using Suc.prems
        by (smt (verit, ccfv_SIG) Zero_not_Suc add_diff_cancel_left' add_mset_remove_trivial_eq
            count_add_mset count_inI linorder_lit.is_maximal_in_mset_iff plus_1_eq_Suc)
    qed

    moreover have "ord_res.ground_factoring C (C - {#Pos A#})"
      unfolding ord_res_ground_factoring_iff
    proof (intro exI conjI)
      show "ord_res.is_maximal_lit (Pos A) C"
        using Suc.prems by metis
    next
      show "count C (Pos A) = Suc (Suc (Suc n))"
        using Suc.prems by metis
    next
      show "remove1_mset (Pos A) C = remove1_mset (Pos A) C" ..
    qed

    ultimately show ?case
      by auto
  qed
qed

lemma minus_mset_replicate_mset_eq_add_mset_filter_mset:
  assumes "count X x = Suc n"
  shows "X - replicate_mset n x = add_mset x {#y ∈# X. y ≠ x#}"
  using assms
  by (metis add_diff_cancel_left' add_mset_diff_bothsides filter_mset_eq filter_mset_neq
      multiset_partition replicate_mset_Suc union_mset_add_mset_right)

lemma minus_mset_replicate_mset_eq_add_mset_add_mset_filter_mset:
  assumes "count X x = Suc (Suc n)"
  shows "X - replicate_mset n x = add_mset x (add_mset x {#y ∈# X. y ≠ x#})"
  using assms
  by (metis add_diff_cancel_left' add_mset_diff_bothsides filter_mset_eq filter_mset_neq
      multiset_partition replicate_mset_Suc union_mset_add_mset_right)

lemma rtrancl_ground_factoring_iff:
  shows "ord_res.ground_factoring⇧^*⇧^* C C' ∧ (∄C''. ord_res.ground_factoring C' C'') ⟷
  ((∄A. ord_res.is_maximal_lit (Pos A) C ∧ count C (Pos A) ≥ 2) ∧ C = C' ∨
   (∃A. ord_res.is_maximal_lit (Pos A) C ∧ C' = add_mset (Pos A) {#L ∈# C. L ≠ Pos A#}))"
proof (intro iffI; elim exE conjE disjE)
  show "ord_res.ground_factoring⇧^*⇧^* C C' ⟹ ∄C''. ord_res.ground_factoring C' C'' ⟹
    (∄A. ord_res.is_maximal_lit (Pos A) C ∧ 2 ≤ count C (Pos A)) ∧ C = C' ∨
    (∃A. ord_res.is_maximal_lit (Pos A) C ∧ C' = add_mset (Pos A) {#L ∈# C. L ≠ Pos A#})"
  proof (induction C rule: converse_rtranclp_induct)
    case base
    thus ?case
      by (metis add_2_eq_Suc le_Suc_ex ord_res_ground_factoring_iff)
  next
    case (step y z)
    hence "ord_res.ground_factoring⇧⁺⇧⁺ y C' ∧ (∄x. ord_res.ground_factoring C' x)"
      by simp
    thus ?case
      unfolding tranclp_ord_res_ground_factoring_iff
      by (metis minus_mset_replicate_mset_eq_add_mset_filter_mset)
  qed
next
  assume "∄A. ord_res.is_maximal_lit (Pos A) C ∧ 2 ≤ count C (Pos A)" and "C = C'"
  thus "ord_res.ground_factoring⇧^*⇧^* C C' ∧ (∄C''. ord_res.ground_factoring C' C'')"
    by (metis One_nat_def Suc_1 Suc_le_eq Suc_le_mono ord_res_ground_factoring_iff
        rtranclp.rtrancl_refl zero_less_Suc)
next
  fix A assume "ord_res.is_maximal_lit (Pos A) C"
  then obtain n where "count C (Pos A) = Suc n"
    by (meson in_countE linorder_lit.is_maximal_in_mset_iff)
  with ‹ord_res.is_maximal_lit (Pos A) C› show "C' = add_mset (Pos A) {#L ∈# C. L ≠ Pos A#} ⟹
    ord_res.ground_factoring⇧^*⇧^* C C' ∧ (∄C''. ord_res.ground_factoring C' C'')"
  proof (induction n arbitrary: C)
    case 0

    have "(∄a. ord_res.ground_factoring C a)"
    proof (intro notI, elim exE)
      fix D assume "ord_res.ground_factoring C D"
      thus False
      proof (cases rule: ord_res.ground_factoring.cases)
        case (ground_factoringI A' P')
        hence "A' = A"
          using ‹ord_res.is_maximal_lit (Pos A) C›
          using linorder_lit.Uniq_is_maximal_in_mset
          by (metis Uniq_D literal.inject(1))
        thus False
          using ‹count C (Pos A) = Suc 0› ‹C = add_mset (Pos A') (add_mset (Pos A') P')› by simp
      qed
    qed
    thus ?case
      by (metis "0.prems"(1) "0.prems"(3) diff_zero
          minus_mset_replicate_mset_eq_add_mset_filter_mset replicate_mset_0 rtranclp.rtrancl_refl)
  next
    case (Suc x)
    then show ?case
      by (metis minus_mset_replicate_mset_eq_add_mset_filter_mset tranclp_into_rtranclp
          tranclp_ord_res_ground_factoring_iff)
  qed
qed

lemma efac_spec: "efac C = C ∨
  (∃A. ord_res.is_maximal_lit (Pos A) C ∧ efac C = add_mset (Pos A) {#L ∈# C. L ≠ Pos A#})"
  using efac_eq_disj[of C]
proof (elim disjE)
  assume "efac C = C"
  thus "efac C = C ∨
    (∃A. ord_res.is_maximal_lit (Pos A) C ∧ efac C = add_mset (Pos A) {#L ∈# C. L ≠ Pos A#})"
    by metis
next
  assume "∃!C'. efac C = C' ∧ ord_res.ground_factoring⇧^*⇧^* C C' ∧
    (∄C''. ord_res.ground_factoring C' C'')"
  then obtain C' where
    "efac C = C'" and
    "ord_res.ground_factoring⇧^*⇧^* C C' ∧ (∄C''. ord_res.ground_factoring C' C'')"
    by metis
  thus "efac C = C ∨
    (∃A. ord_res.is_maximal_lit (Pos A) C ∧ efac C = add_mset (Pos A) {#L ∈# C. L ≠ Pos A#})"
    unfolding rtrancl_ground_factoring_iff
    by metis
qed

lemma efac_spec_if_pos_lit_is_maximal:
  assumes L_pos: "is_pos L" and L_max: "ord_res.is_maximal_lit L C"
  shows "efac C = add_mset L {#K ∈# C. K ≠ L#}"
proof -
  from assms obtain C' where
    "efac C = C'" and
    "ord_res.ground_factoring⇧^*⇧^* C C' ∧ (∄C''. ord_res.ground_factoring C' C'')"
    using ex1_efac_eq_factoring_chain by metis
  thus ?thesis
    unfolding rtrancl_ground_factoring_iff
  proof (elim disjE conjE)
    assume hyps: "∄A. ord_res.is_maximal_lit (Pos A) C ∧ 2 ≤ count C (Pos A)" "C = C'"
    with assms have "count C L = 1"
      by (metis One_nat_def in_countE is_pos_def le_less_linear less_2_cases_iff
          linorder_lit.is_maximal_in_mset_iff nat_less_le zero_less_Suc)
    hence "C = add_mset L {#K ∈# C. K ≠ L#}"
      by (metis One_nat_def diff_zero minus_mset_replicate_mset_eq_add_mset_filter_mset
          replicate_mset_0)
    thus "efac C = add_mset L {#K ∈# C. K ≠ L#}"
      using ‹efac C = C'› ‹C = C'› by argo
  next
    assume "∃A. ord_res.is_maximal_lit (Pos A) C ∧ C' = add_mset (Pos A) {#L ∈# C. L ≠ Pos A#}"
    thus "efac C = add_mset L {#K ∈# C. K ≠ L#}"
      by (metis L_max Uniq_D ‹efac C = C'› linorder_lit.Uniq_is_maximal_in_mset)
  qed
qed

lemma efac_mempty[simp]: "efac {#} = {#}"
  by (metis empty_iff linorder_lit.is_maximal_in_mset_iff set_mset_empty efac_spec)

lemma set_mset_efac[simp]: "set_mset (efac C) = set_mset C"
  using efac_spec[of C]
proof (elim disjE exE conjE)
  show "efac C = C ⟹ set_mset (efac C) = set_mset C"
    by simp
next
  fix A
  assume "ord_res.is_maximal_lit (Pos A) C"
  hence "Pos A ∈# C"
    by (simp add: linorder_lit.is_maximal_in_mset_iff)

  assume efac_C_eq: "efac C = add_mset (Pos A) {#L ∈# C. L ≠ Pos A#}"
  show "set_mset (efac C) = set_mset C"
  proof (intro Set.subset_antisym Set.subsetI)
    fix L assume "L ∈# efac C"
    then show "L ∈# C"
      unfolding efac_C_eq
      using ‹Pos A ∈# C› by auto
  next
    fix L assume "L ∈# C"
    then show "L ∈# efac C"
      unfolding efac_C_eq
      by simp
  qed
qed

lemma efac_subset: "efac C ⊆# C"
  using efac_spec[of C]
proof (elim disjE exE conjE)
  show "efac C = C ⟹ efac C ⊆# C"
    by simp
next
  fix A
  assume "ord_res.is_maximal_lit (Pos A) C" and
    efac_C_eq: "efac C = add_mset (Pos A) {#L ∈# C. L ≠ Pos A#}"
  then show "efac C ⊆# C"
    by (smt (verit, ccfv_SIG) filter_mset_add_mset insert_DiffM insert_subset_eq_iff
        linorder_lit.is_maximal_in_mset_iff multiset_filter_subset)
qed

lemma true_cls_efac_iff[simp]:
  fixes ℐ :: "'f gterm set" and C :: "'f gclause"
  shows "ℐ ⊫ efac C ⟷ ℐ ⊫ C"
  by (metis set_mset_efac true_cls_iff_set_mset_eq)

lemma obtains_positive_greatest_lit_if_efac_not_ident:
  assumes "efac C ≠ C"
  obtains L where "is_pos L" and "linorder_lit.is_greatest_in_mset (efac C) L"
proof -
  from ‹efac C ≠ C› obtain A where
    Pos_A_maximal: "linorder_lit.is_maximal_in_mset C (Pos A)" and
    efac_C_eq: "efac C = add_mset (Pos A) {#L ∈# C. L ≠ Pos A#}"
    using efac_spec by metis

  assume hyp: "⋀L. is_pos L ⟹ linorder_lit.is_greatest_in_mset (efac C) L ⟹ thesis"
  show thesis
  proof (rule hyp)
    show "is_pos (Pos A)"
      by simp
  next
    show "linorder_lit.is_greatest_in_mset(efac C) (Pos A)"
      unfolding efac_C_eq linorder_lit.is_greatest_in_mset_iff
      using Pos_A_maximal[unfolded linorder_lit.is_maximal_in_mset_iff]
      by auto
  qed
qed

lemma mempty_in_image_efac_iff[simp]: "{#} ∈ efac ` N ⟷ {#} ∈ N"
  by (metis empty_iff imageE image_eqI linorder_lit.is_maximal_in_mset_iff set_mset_empty set_mset_efac efac_spec)

lemma greatest_literal_in_efacI:
  assumes "is_pos L" and C_max_lit: "linorder_lit.is_maximal_in_mset C L"
  shows "linorder_lit.is_greatest_in_mset (efac C) L"
  unfolding efac_spec_if_pos_lit_is_maximal[OF assms] linorder_lit.is_greatest_in_mset_iff
proof (intro conjI ballI)
  show "L ∈# add_mset L {#K ∈# C. K ≠ L#}"
    by simp
next
  fix y :: "'f gterm literal"
  assume "y ∈# remove1_mset L (add_mset L {#K ∈# C. K ≠ L#})"
  then show "y ≺⇩_l L"
    using C_max_lit[unfolded linorder_lit.is_maximal_in_mset_iff]
    by  auto
qed

lemma "linorder_lit.is_maximal_in_mset (efac C) L ⟷ linorder_lit.is_maximal_in_mset C L"
  by (simp add: linorder_lit.is_maximal_in_mset_iff)

lemma
  assumes "is_pos L"
  shows "linorder_lit.is_greatest_in_mset (efac C) L ⟷ linorder_lit.is_maximal_in_mset C L"
  by (metis (no_types, opaque_lifting) Uniq_D assms efac_spec greatest_literal_in_efacI
      linorder_lit.Uniq_is_greatest_in_mset linorder_lit.is_maximal_in_mset_if_is_greatest_in_mset
      literal.disc(1))

lemma factorizable_if_neq_efac:
  assumes "C ≠ efac C"
  shows "∃C'. ord_res.ground_factoring C C'"
  using assms
  by (metis converse_rtranclpE ex1_efac_eq_factoring_chain)

lemma nex_strictly_maximal_pos_lit_if_neq_efac:
  assumes "C ≠ efac C"
  shows "∄L. is_pos L ∧ ord_res.is_strictly_maximal_lit L C"
  using assms factorizable_if_neq_efac nex_strictly_maximal_pos_lit_if_factorizable by metis

lemma efac_properties_if_not_ident:
  assumes "efac C ≠ C"
  shows "efac C ≺⇩_c C" and "{efac C} ⊫e {C}"
proof -
  have "efac C ⊆# C"
    using efac_subset .
  hence "efac C ≼⇩_c C"
    using subset_implies_reflclp_multp by blast
  thus "efac C ≺⇩_c C"
    using ‹efac C ≠ C› by order

  show "{efac C} ⊫e {C}"
    using ‹efac C ⊆# C› true_clss_subclause by metis
qed

end

end