# 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 {#} = {||}"

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"
using ‹C ∈ N› ‹is_ground_cls (C ⋅ γ ⋅ γ⇩C)›
unfolding grounding_of_clss_def
by (metis (no_types, opaque_lifting) UN_iff grounding_of_cls_ground
grounding_of_subst_cls_subset insert_subset subsetD)

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 γ›
qed
qed

corollary
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```