Theory Initial_Literals_Generalize_Learned_Literals

theory Initial_Literals_Generalize_Learned_Literals
  imports SCL_FOL
begin

syntax (input)
  "_fBall"       :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3! (_/|:|_)./ _)" [0, 0, 10] 10)
  "_fBex"        :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3? (_/|:|_)./ _)" [0, 0, 10] 10)

syntax
  "_fBall"       :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3∀(_/|∈|_)./ _)" [0, 0, 10] 10)
  "_fBex"        :: "pttrn ⇒ 'a fset ⇒ bool ⇒ bool"      ("(3∃(_/|∈|_)./ _)" [0, 0, 10] 10)

translations
  "∀x|∈|A. P" ⇌ "CONST fBall A (λx. P)"
  "∃x|∈|A. P" ⇌ "CONST fBex A (λx. P)"

print_translation ‹
 [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>‹fBall› \<^syntax_const>‹_fBall›,
  Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>‹fBex› \<^syntax_const>‹_fBex›]
› ― ‹to avoid eta-contraction of body›

global_interpretation comp_finsert_commute: comp_fun_commute finsert
proof (unfold_locales)
  show "⋀y x. finsert y ∘ finsert x = finsert x ∘ finsert y"
    by auto
qed

definition fset_mset :: "'a multiset ⇒ 'a fset"
  where "fset_mset = fold_mset finsert {||}"

lemma fset_mset_mempty[simp]: "fset_mset {#} = {||}"
  by (simp add: fset_mset_def)

lemma fset_mset_add_mset[simp]: "fset_mset (add_mset x M) = finsert x (fset_mset M)"
  by (simp add: fset_mset_def)

lemma fset_fset_mset[simp]: "fset (fset_mset M) = set_mset M"
  by (induction M rule: multiset_induct) simp_all

lemma fmember_fset_mset_iff[simp]: "x |∈| fset_mset M ⟷ x ∈# M"
  by (induction M rule: multiset_induct) simp_all

lemma fBall_fset_mset_iff[simp]: "(∀x |∈| fset_mset M. P x) ⟷ (∀x ∈# M. P x)"
  by simp

lemma fBex_fset_mset_iff[simp]: "(∃x |∈| fset_mset M. P x) ⟷ (∃x ∈# M. P x)"
  by simp

lemma fmember_ffUnion_iff: "a |∈| ffUnion (f |`| A) ⟷ (∃x |∈| A. a |∈| f x)"
  unfolding ffUnion.rep_eq by simp

lemma fBex_ffUnion_iff: "(∃z |∈| ffUnion (f |`| A). P z) ⟷ (∃x |∈| A. ∃z |∈| f x. P z)"
  unfolding ffUnion.rep_eq fimage.rep_eq by blast

lemma fBall_ffUnion_iff: "(∀z |∈| ffUnion (f |`| A). P z) ⟷ (∀x |∈| A. ∀z |∈| f x. P z)"
  unfolding ffUnion.rep_eq fimage.rep_eq by blast


abbreviation grounding_lits_of_clss where
  "grounding_lits_of_clss N ≡ {L ⋅l γ | L γ. L ∈ ⋃(set_mset ` N) ∧ is_ground_lit (L ⋅l γ)}"

context scl_fol_calculus begin

corollary grounding_lits_of_learned_subset_grounding_lits_of_initial:
  assumes "initial_lits_generalize_learned_trail_conflict N S"
  shows "grounding_lits_of_clss (fset (state_learned S)) ⊆ grounding_lits_of_clss (fset N)"
  (is "?lhs ⊆ ?rhs")
