Theory Clause_Could_Propagate

theory Clause_Could_Propagate
  imports
    Background
    Implicit_Exhaustive_Factorization
begin

context simulation_SCLFOL_ground_ordered_resolution begin

definition clause_could_propagate where
  "clause_could_propagate Γ C L ⟷ ¬ trail_defined_lit Γ L ∧
    linorder_lit.is_maximal_in_mset C L ∧ trail_false_cls Γ {#K ∈# C. K ≠ L#}"

lemma trail_false_if_could_have_propagatated:
  "clause_could_propagate Γ C L ⟹ trail_false_cls ((- L, n) # Γ) C"
  unfolding clause_could_propagate_def trail_false_cls_def trail_false_lit_def by auto

lemma atoms_of_trail_lt_atom_of_propagatable_literal:
  assumes
    Γ_lower: "linorder_trm.is_lower_set (fset (trail_atms Γ)) 𝒜" and
    C_prop: "clause_could_propagate Γ C L" and
    "atm_of L ∈ 𝒜"
  shows "∀A |∈| trail_atms Γ. A ≺⇩t atm_of L"
proof -
  have "atm_of L |∉| trail_atms Γ"
    using C_prop
    unfolding clause_could_propagate_def trail_defined_lit_iff_trail_defined_atm
    by argo

  then show ?thesis
    using Γ_lower ‹atm_of L ∈ 𝒜›
    by (metis linorder_trm.is_lower_set_iff linorder_trm.neqE)
qed

lemma trail_false_cls_filter_mset_iff:
  "trail_false_cls Γ {#Ka ∈# C. Ka ≠ K#} ⟷ (∀L∈#C. L ≠ K ⟶ trail_false_lit Γ L)"
  unfolding trail_false_cls_def by auto

lemma clause_could_propagate_iff: "clause_could_propagate Γ C K ⟷
  ¬ trail_defined_lit Γ K ∧ ord_res.is_maximal_lit K C ∧ (∀L∈#C. L ≠ K ⟶ trail_false_lit Γ L)"
  unfolding clause_could_propagate_def trail_false_cls_filter_mset_iff ..

lemma clause_could_propagate_efac: "clause_could_propagate Γ (efac C) = clause_could_propagate Γ C"
proof (rule ext)
  fix L
  show "clause_could_propagate Γ (efac C) L ⟷ clause_could_propagate Γ C L"
    unfolding clause_could_propagate_def
    by (metis (mono_tags, lifting) ex1_efac_eq_factoring_chain mem_Collect_eq
        ord_res.ground_factorings_preserves_maximal_literal set_mset_efac set_mset_filter
        trail_false_cls_def)
qed

lemma bex_clause_could_propagate_simp:
  fixes ℱ N Γ L
  shows "fBex (iefac ℱ |`| N) (λC. clause_could_propagate Γ C L) ⟷
    fBex N (λC. clause_could_propagate Γ C L)"
  sketch (rule iffI; elim bexE)
proof (rule iffI ; elim bexE)
  fix C :: "'f gclause"
  assume "C |∈| iefac ℱ |`| N" and "clause_could_propagate Γ C L"
  thus "∃C |∈| N. clause_could_propagate Γ C L"
    by (metis clause_could_propagate_efac fimageE iefac_def)
next
  fix C :: "'f gclause"
  assume "C |∈| N" and "clause_could_propagate Γ C L"
  thus "∃C|∈|iefac ℱ |`| N. clause_could_propagate Γ C L"
    by (metis clause_could_propagate_efac fimageI iefac_def)
qed

end

end