# Theory Given_Clause_Architectures_Revisited

```(*  Title:       New Fairness Proofs for the Given Clause Prover Architectures
Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2020
*)

section ‹New Fairness Proofs for the Given Clause Prover Architectures›

theory Given_Clause_Architectures_Revisited
imports Saturation_Framework.Given_Clause_Architectures
begin

text ‹The given clause and lazy given clause procedures satisfy key invariants. This
provides an alternative way to prove fairness and hence saturation of the limit.›

subsection ‹Given Clause Procedure›

context given_clause
begin

definition gc_invar :: "('f × 'l) set llist ⇒ enat ⇒ bool" where
"gc_invar Ns i ⟷
Inf_from (active_subset (Liminf_upto_llist Ns i)) ⊆ Sup_upto_llist (lmap Red_I_𝒢 Ns) i"

lemma gc_invar_infinity:
assumes
nnil: "¬ lnull Ns" and
invar: "∀i. enat i < llength Ns ⟶ gc_invar Ns (enat i)"
shows "gc_invar Ns ∞"
unfolding gc_invar_def
proof (intro subsetI, unfold Liminf_upto_llist_infinity Sup_upto_llist_infinity)
fix ι
assume ι_inff: "ι ∈ Inf_from (active_subset (Liminf_llist Ns))"

define As where
"As = lmap active_subset Ns"

have act_ns: "active_subset (Liminf_llist Ns) = Liminf_llist As"
unfolding As_def active_subset_def Liminf_set_filter_commute[symmetric] ..

note ι_inf = Inf_if_Inf_from[OF ι_inff]
note ι_inff' = ι_inff[unfolded act_ns]

have "¬ lnull As"
unfolding As_def using nnil by auto
moreover have "set (prems_of ι) ⊆ Liminf_llist As"
using ι_inff'[unfolded Inf_from_def] by simp
ultimately obtain i where
i_lt_as: "enat i < llength As" and
prems_sub_ge_i: "set (prems_of ι) ⊆ (⋂j ∈ {j. i ≤ j ∧ enat j < llength As}. lnth As j)"
using finite_subset_Liminf_llist_imp_exists_index by blast

note i_lt_ns = i_lt_as[unfolded As_def, simplified]

have "set (prems_of ι) ⊆ lnth As i"
using prems_sub_ge_i i_lt_as by auto
then have "ι ∈ Inf_from (active_subset (lnth Ns i))"
using i_lt_as ι_inf unfolding Inf_from_def As_def by auto
then have "ι ∈ Sup_upto_llist (lmap Red_I_𝒢 Ns) (enat i)"
using nnil i_lt_ns invar[unfolded gc_invar_def] by auto
then show "ι ∈ Sup_llist (lmap Red_I_𝒢 Ns)"
using Sup_upto_llist_subset_Sup_llist by fastforce
qed

lemma gc_invar_gc_init:
assumes
"¬ lnull Ns" and
"active_subset (lhd Ns) = {}"
shows "gc_invar Ns 0"
using assms labeled_inf_have_prems unfolding gc_invar_def Inf_from_def by auto

lemma gc_invar_gc_step:
assumes
Si_lt: "enat (Suc i) < llength Ns" and
invar: "gc_invar Ns i" and
step: "lnth Ns i ↝GC lnth Ns (Suc i)"
shows "gc_invar Ns (Suc i)"
using step Si_lt invar
proof cases
have i_lt: "enat i < llength Ns"
using Si_lt Suc_ile_eq order.strict_implies_order by blast
have lim_i: "Liminf_upto_llist Ns (enat i) = lnth Ns i"
using i_lt by auto
have lim_Si: "Liminf_upto_llist Ns (enat (Suc i)) = lnth Ns (Suc i)"
using Si_lt by auto

{
case (process N M M')
note ni = this(1) and nSi = this(2) and m'_pas = this(4)

have "Inf_from (active_subset (N ∪ M')) ⊆ Inf_from (active_subset (N ∪ M))"
using m'_pas by (simp add: Inf_from_mono)
also have "… ⊆ Sup_upto_llist (lmap Red_I_𝒢 Ns) (enat i)"
using invar unfolding gc_invar_def lim_i ni by auto
also have "… ⊆ Sup_upto_llist (lmap Red_I_𝒢 Ns) (enat (Suc i))"
by simp
finally show ?thesis
unfolding gc_invar_def lim_Si nSi .
next
case (infer N C L M)
note ni = this(1) and nSi = this(2) and l_pas = this(3) and m_pas = this(4) and
inff_red = this(5)

{
fix ι
assume ι_inff: "ι ∈ Inf_from (active_subset (N ∪ {(C, active)} ∪ M))"

have ι_inf: "ι ∈ Inf_FL"
using ι_inff unfolding Inf_from_def by auto
then have Fι_inf: "to_F ι ∈ Inf_F"
using in_Inf_FL_imp_to_F_in_Inf_F by blast

have "ι ∈ Inf_from (active_subset N ∪ {(C, active)})"
using ι_inff m_pas by simp
then have Fι_inff:
"to_F ι ∈ no_labels.Inf_from (fst ` (active_subset N ∪ {(C, active)}))"
using Fι_inf unfolding to_F_def Inf_from_def no_labels.Inf_from_def by auto

