# Theory SCL_FOL

theory SCL_FOL
imports
Main

Saturation_Framework.Calculus
Saturation_Framework_Extensions.Clausal_Calculus
Ordered_Resolution_Prover.Clausal_Logic
Ordered_Resolution_Prover.Abstract_Substitution
Ordered_Resolution_Prover.Herbrand_Interpretation
First_Order_Terms.Subsumption
First_Order_Terms.Term
First_Order_Terms.Unification
Abstract_Renaming_Apart
Ordered_Resolution_Prover_Extra
begin

section ‹Extra Lemmas›

subsection ‹Set Extra›

lemma not_in_iff: "L  xs  (yxs. L  y)"
by auto

lemma disjoint_iff': "A  B = {}  (a  A. a  B)  (b  B. b  A)"
by blast

lemma set_filter_insert_conv:
"{x  insert y S. P x} = (if P y then insert y else id) {x  S. P x}"
by auto

lemma not_empty_if_mem: "x  X  X  {}"
by blast

subsection ‹Finite Set Extra›

lemma finite_induct' [case_names empty singleton insert_insert, induct set: finite]:
― ‹Discharging x ∉ F› entails extra work.›
assumes "finite F"
assumes "P {}"
and singleton: "x. P {x}"
and insert_insert: "x y F. finite F  x  y  x  F  y  F  P (insert y F)  P (insert x (insert y F))"
shows "P F"
using finite F
proof induct
show "P {}" by fact
next
fix x F
assume F: "finite F" and P: "P F"
thus "P (insert x F)"
proof (induction F rule: finite.induct)
case emptyI
show ?case by (rule singleton)
next
case (insertI F y)
show ?case
proof (cases "x = y")
case True
then show ?thesis
next
case x_neq_y: False
show ?thesis
proof (cases "x  F  y  F")
case True
then show ?thesis
by (metis insertCI insertI.IH insertI.prems insert_absorb)
next
case False
show ?thesis
proof (rule insert_insert)
show "finite F" using insertI by simp
next
show "x  y" by (rule x_neq_y)
next
show "x  F" using False by simp
next
show "y  F" using False by simp
next
show "P (insert y F)"
qed
qed
qed
qed
qed

subsection ‹Product Type Extra›

lemma insert_Times: "insert a A × B = Pair a ` B  A × B"
by blast

lemma Times_insert: "A × insert b B = (λx. (x, b)) ` A  A × B"
by blast

lemma insert_Times_insert':
"insert a A × insert b B = insert (a, b) ((Pair a ` B)  ((λx. (x, b)) ` A)  (A × B))"
(is "?lhs = ?rhs")
unfolding insert_Times_insert by auto

subsection ‹List Extra›

lemma lt_lengthD:
assumes i_lt_xs: "i < length xs"
shows "xs1 xi xs2. xs = xs1 @ xi # xs2  length xs1 = i"
using assms

