Theory Given_Clause_Architectures
section ‹Given Clause Prover Architectures›
text ‹This section covers all the results presented in the section 4 of the report.
This is where abstract architectures of provers are defined and proven
dynamically refutationally complete.›
theory Given_Clause_Architectures
imports
Lambda_Free_RPOs.Lambda_Free_Util
Labeled_Lifting_to_Non_Ground_Calculi
begin
subsection ‹Basis of the Given Clause Prover Architectures›
locale given_clause_basis = std?: labeled_lifting_intersection Bot_F Inf_F Bot_G Q
entails_q Inf_G_q Red_I_q Red_F_q 𝒢_F_q 𝒢_I_q
"{ι⇩F⇩L :: ('f × 'l) inference. Infer (map fst (prems_of ι⇩F⇩L)) (fst (concl_of ι⇩F⇩L)) ∈ Inf_F}"
for
Bot_F :: "'f set"
and Inf_F :: "'f inference set"
and Bot_G :: "'g set"
and Q :: "'q set"
and entails_q :: "'q ⇒ 'g set ⇒ 'g set ⇒ bool"
and Inf_G_q :: ‹'q ⇒ 'g inference set›
and Red_I_q :: "'q ⇒ 'g set ⇒ 'g inference set"
and Red_F_q :: "'q ⇒ 'g set ⇒ 'g set"
and 𝒢_F_q :: "'q ⇒ 'f ⇒ 'g set"
and 𝒢_I_q :: "'q ⇒ 'f inference ⇒ 'g inference set option"
+ fixes
Equiv_F :: "'f ⇒ 'f ⇒ bool" (infix ‹≐› 50) and
Prec_F :: "'f ⇒ 'f ⇒ bool" (infix ‹≺⋅› 50) and
Prec_L :: "'l ⇒ 'l ⇒ bool" (infix ‹⊏L› 50) and
active :: "'l"
assumes
equiv_equiv_F: "equivp (≐)" and
wf_prec_F: "minimal_element (≺⋅) UNIV" and
wf_prec_L: "minimal_element (⊏L) UNIV" and
compat_equiv_prec: "C1 ≐ D1 ⟹ C2 ≐ D2 ⟹ C1 ≺⋅ C2 ⟹ D1 ≺⋅ D2" and
equiv_F_grounding: "q ∈ Q ⟹ C1 ≐ C2 ⟹ 𝒢_F_q q C1 ⊆ 𝒢_F_q q C2" and
prec_F_grounding: "q ∈ Q ⟹ C2 ≺⋅ C1 ⟹ 𝒢_F_q q C1 ⊆ 𝒢_F_q q C2" and
active_minimal: "l2 ≠ active ⟹ active ⊏L l2" and
at_least_two_labels: "∃l2. active ⊏L l2" and
static_ref_comp: "statically_complete_calculus Bot_F Inf_F (⊨∩𝒢)
no_labels.Red_I_𝒢 no_labels.Red_F_𝒢_empty"
begin
abbreviation Inf_FL :: "('f × 'l) inference set" where
"Inf_FL ≡ {ι⇩F⇩L. Infer (map fst (prems_of ι⇩F⇩L)) (fst (concl_of ι⇩F⇩L)) ∈ Inf_F}"
abbreviation Prec_eq_F :: "'f ⇒ 'f ⇒ bool" (infix ‹≼⋅› 50) where
"C ≼⋅ D ≡ C ≐ D ∨ C ≺⋅ D"
definition Prec_FL :: "('f × 'l) ⇒ ('f × 'l) ⇒ bool" (infix ‹⊏› 50) where
"Cl1 ⊏ Cl2 ⟷ fst Cl1 ≺⋅ fst Cl2 ∨ (fst Cl1 ≐ fst Cl2 ∧ snd Cl1 ⊏L snd Cl2)"
lemma irrefl_prec_F: "¬ C ≺⋅ C"
by (simp add: minimal_element.po[OF wf_prec_F, unfolded po_on_def irreflp_on_def])
lemma trans_prec_F: "C1 ≺⋅ C2 ⟹ C2 ≺⋅ C3 ⟹ C1 ≺⋅ C3"
by (auto intro: minimal_element.po[OF wf_prec_F, unfolded po_on_def transp_on_def, THEN conjunct2,
simplified, rule_format])
lemma wf_prec_FL: "minimal_element (⊏) UNIV"
proof
show "po_on (⊏) UNIV" unfolding po_on_def
proof
show "irreflp (⊏)" unfolding irreflp_on_def Prec_FL_def
proof
fix Cl
assume a_in: "Cl ∈ (UNIV::('f × 'l) set)"
have "¬ (fst Cl ≺⋅ fst Cl)" using wf_prec_F minimal_element.min_elt_ex by force
moreover have "¬ (snd Cl ⊏L snd Cl)" using wf_prec_L minimal_element.min_elt_ex by force
ultimately show "¬ (fst Cl ≺⋅ fst Cl ∨ fst Cl ≐ fst Cl ∧ snd Cl ⊏L snd Cl)" by blast
qed
next
show "transp (⊏)" unfolding Prec_FL_def
proof (rule transpI)
fix Cl1 Cl2 Cl3
assume trans_hyps:
"(fst Cl1 ≺⋅ fst Cl2 ∨ fst Cl1 ≐ fst Cl2 ∧ snd Cl1 ⊏L snd Cl2)"
"(fst Cl2 ≺⋅ fst Cl3 ∨ fst Cl2 ≐ fst Cl3 ∧ snd Cl2 ⊏L snd Cl3)"
have "fst Cl1 ≺⋅ fst Cl2 ⟹ fst Cl2 ≐ fst Cl3 ⟹ fst Cl1 ≺⋅ fst Cl3"
using compat_equiv_prec by (metis equiv_equiv_F equivp_def)
moreover have "fst Cl1 ≐ fst Cl2 ⟹ fst Cl2 ≺⋅ fst Cl3 ⟹ fst Cl1 ≺⋅ fst Cl3"
using compat_equiv_prec by (metis equiv_equiv_F equivp_def)
moreover have "snd Cl1 ⊏L snd Cl2 ⟹ snd Cl2 ⊏L snd Cl3 ⟹ snd Cl1 ⊏L snd Cl3"
using wf_prec_L unfolding minimal_element_def po_on_def transp_def by (meson UNIV_I)
moreover have "fst Cl1 ≐ fst Cl2 ⟹ fst Cl2 ≐ fst Cl3 ⟹ fst Cl1 ≐ fst Cl3"
using equiv_equiv_F by (meson equivp_transp)
ultimately show "fst Cl1 ≺⋅ fst Cl3 ∨ fst Cl1 ≐ fst Cl3 ∧ snd Cl1 ⊏L snd Cl3"
using trans_hyps trans_prec_F by blast
qed
qed
next
show "wfp_on (⊏) UNIV" unfolding wfp_on_def
proof
assume contra: "∃f. ∀i. f i ∈ UNIV ∧ f (Suc i) ⊏ f i"
then obtain f where
f_suc: "∀i. f (Suc i) ⊏ f i"
by blast
define R :: "(('f × 'l) × ('f × 'l)) set" where
"R = {(Cl1, Cl2). fst Cl1 ≺⋅ fst Cl2}"
define S :: "(('f × 'l) × ('f × 'l)) set" where
"S = {(Cl1, Cl2). fst Cl1 ≐ fst Cl2 ∧ snd Cl1 ⊏L snd Cl2}"
obtain k where
f_chain: "∀i. (f (Suc (i + k)), f (i + k)) ∈ S"
proof (atomize_elim, rule wf_infinite_down_chain_compatible[of R f S])
show "wf R"
unfolding R_def using wf_app[OF wf_prec_F[unfolded minimal_element_def, THEN conjunct2,
unfolded wfp_on_UNIV wfp_def]]
by force
next
show "∀i. (f (Suc i), f i) ∈ R ∪ S"
using f_suc unfolding R_def S_def Prec_FL_def by blast
next
show "R O S ⊆ R"
unfolding R_def S_def using compat_equiv_prec equiv_equiv_F equivp_reflp by fastforce
qed
define g where
"⋀i. g i = f (i + k)"
have g_chain: "∀i. (g (Suc i), g i) ∈ S"
unfolding g_def using f_chain by simp
have wf_s: "wf S"
unfolding S_def
by (rule wf_subset[OF wf_app[OF wf_prec_L[unfolded minimal_element_def, THEN conjunct2,
unfolded wfp_on_UNIV wfp_def], of snd]])
fast
show False
using g_chain[unfolded S_def]
wf_s[unfolded S_def, folded wfp_def wfp_on_UNIV, unfolded wfp_on_def]
by auto
qed
qed
definition active_subset :: "('f × 'l) set ⇒ ('f × 'l) set" where
"active_subset M = {CL ∈ M. snd CL = active}"
definition passive_subset :: "('f × 'l) set ⇒ ('f × 'l) set" where
"passive_subset M = {CL ∈ M. snd CL ≠ active}"
lemma active_subset_insert[simp]:
"active_subset (insert Cl N) = (if snd Cl = active then {Cl} else {}) ∪ active_subset N"
unfolding active_subset_def by auto
lemma active_subset_union[simp]: "active_subset (M ∪ N) = active_subset M ∪ active_subset N"
unfolding active_subset_def by auto
lemma passive_subset_insert[simp]:
"passive_subset (insert Cl N) = (if snd Cl ≠ active then {Cl} else {}) ∪ passive_subset N"
unfolding passive_subset_def by auto
lemma passive_subset_union[simp]: "passive_subset (M ∪ N) = passive_subset M ∪ passive_subset N"
unfolding passive_subset_def by auto
sublocale std?: statically_complete_calculus Bot_FL Inf_FL "(⊨∩𝒢L)" Red_I Red_F
using labeled_static_ref[OF static_ref_comp] .
lemma labeled_tiebreaker_lifting:
assumes q_in: "q ∈ Q"
shows "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q)
(Red_I_q q) (Red_F_q q) (𝒢_F_L_q q) (𝒢_I_L_q q) (λg. Prec_FL)"
proof -
have "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q)
(Red_I_q q) (Red_F_q q) (𝒢_F_L_q q) (𝒢_I_L_q q) (λg Cl Cl'. False)"
using ord_fam_lifted_q[OF q_in] .
then have "standard_lifting Inf_FL Bot_G (Inf_G_q q) (entails_q q) (Red_I_q q)
(Red_F_q q) Bot_FL (𝒢_F_L_q q) (𝒢_I_L_q q)"
using lifted_q[OF q_in] by blast
then show "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q)
(Red_I_q q) (Red_F_q q) (𝒢_F_L_q q) (𝒢_I_L_q q) (λg. Prec_FL)"
using wf_prec_FL by (simp add: tiebreaker_lifting.intro tiebreaker_lifting_axioms.intro)
qed
sublocale lifting_intersection Inf_FL Bot_G Q Inf_G_q entails_q Red_I_q Red_F_q
Bot_FL 𝒢_F_L_q 𝒢_I_L_q "λg. Prec_FL"
using labeled_tiebreaker_lifting unfolding lifting_intersection_def
by (simp add: lifting_intersection_axioms.intro
no_labels.ground.consequence_relation_family_axioms
no_labels.ground.inference_system_family_axioms)
notation derive (infix ‹⊳L› 50)
lemma std_Red_I_eq: "std.Red_I = Red_I_𝒢"
unfolding Red_I_𝒢_q_def Red_I_𝒢_L_q_def by simp
lemma std_Red_F_eq: "std.Red_F = Red_F_𝒢_empty"
unfolding Red_F_𝒢_empty_q_def Red_F_𝒢_empty_L_q_def by simp
sublocale statically_complete_calculus Bot_FL Inf_FL "(⊨∩𝒢L)" Red_I Red_F
by unfold_locales (use statically_complete std_Red_I_eq in auto)
lemma labeled_red_inf_eq_red_inf:
assumes i_in: "ι ∈ Inf_FL"
shows "ι ∈ Red_I N ⟷ to_F ι ∈ no_labels.Red_I_𝒢 (fst ` N)"
proof
assume i_in2: "ι ∈ Red_I N"
then have "X ∈ Red_I_𝒢_q ` Q ⟹ ι ∈ X N" for X
unfolding Red_I_def by blast
obtain X0 where "X0 ∈ Red_I_𝒢_q ` Q"
using Q_nonempty by blast
then obtain q0 where x0_is: "X0 N = Red_I_𝒢_q q0 N" by blast
then obtain Y0 where y0_is: "Y0 (fst ` N) = to_F ` (X0 N)" by auto
have "Y0 (fst ` N) = no_labels.Red_I_𝒢_q q0 (fst ` N)"
unfolding y0_is
proof
show "to_F ` X0 N ⊆ no_labels.Red_I_𝒢_q q0 (fst ` N)"
proof
fix ι0
assume i0_in: "ι0 ∈ to_F ` X0 N"
then have i0_in2: "ι0 ∈ to_F ` Red_I_𝒢_q q0 N"
using x0_is by argo
then obtain ι0_FL where i0_FL_in: "ι0_FL ∈ Inf_FL" and i0_to_i0_FL: "ι0 = to_F ι0_FL" and
subs1: "((𝒢_I_L_q q0 ι0_FL) ≠ None ∧
the (𝒢_I_L_q q0 ι0_FL) ⊆ Red_I_q q0 (𝒢_Fset_q q0 N))
∨ ((𝒢_I_L_q q0 ι0_FL = None) ∧
𝒢_F_L_q q0 (concl_of ι0_FL) ⊆ 𝒢_Fset_q q0 N ∪ Red_F_q q0 (𝒢_Fset_q q0 N))"
unfolding Red_I_𝒢_q_def by blast
have concl_swap: "fst (concl_of ι0_FL) = concl_of ι0"
unfolding concl_of_def i0_to_i0_FL to_F_def by simp
have i0_in3: "ι0 ∈ Inf_F"
using i0_to_i0_FL Inf_FL_to_Inf_F[OF i0_FL_in] unfolding to_F_def by blast
{
assume
not_none: "𝒢_I_q q0 ι0 ≠ None" and
"the (𝒢_I_q q0 ι0) ≠ {}"
then obtain ι1 where i1_in: "ι1 ∈ the (𝒢_I_q q0 ι0)" by blast
have "the (𝒢_I_q q0 ι0) ⊆ Red_I_q q0 (no_labels.𝒢_Fset_q q0 (fst ` N))"
using subs1 i0_to_i0_FL not_none by auto
}
moreover {
assume
is_none: "𝒢_I_q q0 ι0 = None"
then have "𝒢_F_q q0 (concl_of ι0) ⊆ no_labels.𝒢_Fset_q q0 (fst ` N)
∪ Red_F_q q0 (no_labels.𝒢_Fset_q q0 (fst ` N))"
using subs1 i0_to_i0_FL concl_swap by simp
}
ultimately show "ι0 ∈ no_labels.Red_I_𝒢_q q0 (fst ` N)"
unfolding no_labels.Red_I_𝒢_q_def using i0_in3 by auto
qed
next
show "no_labels.Red_I_𝒢_q q0 (fst ` N) ⊆ to_F ` X0 N"
proof
fix ι0
assume i0_in: "ι0 ∈ no_labels.Red_I_𝒢_q q0 (fst ` N)"
then have i0_in2: "ι0 ∈ Inf_F"
unfolding no_labels.Red_I_𝒢_q_def by blast
obtain ι0_FL where i0_FL_in: "ι0_FL ∈ Inf_FL" and i0_to_i0_FL: "ι0 = to_F ι0_FL"
using Inf_F_to_Inf_FL[OF i0_in2] unfolding to_F_def
by (smt (verit) Ex_list_of_length fst_conv inference.exhaust_sel inference.sel(1)
inference.sel(2) map_fst_zip)
have concl_swap: "fst (concl_of ι0_FL) = concl_of ι0"
unfolding concl_of_def i0_to_i0_FL to_F_def by simp
have subs1: "((𝒢_I_L_q q0 ι0_FL) ≠ None ∧
the (𝒢_I_L_q q0 ι0_FL) ⊆ Red_I_q q0 (𝒢_Fset_q q0 N))
∨ ((𝒢_I_L_q q0 ι0_FL = None) ∧
𝒢_F_L_q q0 (concl_of ι0_FL) ⊆ (𝒢_Fset_q q0 N ∪ Red_F_q q0 (𝒢_Fset_q q0 N)))"
using i0_in i0_to_i0_FL concl_swap unfolding no_labels.Red_I_𝒢_q_def by simp
then have "ι0_FL ∈ Red_I_𝒢_q q0 N"
using i0_FL_in unfolding Red_I_𝒢_q_def by simp
then show "ι0 ∈ to_F ` X0 N"
using x0_is i0_to_i0_FL i0_in2 by blast
qed
qed
then have "Y ∈ no_labels.Red_I_𝒢_q ` Q ⟹ to_F ι ∈ Y (fst ` N)" for Y
using i_in2 no_labels.Red_I_def std_Red_I_eq red_inf_impl by force
then show "to_F ι ∈ no_labels.Red_I_𝒢 (fst ` N)"
unfolding Red_I_def no_labels.Red_I_𝒢_def by blast
next
assume to_F_in: "to_F ι ∈ no_labels.Red_I_𝒢 (fst ` N)"
have imp_to_F: "X ∈ no_labels.Red_I_𝒢_q ` Q ⟹ to_F ι ∈ X (fst ` N)" for X
using to_F_in unfolding no_labels.Red_I_𝒢_def by blast
then have to_F_in2: "to_F ι ∈ no_labels.Red_I_𝒢_q q (fst ` N)" if "q ∈ Q" for q
using that by auto
have "Red_I_𝒢_q q N = {ι0_FL ∈ Inf_FL. to_F ι0_FL ∈ no_labels.Red_I_𝒢_q q (fst ` N)}" for q
proof
show "Red_I_𝒢_q q N ⊆ {ι0_FL ∈ Inf_FL. to_F ι0_FL ∈ no_labels.Red_I_𝒢_q q (fst ` N)}"
proof
fix q0 ι1
assume
i1_in: "ι1 ∈ Red_I_𝒢_q q0 N"
have i1_in2: "ι1 ∈ Inf_FL"
using i1_in unfolding Red_I_𝒢_q_def by blast
then have to_F_i1_in: "to_F ι1 ∈ Inf_F"
using Inf_FL_to_Inf_F unfolding to_F_def by blast
have concl_swap: "fst (concl_of ι1) = concl_of (to_F ι1)"
unfolding concl_of_def to_F_def by simp
then have i1_to_F_in: "to_F ι1 ∈ no_labels.Red_I_𝒢_q q0 (fst ` N)"
using i1_in to_F_i1_in unfolding Red_I_𝒢_q_def no_labels.Red_I_𝒢_q_def by force
show "ι1 ∈ {ι0_FL ∈ Inf_FL. to_F ι0_FL ∈ no_labels.Red_I_𝒢_q q0 (fst ` N)}"
using i1_in2 i1_to_F_in by blast
qed
next
show "{ι0_FL ∈ Inf_FL. to_F ι0_FL ∈ no_labels.Red_I_𝒢_q q (fst ` N)} ⊆ Red_I_𝒢_q q N"
proof
fix q0 ι1
assume
i1_in: "ι1 ∈ {ι0_FL ∈ Inf_FL. to_F ι0_FL ∈ no_labels.Red_I_𝒢_q q0 (fst ` N)}"
then have i1_in2: "ι1 ∈ Inf_FL" by blast
then have to_F_i1_in: "to_F ι1 ∈ Inf_F"
using Inf_FL_to_Inf_F unfolding to_F_def by blast
have concl_swap: "fst (concl_of ι1) = concl_of (to_F ι1)"
unfolding concl_of_def to_F_def by simp
then have "((𝒢_I_L_q q0 ι1) ≠ None ∧ the (𝒢_I_L_q q0 ι1) ⊆ Red_I_q q0 (𝒢_Fset_q q0 N))
∨ (𝒢_I_L_q q0 ι1 = None ∧
𝒢_F_L_q q0 (concl_of ι1) ⊆ 𝒢_Fset_q q0 N ∪ Red_F_q q0 (𝒢_Fset_q q0 N))"
using i1_in unfolding no_labels.Red_I_𝒢_q_def by auto
then show "ι1 ∈ Red_I_𝒢_q q0 N"
using i1_in2 unfolding Red_I_𝒢_q_def by blast
qed
qed
then have "ι ∈ Red_I_𝒢_q q N" if "q ∈ Q" for q
using that to_F_in2 i_in unfolding Red_I_𝒢_q_def no_labels.Red_I_𝒢_q_def by auto
then show "ι ∈ Red_I_𝒢 N"
unfolding Red_I_𝒢_def by blast
qed
lemma red_labeled_clauses:
assumes ‹C ∈ no_labels.Red_F_𝒢_empty (fst ` N) ∨
(∃C' ∈ fst ` N. C' ≺⋅ C) ∨ (∃(C', L') ∈ N. L' ⊏L L ∧ C' ≼⋅ C)›
shows ‹(C, L) ∈ Red_F N›
proof -
note assms
moreover have i: ‹C ∈ no_labels.Red_F_𝒢_empty (fst ` N) ⟹ (C, L) ∈ Red_F N›
proof -
assume "C ∈ no_labels.Red_F_𝒢_empty (fst ` N)"
then have "C ∈ no_labels.Red_F_𝒢_empty_q q (fst ` N)" if "q ∈ Q" for q
unfolding no_labels.Red_F_𝒢_empty_def using that by fast
then have g_in_red: "𝒢_F_q q C ⊆ Red_F_q q (no_labels.𝒢_Fset_q q (fst ` N))" if "q ∈ Q" for q
unfolding no_labels.Red_F_𝒢_empty_q_def using that by blast
have "𝒢_F_L_q q (C, L) ⊆ Red_F_q q (𝒢_Fset_q q N)" if "q ∈ Q" for q
using that g_in_red by simp
then show ?thesis
unfolding Red_F_def Red_F_𝒢_q_def by blast
qed
moreover have ii: ‹∃C' ∈ fst ` N. C' ≺⋅ C ⟹ (C, L) ∈ Red_F N›
proof -
assume "∃C' ∈ fst ` N. C' ≺⋅ C"
then obtain C' where c'_in: "C' ∈ fst ` N" and c_prec_c': "C' ≺⋅ C" by blast
obtain L' where c'_l'_in: "(C', L') ∈ N" using c'_in by auto
have c'_l'_prec: "(C', L') ⊏ (C, L)"
using c_prec_c' unfolding Prec_FL_def by simp
have c_in_c'_g: "𝒢_F_q q C ⊆ 𝒢_F_q q C'" if "q ∈ Q" for q
using prec_F_grounding[OF that c_prec_c'] by presburger
then have "𝒢_F_L_q q (C, L) ⊆ 𝒢_F_L_q q (C', L')" if "q ∈ Q" for q
using that by auto
then have "(C, L) ∈ Red_F_𝒢_q q N" if "q ∈ Q" for q
unfolding Red_F_𝒢_q_def using that c'_l'_in c'_l'_prec by blast
then show ?thesis
unfolding Red_F_def by blast
qed
moreover have iii: ‹∃(C', L') ∈ N. L' ⊏L L ∧ C' ≼⋅ C ⟹ (C, L) ∈ Red_F N›
proof -
assume "∃(C', L') ∈ N. L' ⊏L L ∧ C' ≼⋅ C"
then obtain C' L' where c'_l'_in: "(C', L') ∈ N" and l'_sub_l: "L' ⊏L L" and c'_sub_c: "C' ≼⋅ C"
by fast
have "(C, L) ∈ Red_F N" if "C' ≺⋅ C"
using that c'_l'_in ii by fastforce
moreover {
assume equiv_c_c': "C ≐ C'"
then have equiv_c'_c: "C' ≐ C"
using equiv_equiv_F by (simp add: equivp_symp)
then have c'_l'_prec: "(C', L') ⊏ (C, L)"
using l'_sub_l unfolding Prec_FL_def by simp
have "𝒢_F_q q C = 𝒢_F_q q C'" if "q ∈ Q" for q
using that equiv_F_grounding equiv_c_c' equiv_c'_c by (simp add: set_eq_subset)
then have "𝒢_F_L_q q (C, L) = 𝒢_F_L_q q (C', L')" if "q ∈ Q" for q
using that by auto
then have "(C, L) ∈ Red_F_𝒢_q q N" if "q ∈ Q" for q
unfolding Red_F_𝒢_q_def using that c'_l'_in c'_l'_prec by blast
then have ?thesis
unfolding Red_F_def by blast
}
ultimately show ?thesis
using c'_sub_c equiv_equiv_F equivp_symp by fastforce
qed
ultimately show ?thesis
by blast
qed
end
subsection ‹Given Clause Procedure›
locale given_clause = given_clause_basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q
Red_F_q 𝒢_F_q 𝒢_I_q Equiv_F Prec_F Prec_L active
for
Bot_F :: "'f set" and
Inf_F :: "'f inference set" and
Bot_G :: "'g set" and
Q :: "'q set" and
entails_q :: "'q ⇒ 'g set ⇒ 'g set ⇒ bool" and
Inf_G_q :: ‹'q ⇒ 'g inference set› and
Red_I_q :: "'q ⇒ 'g set ⇒ 'g inference set" and
Red_F_q :: "'q ⇒ 'g set ⇒ 'g set" and
𝒢_F_q :: "'q ⇒ 'f ⇒ 'g set" and
𝒢_I_q :: "'q ⇒ 'f inference ⇒ 'g inference set option" and
Equiv_F :: "'f ⇒ 'f ⇒ bool" (infix ‹≐› 50) and
Prec_F :: "'f ⇒ 'f ⇒ bool" (infix ‹≺⋅› 50) and
Prec_L :: "'l ⇒ 'l ⇒ bool" (infix ‹⊏L› 50) and
active :: 'l +
assumes
inf_have_prems: "ιF ∈ Inf_F ⟹ prems_of ιF ≠ []"
begin
lemma labeled_inf_have_prems: "ι ∈ Inf_FL ⟹ prems_of ι ≠ []"
using inf_have_prems by fastforce
inductive step :: "('f × 'l) set ⇒ ('f × 'l) set ⇒ bool" (infix ‹↝GC› 50) where
process: "N1 = N ∪ M ⟹ N2 = N ∪ M' ⟹ M ⊆ Red_F (N ∪ M') ⟹
active_subset M' = {} ⟹ N1 ↝GC N2"
| infer: "N1 = N ∪ {(C, L)} ⟹ N2 = N ∪ {(C, active)} ∪ M ⟹ L ≠ active ⟹
active_subset M = {} ⟹
no_labels.Inf_between (fst ` active_subset N) {C}
⊆ no_labels.Red_I (fst ` (N ∪ {(C, active)} ∪ M)) ⟹
N1 ↝GC N2"
lemma one_step_equiv: "N1 ↝GC N2 ⟹ N1 ⊳L N2"
proof (cases N1 N2 rule: step.cases)
show "N1 ↝GC N2 ⟹ N1 ↝GC N2" by blast
next
fix N M M'
assume
gc_step: "N1 ↝GC N2" and
n1_is: "N1 = N ∪ M" and
n2_is: "N2 = N ∪ M'" and
m_red: "M ⊆ Red_F (N ∪ M')" and
active_empty: "active_subset M' = {}"
have "N1 - N2 ⊆ Red_F N2"
using n1_is n2_is m_red by auto
then show "N1 ⊳L N2"
unfolding derive.simps by blast
next
fix N C L M
assume
gc_step: "N1 ↝GC N2" and
n1_is: "N1 = N ∪ {(C, L)}" and
not_active: "L ≠ active" and
n2_is: "N2 = N ∪ {(C, active)} ∪ M" and
active_empty: "active_subset M = {}"
have "(C, active) ∈ N2" using n2_is by auto
moreover have "C ≼⋅ C" using equiv_equiv_F by (metis equivp_def)
moreover have "active ⊏L L" using active_minimal[OF not_active] .
ultimately have "{(C, L)} ⊆ Red_F N2"
using red_labeled_clauses by blast
moreover have "N1 - N2 = {} ∨ N1 - N2 = {(C, L)}" using n1_is n2_is by blast
ultimately have "N1 - N2 ⊆ Red_F N2"
using std_Red_F_eq by blast
then show "N1 ⊳L N2"
unfolding derive.simps by blast
qed
lemma gc_to_red: "chain (↝GC) Ns ⟹ chain (⊳L) Ns"
using one_step_equiv Lazy_List_Chain.chain_mono by blast
lemma (in-) all_ex_finite_set: "(∀(j::nat)∈{0..<m}. ∃(n::nat). P j n) ⟹
(∀n1 n2. ∀j∈{0..<m}. P j n1 ⟶ P j n2 ⟶ n1 = n2) ⟹ finite {n. ∃j ∈ {0..<m}. P j n}" for m P
proof -
fix m::nat and P:: "nat ⇒ nat ⇒ bool"
assume
allj_exn: "∀j∈{0..<m}. ∃n. P j n" and
uniq_n: "∀n1 n2. ∀j∈{0..<m}. P j n1 ⟶ P j n2 ⟶ n1 = n2"
have "{n. ∃j ∈ {0..<m}. P j n} = (⋃((λj. {n. P j n}) ` {0..<m}))" by blast
then have imp_finite: "(∀j∈{0..<m}. finite {n. P j n}) ⟹ finite {n. ∃j ∈ {0..<m}. P j n}"
using finite_UN[of "{0..<m}" "λj. {n. P j n}"] by simp
have "∀j∈{0..<m}. ∃!n. P j n" using allj_exn uniq_n by blast
then have "∀j∈{0..<m}. finite {n. P j n}" by (metis bounded_nat_set_is_finite lessI mem_Collect_eq)
then show "finite {n. ∃j ∈ {0..<m}. P j n}" using imp_finite by simp
qed
lemma gc_fair:
assumes
deriv: "chain (↝GC) Ns" and
init_state: "active_subset (lhd Ns) = {}" and
final_state: "passive_subset (Liminf_llist Ns) = {}"
shows "fair Ns"
unfolding fair_def
proof
fix ι
assume i_in: "ι ∈ Inf_from (Liminf_llist Ns)"
note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
have i_in_inf_fl: "ι ∈ Inf_FL" using i_in unfolding Inf_from_def by blast
have "Liminf_llist Ns = active_subset (Liminf_llist Ns)"
using final_state unfolding passive_subset_def active_subset_def by blast
then have i_in2: "ι ∈ Inf_from (active_subset (Liminf_llist Ns))" using i_in by simp
define m where "m = length (prems_of ι)"
then have m_def_F: "m = length (prems_of (to_F ι))" unfolding to_F_def by simp
have i_in_F: "to_F ι ∈ Inf_F"
using i_in Inf_FL_to_Inf_F unfolding Inf_from_def to_F_def by blast
then have m_pos: "m > 0" using m_def_F using inf_have_prems by blast
have exist_nj: "∀j ∈ {0..<m}. (∃nj. enat (Suc nj) < llength Ns ∧
prems_of ι ! j ∉ active_subset (lnth Ns nj) ∧
(∀k. k > nj ⟶ enat k < llength Ns ⟶ prems_of ι ! j ∈ active_subset (lnth Ns k)))"
proof clarify
fix j
assume j_in: "j ∈ {0..<m}"
then obtain C where c_is: "(C, active) = prems_of ι ! j"
using i_in2 unfolding m_def Inf_from_def active_subset_def
by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv)
then have "(C, active) ∈ Liminf_llist Ns"
using j_in i_in unfolding m_def Inf_from_def by force
then obtain nj where nj_is: "enat nj < llength Ns" and
c_in2: "(C, active) ∈ ⋂ (lnth Ns ` {k. nj ≤ k ∧ enat k < llength Ns})"
unfolding Liminf_llist_def using init_state by blast
then have c_in3: "∀k. k ≥ nj ⟶ enat k < llength Ns ⟶ (C, active) ∈ lnth Ns k" by blast
have nj_pos: "nj > 0" using init_state c_in2 nj_is
unfolding active_subset_def lhd_is by force
obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength Ns ∧
(C, active) ∈ ⋂ (lnth Ns ` {k. nj ≤ k ∧ enat k < llength Ns}))" by blast
then have in_allk: "∀k. k ≥ nj_min ⟶ enat k < llength Ns ⟶ (C, active) ∈ (lnth Ns k)"
using c_in3 nj_is c_in2
by (metis (mono_tags, lifting) INT_E LeastI_ex mem_Collect_eq)
have njm_smaller_D: "enat nj_min < llength Ns"
using nj_min_is
by (smt LeastI_ex ‹⋀thesis. (⋀nj. ⟦enat nj < llength Ns;
(C, active) ∈ ⋂ (lnth Ns ` {k. nj ≤ k ∧ enat k < llength Ns})⟧ ⟹ thesis) ⟹ thesis›)
have "nj_min > 0"
using nj_is c_in2 nj_pos nj_min_is lhd_is
by (metis (mono_tags, lifting) Collect_empty_eq ‹(C, active) ∈ Liminf_llist Ns›
‹Liminf_llist Ns = active_subset (Liminf_llist Ns)›
‹∀k≥nj_min. enat k < llength Ns ⟶ (C, active) ∈ lnth Ns k› active_subset_def init_state
linorder_not_less mem_Collect_eq zero_enat_def chain_length_pos[OF deriv])
then obtain njm_prec where nj_prec_is: "Suc njm_prec = nj_min" using gr0_conv_Suc by auto
then have njm_prec_njm: "njm_prec < nj_min" by blast
then have njm_prec_njm_enat: "enat njm_prec < enat nj_min" by simp
have njm_prec_smaller_d: "njm_prec < llength Ns"
by (rule less_trans[OF njm_prec_njm_enat njm_smaller_D])
have njm_prec_all_suc: "∀k>njm_prec. enat k < llength Ns ⟶ (C, active) ∈ lnth Ns k"
using nj_prec_is in_allk by simp
have notin_njm_prec: "(C, active) ∉ lnth Ns njm_prec"
proof (rule ccontr)
assume "¬ (C, active) ∉ lnth Ns njm_prec"
then have absurd_hyp: "(C, active) ∈ lnth Ns njm_prec" by simp
have prec_smaller: "enat njm_prec < llength Ns" using nj_min_is nj_prec_is
by (smt LeastI_ex Suc_leD ‹⋀thesis. (⋀nj. ⟦enat nj < llength Ns;
(C, active) ∈ ⋂ (lnth Ns ` {k. nj ≤ k ∧ enat k < llength Ns})⟧ ⟹ thesis) ⟹ thesis›
enat_ord_simps(1) le_eq_less_or_eq le_less_trans)
have "(C, active) ∈ ⋂ (lnth Ns ` {k. njm_prec ≤ k ∧ enat k < llength Ns})"
proof -
{
fix k
assume k_in: "njm_prec ≤ k ∧ enat k < llength Ns"
have "k = njm_prec ⟹ (C, active) ∈ lnth Ns k" using absurd_hyp by simp
moreover have "njm_prec < k ⟹ (C, active) ∈ lnth Ns k"
using nj_prec_is in_allk k_in by simp
ultimately have "(C, active) ∈ lnth Ns k" using k_in by fastforce
}
then show "(C, active) ∈ ⋂ (lnth Ns ` {k. njm_prec ≤ k ∧ enat k < llength Ns})" by blast
qed
then have "enat njm_prec < llength Ns ∧
(C, active) ∈ ⋂ (lnth Ns ` {k. njm_prec ≤ k ∧ enat k < llength Ns})"
using prec_smaller by blast
then show False
using nj_min_is nj_prec_is Orderings.wellorder_class.not_less_Least njm_prec_njm by blast
qed
then have notin_active_subs_njm_prec: "(C, active) ∉ active_subset (lnth Ns njm_prec)"
unfolding active_subset_def by blast
then show "∃nj. enat (Suc nj) < llength Ns ∧ prems_of ι ! j ∉ active_subset (lnth Ns nj) ∧
(∀k. k > nj ⟶ enat k < llength Ns ⟶ prems_of ι ! j ∈ active_subset (lnth Ns k))"
using c_is njm_prec_all_suc njm_prec_smaller_d by (metis (mono_tags, lifting)
active_subset_def mem_Collect_eq nj_prec_is njm_smaller_D snd_conv)
qed
define nj_set where "nj_set = {nj. (∃j∈{0..<m}. enat (Suc nj) < llength Ns ∧
prems_of ι ! j ∉ active_subset (lnth Ns nj) ∧
(∀k. k > nj ⟶ enat k < llength Ns ⟶ prems_of ι ! j ∈ active_subset (lnth Ns k)))}"
then have nj_not_empty: "nj_set ≠ {}"
proof -
have zero_in: "0 ∈ {0..<m}" using m_pos by simp
then obtain n0 where "enat (Suc n0) < llength Ns" and
"prems_of ι ! 0 ∉ active_subset (lnth Ns n0)" and
"∀k>n0. enat k < llength Ns ⟶ prems_of ι ! 0 ∈ active_subset (lnth Ns k)"
using exist_nj by fast
then have "n0 ∈ nj_set" unfolding nj_set_def using zero_in by blast
then show "nj_set ≠ {}" by auto
qed
have nj_finite: "finite nj_set"
using all_ex_finite_set[OF exist_nj]
by (metis (no_types, lifting) Suc_ile_eq dual_order.strict_implies_order
linorder_neqE_nat nj_set_def)
have "∃n ∈ nj_set. ∀nj ∈ nj_set. nj ≤ n"
using nj_not_empty nj_finite using Max_ge Max_in by blast
then obtain n where n_in: "n ∈ nj_set" and n_bigger: "∀nj ∈ nj_set. nj ≤ n" by blast
then obtain j0 where j0_in: "j0 ∈ {0..<m}" and suc_n_length: "enat (Suc n) < llength Ns" and
j0_notin: "prems_of ι ! j0 ∉ active_subset (lnth Ns n)" and
j0_allin: "(∀k. k > n ⟶ enat k < llength Ns ⟶ prems_of ι ! j0 ∈ active_subset (lnth Ns k))"
unfolding nj_set_def by blast
obtain C0 where C0_is: "prems_of ι ! j0 = (C0, active)" using j0_in
using i_in2 unfolding m_def Inf_from_def active_subset_def
by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv)
then have C0_prems_i: "(C0, active) ∈ set (prems_of ι)" using in_set_conv_nth j0_in m_def by force
have C0_in: "(C0, active) ∈ (lnth Ns (Suc n))"
using C0_is j0_allin suc_n_length by (simp add: active_subset_def)
have C0_notin: "(C0, active) ∉ (lnth Ns n)" using C0_is j0_notin unfolding active_subset_def by simp
have step_n: "lnth Ns n ↝GC lnth Ns (Suc n)"
using deriv chain_lnth_rel n_in unfolding nj_set_def by blast
have "∃N C L M. (lnth Ns n = N ∪ {(C, L)} ∧
lnth Ns (Suc n) = N ∪ {(C, active)} ∪ M ∧ L ≠ active ∧ active_subset M = {} ∧
no_labels.Inf_between (fst ` active_subset N) {C}
⊆ no_labels.Red_I (fst ` (N ∪ {(C, active)} ∪ M)))"
proof -
have proc_or_infer: "(∃N1 N M N2 M'. lnth Ns n = N1 ∧ lnth Ns (Suc n) = N2 ∧ N1 = N ∪ M ∧
N2 = N ∪ M' ∧ M ⊆ Red_F (N ∪ M') ∧ active_subset M' = {}) ∨
(∃N1 N C L N2 M. lnth Ns n = N1 ∧ lnth Ns (Suc n) = N2 ∧ N1 = N ∪ {(C, L)} ∧
N2 = N ∪ {(C, active)} ∪ M ∧ L ≠ active ∧ active_subset M = {} ∧
no_labels.Inf_between (fst ` active_subset N) {C} ⊆
no_labels.Red_I (fst ` (N ∪ {(C, active)} ∪ M)))"
using step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n by blast
show ?thesis
using C0_in C0_notin proc_or_infer j0_in C0_is
by (smt Un_iff active_subset_def mem_Collect_eq snd_conv sup_bot.right_neutral)
qed
then obtain N M L where inf_from_subs:
"no_labels.Inf_between (fst ` active_subset N) {C0}
⊆ no_labels.Red_I (fst ` (N ∪ {(C0, active)} ∪ M))" and
nth_d_is: "lnth Ns n = N ∪ {(C0, L)}" and
suc_nth_d_is: "lnth Ns (Suc n) = N ∪ {(C0, active)} ∪ M" and
l_not_active: "L ≠ active"
using C0_in C0_notin j0_in C0_is using active_subset_def by fastforce
have "j ∈ {0..<m} ⟹ prems_of ι ! j ≠ prems_of ι ! j0 ⟹ prems_of ι ! j ∈ (active_subset N)" for j
proof -
fix j
assume j_in: "j ∈ {0..<m}" and
j_not_j0: "prems_of ι ! j ≠ prems_of ι ! j0"
obtain nj where nj_len: "enat (Suc nj) < llength Ns" and
nj_prems: "prems_of ι ! j ∉ active_subset (lnth Ns nj)" and
nj_greater: "(∀k. k > nj ⟶ enat k < llength Ns ⟶ prems_of ι ! j ∈ active_subset (lnth Ns k))"
using exist_nj j_in by blast
then have "nj ∈ nj_set" unfolding nj_set_def using j_in by blast
moreover have "nj ≠ n"
proof (rule ccontr)
assume "¬ nj ≠ n"
then have "prems_of ι ! j = (C0, active)"
using C0_in C0_notin step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n
by (smt Un_iff nth_d_is suc_nth_d_is l_not_active active_subset_def insertCI insertE lessI
mem_Collect_eq nj_greater nj_prems snd_conv suc_n_length)
then show False using j_not_j0 C0_is by simp
qed
ultimately have "nj < n" using n_bigger by force
then have "prems_of ι ! j ∈ (active_subset (lnth Ns n))"
using nj_greater n_in Suc_ile_eq dual_order.strict_implies_order unfolding nj_set_def by blast
then show "prems_of ι ! j ∈ (active_subset N)"
using nth_d_is l_not_active unfolding active_subset_def by force
qed
then have "set (prems_of ι) ⊆ active_subset N ∪ {(C0, active)}"
using C0_prems_i C0_is m_def
by (metis Un_iff atLeast0LessThan in_set_conv_nth insertCI lessThan_iff subrelI)
moreover have "¬ (set (prems_of ι) ⊆ active_subset N - {(C0, active)})" using C0_prems_i by blast
ultimately have "ι ∈ Inf_between (active_subset N) {(C0, active)}"
using i_in_inf_fl unfolding Inf_between_def Inf_from_def by blast
then have "to_F ι ∈ no_labels.Inf_between (fst ` active_subset N) {C0}"
unfolding to_F_def Inf_between_def Inf_from_def
no_labels.Inf_between_def no_labels.Inf_from_def using Inf_FL_to_Inf_F
by force
then have "to_F ι ∈ no_labels.Red_I (fst ` (lnth Ns (Suc n)))"
using suc_nth_d_is inf_from_subs by fastforce
then have "∀q ∈ Q. (𝒢_I_q q (to_F ι) ≠ None ∧
the (𝒢_I_q q (to_F ι)) ⊆ Red_I_q q (⋃ (𝒢_F_q q ` fst ` lnth Ns (Suc n))))
∨ (𝒢_I_q q (to_F ι) = None ∧
𝒢_F_q q (concl_of (to_F ι)) ⊆ ⋃ (𝒢_F_q q ` fst ` lnth Ns (Suc n)) ∪
Red_F_q q (⋃ (𝒢_F_q q ` fst ` lnth Ns (Suc n))))"
unfolding to_F_def no_labels.Red_I_def no_labels.Red_I_𝒢_q_def by blast
then have "ι ∈ Red_I_𝒢 (lnth Ns (Suc n))"
using i_in_inf_fl unfolding Red_I_𝒢_def Red_I_𝒢_q_def by (simp add: to_F_def)
then show "ι ∈ Sup_llist (lmap Red_I_𝒢 Ns)"
unfolding Sup_llist_def using suc_n_length by auto
qed
theorem gc_complete_Liminf:
assumes
deriv: "chain (↝GC) Ns" and
init_state: "active_subset (lhd Ns) = {}" and
final_state: "passive_subset (Liminf_llist Ns) = {}" and
b_in: "B ∈ Bot_F" and
bot_entailed: "no_labels.entails_𝒢 (fst ` lhd Ns) {B}"
shows "∃BL ∈ Bot_FL. BL ∈ Liminf_llist Ns"
proof -
note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
have labeled_b_in: "(B, active) ∈ Bot_FL" using b_in by simp
have labeled_bot_entailed: "entails_𝒢_L (lhd Ns) {(B, active)}"
using labeled_entailment_lifting bot_entailed lhd_is by fastforce
have fair: "fair Ns" using gc_fair[OF deriv init_state final_state] .
then show ?thesis
using dynamically_complete_Liminf[OF labeled_b_in gc_to_red[OF deriv] fair
labeled_bot_entailed]
by blast
qed
theorem gc_complete:
assumes
deriv: "chain (↝GC) Ns" and
init_state: "active_subset (lhd Ns) = {}" and
final_state: "passive_subset (Liminf_llist Ns) = {}" and
b_in: "B ∈ Bot_F" and
bot_entailed: "no_labels.entails_𝒢 (fst ` lhd Ns) {B}"
shows "∃i. enat i < llength Ns ∧ (∃BL ∈ Bot_FL. BL ∈ lnth Ns i)"
proof -
note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
have "∃BL∈Bot_FL. BL ∈ Liminf_llist Ns"
using assms by (rule gc_complete_Liminf)
then show ?thesis
unfolding Liminf_llist_def by auto
qed
end
subsection ‹Lazy Given Clause Procedure›
locale lazy_given_clause = given_clause_basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q
Red_F_q 𝒢_F_q 𝒢_I_q Equiv_F Prec_F Prec_L active
for
Bot_F :: "'f set" and
Inf_F :: "'f inference set" and
Bot_G :: "'g set" and
Q :: "'q set" and
entails_q :: "'q ⇒ 'g set ⇒ 'g set ⇒ bool" and
Inf_G_q :: ‹'q ⇒ 'g inference set› and
Red_I_q :: "'q ⇒ 'g set ⇒ 'g inference set" and
Red_F_q :: "'q ⇒ 'g set ⇒ 'g set" and
𝒢_F_q :: "'q ⇒ 'f ⇒ 'g set" and
𝒢_I_q :: "'q ⇒ 'f inference ⇒ 'g inference set option" and
Equiv_F :: "'f ⇒ 'f ⇒ bool" (infix ‹≐› 50) and
Prec_F :: "'f ⇒ 'f ⇒ bool" (infix ‹≺⋅› 50) and
Prec_L :: "'l ⇒ 'l ⇒ bool" (infix ‹⊏L› 50) and
active :: 'l
begin
inductive step :: "'f inference set × ('f × 'l) set ⇒
'f inference set × ('f × 'l) set ⇒ bool" (infix ‹↝LGC› 50) where
process: "N1 = N ∪ M ⟹ N2 = N ∪ M' ⟹ M ⊆ Red_F (N ∪ M') ⟹
active_subset M' = {} ⟹ (T, N1) ↝LGC (T, N2)" |
schedule_infer: "T2 = T1 ∪ T' ⟹ N1 = N ∪ {(C, L)} ⟹ N2 = N ∪ {(C, active)} ⟹
L ≠ active ⟹ T' = no_labels.Inf_between (fst ` active_subset N) {C} ⟹
(T1, N1) ↝LGC (T2, N2)" |
compute_infer: "T1 = T2 ∪ {ι} ⟹ N2 = N1 ∪ M ⟹ active_subset M = {} ⟹
ι ∈ no_labels.Red_I (fst ` (N1 ∪ M)) ⟹ (T1, N1) ↝LGC (T2, N2)" |
delete_orphan_infers: "T1 = T2 ∪ T' ⟹
T' ∩ no_labels.Inf_from (fst ` active_subset N) = {} ⟹ (T1, N) ↝LGC (T2, N)"
lemma premise_free_inf_always_from: "ι ∈ Inf_F ⟹ prems_of ι = [] ⟹ ι ∈ no_labels.Inf_from N"
unfolding no_labels.Inf_from_def by simp
lemma one_step_equiv: "(T1, N1) ↝LGC (T2, N2) ⟹ N1 ⊳L N2"
proof (cases "(T1, N1)" "(T2, N2)" rule: step.cases)
show "(T1, N1) ↝LGC (T2, N2) ⟹ (T1, N1) ↝LGC (T2, N2)" by blast
next
fix N M M'
assume
n1_is: "N1 = N ∪ M" and
n2_is: "N2 = N ∪ M'" and
m_red: "M ⊆ Red_F (N ∪ M')"
have "N1 - N2 ⊆ Red_F N2"
using n1_is n2_is m_red by auto
then show "N1 ⊳L N2"
unfolding derive.simps by blast
next
fix N C L M
assume
n1_is: "N1 = N ∪ {(C, L)}" and
not_active: "L ≠ active" and
n2_is: "N2 = N ∪ {(C, active)}"
have "(C, active) ∈ N2" using n2_is by auto
moreover have "C ≼⋅ C" by (metis equivp_def equiv_equiv_F)
moreover have "active ⊏L L" using active_minimal[OF not_active] .
ultimately have "{(C, L)} ⊆ Red_F N2"
using red_labeled_clauses by blast
then have "N1 - N2 ⊆ Red_F N2"
using std_Red_F_eq using n1_is n2_is by blast
then show "N1 ⊳L N2"
unfolding derive.simps by blast
next
fix M
assume
n2_is: "N2 = N1 ∪ M"
have "N1 - N2 ⊆ Red_F N2"
using n2_is by blast
then show "N1 ⊳L N2"
unfolding derive.simps by blast
next
assume n2_is: "N2 = N1"
have "N1 - N2 ⊆ Red_F N2"
using n2_is by blast
then show "N1 ⊳L N2"
unfolding derive.simps by blast
qed
lemma lgc_to_red: "chain (↝LGC) Ns ⟹ chain (⊳L) (lmap snd Ns)"
using one_step_equiv Lazy_List_Chain.chain_mono by (smt chain_lmap prod.collapse)
lemma lgc_fair:
assumes
deriv: "chain (↝LGC) Ns" and
init_state: "active_subset (snd (lhd Ns)) = {}" and
final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and
no_prems_init: "∀ι ∈ Inf_F. prems_of ι = [] ⟶ ι ∈ fst (lhd Ns)" and
final_schedule: "Liminf_llist (lmap fst Ns) = {}"
shows "fair (lmap snd Ns)"
unfolding fair_def
proof
fix ι
assume i_in: "ι ∈ Inf_from (Liminf_llist (lmap snd Ns))"
note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]]
have i_in_inf_fl: "ι ∈ Inf_FL" using i_in unfolding Inf_from_def by blast
have "Liminf_llist (lmap snd Ns) = active_subset (Liminf_llist (lmap snd Ns))"
using final_state unfolding passive_subset_def active_subset_def by blast
then have i_in2: "ι ∈ Inf_from (active_subset (Liminf_llist (lmap snd Ns)))"
using i_in by simp
define m where "m = length (prems_of ι)"
then have m_def_F: "m = length (prems_of (to_F ι))" unfolding to_F_def by simp
have i_in_F: "to_F ι ∈ Inf_F"
using i_in Inf_FL_to_Inf_F unfolding Inf_from_def to_F_def by blast
have exist_nj: "∀j ∈ {0..<m}. (∃nj. enat (Suc nj) < llength Ns ∧
prems_of ι ! j ∉ active_subset (snd (lnth Ns nj)) ∧
(∀k. k > nj ⟶ enat k < llength Ns ⟶ prems_of ι ! j ∈ active_subset (snd (lnth Ns k))))"
proof clarify
fix j
assume j_in: "j ∈ {0..<m}"
then obtain C where c_is: "(C, active) = prems_of ι ! j"
using i_in2 unfolding m_def Inf_from_def active_subset_def
by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv)
then have "(C, active) ∈ Liminf_llist (lmap snd Ns)"
using j_in i_in unfolding m_def Inf_from_def by force
then obtain nj where nj_is: "enat nj < llength Ns" and
c_in2: "(C, active) ∈ ⋂ (snd ` (lnth Ns ` {k. nj ≤ k ∧ enat k < llength Ns}))"
unfolding Liminf_llist_def using init_state by fastforce
then have c_in3: "∀k. k ≥ nj ⟶ enat k < llength Ns ⟶ (C, active) ∈ snd (lnth Ns k)" by blast
have nj_pos: "nj > 0" using init_state c_in2 nj_is unfolding active_subset_def lhd_is by fastforce
obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength Ns ∧
(C, active) ∈ ⋂ (snd ` (lnth Ns ` {k. nj ≤ k ∧ enat k < llength Ns})))" by blast
then have in_allk: "∀k. k ≥ nj_min ⟶ enat k < llength Ns ⟶ (C, active) ∈ snd (lnth Ns k)"
using c_in3 nj_is c_in2 INT_E LeastI_ex
[of "λn. enat n < llength Ns
∧ (C, active) ∈ ⋂ (snd ` lnth Ns ` {na. n ≤ na ∧ enat na < llength Ns})"]
by blast
have njm_smaller_D: "enat nj_min < llength Ns"
using nj_min_is
by (smt LeastI_ex ‹⋀thesis. (⋀nj. ⟦enat nj < llength Ns;
(C, active) ∈ ⋂ (snd ` (lnth Ns ` {k. nj ≤ k ∧ enat k < llength Ns}))⟧ ⟹ thesis) ⟹ thesis›)
have "nj_min > 0"
using nj_is c_in2 nj_pos nj_min_is lhd_is
by (metis (mono_tags, lifting) active_subset_def emptyE in_allk init_state mem_Collect_eq
not_less snd_conv zero_enat_def chain_length_pos[OF deriv])
then obtain njm_prec where nj_prec_is: "Suc njm_prec = nj_min" using gr0_conv_Suc by auto
then have njm_prec_njm: "njm_prec < nj_min" by blast
then have njm_prec_njm_enat: "enat njm_prec < enat nj_min" by simp
have njm_prec_smaller_d: "njm_prec < llength Ns"
by (rule less_trans[OF njm_prec_njm_enat njm_smaller_D])
have njm_prec_all_suc: "∀k>njm_prec. enat k < llength Ns ⟶ (C, active) ∈ snd (lnth Ns k)"
using nj_prec_is in_allk by simp
have notin_njm_prec: "(C, active) ∉ snd (lnth Ns njm_prec)"
proof (rule ccontr)
assume "¬ (C, active) ∉ snd (lnth Ns njm_prec)"
then have absurd_hyp: "(C, active) ∈ snd (lnth Ns njm_prec)" by simp
have prec_smaller: "enat njm_prec < llength Ns" using nj_min_is nj_prec_is
by (smt LeastI_ex Suc_leD ‹⋀thesis. (⋀nj. ⟦enat nj < llength Ns;
(C, active) ∈ ⋂ (snd ` (lnth Ns ` {k. nj ≤ k ∧ enat k < llength Ns}))⟧ ⟹ thesis) ⟹ thesis›
enat_ord_simps(1) le_eq_less_or_eq le_less_trans)
have "(C, active) ∈ ⋂ (snd ` (lnth Ns ` {k. njm_prec ≤ k ∧ enat k < llength Ns}))"
proof -
{
fix k
assume k_in: "njm_prec ≤ k ∧ enat k < llength Ns"
have "k = njm_prec ⟹ (C, active) ∈ snd (lnth Ns k)" using absurd_hyp by simp
moreover have "njm_prec < k ⟹ (C, active) ∈ snd (lnth Ns k)"
using nj_prec_is in_allk k_in by simp
ultimately have "(C, active) ∈ snd (lnth Ns k)" using k_in by fastforce
}
then show "(C, active) ∈ ⋂ (snd ` (lnth Ns ` {k. njm_prec ≤ k ∧ enat k < llength Ns}))"
by blast
qed
then have "enat njm_prec < llength Ns ∧
(C, active) ∈ ⋂ (snd ` (lnth Ns ` {k. njm_prec ≤ k ∧ enat k < llength Ns}))"
using prec_smaller by blast
then show False
using nj_min_is nj_prec_is Orderings.wellorder_class.not_less_Least njm_prec_njm by blast
qed
then have notin_active_subs_njm_prec: "(C, active) ∉ active_subset (snd (lnth Ns njm_prec))"
unfolding active_subset_def by blast
then show "∃nj. enat (Suc nj) < llength Ns ∧ prems_of ι ! j ∉ active_subset (snd (lnth Ns nj)) ∧
(∀k. k > nj ⟶ enat k < llength Ns ⟶ prems_of ι ! j ∈ active_subset (snd (lnth Ns k)))"
using c_is njm_prec_all_suc njm_prec_smaller_d by (metis (mono_tags, lifting)
active_subset_def mem_Collect_eq nj_prec_is njm_smaller_D snd_conv)
qed
define nj_set where "nj_set = {nj. (∃j∈{0..<m}. enat (Suc nj) < llength Ns ∧
prems_of ι ! j ∉ active_subset (snd (lnth Ns nj)) ∧
(∀k. k > nj ⟶ enat k < llength Ns ⟶ prems_of ι ! j ∈ active_subset (snd (lnth Ns k))))}"
{
assume m_null: "m = 0"
then have "enat 0 < llength Ns ∧ to_F ι ∈ fst (lhd Ns)"
using no_prems_init i_in_F m_def_F zero_enat_def chain_length_pos[OF deriv] by auto
then have "∃n. enat n < llength Ns ∧ to_F ι ∈ fst (lnth Ns n)"
unfolding lhd_is by blast
}
moreover {
assume m_pos: "m > 0"
have nj_not_empty: "nj_set ≠ {}"
proof -
have zero_in: "0 ∈ {0..<m}" using m_pos by simp
then obtain n0 where "enat (Suc n0) < llength Ns" and
"prems_of ι ! 0 ∉ active_subset (snd (lnth Ns n0))" and
"∀k>n0. enat k < llength Ns ⟶ prems_of ι ! 0 ∈ active_subset (snd (lnth Ns k))"
using exist_nj by fast
then have "n0 ∈ nj_set" unfolding nj_set_def using zero_in by blast
then show "nj_set ≠ {}" by auto
qed
have nj_finite: "finite nj_set"
using all_ex_finite_set[OF exist_nj] by (metis (no_types, lifting) Suc_ile_eq
dual_order.strict_implies_order linorder_neqE_nat nj_set_def)
have "∃n ∈ nj_set. ∀nj ∈ nj_set. nj ≤ n"
using nj_not_empty nj_finite using Max_ge Max_in by blast
then obtain n where n_in: "n ∈ nj_set" and n_bigger: "∀nj ∈ nj_set. nj ≤ n" by blast
then obtain j0 where j0_in: "j0 ∈ {0..<m}" and suc_n_length: "enat (Suc n) < llength Ns" and
j0_notin: "prems_of ι ! j0 ∉ active_subset (snd (lnth Ns n))" and
j0_allin: "(∀k. k > n ⟶ enat k < llength Ns ⟶
prems_of ι ! j0 ∈ active_subset (snd (lnth Ns k)))"
unfolding nj_set_def by blast
obtain C0 where C0_is: "prems_of ι ! j0 = (C0, active)"
using j0_in i_in2 unfolding m_def Inf_from_def active_subset_def
by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv)
then have C0_prems_i: "(C0, active) ∈ set (prems_of ι)" using in_set_conv_nth j0_in m_def by force
have C0_in: "(C0, active) ∈ (snd (lnth Ns (Suc n)))"
using C0_is j0_allin suc_n_length by (simp add: active_subset_def)
have C0_notin: "(C0, active) ∉ (snd (lnth Ns n))"
using C0_is j0_notin unfolding active_subset_def by simp
have step_n: "lnth Ns n ↝LGC lnth Ns (Suc n)"
using deriv chain_lnth_rel n_in unfolding nj_set_def by blast
have is_scheduled: "∃T2 T1 T' N1 N C L N2. lnth Ns n = (T1, N1) ∧ lnth Ns (Suc n) = (T2, N2) ∧
T2 = T1 ∪ T' ∧ N1 = N ∪ {(C, L)} ∧ N2 = N ∪ {(C, active)} ∧ L ≠ active ∧
T' = no_labels.Inf_between (fst ` active_subset N) {C}"
using step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n C0_in C0_notin
unfolding active_subset_def by fastforce
then obtain T2 T1 T' N1 N L N2 where nth_d_is: "lnth Ns n = (T1, N1)" and
suc_nth_d_is: "lnth Ns (Suc n) = (T2, N2)" and t2_is: "T2 = T1 ∪ T'" and
n1_is: "N1 = N ∪ {(C0, L)}" "N2 = N ∪ {(C0, active)}" and
l_not_active: "L ≠ active" and
tp_is: "T' = no_labels.Inf_between (fst ` active_subset N) {C0}"
using C0_in C0_notin j0_in C0_is using active_subset_def by fastforce
have "j ∈ {0..<m} ⟹ prems_of ι ! j ≠ prems_of ι ! j0 ⟹ prems_of ι ! j ∈ (active_subset N)"
for j
proof -
fix j
assume j_in: "j ∈ {0..<m}" and
j_not_j0: "prems_of ι ! j ≠ prems_of ι ! j0"
obtain nj where nj_len: "enat (Suc nj) < llength Ns" and
nj_prems: "prems_of ι ! j ∉ active_subset (snd (lnth Ns nj))" and
nj_greater: "(∀k. k > nj ⟶ enat k < llength Ns ⟶
prems_of ι ! j ∈ active_subset (snd (lnth Ns k)))"
using exist_nj j_in by blast
then have "nj ∈ nj_set" unfolding nj_set_def using j_in by blast
moreover have "nj ≠ n"
proof (rule ccontr)
assume "¬ nj ≠ n"
then have "prems_of ι ! j = (C0, active)"
using C0_in C0_notin step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n
active_subset_def is_scheduled nj_greater nj_prems suc_n_length by auto
then show False using j_not_j0 C0_is by simp
qed
ultimately have "nj < n" using n_bigger by force
then have "prems_of ι ! j ∈ (active_subset (snd (lnth Ns n)))"
using nj_greater n_in Suc_ile_eq dual_order.strict_implies_order
unfolding nj_set_def by blast
then show "prems_of ι ! j ∈ (active_subset N)"
using nth_d_is l_not_active n1_is unfolding active_subset_def by force
qed
then have prems_i_active: "set (prems_of ι) ⊆ active_subset N ∪ {(C0, active)}"
using C0_prems_i C0_is m_def
by (metis Un_iff atLeast0LessThan in_set_conv_nth insertCI lessThan_iff subrelI)
moreover have "¬ (set (prems_of ι) ⊆ active_subset N - {(C0, active)})" using C0_prems_i by blast
ultimately have "ι ∈ Inf_between (active_subset N) {(C0, active)}"
using i_in_inf_fl prems_i_active unfolding Inf_between_def Inf_from_def by blast
then have "to_F ι ∈ no_labels.Inf_between (fst ` active_subset N) {C0}"
unfolding to_F_def Inf_between_def Inf_from_def
no_labels.Inf_between_def no_labels.Inf_from_def
using Inf_FL_to_Inf_F by force
then have i_in_t2: "to_F ι ∈ T2" using tp_is t2_is by simp
have "j ∈ {0..<m} ⟹ (∀k. k > n ⟶ enat k < llength Ns ⟶
prems_of ι ! j ∈ active_subset (snd (lnth Ns k)))" for j
proof (cases "j = j0")
case True
assume "j = j0"
then show "(∀k. k > n ⟶ enat k < llength Ns ⟶
prems_of ι ! j ∈ active_subset (snd (lnth Ns k)))" using j0_allin by simp
next
case False
assume j_in: "j ∈ {0..<m}" and
"j ≠ j0"
obtain nj where nj_len: "enat (Suc nj) < llength Ns" and
nj_prems: "prems_of ι ! j ∉ active_subset (snd (lnth Ns nj))" and
nj_greater: "(∀k. k > nj ⟶ enat k < llength Ns ⟶
prems_of ι ! j ∈ active_subset (snd (lnth Ns k)))"
using exist_nj j_in by blast
then have "nj ∈ nj_set" unfolding nj_set_def using j_in by blast
then show "(∀k. k > n ⟶ enat k < llength Ns ⟶
prems_of ι ! j ∈ active_subset (snd (lnth Ns k)))"
using nj_greater n_bigger by auto
qed
then have allj_allk: "(∀c∈ set (prems_of ι). (∀k. k > n ⟶ enat k < llength Ns ⟶
c ∈ active_subset (snd (lnth Ns k))))"
using m_def by (metis atLeast0LessThan in_set_conv_nth lessThan_iff)
have "∀c∈ set (prems_of ι). snd c = active"
using prems_i_active unfolding active_subset_def by auto
then have ex_n_i_in: "∃n. enat (Suc n) < llength Ns ∧ to_F ι ∈ fst (lnth Ns (Suc n)) ∧
(∀c∈ set (prems_of ι). snd c = active) ∧
(∀c∈ set (prems_of ι). (∀k. k > n ⟶ enat k < llength Ns ⟶
c ∈ active_subset (snd (lnth Ns k))))"
using allj_allk i_in_t2 suc_nth_d_is fstI n_in nj_set_def
by auto
then have "∃n. enat n < llength Ns ∧ to_F ι ∈ fst (lnth Ns n) ∧
(∀c∈ set (prems_of ι). snd c = active) ∧ (∀c∈ set (prems_of ι). (∀k. k ≥ n ⟶
enat k < llength Ns ⟶ c ∈ active_subset (snd (lnth Ns k))))"
by auto
}
ultimately obtain n T2 N2 where i_in_suc_n: "to_F ι ∈ fst (lnth Ns n)" and
all_prems_active_after: "m > 0 ⟹ (∀c∈ set (prems_of ι). (∀k. k ≥ n ⟶ enat k < llength Ns ⟶
c ∈ active_subset (snd (lnth Ns k))))" and
suc_n_length: "enat n < llength Ns" and suc_nth_d_is: "lnth Ns n = (T2, N2)"
by (metis less_antisym old.prod.exhaust zero_less_Suc)
then have i_in_t2: "to_F ι ∈ T2" by simp
have "∃p≥n. enat (Suc p) < llength Ns ∧ to_F ι ∈ (fst (lnth Ns p)) ∧ to_F ι ∉ (fst (lnth Ns (Suc p)))"
proof (rule ccontr)
assume
contra: "¬ (∃p≥n. enat (Suc p) < llength Ns ∧ to_F ι ∈ (fst (lnth Ns p)) ∧
to_F ι ∉ (fst (lnth Ns (Suc p))))"
then have i_in_suc: "p0 ≥ n ⟹ enat (Suc p0) < llength Ns ⟹ to_F ι ∈ (fst (lnth Ns p0)) ⟹
to_F ι ∈ (fst (lnth Ns (Suc p0)))" for p0
by blast
have "p0 ≥ n ⟹ enat p0 < llength Ns ⟹ to_F ι ∈ (fst (lnth Ns p0))" for p0
proof (induction rule: nat_induct_at_least)
case base
then show ?case using i_in_t2 suc_nth_d_is
by simp
next
case (Suc p0)
assume p_bigger_n: "n ≤ p0" and
induct_hyp: "enat p0 < llength Ns ⟹ to_F ι ∈ fst (lnth Ns p0)" and
sucsuc_smaller_d: "enat (Suc p0) < llength Ns"
have suc_p_bigger_n: "n ≤ p0" using p_bigger_n by simp
have suc_smaller_d: "enat p0 < llength Ns"
using sucsuc_smaller_d Suc_ile_eq dual_order.strict_implies_order by blast
then have "to_F ι ∈ fst (lnth Ns p0)" using induct_hyp by blast
then show ?case using i_in_suc[OF suc_p_bigger_n sucsuc_smaller_d] by blast
qed
then have i_in_all_bigger_n: "∀j. j ≥ n ∧ enat j < llength Ns ⟶ to_F ι ∈ (fst (lnth Ns j))"
by presburger
have "llength (lmap fst Ns) = llength Ns" by force
then have "to_F ι ∈ ⋂ (lnth (lmap fst Ns) ` {j. n ≤ j ∧ enat j < llength (lmap fst Ns)})"
using i_in_all_bigger_n using Suc_le_D by auto
then have "to_F ι ∈ Liminf_llist (lmap fst Ns)"
unfolding Liminf_llist_def using suc_n_length by auto
then show False using final_schedule by fast
qed
then obtain p where p_greater_n: "p ≥ n" and p_smaller_d: "enat (Suc p) < llength Ns" and
i_in_p: "to_F ι ∈ (fst (lnth Ns p))" and i_notin_suc_p: "to_F ι ∉ (fst (lnth Ns (Suc p)))"
by blast
have p_neq_n: "Suc p ≠ n" using i_notin_suc_p i_in_suc_n by blast
have step_p: "lnth Ns p ↝LGC lnth Ns (Suc p)" using deriv p_smaller_d chain_lnth_rel by blast
then have "∃T1 T2 ι N2 N1 M. lnth Ns p = (T1, N1) ∧ lnth Ns (Suc p) = (T2, N2) ∧
T1 = T2 ∪ {ι} ∧ N2 = N1 ∪ M ∧ active_subset M = {} ∧
ι ∈ no_labels.Red_I_𝒢 (fst ` (N1 ∪ M))"
proof -
have ci_or_do: "(∃T1 T2 ι N2 N1 M. lnth Ns p = (T1, N1) ∧ lnth Ns (Suc p) = (T2, N2) ∧
T1 = T2 ∪ {ι} ∧ N2 = N1 ∪ M ∧ active_subset M = {} ∧
ι ∈ no_labels.Red_I_𝒢 (fst ` (N1 ∪ M))) ∨
(∃T1 T2 T' N. lnth Ns p = (T1, N) ∧ lnth Ns (Suc p) = (T2, N) ∧
T1 = T2 ∪ T' ∧ T' ∩ no_labels.Inf_from (fst ` active_subset N) = {})"
using step.simps[of "lnth Ns p" "lnth Ns (Suc p)"] step_p i_in_p i_notin_suc_p by fastforce
then have p_greater_n_strict: "n < Suc p"
using suc_nth_d_is p_greater_n i_in_t2 i_notin_suc_p le_eq_less_or_eq by force
have "m > 0 ⟹ j ∈ {0..<m} ⟹ prems_of (to_F ι) ! j ∈ fst ` active_subset (snd (lnth Ns p))"
for j
proof -
fix j
assume
m_pos: "m > 0" and
j_in: "j ∈ {0..<m}"
then have "prems_of ι ! j ∈ (active_subset (snd (lnth Ns p)))"
using all_prems_active_after[OF m_pos] p_smaller_d m_def p_greater_n p_neq_n
by (meson Suc_ile_eq atLeastLessThan_iff dual_order.strict_implies_order nth_mem
p_greater_n_strict)
then have "fst (prems_of ι ! j) ∈ fst ` active_subset (snd (lnth Ns p))"
by blast
then show "prems_of (to_F ι) ! j ∈ fst ` active_subset (snd (lnth Ns p))"
unfolding to_F_def using j_in m_def by simp
qed
then have prems_i_active_p: "m > 0 ⟹
to_F ι ∈ no_labels.Inf_from (fst ` active_subset (snd (lnth Ns p)))"
using i_in_F unfolding no_labels.Inf_from_def
by (smt atLeast0LessThan in_set_conv_nth lessThan_iff m_def_F mem_Collect_eq subsetI)
have "m = 0 ⟹ (∃T1 T2 ι N2 N1 M. lnth Ns p = (T1, N1) ∧ lnth Ns (Suc p) = (T2, N2) ∧
T1 = T2 ∪ {ι} ∧ N2 = N1 ∪ M ∧ active_subset M = {} ∧
ι ∈ no_labels.Red_I_𝒢 (fst ` (N1 ∪ M)))"
using ci_or_do premise_free_inf_always_from[of "to_F ι" "fst ` active_subset _", OF i_in_F]
m_def i_in_p i_notin_suc_p m_def_F by auto
then show "(∃T1 T2 ι N2 N1 M. lnth Ns p = (T1, N1) ∧ lnth Ns (Suc p) = (T2, N2) ∧
T1 = T2 ∪ {ι} ∧ N2 = N1 ∪ M ∧ active_subset M = {} ∧
ι ∈ no_labels.Red_I_𝒢 (fst ` (N1 ∪ M)))"
using ci_or_do i_in_p i_notin_suc_p prems_i_active_p unfolding active_subset_def by force
qed
then obtain T1p T2p N1p N2p Mp where "lnth Ns p = (T1p, N1p)" and
suc_p_is: "lnth Ns (Suc p) = (T2p, N2p)" and "T1p = T2p ∪ {to_F ι}" and "T2p ∩ {to_F ι} = {}" and
n2p_is: "N2p = N1p ∪ Mp"and "active_subset Mp = {}" and
i_in_red_inf: "to_F ι ∈ no_labels.Red_I_𝒢
(fst ` (N1p ∪ Mp))"
using i_in_p i_notin_suc_p by fastforce
have "to_F ι ∈ no_labels.Red_I (fst ` (snd (lnth Ns (Suc p))))"
using i_in_red_inf suc_p_is n2p_is by fastforce
then have "∀q ∈ Q. (𝒢_I_q q (to_F ι) ≠ None ∧
the (𝒢_I_q q (to_F ι)) ⊆ Red_I_q q (⋃ (𝒢_F_q q ` fst ` snd (lnth Ns (Suc p)))))
∨ (𝒢_I_q q (to_F ι) = None ∧
𝒢_F_q q (concl_of (to_F ι)) ⊆ ⋃ (𝒢_F_q q ` fst ` snd (lnth Ns (Suc p))) ∪
Red_F_q q (⋃ (𝒢_F_q q ` fst ` snd (lnth Ns (Suc p)))))"
unfolding to_F_def no_labels.Red_I_def no_labels.Red_I_𝒢_q_def by blast
then have "ι ∈ Red_I_𝒢 (snd (lnth Ns (Suc p)))"
using i_in_inf_fl unfolding Red_I_𝒢_def Red_I_𝒢_q_def by (simp add: to_F_def)
then show "ι ∈ Sup_llist (lmap Red_I_𝒢 (lmap snd Ns))"
unfolding Sup_llist_def using suc_n_length p_smaller_d by auto
qed
theorem lgc_complete_Liminf:
assumes
deriv: "chain (↝LGC) Ns" and
init_state: "active_subset (snd (lhd Ns)) = {}" and
final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and
no_prems_init: "∀ι ∈ Inf_F. prems_of ι = [] ⟶ ι ∈ fst (lhd Ns)" and
final_schedule: "Liminf_llist (lmap fst Ns) = {}" and
b_in: "B ∈ Bot_F" and
bot_entailed: "no_labels.entails_𝒢 (fst ` snd (lhd Ns)) {B}"
shows "∃BL ∈ Bot_FL. BL ∈ Liminf_llist (lmap snd Ns)"
proof -
have labeled_b_in: "(B, active) ∈ Bot_FL" using b_in by simp
have simp_snd_lmap: "lhd (lmap snd Ns) = snd (lhd Ns)"
by (rule llist.map_sel(1)[OF chain_not_lnull[OF deriv]])
have labeled_bot_entailed: "entails_𝒢_L (snd (lhd Ns)) {(B, active)}"
using labeled_entailment_lifting bot_entailed by fastforce
have "fair (lmap snd Ns)"
using lgc_fair[OF deriv init_state final_state no_prems_init final_schedule] .
then show ?thesis
using dynamically_complete_Liminf labeled_b_in lgc_to_red[OF deriv]
labeled_bot_entailed simp_snd_lmap std_Red_I_eq
by presburger
qed
theorem lgc_complete:
assumes
deriv: "chain (↝LGC) Ns" and
init_state: "active_subset (snd (lhd Ns)) = {}" and
final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and
no_prems_init: "∀ι ∈ Inf_F. prems_of ι = [] ⟶ ι ∈ fst (lhd Ns)" and
final_schedule: "Liminf_llist (lmap fst Ns) = {}" and
b_in: "B ∈ Bot_F" and
bot_entailed: "no_labels.entails_𝒢 (fst ` snd (lhd Ns)) {B}"
shows "∃i. enat i < llength Ns ∧ (∃BL ∈ Bot_FL. BL ∈ snd (lnth Ns i))"
proof -
have "∃BL∈Bot_FL. BL ∈ Liminf_llist (lmap snd Ns)"
using assms by (rule lgc_complete_Liminf)
then show ?thesis
unfolding Liminf_llist_def by auto
qed
end
end