have "ι ∈ Sup_upto_llist (lmap Red_I_𝒢 Ns) (enat (Suc i))"
proof (cases "to_F ι ∈ no_labels.Inf_between (fst ` active_subset N) {C}")
case True
then have "to_F ι ∈ no_labels.Red_I_𝒢 (fst ` (N ∪ {(C, active)} ∪ M))"
using inff_red by auto
then have "ι ∈ Red_I_𝒢 (N ∪ {(C, active)} ∪ M)"
by (subst labeled_red_inf_eq_red_inf[OF ι_inf])
then show ?thesis
using Si_lt using nSi by auto
next
case False
then have "to_F ι ∈ no_labels.Inf_from (fst ` active_subset N)"
using Fι_inff unfolding no_labels.Inf_from_def no_labels.Inf_between_def by auto
then have "ι ∈ Inf_from (active_subset N)"
using ι_inf l_pas unfolding to_F_def Inf_from_def no_labels.Inf_from_def
by clarsimp (smt ι_inff[unfolded Inf_from_def] active_subset_def imageE image_subset_iff
in_mono mem_Collect_eq prod.collapse)
then show ?thesis
using invar l_pas unfolding gc_invar_def lim_i ni by auto
qed
}
then show ?thesis
unfolding gc_invar_def lim_Si nSi by blast
}
qed

lemma gc_invar_gc:
assumes
gc: "chain (↝GC) Ns" and
init: "active_subset (lhd Ns) = {}" and
i_lt: "i < llength Ns"
shows "gc_invar Ns i"
using i_lt
proof (induct i)
case (enat i)
then show ?case
proof (induct i)
case 0
then show ?case
using gc_invar_gc_init[OF chain_not_lnull[OF gc] init] by (simp add: enat_0)
next
case (Suc i)
note ih = this(1) and Si_lt = this(2)
have i_lt: "enat i < llength Ns"
using Si_lt Suc_ile_eq less_le by blast
show ?case
by (rule gc_invar_gc_step[OF Si_lt ih[OF i_lt] chain_lnth_rel[OF gc Si_lt]])
qed
qed simp

lemma gc_fair_new_proof:
assumes
gc: "chain (↝GC) Ns" and
init: "active_subset (lhd Ns) = {}" and
lim: "passive_subset (Liminf_llist Ns) = {}"
shows "fair Ns"
unfolding fair_def
proof -
have "Inf_from (Liminf_llist Ns) ⊆ Inf_from (active_subset (Liminf_llist Ns))" (is "?lhs ⊆ _")
using lim unfolding active_subset_def passive_subset_def
by (metis (no_types, lifting) Inf_from_mono empty_Collect_eq mem_Collect_eq subsetI)
also have "... ⊆ Sup_llist (lmap Red_I_𝒢 Ns)" (is "_ ⊆ ?rhs")
using gc_invar_infinity[OF chain_not_lnull[OF gc]] gc_invar_gc[OF gc init]
unfolding gc_invar_def by fastforce
finally show "?lhs ⊆ ?rhs"
.
qed

end

subsection ‹Lazy Given Clause›

context lazy_given_clause
begin

definition from_F :: "'f inference ⇒ ('f × 'l) inference set" where
"from_F ι = {ι' ∈ Inf_FL. to_F ι' = ι}"

definition lgc_invar :: "('f inference set × ('f × 'l) set) llist ⇒ enat ⇒ bool" where
"lgc_invar TNs i ⟷
Inf_from (active_subset (Liminf_upto_llist (lmap snd TNs) i))
⊆ ⋃ (from_F ` Liminf_upto_llist (lmap fst TNs) i) ∪ Sup_upto_llist (lmap (Red_I_𝒢 ∘ snd) TNs) i"

lemma lgc_invar_infinity:
assumes
nnil: "¬ lnull TNs" and
invar: "∀i. enat i < llength TNs ⟶ lgc_invar TNs (enat i)"
shows "lgc_invar TNs ∞"
unfolding lgc_invar_def
proof (intro subsetI, unfold Liminf_upto_llist_infinity Sup_upto_llist_infinity)
fix ι
assume ι_inff: "ι ∈ Inf_from (active_subset (Liminf_llist (lmap snd TNs)))"

define As where
"As = lmap (active_subset ∘ snd) TNs"

have act_ns: "active_subset (Liminf_llist (lmap snd TNs)) = Liminf_llist As"
unfolding As_def active_subset_def Liminf_set_filter_commute[symmetric] llist.map_comp ..

note ι_inf = Inf_if_Inf_from[OF ι_inff]
note ι_inff' = ι_inff[unfolded act_ns]

show "ι ∈ ⋃ (from_F ` Liminf_llist (lmap fst TNs)) ∪ Sup_llist (lmap (Red_I_𝒢 ∘ snd) TNs)"
proof -
{
assume ι_ni_lim: "ι ∉ ⋃ (from_F ` Liminf_llist (lmap fst TNs))"

have "¬ lnull As"
unfolding As_def using nnil by auto
moreover have "set (prems_of ι) ⊆ Liminf_llist As"
using ι_inff'[unfolded Inf_from_def] by simp
ultimately obtain i where
i_lt_as: "enat i < llength As" and
prems_sub_ge_i: "set (prems_of ι) ⊆ (⋂j ∈ {j. i ≤ j ∧ enat j < llength As}. lnth As j)"
using finite_subset_Liminf_llist_imp_exists_index by blast

have ts_nnil: "¬ lnull (lmap fst TNs)"
using As_def nnil by simp

have Fι_ni_lim: "to_F ι ∉ Liminf_llist (lmap fst TNs)"
using ι_inf ι_ni_lim unfolding from_F_def by auto
obtain i' where
i_le_i': "i ≤ i'" and
i'_lt_as: "enat i' < llength As" and
Fι_ni_i': "to_F ι ∉ lnth (lmap fst TNs) i'"
using i_lt_as not_Liminf_llist_imp_exists_index[OF ts_nnil Fι_ni_lim, of i] unfolding As_def
by auto

have ι_ni_i': "ι ∉ ⋃ (from_F ` fst (lnth TNs i'))"
using Fι_ni_i' i'_lt_as[unfolded As_def] unfolding from_F_def by auto

