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_syntaxfBall syntax_const‹_fBall›,
  Syntax_Trans.preserve_binder_abs2_tr' const_syntaxfBex 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 LN σN where "LN  (set_mset ` fset N)" and "LN ⋅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 LN ⋅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