proof (rule subsetI)
  from assms(1) have N_lits_sup: "clss_lits_generalize_clss_lits (fset N) (fset (state_learned S))"
    unfolding initial_lits_generalize_learned_trail_conflict_def
    using clss_lits_generalize_clss_lits_subset by auto

  fix L
  assume "L ∈ ?lhs"
  then obtain L' γ where
    L_def: "L = L' ⋅l γ" and
    "L' ∈ ⋃ (set_mset ` fset (state_learned S))" and
    "is_ground_lit (L' ⋅l γ)"
    by auto
  then obtain L⇩N σ⇩N where "L⇩N ∈ ⋃(set_mset ` fset N)" and "L⇩N ⋅l σ⇩N = L'"
    using N_lits_sup[unfolded clss_lits_generalize_clss_lits_def]
    unfolding fBex_ffUnion_iff fBall_ffUnion_iff fBex_fset_mset_iff fBall_fset_mset_iff
      generalizes_lit_def by meson
  then show "L ∈ ?rhs"
    unfolding mem_Collect_eq
    using ‹is_ground_lit (L' ⋅l γ)›
    unfolding L_def ‹L⇩N ⋅l σ⇩N = L'›[symmetric]
    by (metis subst_lit_comp_subst)
qed

lemma grounding_lits_of_clss_conv:
  "grounding_lits_of_clss N = {L | L C. add_mset L C ∈ grounding_of_clss N}"
  (is "?lhs = ?rhs")
proof (intro Set.equalityI Set.subsetI)
  fix L
  assume "L ∈ ?lhs"
  then obtain L' γ where "L = L' ⋅l γ" and "L' ∈ ⋃ (set_mset ` N)" and "is_ground_lit (L' ⋅l γ)"
    by auto

  from ‹L' ∈ ⋃ (set_mset ` N)› obtain C where "C ∈ N" and "L' ∈# C"
    by blast

  obtain γ⇩C where "is_ground_cls (C ⋅ γ ⋅ γ⇩C)"
    using ex_ground_subst ground_subst_ground_cls by blast
  hence "L ∈# C ⋅ γ ⋅ γ⇩C"
    using ‹L' ∈# C› ‹L = L' ⋅l γ›
    by (metis Melem_subst_cls ‹is_ground_lit (L' ⋅l γ)› is_ground_subst_lit)
  then obtain C' where "C ⋅ γ ⋅ γ⇩C = add_mset L C'"
    using multi_member_split by metis

  moreover have "C ⋅ γ ⋅ γ⇩C ∈ grounding_of_clss N"
    unfolding grounding_of_clss_def
  proof (rule UN_I)
    show "C ∈ N"
      using ‹C ∈ N› .
  next
    show "C ⋅ γ ⋅ γ⇩C ∈ grounding_of_cls C"
      using ‹is_ground_cls (C ⋅ γ ⋅ γ⇩C)›
      by (metis grounding_of_cls_ground grounding_of_subst_cls_subset insert_absorb insert_subset)
  qed

  ultimately show "L ∈ ?rhs"
    by auto
next
  fix L
  assume "L ∈ ?rhs"
  then obtain C where "add_mset L C ∈ grounding_of_clss N"
    by auto
  then obtain CC γ where "CC ∈ N" and "CC ⋅ γ = add_mset L C"
    unfolding grounding_of_clss_def
    by (smt (verit, best) UN_iff grounding_of_cls_def mem_Collect_eq)
  then obtain L' C' where "CC = add_mset L' C'" and "L = L' ⋅l γ" and "C = C' ⋅ γ"
    by (metis (no_types, lifting) msed_map_invR subst_cls_def)

  show "L ∈ ?lhs"
  proof (intro CollectI exI conjI)
    show "L = L' ⋅l γ"
      using ‹L = L' ⋅l γ› by simp
  next
    show "L' ∈ ⋃ (set_mset ` N)"
      using ‹CC ∈ N› ‹CC = add_mset L' C'›
      by (metis Union_iff image_eqI union_single_eq_member)
  next
    show "is_ground_lit (L' ⋅l γ)"
      using ‹add_mset L C ∈ grounding_of_clss N› ‹L = L' ⋅l γ›
      by (metis grounding_ground is_ground_cls_add_mset)
  qed
qed

corollary groundings_of_learned_subset_groundings_of_initial:
  assumes "initial_lits_generalize_learned_trail_conflict N S"
  defines "U ≡ state_learned S"
  shows "{L | L C. add_mset L C ∈ grounding_of_clss (fset U)} ⊆
    {L | L C. add_mset L C ∈ grounding_of_clss (fset N)}"
  using assms grounding_lits_of_learned_subset_grounding_lits_of_initial
  unfolding grounding_lits_of_clss_conv
  by simp

end

end