have "set (prems_of ι) ⊆ (⋂j ∈ {j. i' ≤ j ∧ enat j < llength As}. lnth As j)"
using prems_sub_ge_i i_le_i' by auto
then have "set (prems_of ι) ⊆ lnth As i'"
using i'_lt_as by auto
then have "ι ∈ Inf_from (active_subset (snd (lnth TNs i')))"
using i'_lt_as ι_inf unfolding Inf_from_def As_def by auto
then have ι_in_i': "ι ∈ Sup_upto_llist (lmap (Red_I_𝒢 ∘ snd) TNs) (enat i')"
using ι_ni_i' i'_lt_as[unfolded As_def] invar[unfolded lgc_invar_def] by auto
then have "ι ∈ Sup_llist (lmap (Red_I_𝒢 ∘ snd) TNs)"
using Sup_upto_llist_subset_Sup_llist by fastforce
}
then show ?thesis
by blast
qed
qed

lemma lgc_invar_lgc_init:
assumes
nnil: "¬ lnull TNs" and
n_init: "active_subset (snd (lhd TNs)) = {}" and
t_init: "∀ι ∈ Inf_F. prems_of ι = [] ⟶ ι ∈ fst (lhd TNs)"
shows "lgc_invar TNs 0"
unfolding lgc_invar_def
proof -
have "Inf_from (active_subset (Liminf_upto_llist (lmap snd TNs) 0)) =
Inf_from {}" (is "?lhs = _")
using nnil n_init by auto
also have "... ⊆ ⋃ (from_F ` fst (lhd TNs))"
using t_init Inf_FL_to_Inf_F unfolding Inf_from_def from_F_def to_F_def by force
also have "... ⊆ ⋃ (from_F ` fst (lhd TNs)) ∪ Red_I_𝒢 (snd (lhd TNs))"
by fast
also have "... = ⋃ (from_F ` Liminf_upto_llist (lmap fst TNs) 0)
∪ Sup_upto_llist (lmap (Red_I_𝒢 ∘ snd) TNs) 0" (is "_ = ?rhs")
using nnil by auto
finally show "?lhs ⊆ ?rhs"
.
qed

lemma lgc_invar_lgc_step:
assumes
Si_lt: "enat (Suc i) < llength TNs" and
invar: "lgc_invar TNs i" and
step: "lnth TNs i ↝LGC lnth TNs (Suc i)"
shows "lgc_invar TNs (Suc i)"
using step Si_lt invar
proof cases
let ?Sup_Red_i = "Sup_upto_llist (lmap (Red_I_𝒢 ∘ snd) TNs) (enat i)"
let ?Sup_Red_Si = "Sup_upto_llist (lmap (Red_I_𝒢 ∘ snd) TNs) (enat (Suc i))"

have i_lt: "enat i < llength TNs"
using Si_lt Suc_ile_eq order.strict_implies_order by blast

have lim_i:
"Liminf_upto_llist (lmap fst TNs) (enat i) = lnth (lmap fst TNs) i"
"Liminf_upto_llist (lmap snd TNs) (enat i) = lnth (lmap snd TNs) i"
using i_lt by auto
have lim_Si:
"Liminf_upto_llist (lmap fst TNs) (enat (Suc i)) = lnth (lmap fst TNs) (Suc i)"
"Liminf_upto_llist (lmap snd TNs) (enat (Suc i)) = lnth (lmap snd TNs) (Suc i)"
using Si_lt by auto

{
case (process N1 N M N2 M' T)
note tni = this(1) and tnSi = this(2) and n1 = this(3) and n2 = this(4) and m_red = this(5) and
m'_pas = this(6)

have ni: "lnth (lmap snd TNs) i = N ∪ M"
by (simp add: i_lt n1 tni)
have nSi: "lnth (lmap snd TNs) (Suc i) = N ∪ M'"
by (simp add: Si_lt n2 tnSi)
have ti: "lnth (lmap fst TNs) i = T"
have tSi: "lnth (lmap fst TNs) (Suc i) = T"

have "Inf_from (active_subset (N ∪ M')) ⊆ Inf_from (active_subset (N ∪ M))"
using m'_pas by (simp add: Inf_from_mono)
also have "… ⊆ ⋃ (from_F ` T) ∪ ?Sup_Red_i"
using invar unfolding lgc_invar_def lim_i ni ti .
also have "… ⊆ ⋃ (from_F ` T) ∪ ?Sup_Red_Si"
using Sup_upto_llist_mono by auto
finally show ?thesis
unfolding lgc_invar_def lim_Si nSi tSi .
next
case (schedule_infer T2 T1 T' N1 N C L N2)
note tni = this(1) and tnSi = this(2) and t2 = this(3) and n1 = this(4) and n2 = this(5) and
l_pas = this(6) and t' = this(7)

have ni: "lnth (lmap snd TNs) i = N ∪ {(C, L)}"
by (simp add: i_lt n1 tni)
have nSi: "lnth (lmap snd TNs) (Suc i) = N ∪ {(C, active)}"
by (simp add: Si_lt n2 tnSi)
have ti: "lnth (lmap fst TNs) i = T1"
have tSi: "lnth (lmap fst TNs) (Suc i) = T1 ∪ T'"
by (simp add: Si_lt t2 tnSi)

{
fix ι
assume ι_inff: "ι ∈ Inf_from (active_subset (N ∪ {(C, active)}))"

have ι_inf: "ι ∈ Inf_FL"
using ι_inff unfolding Inf_from_def by auto
then have Fι_inf: "to_F ι ∈ Inf_F"
using in_Inf_FL_imp_to_F_in_Inf_F by blast

have "ι ∈ ⋃ (from_F ` (T1 ∪ T')) ∪ ?Sup_Red_Si"
proof (cases "to_F ι ∈ no_labels.Inf_between (fst ` active_subset N) {C}")
case True
then have "ι ∈ ⋃ (from_F ` (T1 ∪ T'))"
unfolding t' from_F_def using ι_inf by auto
then show ?thesis
by blast
next
case False
moreover have "to_F ι ∈ no_labels.Inf_from (fst ` (active_subset N ∪ {(C, active)}))"
using ι_inff Fι_inf unfolding to_F_def Inf_from_def no_labels.Inf_from_def by auto
ultimately have "to_F ι ∈ no_labels.Inf_from (fst ` active_subset N)"
unfolding no_labels.Inf_from_def no_labels.Inf_between_def by auto
then have "ι ∈ Inf_from (active_subset N)"
using ι_inf unfolding to_F_def no_labels.Inf_from_def
by clarsimp (smt Inf_from_def Un_insert_right ι_inff active_subset_def
boolean_algebra_cancel.sup0 imageE image_subset_iff insert_iff mem_Collect_eq
prod.collapse snd_conv subset_iff)
then have "ι ∈ ⋃ (from_F ` (T1 ∪ T')) ∪ ?Sup_Red_i"
using invar[unfolded lgc_invar_def] l_pas unfolding lim_i ni ti by auto
then show ?thesis
using Sup_upto_llist_mono by force
qed
}
then show ?thesis
unfolding lgc_invar_def lim_i lim_Si nSi tSi by fast
next
case (compute_infer T1 T2 ι' N2 N1 M)
note tni = this(1) and tnSi = this(2) and t1 = this(3) and n2 = this(4) and m_pas = this(5) and
ι'_red = this(6)

have ni: "lnth (lmap snd TNs) i = N1"
have nSi: "lnth (lmap snd TNs) (Suc i) = N1 ∪ M"
by (simp add: Si_lt n2 tnSi)
have ti: "lnth (lmap fst TNs) i = T2 ∪ {ι'}"
by (simp add: i_lt t1 tni)
have tSi: "lnth (lmap fst TNs) (Suc i) = T2"

{
fix ι
assume ι_inff: "ι ∈ Inf_from (active_subset (N1 ∪ M))"

have ι_bef: "ι ∈ ⋃ (from_F ` (T2 ∪ {ι'})) ∪ ?Sup_Red_i"
using ι_inff invar[unfolded lgc_invar_def lim_i ti ni] m_pas by auto
have "ι ∈ ⋃ (from_F ` T2) ∪ ?Sup_Red_Si"
proof (cases "ι ∈ from_F ι'")
case ι_in_ι': True
then have "ι ∈ Red_I_𝒢 (N1 ∪ M)"
using ι'_red from_F_def labeled_red_inf_eq_red_inf by auto
then have "ι ∈ ?Sup_Red_Si"
using Si_lt by (simp add: n2 tnSi)
then show ?thesis
by auto
next
case False
then show ?thesis
using ι_bef by auto
qed
}
then show ?thesis
unfolding lgc_invar_def lim_Si tSi nSi by blast
next
case (delete_orphan_infers T1 T2 T' N)
note tni = this(1) and tnSi = this(2) and t1 = this(3) and t'_orph = this(4)

have ni: "lnth (lmap snd TNs) i = N"
have nSi: "lnth (lmap snd TNs) (Suc i) = N"
have ti: "lnth (lmap fst TNs) i = T2 ∪ T'"
by (simp add: i_lt t1 tni)
have tSi: "lnth (lmap fst TNs) (Suc i) = T2"

{
fix ι
assume ι_inff: "ι ∈ Inf_from (active_subset N)"

have "to_F ι ∉ T'"
using t'_orph ι_inff in_Inf_from_imp_to_F_in_Inf_from by blast
hence "ι ∉ ⋃ (from_F ` T')"
unfolding from_F_def by auto
then have "ι ∈ ⋃ (from_F ` T2) ∪ ?Sup_Red_Si"
using ι_inff invar unfolding lgc_invar_def lim_i ni ti by auto
}
then show ?thesis
unfolding lgc_invar_def lim_Si tSi nSi by blast
}
qed

lemma lgc_invar_lgc:
assumes
lgc: "chain (↝LGC) TNs" and
n_init: "active_subset (snd (lhd TNs)) = {}" and
t_init: "∀ι ∈ Inf_F. prems_of ι = [] ⟶ ι ∈ fst (lhd TNs)" and
i_lt: "i < llength TNs"
shows "lgc_invar TNs i"
using i_lt
proof (induct i)
case (enat i)
then show ?case
proof (induct i)
case 0
then show ?case
using lgc_invar_lgc_init[OF chain_not_lnull[OF lgc] n_init t_init] by (simp add: enat_0)
next
case (Suc i)
note ih = this(1) and Si_lt = this(2)
have i_lt: "enat i < llength TNs"
using Si_lt Suc_ile_eq less_le by blast
show ?case
by (rule lgc_invar_lgc_step[OF Si_lt ih[OF i_lt] chain_lnth_rel[OF lgc Si_lt]])
qed
qed simp

lemma lgc_fair_new_proof:
assumes
lgc: "chain (↝LGC) TNs" and
n_init: "active_subset (snd (lhd TNs)) = {}" and
n_lim: "passive_subset (Liminf_llist (lmap snd TNs)) = {}" and
t_init: "∀ι ∈ Inf_F. prems_of ι = [] ⟶ ι ∈ fst (lhd TNs)" and
t_lim: "Liminf_llist (lmap fst TNs) = {}"
shows "fair (lmap snd TNs)"
unfolding fair_def llist.map_comp
proof -
have "Inf_from (Liminf_llist (lmap snd TNs))
⊆ Inf_from (active_subset (Liminf_llist (lmap snd TNs)))" (is "?lhs ⊆ _")
by (rule Inf_from_mono) (use n_lim passive_subset_def active_subset_def in blast)
also have "... ⊆ ⋃ (from_F ` Liminf_upto_llist (lmap fst TNs) ∞)
∪ Sup_llist (lmap (Red_I_𝒢 ∘ snd) TNs)"
using lgc_invar_infinity[OF chain_not_lnull[OF lgc]] lgc_invar_lgc[OF lgc n_init t_init]
unfolding lgc_invar_def by fastforce
also have "... ⊆ Sup_llist (lmap (Red_I_𝒢 ∘ snd) TNs)" (is "_ ⊆ ?rhs")
using t_lim by auto
finally show "?lhs ⊆ ?rhs"
.
qed

end

end
```