lemma lt_lt_lengthD:
assumes i_lt_xs: "i < length xs" and j_lt_xs: "j < length xs" and
i_lt_j: "i < j"
shows "xs1 xi xs2 xj xs3. xs = xs1 @ xi # xs2 @ xj # xs3  length xs1 = i
length (xs1 @ xi # xs2) = j"
proof -
from i_lt_xs obtain xs1 xi xs' where "xs = xs1 @ xi # xs'" and "length xs1 = i"
using lt_lengthD by blast
with j_lt_xs obtain xs2 xj xs3 where "xs = xs1 @ xi # xs2 @ xj # xs3" and "length (xs1 @ xi # xs2) = j"
using lt_lengthD
by (smt (verit, del_insts) append.assoc append_Cons append_eq_append_conv i_lt_j list.inject)
thus ?thesis
using length xs1 = i by blast
qed

subsection ‹Sublist Extra›

lemma not_mem_strict_suffix:
shows "strict_suffix xs (y # ys)  y  set ys  y  set xs"
unfolding strict_suffix_def suffix_def
by (metis Cons_eq_append_conv Un_iff set_append)

lemma not_mem_strict_suffix':
shows "strict_suffix xs (y # ys)  f y  f ` set ys  f y  f ` set xs"
using not_mem_strict_suffix[of "map f xs" "f y" "map f ys", unfolded list.set_map]
using map_mono_strict_suffix[of _ "_ # _", unfolded list.map]
by fast

subsection ‹Multiset Extra›

lemma multpDM_implies_one_step:
"multpDM R M N  I J K. N = I + J  M = I + K  J  {#}  (k∈#K. x∈#J. R k x)"
unfolding multpDM_def

lemma multpHO_implies_one_step:
"multpHO R M N  I J K. N = I + J  M = I + K  J  {#}  (k∈#K. x∈#J. R k x)"
by (metis multpDM_implies_one_step multpHO_imp_multpDM)

lemma Multiset_Bex_plus_iff: "(x ∈# (M1 + M2). P x)  (x ∈# M1. P x)  (x ∈# M2. P x)"
by auto

lemma multp_singleton_rightD:
assumes "multp R M {#x#}" and "transp R"
shows "y ∈# M  R y x"
using multp_implies_one_step[OF transp R multp R M {#x#}]
by (metis add_cancel_left_left set_mset_single single_is_union singletonD)

subsubsection ‹Calculus Extra›

lemma (in consequence_relation) entails_one_formula: "N  U  D  U  N  {D}"
using entail_set_all_formulas by blast

subsection ‹Clausal Calculus Extra›

subsubsection ‹Clausal Calculus Only›

lemma true_cls_iff_set_mset_eq: "set_mset C = set_mset D  I  C  I  D"

lemma true_clss_if_set_mset_eq: "(D  𝒟. C  𝒞. set_mset D = set_mset C)  I ⊫s 𝒞  I ⊫s 𝒟"
using true_cls_iff_set_mset_eq by (metis true_clss_def)

lemma entails_clss_insert: "N ⊫e insert C U  N ⊫e {C}  N ⊫e U"
by auto

lemma Collect_lits_from_atms_conv: "{L. P (atm_of L)} = (x  {x. P x}. {Pos x, Neg x})"
(is "?lhs = ?rhs")
proof (rule Set.equalityI; rule Set.subsetI)
fix L
show "L  ?lhs  L  ?rhs"
by (cases L) simp_all
next
fix L
show "L  ?rhs  L  ?lhs"
by auto
qed

subsubsection ‹Clausal Calculus and Abstract Substitution›

lemma (in substitution) is_ground_lit_Pos[simp]: "is_ground_atm atm  is_ground_lit (Pos atm)"

lemma (in substitution) is_ground_lit_Neg[simp]: "is_ground_atm atm  is_ground_lit (Neg atm)"

subsection ‹First Order Terms Extra›

subsubsection ‹First Order Terms Only›

lemma atm_of_eq_uminus_if_lit_eq: "L = - K  atm_of L = atm_of K"
by (cases L; cases K) simp_all

lemma subst_subst_eq_subst_subst_if_subst_eq_substI:
assumes "t  σ = u  δ" and
t_inter_δ_empty:  and
u_inter_σ_empty:
shows
"range_vars σ  subst_domain δ = {}  t  σ  δ = u  σ  δ"
"range_vars δ  subst_domain σ = {}  t  δ  σ = u  δ  σ"
proof -
from u_inter_σ_empty have "u  σ  δ = u  δ"
with t  σ = u  δ show "range_vars σ  subst_domain δ = {}  t  σ  δ = u  σ  δ"
unfolding subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs[OF _ t_inter_δ_empty]
by simp

from t_inter_δ_empty have "t  δ  σ = t  σ"
with t  σ = u  δ show "range_vars δ  subst_domain σ = {}  t  δ  σ = u  δ  σ"
unfolding subst_apply_term_subst_apply_term_eq_subst_apply_term_lhs[OF _ u_inter_σ_empty]
by simp
qed

lemma subst_compose_in_unifiersI:
assumes "t  σ = u  δ" and
and

shows
"range_vars σ  subst_domain δ = {}  σ s δ  unifiers {(t, u)}"
"range_vars δ  subst_domain σ = {}  δ s σ  unifiers {(t, u)}"
using subst_subst_eq_subst_subst_if_subst_eq_substI(1)[OF assms]
using subst_subst_eq_subst_subst_if_subst_eq_substI(2)[OF assms]

lemma subst_ident_if_not_in_domain: "x  subst_domain μ  μ x = Var x"

(* lemma fixes υ :: "'a ⇒ ('b, 'a) Term.term" assumes "υ ∈ unifiers E" shows "∃μ. is_mgu μ E"
unfolding is_mgu_def
proof (rule ccontr)
assume "∄μ. μ ∈ unifiers E ∧ (∀τ∈unifiers E. ∃γ. τ = μ ∘s γ)"
fix epred5_5 :: "('b, 'a) Term.term set ⇒ ('a ⇒ ('b, 'a) Term.term) ⇒ ('b, 'a) Term.term set ⇒ ('a ⇒ ('b, 'a) Term.term) ⇒  ('b, 'a) Term.term set ⇒ bool"
have "⋀(X1 :: 'a ⇒ ('b, 'a) Term.term) (X2 :: ('b, 'a) Term.term set)
(X3 :: 'a ⇒ ('b, 'a) Term.term)  (X4 :: ('b, 'a) Term.term set) (X5 :: ('b, 'a) Term.term set).
epred5_5 X5 X3 X4 X1 X2 ⟷ ¬ (X3 ∈ X4 ⟶ True)"
(* thf(c_0_5, plain,
![X1:a > term_b_a, X2:set_a_term_b_a, X3:a > term_b_a, X4:set_a_term_b_a, X5:set_a_term_b_a]:
(((epred5_5 @ X5 @ X3 @ X4 @ X1 @ X2)<=>
(~(member_a_term_b_a @ X3 @ X4)=>
(((insert_a_term_b_a @ X1 @ X2)=(insert_a_term_b_a @ X3 @ X4))<=>
((((X1)!=(X3))|(((X2)=(X4))))&
(((X1)=(X3))|((~((((X2)=(insert_a_term_b_a @ X3 @ X5))&
(~(member_a_term_b_a @ X3 @ X5)&
(((X4)=(insert_a_term_b_a @ X1 @ X5))&~(member_a_term_b_a @ X1 @ X5)))))
|(?[X5:set_a_term_b_a]:(\$true)))&
((((X2)=(insert_a_term_b_a @ X3 @ X5))&
(~(member_a_term_b_a @ X3 @ X5)&
(((X4)=(insert_a_term_b_a @ X1 @ X5))&~(member_a_term_b_a @ X1 @ X5))))|
(?[X5:set_a_term_b_a]:(\$false)))))))))), introduced(definition)). *)
show False
using insert_eq_iff mk_disjoint_insert subst_monoid_mult.mult.right_neutral
(* sledgehammer [e, slices = 1, dont_minimize, isar_proof, compress = 1, timeout = 30, preplay_timeout = 10, overlord] (insert_eq_iff mk_disjoint_insert subst_monoid_mult.mult.right_neutral) *)
(* by (metis insert_eq_iff mk_disjoint_insert subst_monoid_mult.mult.right_neutral) *)
using ex_in_conv insertI1 insert_absorb insert_commute insert_eq_iff insert_iff
insert_not_empty is_mgu_def mk_disjoint_insert subst_monoid_mult.mult.right_neutral
(* by (smt (verit) ex_in_conv insertI1 insert_absorb insert_commute insert_eq_iff insert_iff
insert_not_empty is_mgu_def mk_disjoint_insert subst_monoid_mult.mult.right_neutral) *) *)

lemma "is_renaming (Var(x := Var x'))"
proof (unfold is_renaming_def, intro conjI allI)
fix y show "is_Var ((Var(x := Var x')) y)"
by simp
next
show "inj_on (Var(x := Var x')) (subst_domain (Var(x := Var x')))"
apply (rule inj_onI)
by presburger
qed

lemma ex_mgu_if_subst_eq_subst_and_disj_vars:
fixes t u :: "('f, 'v) Term.term" and σt σu :: "('f, 'v) subst"
assumes "t  σt = u  σu" and
shows "μ :: ('f, 'v) subst. Unification.mgu t u = Some μ"
proof -
from assms obtain σ :: "('f, 'v) subst" where "t  σ = u  σ"
using vars_term_disjoint_imp_unifier by metis
thus ?thesis
using ex_mgu_if_subst_apply_term_eq_subst_apply_term
by metis
qed

(* corollary
fixes μ :: "('f, 'v) subst" and E :: "('f, 'v) equations" and Evars :: "'v set"
assumes imgu_μ: "is_imgu μ E" and fin_E: "finite E"
defines "Evars ≡ (⋃e ∈ E. vars_term (fst e) ∪ vars_term (snd e))"
shows "(⋃x ∈ -Evars. vars_term (μ x)) ⊆ -Evars"
using imgu_subst_domain_subset[OF assms(1,2), folded Evars_def] *)
(*   by (smt (verit, del_insts) ComplD SUP_le_iff Term.term.simps(17) compl_le_swap1
subset_Compl_singleton subset_eq subst_ident_if_not_in_domain) *)

lemma restrict_subst_domain_subst_composition:
fixes σA σB A B
assumes
distinct_domains: "A  B = {}" and
distinct_range: "x  A. vars_term (σA x)  subst_domain σB = {}"
defines "σ  restrict_subst_domain A σA s σB"
shows "x  A  σ x = σA x" "x  B  σ x = σB x"
proof -
assume "x  A"
hence "restrict_subst_domain A σA x = σA x"
moreover have "σA x  σB = σA x"
using distinct_range
by (simp add: x  A subst_apply_term_ident)
ultimately show "σ x = σA x"
next
assume "x  B"
hence "restrict_subst_domain A σA x = Var x"
using distinct_domains
by (metis Int_iff empty_iff restrict_subst_domain_def)
then show "σ x = σB x"
qed

lemma merge_substs_on_disjoint_domains:
fixes σA σB A B
assumes distinct_domains: "A  B = {}"
defines "σ  (λx. if x  A then σA x else if x  B then σB x else Var x)"
shows
"x  A  σ x = σA x"
"x  B  σ x = σB x"
"x  A  B  σ x = Var x"
proof -
show "x  A  σ x = σA x"
next
assume "x  B"
moreover hence "x  A"
using distinct_domains by auto
ultimately show "σ x = σB x"
next
show "x  A  B  σ x = Var x"
qed

definition is_grounding_merge where
"is_grounding_merge γ A γA B γB
A  B = {}  (x  A. vars_term (γA x) = {})  (x  B. vars_term (γB x) = {})
(x  A. γ x = γA x)  (x  B. γ x = γB x)"

lemma is_grounding_merge_if_mem_then_else[simp]:
fixes γA γB A B
defines "γ  (λx. if x  A then γA x else γB x)"
shows "is_grounding_merge γ A γA B γB"
unfolding is_grounding_merge_def
by (auto simp: γ_def)

lemma is_grounding_merge_restrict_subst_domain_comp[simp]:
fixes γA γB A B
defines "γ  restrict_subst_domain A γA s γB"
shows "is_grounding_merge γ A γA B γB"
unfolding is_grounding_merge_def
proof (intro impI)
assume disjoint: "A  B = {}" and
ball_A_ground: "xA. vars_term (γA x) = {}" and
ball_B_ground: "xB. vars_term (γB x) = {}"

from ball_A_ground have "xA. vars_term (γA x)  subst_domain γB = {}"
by simp
thus "(xA. γ x = γA x)  (xB. γ x = γB x)"
using restrict_subst_domain_subst_composition[OF disjoint, of γA γB]
qed

subsubsection ‹First Order Terms And Abstract Substitution›

no_notation subst_apply_term (infixl "" 67)
no_notation subst_compose (infixl "s" 75)

global_interpretation substitution_ops subst_apply_term Var subst_compose .

notation subst_atm_abbrev (infixl "⋅a" 67)
notation subst_atm_list (infixl "⋅al" 67)
notation subst_lit (infixl "⋅l" 67)
notation subst_cls (infixl "" 67)
notation subst_clss (infixl "⋅cs" 67)
notation subst_cls_list (infixl "⋅cl" 67)
notation subst_cls_lists (infixl "⋅⋅cl" 67)
notation comp_subst_abbrev (infixl "" 67)

abbreviation vars_lit :: "('f, 'v) Term.term literal  'v set" where
"vars_lit L  vars_term (atm_of L)"

definition vars_cls :: "('f, 'v) term clause  'v set" where
"vars_cls C = Union (set_mset (image_mset vars_lit C))"

definition vars_clss :: "('f, 'v) term clause set  'v set" where
"vars_clss N = (C  N. vars_cls C)"

lemma vars_clss_empty[simp]:

lemma vars_clss_insert[simp]:

lemma vars_clss_union[simp]: "vars_clss (CC  DD) = vars_clss CC  vars_clss DD"

lemma vars_cls_empty[simp]:
unfolding vars_cls_def by simp

lemma finite_vars_cls[simp]: "finite (vars_cls C)"
unfolding vars_cls_def by simp

lemma vars_cls_plus_iff: "vars_cls (C + D) = vars_cls C  vars_cls D"
unfolding vars_cls_def by simp

lemma vars_cls_subset_vars_cls_if_subset_mset: "C ⊆# D  vars_cls C  vars_cls D"

lemma is_ground_atm_iff_vars_empty:
by (metis (mono_tags, opaque_lifting) equals0D equals0I is_ground_atm_def subst_apply_term_empty
subst_def subst_simps(1) term.distinct(1) term_subst_eq term_subst_eq_rev)

lemma is_ground_lit_iff_vars_empty:

lemma is_ground_cls_iff_vars_empty:
by (auto simp: is_ground_cls_def is_ground_lit_iff_vars_empty vars_cls_def)

lemma is_ground_atm_is_ground_on_var:
assumes "is_ground_atm (A ⋅a σ)" and "v  vars_term A"
shows "is_ground_atm (σ v)"
using assms proof (induction A)
case (Var x)
then show ?case by auto
next
case (Fun f ts)
then show ?case unfolding is_ground_atm_def
by auto
qed

lemma is_ground_lit_is_ground_on_var:
assumes ground_lit: "is_ground_lit (subst_lit L σ)" and v_in_L: "v  vars_lit L"
shows "is_ground_atm (σ v)"
proof -
let ?A = "atm_of L"
from v_in_L have A_p: "v  vars_term ?A"
by auto
then have "is_ground_atm (?A ⋅a σ)"
using ground_lit unfolding is_ground_lit_def by auto
then show ?thesis
using A_p is_ground_atm_is_ground_on_var by metis
qed

lemma is_ground_cls_is_ground_on_var:
assumes
ground_clause: "is_ground_cls (subst_cls C σ)" and
v_in_C: "v  vars_cls C"
shows "is_ground_atm (σ v)"
proof -
from v_in_C obtain L where L_p: "L ∈# C" "v  vars_lit L"
unfolding vars_cls_def by auto
then have "is_ground_lit (subst_lit L σ)"
using ground_clause unfolding is_ground_cls_def subst_cls_def by auto
then show ?thesis
using L_p is_ground_lit_is_ground_on_var by metis
qed

lemma vars_atm_subset_subst_domain_if_grounding:
assumes "is_ground_atm (t ⋅a γ)"
shows
using assms
by (metis empty_iff is_ground_atm_iff_vars_empty is_ground_atm_is_ground_on_var subsetI
subst_ident_if_not_in_domain term.set_intros(3))

lemma vars_lit_subset_subst_domain_if_grounding:
assumes "is_ground_lit (L ⋅l γ)"
shows
using assms vars_atm_subset_subst_domain_if_grounding
by (metis atm_of_subst_lit is_ground_lit_def)

lemma vars_cls_subset_subst_domain_if_grounding:
assumes "is_ground_cls (C  σ)"
shows
proof (rule Set.subsetI)
fix x assume "x  vars_cls C"
thus "x  subst_domain σ"
unfolding subst_domain_def mem_Collect_eq
by (metis assms empty_iff is_ground_atm_iff_vars_empty is_ground_cls_is_ground_on_var
term.set_intros(3))
qed

lemma same_on_vars_lit:
assumes "v  vars_lit L. σ v = τ v"
shows "subst_lit L σ = subst_lit L τ"
using assms
proof (induction L)
case (Pos x)
then have "v  vars_term x. σ v = τ v  subst_atm_abbrev x σ = subst_atm_abbrev x τ"
using term_subst_eq by metis+
then show ?case
unfolding subst_lit_def using Pos by auto
next
case (Neg x)
then have "v  vars_term x. σ v = τ v  subst_atm_abbrev x σ = subst_atm_abbrev x τ"
using term_subst_eq by metis+
then show ?case
unfolding subst_lit_def using Neg by auto
qed

lemma same_on_vars_clause:
assumes "v  vars_cls S. σ v = τ v"
shows "subst_cls S σ = subst_cls S τ"
by (smt assms image_eqI image_mset_cong2 mem_simps(9) same_on_vars_lit set_image_mset
subst_cls_def vars_cls_def)

lemma same_on_lits_clause:
assumes "L ∈# C. subst_lit L σ = subst_lit L τ"
shows "subst_cls C σ = subst_cls C τ"
using assms unfolding subst_cls_def
by simp

global_interpretation substitution "(⋅a)" "Var :: _  ('f, 'v) term" "(⊙)"
proof unfold_locales
show "A. A ⋅a Var = A"
by auto
next
show "A τ σ. A ⋅a (τ  σ) = A ⋅a τ ⋅a σ"
by auto
next
show "σ τ. (A. A ⋅a σ = A ⋅a τ)  σ = τ"
next
fix C :: "('f, 'v) term clause" and σ :: "('f, 'v) subst"
assume "is_ground_cls (subst_cls C σ)"
hence ground_atms_σ: "v. v  vars_cls C  is_ground_atm (σ v)"
by (meson is_ground_cls_is_ground_on_var)

define some_ground_trm :: "('f, 'v) term" where "some_ground_trm = (Fun undefined [])"
have ground_trm: "is_ground_atm some_ground_trm"
unfolding is_ground_atm_def some_ground_trm_def by auto
define τ where "τ = (λv. if v  vars_cls C then σ v else some_ground_trm)"
then have τ_σ: "v  vars_cls C. σ v = τ v"
unfolding τ_def by auto

have all_ground_τ: "is_ground_atm (τ v)" for v
proof (cases "v  vars_cls C")
case True
then show ?thesis
using ground_atms_σ τ_σ by auto
next
case False
then show ?thesis
unfolding τ_def using ground_trm by auto
qed
have
unfolding is_ground_subst_def
proof
fix A
show "is_ground_atm (A ⋅a τ)"
proof (induction A)
case (Var v)
thus ?case using all_ground_τ by auto
next
case (Fun f As)
thus ?case using all_ground_τ by (simp add: is_ground_atm_def)
qed
qed
moreover with τ_σ have "C  σ = C  τ"
using same_on_vars_clause by auto
ultimately show "τ. is_ground_subst τ  C  τ = C  σ"
by auto
next
show "wfP (strictly_generalizes_atm :: ('f, 'v) term  _  _)"
unfolding wfP_def
by (rule wf_subset[OF wf_subsumes])
(auto simp: strictly_generalizes_atm_def generalizes_atm_def term_subsumable.subsumes_def
subsumeseq_term.simps)
qed

lemma vars_subst_lit_eq_vars_subst_atm: "vars_lit (L ⋅l σ) = vars_term (atm_of L ⋅a σ)"
by (cases L) simp_all

lemma vars_subst_lit_eq:
"vars_lit (L ⋅l σ) = (x  vars_lit L. vars_term (σ x))"
using vars_term_subst_apply_term by (metis atm_of_subst_lit)

lemma vars_subst_cls_eq:
"vars_cls (C  σ) = (x  vars_cls C. vars_term (σ x))"
by (simp add: vars_cls_def multiset.set_map UN_UN_flatten subst_cls_def
vars_subst_lit_eq[symmetric])

lemma vars_subst_lit_subset:
using vars_term_subst_apply_term_subset[of "atm_of L"] by simp

lemma vars_subst_cls_subset:
unfolding vars_cls_def subst_cls_def
apply simp
using vars_subst_lit_subset
by fastforce

lemma vars_subst_cls_subset_weak: "vars_cls (C  σ)  vars_cls C  range_vars σ"
unfolding vars_cls_def subst_cls_def
apply simp
using vars_subst_lit_subset
by fastforce

lemma vars_cls_plus[simp]: "vars_cls (C + D) = vars_cls C  vars_cls D"
unfolding vars_cls_def by simp

lemma UN_vars_term_atm_of_cls[simp]: "(T{atm_of ` set_mset C}.  (vars_term ` T)) = vars_cls C"
by (induction C) simp_all

lemma vars_lit_subst_subset_vars_cls_substI[intro]:
"vars_lit L  vars_cls C  vars_lit (L ⋅l σ)  vars_cls (C  σ)"

lemma vars_subst_cls_subset_vars_cls_subst:
"vars_cls C  vars_cls D  vars_cls (C  σ)  vars_cls (D  σ)"
by (metis subset_Un_eq subst_cls_union vars_cls_plus_iff vars_subst_cls_eq)

lemma vars_cls_subst_subset:
assumes range_vars_η:
proof -
have "vars_cls ((add_mset L D)  η)  vars_cls (add_mset L D) - subst_domain η  range_vars η"
by (rule vars_subst_cls_subset[of "add_mset L D" η])
also have "...  vars_cls (add_mset L D) - (vars_lit L  vars_lit L')  vars_lit L  vars_lit L'"
using range_vars_η by blast
also have "...  vars_cls (add_mset L D)  vars_lit L'  vars_lit L"
by auto
also have "...  vars_cls D  vars_lit L'  vars_lit L"
by auto
by auto
finally show ?thesis
by assumption
qed

definition disjoint_vars where
"disjoint_vars C D  vars_cls C  vars_cls D = {}"

lemma disjoint_vars_iff_inter_empty:
by (rule disjoint_vars_def)

hide_fact disjoint_vars_def

lemma disjoint_vars_sym:
unfolding disjoint_vars_iff_inter_empty by blast

lemma disjoint_vars_plus_iff: "disjoint_vars (C + D) E  disjoint_vars C E  disjoint_vars D E"
unfolding disjoint_vars_iff_inter_empty vars_cls_plus_iff

lemma disjoint_vars_subset_mset: "disjoint_vars C D  E ⊆# C  disjoint_vars E D"

lemma disjoint_vars_subst_clsI:
"disjoint_vars C D  range_vars σ  vars_cls D = {}  disjoint_vars (C  σ) D"
unfolding disjoint_vars_iff_inter_empty
unfolding vars_subst_cls_eq
by (smt (verit, best) Diff_subset Un_iff disjoint_iff image_cong subsetD vars_subst_cls_eq
vars_subst_cls_subset)

lemma is_renaming_iff: "is_renaming ρ  (x. is_Var (ρ x))  inj ρ"
(is "?lhs  ?rhs")
proof (rule iffI)
show "?lhs  ?rhs"
unfolding is_renaming_def
apply safe
apply (metis subst_apply_eq_Var subst_compose term.disc(1))
by (metis injI subst_compose_def term.sel(1))
next
show "?rhs  ?lhs"
by (auto simp: is_renaming_def intro: ex_inverse_of_renaming)
qed

lemma subst_cls_idem_if_disj_vars: "subst_domain σ  vars_cls C = {}  C  σ = C"
by (metis (mono_tags, lifting) Int_iff empty_iff mem_Collect_eq same_on_vars_clause
subst_cls_id_subst subst_domain_def)

lemma subst_lit_idem_if_disj_vars: "subst_domain σ  vars_lit L = {}  L ⋅l σ = L"
by (rule subst_cls_idem_if_disj_vars[of _ "{#L#}", simplified])

lemma subst_lit_restrict_subst_domain: "vars_lit L  V  L ⋅l restrict_subst_domain V σ = L ⋅l σ"
by (simp add: restrict_subst_domain_def same_on_vars_lit subsetD)

lemma subst_cls_restrict_subst_domain: "vars_cls C  V  C  restrict_subst_domain V σ = C  σ"
by (simp add: restrict_subst_domain_def same_on_vars_clause subsetD)

lemma subst_clss_insert[simp]: "insert C U ⋅cs η = insert (C  η) (U ⋅cs η)"

lemma valid_grounding_of_renaming:
assumes "is_renaming ρ"
shows
proof -
have
by (rule grounding_of_subst_cls_renaming_ident[OF is_renaming ρ])
thus ?thesis
by simp
qed

lemma is_unifier_iff_mem_unifiers_Times:
assumes fin_AA: "finite AA"
shows "is_unifier υ AA  υ  unifiers (AA × AA)"
proof (rule iffI)
assume unif_υ_AA: "is_unifier υ AA"
show "υ  unifiers (AA × AA)"
unfolding unifiers_def mem_Collect_eq
proof (rule ballI)
have "card (AA set υ)  1"
by (rule unif_υ_AA[unfolded is_unifier_def subst_atms_def])

fix p assume "p  AA × AA"
then obtain a b where p_def: "p = (a, b)" and "a  AA" and "b  AA"
by auto
hence "card (AA set υ) = 1"
using fin_AA card (AA set υ)  1 antisym_conv2 by fastforce

hence "a ⋅a υ = b ⋅a υ"
using a  AA b  AA fin_AA is_unifier_subst_atm_eqI unif_υ_AA by blast
thus "fst p ⋅a υ = snd p ⋅a υ"
qed
next
assume unif_υ_AA: "υ  unifiers (AA × AA)"
show "is_unifier υ AA"
using fin_AA unif_υ_AA
proof (induction AA arbitrary: υ rule: finite_induct)
case empty
then show ?case
next
case (insert a AA)
from insert.prems have
υ_in: "υ  unifiers ((insert (a, a) (Pair a ` AA)  (λx. (x, a)) ` AA)  AA × AA)"
unfolding insert_Times_insert'[of a AA a AA] by simp
then show ?case
by (smt (verit, del_insts) Set.set_insert Un_insert_left finite.insertI fst_conv image_insert
insert.hyps(1) insert_compr is_unifier_alt mem_Collect_eq snd_conv unifiers_def)
qed
qed

lemma is_mgu_singleton_iff_Unifiers_is_mgu_Times:
assumes fin: "finite AA"
shows "is_mgu υ {AA}  Unifiers.is_mgu υ (AA × AA)"
by (auto simp: is_mgu_def Unifiers.is_mgu_def is_unifiers_def
is_unifier_iff_mem_unifiers_Times[OF fin])

lemma is_imgu_singleton_iff_Unifiers_is_imgu_Times:
assumes fin: "finite AA"
shows "is_imgu υ {AA}  Unifiers.is_imgu υ (AA × AA)"
by (auto simp: is_imgu_def Unifiers.is_imgu_def is_unifiers_def
is_unifier_iff_mem_unifiers_Times[OF fin])

lemma unifiers_without_refl: "unifiers E = unifiers {e  E. fst e  snd e}"
(is "?lhs = ?rhs")
unfolding unifiers_def by fastforce

assumes ren_ρ: "is_renaming ρ" and vars_L:
shows "L ⋅l ρ ⋅l rename_subst_domain ρ σ = L ⋅l σ"
proof -
from ren_ρ have is_var_ρ: "x. is_Var (ρ x)" and "inj ρ"

show ?thesis
using vars_L renaming_cancels_rename_subst_domain[OF is_var_ρ inj ρ]
by (cases L) (simp_all add: subst_lit_def)
qed

assumes ren_ρ: "is_renaming ρ" and vars_D:
shows "D  ρ  rename_subst_domain ρ σ = D  σ"
unfolding subst_cls_comp_subst[symmetric]
proof (intro same_on_lits_clause ballI)
fix L assume "L ∈# D"
with vars_D have
by (auto dest!: multi_member_split)
thus "L ⋅l (ρ  rename_subst_domain ρ σ) = L ⋅l σ"
unfolding subst_lit_comp_subst
qed

lemma subst_domain_rename_subst_domain_subset':
assumes is_var_ρ: "x. is_Var (ρ x)"
shows "subst_domain (rename_subst_domain ρ σ)  (x  subst_domain σ. vars_term (ρ x))"
proof (rule subset_trans)
show
by (rule subst_domain_rename_subst_domain_subset[OF is_var_ρ])
next
show "the_Var ` ρ ` subst_domain σ  (xsubst_domain σ. vars_term (ρ x))"
unfolding image_the_Var_image_subst_renaming_eq[OF is_var_ρ] by simp
qed

lemma range_vars_eq_empty_if_is_ground:

unfolding range_vars_def UNION_empty_conv subst_range.simps is_ground_cls_iff_vars_empty
by (metis (no_types, opaque_lifting) dual_order.eq_iff imageE is_ground_atm_iff_vars_empty
is_ground_cls_iff_vars_empty is_ground_cls_is_ground_on_var
vars_cls_subset_subst_domain_if_grounding)

subsubsection ‹Minimal, Idempotent Most General Unifier›

lemma is_imgu_if_mgu_eq_Some:
assumes mgu: "Unification.mgu t u = Some μ"
shows "is_imgu μ {{t, u}}"
proof -
have "unifiers ({t, u} × {t, u}) = unifiers {(t, u)}"
by (auto simp: unifiers_def)
hence  "Unifiers.is_imgu μ ({t, u} × {t, u})"
using mgu_sound[OF mgu]
thus ?thesis
qed

primrec pairs where
"pairs [] = []" |
"pairs (x # xs) = (x, x) # map (Pair x) xs @ map (λy. (y, x)) xs @ pairs xs"

lemma "set (pairs [a, b, c, d]) =
{(a, a), (a, b), (a, c), (a, d),
(b, a), (b, b), (b, c), (b, d),
(c, a), (c, b), (c, c), (c, d),
(d, a), (d, b), (d, c), (d, d)}"
by auto

lemma set_pairs: "set (pairs xs) = set xs × set xs"
by (induction xs) auto

text ‹Reflexive and symmetric pairs are not necessary to computing the MGU, but it makes the set of
the resulting list equivalent to @{term "{(x, y). x  xs  y  ys}"}, which is necessary for the
following properties.›

lemma pair_in_set_pairs: "a  set as  b  set as  (a, b)  set (pairs as)"
by (induction as) auto

lemma fst_pair_in_set_if_pair_in_pairs: "p  set (pairs as)  fst p  set as"
by (induction as) auto

lemma snd_pair_in_set_if_pair_in_pairs: "p  set (pairs as)  snd p  set as"
by (induction as) auto

lemma vars_mset_mset_pairs:
"vars_mset (mset (pairs as)) = (b  set as. a  set as. vars_term a  vars_term b)"
by (induction as) (auto simp: vars_mset_def)

definition mgu_sets where
"mgu_sets μ AAA  (ass. set (map set ass) = AAA
map_option subst_of (unify (concat (map pairs ass)) []) = Some μ)"

lemma is_imgu_if_mgu_sets:
assumes mgu_AAA: "mgu_sets μ AAA"
shows "is_imgu μ AAA"
proof -
from mgu_AAA obtain ass xs where
AAA_def: "AAA = set (map set ass)" and
unify: "unify (concat (map pairs ass)) [] = Some xs" and
"subst_of xs = μ"
unfolding mgu_sets_def by auto
hence "Unifiers.is_imgu μ (set (concat (map pairs ass)))"
using unify_sound[OF unify] by simp
moreover have "unifiers (set (concat (map pairs ass))) = {υ. is_unifiers υ AAA}"
unfolding AAA_def
proof (rule Set.equalityI; rule Set.subsetI; unfold mem_Collect_eq)
fix x assume x_in: "x  unifiers (set (concat (map pairs ass)))"
show "is_unifiers x (set (map set ass))"
unfolding is_unifiers_def
proof (rule ballI)
fix As assume "As  set (map set ass)"
hence "finite As" by auto

from As  set (map set ass) obtain as where
as_in: "as  set ass" and As_def: "As = set as"
by auto

show "is_unifier x As"
unfolding is_unifier_alt[OF finite As]
proof (intro ballI)
fix A B assume "A  As" "B  As"
hence "xs  set ass. (A, B)  set (pairs xs)"
using as_in by (auto simp: As_def intro: pair_in_set_pairs)
thus "A ⋅a x = B ⋅a x"
using x_in[unfolded unifiers_def mem_Collect_eq, rule_format, of "(A, B)", simplified]
by simp
qed
qed
next
fix x assume is_unifs_x: "is_unifiers x (set (map set ass))"
show "x  unifiers (set (concat (map pairs ass)))"
unfolding unifiers_def mem_Collect_eq
proof (rule ballI)
fix p assume "p  set (concat (map pairs ass))"
then obtain as where "as  set ass" and p_in: "p  set (pairs as)"
by auto
hence is_unif_x: "is_unifier x (set as)"
using is_unifs_x[unfolded is_unifiers_def] by simp
moreover have "fst p  set as"
by (rule p_in[THEN fst_pair_in_set_if_pair_in_pairs])
moreover have "snd p  set as"
by (rule p_in[THEN snd_pair_in_set_if_pair_in_pairs])
ultimately show "fst p ⋅a x = snd p ⋅a x"
unfolding is_unifier_alt[of "set as", simplified]
by blast
qed
qed
ultimately show "is_imgu μ AAA"
unfolding Unifiers.is_imgu_def is_imgu_def by simp
qed

subsubsection ‹Renaming Extra›

context renaming_apart begin

lemma inj_Var_comp_renaming: "finite V  inj (Var  renaming V)"
using inj_compose inj_renaming by (metis inj_def term.inject(1))

lemma is_renaming_Var_comp_renaming: "finite V  Term.is_renaming (Var  renaming V)"
unfolding Term.is_renaming_def
using inj_Var_comp_renaming by (metis comp_apply inj_on_subset term.disc(1) top_greatest)

lemma vars_term_subst_term_Var_comp_renaming_disj:
assumes fin_V: "finite V"
shows "vars_term (t ⋅a (Var  renaming V))  V = {}"
using is_renaming_Var_comp_renaming[OF fin_V] renaming_correct[OF fin_V]
by (induction t) auto

lemma vars_term_subst_term_Var_comp_renaming_disj':
assumes fin_V: "finite V1" and sub: "V2  V1"
shows "vars_term (t ⋅a (Var  renaming V1))  V2 = {}"
by (meson disjoint_iff fin_V sub subsetD vars_term_subst_term_Var_comp_renaming_disj)

lemma vars_lit_subst_renaming_disj:
assumes fin_V: "finite V"
shows "vars_lit (L ⋅l (Var  renaming V))  V = {}"
using vars_term_subst_term_Var_comp_renaming_disj[OF fin_V] by auto

lemma vars_cls_subst_renaming_disj:
assumes fin_V: "finite V"
shows "vars_cls (C  (Var  renaming V))  V = {}"
unfolding vars_cls_def
apply simp
using vars_lit_subst_renaming_disj[OF fin_V]
by (smt (verit, best) UN_iff UN_simps(10) disjoint_iff multiset.set_map subst_cls_def)

abbreviation renaming_wrt :: "('f, _) Term.term clause set  _  ('f, _) Term.term" where
"renaming_wrt N  Var  renaming (vars_clss N)"

lemma is_renaming_renaming_wrt:
by (simp add: inj_Var_comp_renaming is_renaming_iff vars_clss_def)

lemma ex_renaming_to_disjoint_vars:
fixes C :: "('f, 'a) Term.term clause" and N :: "('f, 'a) Term.term clause set"
assumes fin: "finite N"
shows "ρ. is_renaming ρ  vars_cls (C  ρ)  vars_clss N = {}"
proof (intro exI conjI)
show
using fin is_renaming_renaming_wrt by metis
next
show
by (simp add: fin vars_cls_subst_renaming_disj vars_clss_def)
qed

end

section ‹SCL State›

type_synonym ('f, 'v) closure = "('f, 'v) term clause × ('f, 'v) subst"
type_synonym ('f, 'v) closure_with_lit =
"('f, 'v) term clause × ('f, 'v) term literal × ('f, 'v) subst"
type_synonym ('f, 'v) trail = "(('f, 'v) term literal × ('f, 'v) closure_with_lit option) list"
type_synonym ('f, 'v) state =
"('f, 'v) trail × ('f, 'v) term clause fset × ('f, 'v) closure option"

text ‹Note that, in contrast to Bromberger, Schwarz, and Weidenbach, the level is not part of the
state. It would be redundant because it can always be computed from the trail.›

abbreviation initial_state :: "('f, 'v) state" where
"initial_state  ([], {||}, None)"

definition state_trail :: "('f, 'v) state  ('f, 'v) trail" where
"state_trail S = fst S"

lemma state_trail_simp[simp]: "state_trail (Γ, U, u) = Γ"

definition state_learned :: "('f, 'v) state  ('f, 'v) term clause fset" where
"state_learned S = fst (snd S)"

lemma state_learned_simp[simp]: "state_learned (Γ, U, u) = U"

definition state_conflict :: "('f, 'v) state  ('f, 'v) closure option" where
"state_conflict S = snd (snd S)"

lemma state_conflict_simp[simp]: "state_conflict (Γ, U, u) = u"

lemmas state_proj_simp = state_trail_simp state_learned_simp state_conflict_simp

lemma state_simp[simp]: "(state_trail S, state_learned S, state_conflict S) = S"
by (simp add: state_conflict_def state_learned_def state_trail_def)

fun clss_of_trail_lit where
"clss_of_trail_lit (_, None) = {||}" |
"clss_of_trail_lit (_, Some (C, L, _)) = {|add_mset L C|}"

primrec clss_of_trail :: "('f, 'v) trail  ('f, 'v) term clause fset" where
"clss_of_trail [] = {||}" |
"clss_of_trail (Ln # Γ) = clss_of_trail_lit Ln |∪| clss_of_trail Γ"

hide_fact clss_of_trail_def

lemma clss_of_trail_append: "clss_of_trail (Γ0 @ Γ1) = clss_of_trail Γ0 |∪| clss_of_trail Γ1"
by (induction Γ0) (simp_all add: funion_assoc)

fun clss_of_closure where
"clss_of_closure None = {||}" |
"clss_of_closure (Some (C, _)) = {|C|}"

definition propagate_lit where
"propagate_lit L C γ = (L ⋅l γ, Some (C, L, γ))"

abbreviation trail_propagate ::
"('f, 'v) trail  ('f, 'v) term literal  ('f, 'v) term clause  ('f, 'v) subst
('f, 'v) trail" where
"trail_propagate Γ L C γ  propagate_lit L C γ # Γ"

lemma suffix_trail_propagate[simp]: "suffix Γ (trail_propagate Γ L C δ)"
unfolding suffix_def propagate_lit_def
by simp

lemma clss_of_trail_trail_propagate[simp]:
"clss_of_trail (trail_propagate Γ L C γ) = finsert (add_mset L C) (clss_of_trail Γ)"
unfolding propagate_lit_def by simp

definition decide_lit where
"decide_lit L = (L, None)"

abbreviation trail_decide :: "('f, 'v) trail  ('f, 'v) term literal  ('f, 'v) trail" where
"trail_decide Γ L  decide_lit L # Γ"

lemma clss_of_trail_trail_decide[simp]:

definition is_decision_lit
:: "('f, 'v) term literal × ('f, 'v) closure_with_lit option  bool" where
"is_decision_lit Ln  snd Ln = None"

definition trail_interp :: "('f, 'v) trail  ('f, 'v) term interp" where
"trail_interp Γ = ((λL. case L of Pos A  {A} | Neg A  {}) ` fst ` set Γ)"

lemma "trail_interp Γ = (Ln  set Γ. case fst Ln of Pos t  {t} | Neg t  {})"
unfolding trail_interp_def by simp

definition trail_true_lit :: "('f, 'v) trail  ('f, 'v) term literal  bool" where
"trail_true_lit Γ L  L  fst ` set Γ"

definition trail_false_lit :: "('f, 'v) trail  ('f, 'v) term literal  bool" where
"trail_false_lit Γ L  - L  fst ` set Γ"

definition trail_true_cls :: "('f, 'v) trail  ('f, 'v) term clause  bool" where
"trail_true_cls Γ C  (L ∈# C. trail_true_lit Γ L)"

definition trail_false_cls :: "('f, 'v) trail  ('f, 'v) term clause  bool" where
"trail_false_cls Γ C  (L ∈# C. trail_false_lit Γ L)"

definition trail_true_clss :: "('f, 'v) trail  ('f, 'v) term clause set  bool" where
"trail_true_clss Γ N  (C  N. trail_true_cls Γ C)"

definition trail_defined_lit :: "('f, 'v) trail  ('f, 'v) term literal  bool" where
"trail_defined_lit Γ L  (L  fst ` set Γ  - L  fst ` set Γ)"

definition trail_defined_cls :: "('f, 'v) trail  ('f, 'v) term clause  bool" where
"trail_defined_cls Γ C  (L ∈# C. trail_defined_lit Γ L)"

lemma trail_defined_lit_iff_true_or_false:

unfolding trail_defined_lit_def trail_false_lit_def trail_true_lit_def by (rule refl)

lemma trail_true_or_false_cls_if_defined:

unfolding trail_defined_cls_def trail_false_cls_def trail_true_cls_def
unfolding trail_defined_lit_iff_true_or_false
by blast

lemma trail_false_cls_mempty[simp]:

by (auto simp: trail_false_cls_def)

lemma trail_false_cls_plus:

by (auto simp: trail_false_cls_def)

lemma not_trail_true_Nil[simp]:

by (simp_all add: trail_true_lit_def trail_true_cls_def trail_true_clss_def)

lemma not_trail_false_Nil[simp]:

lemma not_trail_defined_lit_Nil[simp]:

lemma trail_false_lit_if_trail_false_suffix:
"suffix Γ' Γ  trail_false_lit Γ' K  trail_false_lit Γ K"
by (meson image_mono set_mono_suffix subsetD trail_false_lit_def)

lemma trail_false_cls_if_trail_false_suffix:
"suffix Γ' Γ  trail_false_cls Γ' C  trail_false_cls Γ C"
using trail_false_cls_def trail_false_lit_if_trail_false_suffix by metis

lemma trail_interp_Cons: "trail_interp (Ln # Γ) = trail_interp [Ln]  trail_interp Γ"
unfolding trail_interp_def by simp

lemma trail_interp_Cons': "trail_interp (Ln # Γ) = (case fst Ln of Pos A  {A} | Neg A  {})  trail_interp Γ"
unfolding trail_interp_def by simp

lemma true_lit_thick_unionD: "(I1  I2) ⊫l L  I1 ⊫l L  I2 ⊫l L"
by auto

lemma subtrail_falseI:
assumes tr_false: "trail_false_cls ((L, Cl) # Γ) C" and L_not_in: "-L ∉# C"
shows "trail_false_cls Γ C"
unfolding trail_false_cls_def
proof (rule ballI)
fix M
assume M_in: "M ∈# C"

from M_in L_not_in have M_neq_L: "M  -L" by auto

from M_in tr_false have tr_false_lit_M: "trail_false_lit ((L, Cl) # Γ) M"
unfolding trail_false_cls_def by simp
thus "trail_false_lit Γ M"
unfolding trail_false_lit_def
using M_neq_L
by (cases L; cases M) (simp_all add: trail_interp_def trail_false_lit_def)
qed

lemma trail_false_cls_ignores_duplicates:

lemma ball_trail_propagate_is_ground_lit:
assumes "xset Γ. is_ground_lit (fst x)" and "is_ground_lit (L ⋅l σ)"
shows "xset (trail_propagate Γ L C σ). is_ground_lit (fst x)"
unfolding propagate_lit_def
using assms by simp

lemma ball_trail_decide_is_ground_lit:
assumes "xset Γ. is_ground_lit (fst x)" and
shows "xset (trail_decide Γ L). is_ground_lit (fst x)"
using assms

lemma trail_false_cls_subst_mgu_before_grounding:
assumes tr_false_cls: "trail_false_cls Γ ((D + {#L, L'#})  σ)" and
imgu_μ: "is_imgu μ {{atm_of L, atm_of L'}}" and
unif_σ: "is_unifiers σ {{atm_of L, atm_of L'}}"
shows "trail_false_cls Γ ((D + {#L#})  μ  σ)"
unfolding trail_false_cls_def
proof (rule ballI)
fix K
assume "K ∈# (D + {#L#})  μ  σ"
hence "K ∈# D  μ  σ  K = L  ⋅l μ ⋅l σ" by force
thus "trail_false_lit Γ K"
proof (elim disjE)
show "K ∈# D  μ  σ  trail_false_lit Γ K"
using imgu_μ unif_σ
by (metis is_imgu_def subst_cls_comp_subst subst_cls_union tr_false_cls trail_false_cls_def
union_iff)
next
have "L ⋅l μ ⋅l σ = L ⋅l σ"
using imgu_μ unif_σ by (metis is_imgu_def subst_lit_comp_subst)
thus "K = L ⋅l μ ⋅l σ  trail_false_lit Γ K"
by (auto intro: tr_false_cls[unfolded trail_false_cls_def, rule_format])
qed
qed

lemma trail_defined_lit_iff_defined_uminus:

lemma trail_defined_lit_iff:

lemma trail_interp_conv: "trail_interp Γ = atm_of ` {L  fst ` set Γ. is_pos L}"
proof (induction Γ)
case Nil
show ?case by (simp add: trail_interp_def)
next
case (Cons Ln Γ)
then show ?case
unfolding list.set image_insert set_filter_insert_conv trail_interp_Cons'
qed

lemma not_in_trail_interp_if_not_in_trail: "t  atm_of ` fst ` set Γ  t  trail_interp Γ"
by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
literal.sel(2) mem_Collect_eq trail_interp_conv)

inductive trail_consistent where
Nil[simp]: "trail_consistent []" |
Cons: "¬ trail_defined_lit Γ L  trail_consistent Γ  trail_consistent ((L, u) # Γ)"

lemma distinct_atm_of_trail_if_trail_consistent:

by (induction Γ rule: trail_consistent.induct)

lemma trail_consistent_appendD: "trail_consistent (Γ @ Γ')  trail_consistent Γ'"
by (induction Γ) (auto elim: trail_consistent.cases)

lemma trail_consistent_if_suffix:
"trail_consistent Γ  suffix Γ' Γ  trail_consistent Γ'"
by (auto simp: suffix_def intro: trail_consistent_appendD)

lemma trail_interp_lit_if_trail_true:
shows
proof (induction Γ rule: trail_consistent.induct)
case Nil
thus ?case
next
case (Cons Γ K u)
show ?case
proof (cases "L = K  L = - K")
case True
then show ?thesis
proof (elim disjE)
assume "L = K"
thus ?thesis
proof (cases L; cases K)
fix tL tK
from L = K show "L = Pos tL  K = Pos tK  ?thesis"
next
fix tL tK
from L = K show "L = Neg tL  K = Neg tK  ?thesis"
using Cons.hyps(1)
not_in_trail_interp_if_not_in_trail)
qed simp_all
next
assume "L = - K"
then show ?thesis
proof (cases L; cases K)
fix tL tK
from L = - K show "L = Pos tL  K = Neg tK  ?thesis"
unfolding trail_interp_Cons'
using Cons.hyps(1) Cons.prems
by (metis (no_types, lifting) image_insert insertE list.simps(15) literal.distinct(1)
prod.sel(1) trail_defined_lit_def trail_true_lit_def)
next
fix tL tK
from L = - K show "L = Neg tL  K = Pos tK  ?thesis"
unfolding trail_interp_Cons'
using Cons.hyps(1) Cons.prems
by (metis (no_types, lifting) image_insert insertE list.simps(15) literal.distinct(1)
prod.sel(1) trail_defined_lit_def trail_true_lit_def)
qed simp_all
qed
next
case False
with Cons.prems have "trail_true_lit Γ L"
with Cons.IH have "trail_interp Γ ⊫l L"
by simp
with False show ?thesis
by (cases L; cases K) (simp_all add: trail_interp_def del: true_lit_iff)
qed
qed

lemma trail_interp_cls_if_trail_true:
assumes  and "trail_true_cls Γ C"
shows "trail_interp Γ  C"
proof -
from trail_true_cls Γ C obtain L where "L ∈# C" and "trail_true_lit Γ L"
by (auto simp: trail_true_cls_def)
show ?thesis
unfolding true_cls_def
proof (rule bexI[OF _ L ∈# C])
show "trail_interp Γ ⊫l L"
by (rule trail_interp_lit_if_trail_true[OF  trail_true_lit Γ L])
qed
qed

lemma trail_true_cls_iff_trail_interp_entails:
assumes  "L ∈# C. trail_defined_lit Γ L"
shows
proof (rule iffI)
assume "trail_true_cls Γ C"
thus "trail_interp Γ  C"
using assms(1) trail_interp_cls_if_trail_true by fast
next
assume "trail_interp Γ  C"
then obtain L where "L ∈# C" and "trail_interp Γ ⊫l L"
by (auto simp: true_cls_def)
show "trail_true_cls Γ C"
proof (cases L)
case (Pos t)
hence "t  trail_interp Γ"
using trail_interp Γ ⊫l L by simp
then show ?thesis
unfolding trail_true_cls_def
using L ∈# C Pos
by (metis assms(1) assms(2) trail_defined_lit_def trail_interp_lit_if_trail_true
trail_true_lit_def true_lit_simps(2) uminus_Pos)
next
case (Neg t)
then show ?thesis
by (metis L ∈# C trail_interp Γ ⊫l L assms(1) assms(2) trail_defined_lit_def
trail_interp_lit_if_trail_true trail_true_cls_def trail_true_lit_def true_lit_simps(1,2)
uminus_Neg)
qed
qed

lemma trail_false_cls_iff_not_trail_interp_entails:
assumes  "L ∈# C. trail_defined_lit Γ L"
shows
proof (rule iffI)
show
by (metis (mono_tags, opaque_lifting) assms(1) trail_false_cls_def trail_false_lit_def
trail_interp_lit_if_trail_true trail_true_lit_def true_cls_def true_lit_iff
true_lit_simps(1) true_lit_simps(2) uminus_Neg uminus_Pos)
next
show
using assms(1) assms(2) trail_defined_cls_def trail_interp_cls_if_trail_true
trail_true_or_false_cls_if_defined by blast
qed

inductive trail_closures_false where
Nil[simp]: "trail_closures_false []" |
Cons:
"(D K γ. Kn = propagate_lit K D γ  trail_false_cls Γ (D  γ))
trail_closures_false Γ  trail_closures_false (Kn # Γ)"

lemma trail_closures_false_ConsD:
by (auto elim: trail_closures_false.cases)

lemma trail_closures_false_appendD:
by (induction Γ) (auto elim: trail_closures_false.cases)

lemma is_ground_lit_if_true_in_ground_trail:
assumes "L  fst ` set Γ. is_ground_lit L"
shows
using assms by (metis trail_true_lit_def)

lemma is_ground_lit_if_false_in_ground_trail:
assumes "L  fst ` set Γ. is_ground_lit L"
shows
using assms by (metis trail_false_lit_def atm_of_uminus is_ground_lit_def)

lemma is_ground_lit_if_defined_in_ground_trail:
assumes "L  fst ` set Γ. is_ground_lit L"
shows
using assms is_ground_lit_if_true_in_ground_trail is_ground_lit_if_false_in_ground_trail
unfolding trail_defined_lit_iff_true_or_false
by fast

lemma is_ground_cls_if_false_in_ground_trail:
assumes "L  fst ` set Γ. is_ground_lit L"
shows
unfolding trail_false_cls_def is_ground_cls_def
using assms by (auto intro: is_ground_lit_if_false_in_ground_trail)

section ‹SCL(FOL) Calculus›

locale scl_fol_calculus = renaming_apart renaming_vars
for renaming_vars :: "'v set  'v  'v" +
fixes less_B :: "('f, 'v) term  ('f, 'v) term  bool" (infix "B" 50)
assumes
finite_less_B: "β. finite {x. x B β}"
begin

abbreviation lesseq_B (infix "B" 50) where
"lesseq_B  (≺B)=="

lemma lits_less_B_conv: "{L. atm_of L B β} = (x{x. x B β}. {Pos x, Neg x})"
by (rule Collect_lits_from_atms_conv)

lemma lits_eq_conv: "{L. atm_of L = β} = {Pos β, Neg β}"
by (rule Collect_lits_from_atms_conv[of "λx. x  β", simplified])

lemma lits_less_eq_B_conv:
"{L. atm_of L B β  atm_of L = β} = insert (Pos β) (insert (Neg β) {L. atm_of L B β})"
unfolding Collect_disj_eq lits_eq_conv by simp

lemma finite_lits_less_B: "finite {L. atm_of L B β}"
unfolding lits_less_B_conv
proof (rule finite_UN_I)
show "finite {x. x B β}"
by (rule finite_less_B)
next
show "x. x  {x. x B β}  finite {Pos x, Neg x}"
by simp
qed

lemma finite_lits_less_eq_B: "finite {L. atm_of L B β}"
using finite_lits_less_B by (simp add: lits_less_eq_B_conv)

lemma Collect_ball_eq_Pow_Collect: "{X. x  X. P x} = Pow {x. P x}"
by blast

lemma finite_lit_clss_nodup_less_B: "finite {C. L ∈# C. atm_of L B β  count C L = 1}"
proof -
have 1: "(L ∈# C. P L  count C L = 1)  (C'. C = mset_set C'  finite C'  (L  C'. P L))"
for C P
by (smt (verit) count_eq_zero_iff count_mset_set' finite_set_mset finite_set_mset_mset_set
multiset_eqI)

have 2: "finite {C'. LC'. atm_of L B β}"
unfolding Collect_ball_eq_Pow_Collect finite_Pow_iff
by (rule finite_lits_less_B)

show ?thesis
unfolding 1
unfolding setcompr_eq_image
apply (rule finite_imageI)
using 2 by simp
qed

subsection ‹Rules›

inductive propagate :: "('f, 'v) term clause fset  ('f, 'v) term  ('f, 'v) state
('f, 'v) state  bool" for N β where
propagateI: "C |∈| N |∪| U  C = add_mset L C'  is_ground_cls (C  γ)
K ∈# C  γ. atm_of K B β
C0 = {#K ∈# C'. K ⋅l γ  L ⋅l γ#}  C1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#}
trail_false_cls Γ (C0  γ)  ¬ trail_defined_lit Γ (L ⋅l γ)
is_imgu μ {atm_of ` set_mset (add_mset L C1)}
propagate N β (Γ, U, None) (trail_propagate Γ (L ⋅l μ) (C0  μ) γ, U, None)"

lemma "C |∈| N |∪| U  C = add_mset L C'  is_ground_cls (C  γ)
K ∈# C. atm_of (K ⋅l γ) B β
C0 = {#K ∈# C'. K ⋅l γ  L ⋅l γ#}  C1 = {#K ∈# C'. K ⋅l γ = L ⋅l γ#}
trail_false_cls Γ (C0  γ)  ¬ trail_defined_lit Γ (L ⋅l γ)
is_imgu μ {atm_of ` set_mset (add_mset L C1)}
propagate N β (Γ, U, None) (trail_propagate Γ (L ⋅l μ) (C0  μ) γ, U, None)"
apply (rule propagateI[of C N U L C' γ β _ _ Γ μ]; assumption?)
by (metis Melem_subst_cls)

(* Whatch out for equality! *)

inductive decide :: "('f, 'v) term clause fset  ('f, 'v) term  ('f, 'v) state
('f, 'v) state  bool" for N β where
decideI: "L  (set_mset ` fset N)  is_ground_lit (L ⋅l γ)
¬ trail_defined_lit Γ (L ⋅l γ)  atm_of L ⋅a γ B β
decide N β (Γ, U, None) (trail_decide Γ (L ⋅l γ), U, None)"

lemma "add_mset L C |∈| N  is_ground_lit (L ⋅l γ)
¬ trail_defined_lit Γ (L ⋅l γ)  atm_of L ⋅a γ B β
decide N β (Γ, U, None) (trail_decide Γ (L ⋅l γ), U, None)"
by (auto intro!: decideI)

inductive conflict :: "('f, 'v) term clause fset  ('f, 'v) term  ('f, 'v) state
('f, 'v) state  bool" for N β where
conflictI: "D |∈| N |∪| U  is_ground_cls (D  γ)  trail_false_cls Γ (D  γ)
conflict N β (Γ, U, None) (Γ, U, Some (D, γ))"

inductive skip :: "('f, 'v) term clause fset  ('f, 'v) term  ('f, 'v) state
('f, 'v) state  bool" for N β where
skipI: "-L ∉# D  σ
skip N β ((L, n) # Γ, U, Some (D, σ)) (Γ, U, Some (D, σ))"

lemma "-(fst 𝒦) ∉# D  σ  skip N β (𝒦 # Γ, U, Some (D, σ)) (Γ, U, Some (D, σ))"
by (metis prod.exhaust_sel skipI)

inductive factorize :: "('f, 'v) term clause fset  ('f, 'v) term  ('f, 'v) state
('f, 'v) state  bool" for N β where
factorizeI: "L ⋅l γ = L' ⋅l γ  is_imgu μ {{atm_of L, atm_of L'}}
factorize N β (Γ, U, Some (add_mset L' (add_mset L D), γ)) (Γ, U, Some (add_mset L D  μ, γ))"

inductive resolve :: "('f, 'v) term clause fset  ('f, 'v) term  ('f, 'v) state
('f, 'v) state  bool" for N β where
resolveI: "Γ = trail_propagate Γ' K D γD  K ⋅l γD = -(L ⋅l γC)
is_renaming ρC  is_renaming ρD
vars_cls (add_mset L C  ρC)  vars_cls (add_mset K D  ρD) = {}
is_imgu μ {{atm_of L ⋅a ρC, atm_of K ⋅a ρD}}
is_grounding_merge γ
(vars_cls (add_mset L C  ρC)) (rename_subst_domain ρC γC)
(vars_cls (add_mset K D  ρD)) (rename_subst_domain ρD γD)
resolve N β (Γ, U, Some (add_mset L C, γC)) (Γ, U, Some ((C  ρC + D  ρD)  μ, γ))"

(* Think about showing that the more specific rule from the paper is an instance of this generic rule. *)

inductive backtrack :: "('f, 'v) term clause fset  ('f, 'v) term  ('f, 'v) state
('f, 'v) state  bool" for N β where
backtrackI: "Γ = trail_decide (Γ' @ Γ'') K  K = - (L ⋅l σ)
γ. is_ground_cls (add_mset L D  γ)  trail_false_cls Γ'' (add_mset L D  γ)
backtrack N β (Γ, U, Some (add_mset L D, σ)) (Γ'', finsert (add_mset L D) U, None)"

definition scl :: "('f, 'v) term clause fset  ('f, 'v) term  ('f, 'v) state
('f, 'v) state  bool" where
"scl N β S S'  propagate N β S S'  decide N β S S'  conflict N β S S'  skip N β S S'
factorize N β S S'  resolve N β S S'  backtrack N β S S'"

text ‹Note that, in contrast to Fiori and Weidenbach (CADE 2019), the set @{term N} of initial
clauses and the ground atom @{term β} are parameters of the relation instead of being repeated twice
in the states. This is to highlight the fact that they are constant.›

subsection ‹Well-Defined›

lemma propagate_well_defined:
assumes "propagate N β S S'"
shows
"¬ decide N' β' S S'"
"¬ conflict N' β' S S'"
"¬ skip N' β' S S'"
"¬ factorize N' β' S S'"
"¬ resolve N' β' S S'"
"¬ backtrack N' β' S S'"
proof -
from assms obtain L C γ Γ U where
S_def: "S = (Γ, U, None)" and
S'_def: "S' = (trail_propagate Γ L C γ, U, None)"
by (auto elim: propagate.cases)

show "¬ decide N' β' S S'"
using S_def S'_def
by (auto simp add: decide_lit_def propagate_lit_def elim: decide.cases)

show "¬ conflict N' β' S S'"
using S_def S'_def
by (auto elim: conflict.cases)

show "¬ skip N' β' S S'"
using S_def S'_def
by (auto elim: skip.cases)

show "¬ factorize N' β' S S'"
using S_def S'_def
by (auto elim: factorize.cases)

show "¬ resolve N' β' S S'"
using S_def S'_def
by (auto elim: resolve.cases)

show "¬ backtrack N' β' S S'"
using S_def S'_def
by (auto elim: backtrack.cases)
qed

lemma decide_well_defined:
assumes "decide N β S S'"
shows
"¬ propagate N' β' S S'"
"¬ conflict N' β' S S'"
"¬ skip N' β' S S'"
"¬ factorize N' β' S S'"
"¬ resolve N' β' S S'"
"¬ backtrack N' β' S S'"
proof -
from assms obtain L γ Γ U where
S_def: "S = (Γ, U, None)" and
S'_def: "S' = (trail_decide Γ (L ⋅l γ), U, None)"
by (auto elim: decide.cases)

show "¬ propagate N' β' S S'"
using S_def S'_def
by (auto simp add: decide_lit_def propagate_lit_def elim: propagate.cases)

show "¬ conflict N' β' S S'"
using S_def S'_def
by (auto elim: conflict.cases)

show "¬ skip N' β' S S'"
using S_def S'_def
by (auto elim: skip.cases)

show "¬ factorize N' β' S S'"
using S_def S'_def
by (auto elim: factorize.cases)

show "¬ resolve N' β' S S'"
using S_def S'_def
by (auto elim: resolve.cases)

show "¬ backtrack N' β' S S'"
using S_def S'_def
by (auto elim: backtrack.cases)
qed

lemma conflict_well_defined:
assumes "conflict N β S S'"
shows
"¬ propagate N' β' S S'"
"¬ decide N' β' S S'"
"¬ skip N' β' S S'"
"¬ factorize N' β' S S'"
"¬ resolve N' β' S S'"
"¬ backtrack N' β' S S'"
proof -
from assms obtain C γ Γ U where
S_def: "S = (Γ, U, None)" and
S'_def: "S' = (Γ, U, Some (C, γ))"
by (auto elim: conflict.cases)

show "¬ propagate N' β' S S'"
using S_def S'_def
by (auto simp add: decide_lit_def propagate_lit_def elim: propagate.cases)

show "¬ decide N' β' S S'"
using S_def S'_def
by (auto elim: decide.cases)

show "¬ skip N' β' S S'"
using S_def S'_def
by (auto elim: skip.cases)

show "¬ factorize N' β' S S'"
using S_def S'_def
by (auto elim: factorize.cases)

show "¬ resolve N' β' S S'"
using S_def S'_def
by (auto elim: resolve.cases)

show "¬ backtrack N' β' S S'"
using S_def S'_def
by (auto elim: backtrack.cases)
qed

lemma skip_well_defined:
assumes "skip N β S S'"
shows
"¬ propagate N' β' S S'"
"¬ decide N' β' S S'"
"¬ conflict N' β' S S'"
"¬ factorize N' β' S S'"
"¬ resolve N' β' S S'"
"¬ backtrack N' β' S S'"
proof -
from assms obtain Ln Γ U opt where
S_def: "S = (Ln # Γ, U, opt)" and
S'_def: "S' = (Γ, U, opt)"
by (auto elim: skip.cases)

show "¬ propagate N' β' S S'"
using S_def S'_def
by (auto simp add: decide_lit_def propagate_lit_def elim: