diff --git a/thys/Saturation_Framework/Prover_Architectures.thy b/thys/Saturation_Framework/Prover_Architectures.thy --- a/thys/Saturation_Framework/Prover_Architectures.thy +++ b/thys/Saturation_Framework/Prover_Architectures.thy @@ -1,1267 +1,1263 @@ (* Title: Prover Architectures of the Saturation Framework * Author: Sophie Tourret , 2019-2020 *) section \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 Prover_Architectures imports Lambda_Free_RPOs.Lambda_Free_Util Labeled_Lifting_to_Non_Ground_Calculi begin subsection \Basis of the Prover Architectures\ locale Prover_Architecture_Basis = labeled_lifting_with_red_crit_family Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_Inf_q Red_F_q \_F_q \_Inf_q Inf_FL 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_Inf_q :: "'q \ 'g set \ 'g inference set" and Red_F_q :: "'q \ 'g set \ 'g set" and \_F_q :: "'q \ 'f \ 'g set" and \_Inf_q :: "'q \ 'f inference \ 'g inference set option" and Inf_FL :: \('f \ 'l) inference set\ + 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) 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 static_ref_comp: "static_refutational_complete_calculus Bot_F Inf_F (\\) no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_F_Q" begin 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_on (\) UNIV" 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_on (\) UNIV" unfolding transp_on_def Prec_FL_def proof (simp, intro allI impI) fix C1 l1 C2 l2 C3 l3 assume trans_hyp: "(C1 \\ C2 \ C1 \ C2 \ l1 \l l2) \ (C2 \\ C3 \ C2 \ C3 \ l2 \l l3)" have "C1 \\ C2 \ C2 \ C3 \ C1 \\ C3" using compat_equiv_prec by (metis equiv_equiv_F equivp_def) moreover have "C1 \ C2 \ C2 \\ C3 \ C1 \\ C3" using compat_equiv_prec by (metis equiv_equiv_F equivp_def) moreover have "l1 \l l2 \ l2 \l l3 \ l1 \l l3" using wf_prec_l unfolding minimal_element_def po_on_def transp_on_def by (meson UNIV_I) moreover have "C1 \ C2 \ C2 \ C3 \ C1 \ C3" using equiv_equiv_F by (meson equivp_transp) ultimately show "C1 \\ C3 \ C1 \ C3 \ l1 \l l3" using trans_hyp using 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 lemma labeled_static_ref_comp: "static_refutational_complete_calculus Bot_FL Inf_FL (\\L) with_labels.Red_Inf_Q with_labels.Red_F_Q" using labeled_static_ref[OF static_ref_comp] . lemma standard_labeled_lifting_family: assumes q_in: "q \ Q" shows "lifting_with_wf_ordering_family Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) (Red_Inf_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q) (\g. Prec_FL)" proof - have "lifting_with_wf_ordering_family Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) (Red_Inf_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q) (\g. Labeled_Empty_Order)" using ord_fam_lifted_q[OF q_in] . then have "standard_lifting Bot_FL Inf_FL Bot_G (Inf_G_q q) (entails_q q) (Red_Inf_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q)" using lifted_q[OF q_in] by blast then show "lifting_with_wf_ordering_family Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) (Red_Inf_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q) (\g. Prec_FL)" using wf_prec_FL by (simp add: lifting_with_wf_ordering_family.intro lifting_with_wf_ordering_family_axioms.intro) qed sublocale labeled_ord_red_crit_fam: standard_lifting_with_red_crit_family Inf_FL Bot_G Q Inf_G_q entails_q Red_Inf_q Red_F_q Bot_FL \_F_L_q \_Inf_L_q "\g. Prec_FL" using standard_labeled_lifting_family no_labels.Ground_family.calculus_family_with_red_crit_family_axioms by (simp add: standard_lifting_with_red_crit_family.intro standard_lifting_with_red_crit_family_axioms.intro) lemma entail_equiv: "labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.entails_Q N1 N2 \ (N1 \\L N2)" unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.entails_Q_def entails_\_L_Q_def entails_\_L_q_def labeled_ord_red_crit_fam.entails_\_q_def labeled_ord_red_crit_fam.\_set_q_def \_set_L_q_def by simp lemma entail_equiv2: "labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.entails_Q = (\\L)" using entail_equiv by auto lemma red_inf_equiv: "labeled_ord_red_crit_fam.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q N = with_labels.Red_Inf_Q N" unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_Inf_Q_def with_labels.Red_Inf_Q_def labeled_ord_red_crit_fam.Red_Inf_\_q_def Red_Inf_\_L_q_def labeled_ord_red_crit_fam.\_set_q_def \_set_L_q_def by simp lemma red_inf_equiv2: "labeled_ord_red_crit_fam.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q = with_labels.Red_Inf_Q" using red_inf_equiv by auto lemma empty_red_f_equiv: "labeled_ord_red_crit_fam.empty_ord_lifted_calc_w_red_crit_family.Red_F_Q N = with_labels.Red_F_Q N" unfolding labeled_ord_red_crit_fam.empty_ord_lifted_calc_w_red_crit_family.Red_F_Q_def with_labels.Red_F_Q_def labeled_ord_red_crit_fam.Red_F_\_empty_q_def Red_F_\_empty_L_q_def labeled_ord_red_crit_fam.\_set_q_def \_set_L_q_def by simp lemma empty_red_f_equiv2: "labeled_ord_red_crit_fam.empty_ord_lifted_calc_w_red_crit_family.Red_F_Q = with_labels.Red_F_Q" using empty_red_f_equiv by auto sublocale stat_ref_calc: static_refutational_complete_calculus Bot_FL Inf_FL labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.entails_Q labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_Inf_Q labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q using labeled_ord_red_crit_fam.static_empty_ord_inter_equiv_static_inter empty_red_f_equiv2 red_inf_equiv2 entail_equiv2 labeled_static_ref_comp by argo (* lem:redundant-labeled-inferences *) lemma labeled_red_inf_eq_red_inf: "\ \ Inf_FL \ \ \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_Inf_Q N \ to_F \ \ no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` N)" for \ proof - fix \ assume i_in: "\ \ Inf_FL" have "\ \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_Inf_Q N \ to_F \ \ no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` N)" proof - assume i_in2: "\ \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_Inf_Q N" then have "X \ labeled_ord_red_crit_fam.Red_Inf_\_q ` Q \ \ \ X N" for X unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_Inf_Q_def by blast obtain X0 where "X0 \ labeled_ord_red_crit_fam.Red_Inf_\_q ` Q" using with_labels.Q_nonempty by blast then obtain q0 where x0_is: "X0 N = labeled_ord_red_crit_fam.Red_Inf_\_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_Inf_\_q q0 (fst ` N)" unfolding y0_is proof show "to_F ` X0 N \ no_labels.Red_Inf_\_q q0 (fst ` N)" proof fix \0 assume i0_in: "\0 \ to_F ` X0 N" then have i0_in2: "\0 \ to_F ` (labeled_ord_red_crit_fam.Red_Inf_\_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: "((\_Inf_L_q q0 \0_FL) \ None \ the (\_Inf_L_q q0 \0_FL) \ Red_Inf_q q0 (labeled_ord_red_crit_fam.\_set_q q0 N)) \ ((\_Inf_L_q q0 \0_FL = None) \ \_F_L_q q0 (concl_of \0_FL) \ (labeled_ord_red_crit_fam.\_set_q q0 N \ Red_F_q q0 (labeled_ord_red_crit_fam.\_set_q q0 N)))" unfolding labeled_ord_red_crit_fam.Red_Inf_\_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: "\_Inf_q q0 \0 \ None" and "the (\_Inf_q q0 \0) \ {}" then obtain \1 where i1_in: "\1 \ the (\_Inf_q q0 \0)" by blast have "the (\_Inf_q q0 \0) \ Red_Inf_q q0 (no_labels.\_set_q q0 (fst ` N))" using subs1 i0_to_i0_FL not_none unfolding no_labels.\_set_q_def labeled_ord_red_crit_fam.\_set_q_def \_Inf_L_q_def \_F_L_q_def by auto } moreover { assume is_none: "\_Inf_q q0 \0 = None" then have "\_F_q q0 (concl_of \0) \ no_labels.\_set_q q0 (fst ` N) \ Red_F_q q0 (no_labels.\_set_q q0 (fst ` N))" using subs1 i0_to_i0_FL concl_swap unfolding no_labels.\_set_q_def labeled_ord_red_crit_fam.\_set_q_def \_Inf_L_q_def \_F_L_q_def by simp } ultimately show "\0 \ no_labels.Red_Inf_\_q q0 (fst ` N)" unfolding no_labels.Red_Inf_\_q_def using i0_in3 by auto qed next show "no_labels.Red_Inf_\_q q0 (fst ` N) \ to_F ` X0 N" proof fix \0 assume i0_in: "\0 \ no_labels.Red_Inf_\_q q0 (fst ` N)" then have i0_in2: "\0 \ Inf_F" unfolding no_labels.Red_Inf_\_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 (metis Ex_list_of_length fst_conv inference.exhaust_sel inference.inject 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: "((\_Inf_L_q q0 \0_FL) \ None \ the (\_Inf_L_q q0 \0_FL) \ Red_Inf_q q0 (labeled_ord_red_crit_fam.\_set_q q0 N)) \ ((\_Inf_L_q q0 \0_FL = None) \ \_F_L_q q0 (concl_of \0_FL) \ (labeled_ord_red_crit_fam.\_set_q q0 N \ Red_F_q q0 (labeled_ord_red_crit_fam.\_set_q q0 N)))" using i0_in i0_to_i0_FL concl_swap unfolding no_labels.Red_Inf_\_q_def \_Inf_L_q_def no_labels.\_set_q_def labeled_ord_red_crit_fam.\_set_q_def \_F_L_q_def by simp then have "\0_FL \ labeled_ord_red_crit_fam.Red_Inf_\_q q0 N" using i0_FL_in unfolding labeled_ord_red_crit_fam.Red_Inf_\_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_Inf_\_q ` Q \ (to_F \) \ Y (fst ` N)" for Y using i_in2 no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q_def red_inf_equiv2 red_inf_impl by fastforce then show "(to_F \) \ no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` N)" unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_Inf_Q_def no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q_def by blast qed moreover have "(to_F \) \ no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` N) \ \ \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_Inf_Q N" proof - assume to_F_in: "to_F \ \ no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` N)" have imp_to_F: "X \ no_labels.Red_Inf_\_q ` Q \ to_F \ \ X (fst ` N)" for X using to_F_in unfolding no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q_def by blast then have to_F_in2: "to_F \ \ no_labels.Red_Inf_\_q q (fst ` N)" if "q \ Q" for q using that by auto have "labeled_ord_red_crit_fam.Red_Inf_\_q q N = {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_Inf_\_q q (fst ` N)}" for q proof show "labeled_ord_red_crit_fam.Red_Inf_\_q q N \ {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_Inf_\_q q (fst ` N)}" proof fix q0 \1 assume i1_in: "\1 \ labeled_ord_red_crit_fam.Red_Inf_\_q q0 N" have i1_in2: "\1 \ Inf_FL" using i1_in unfolding labeled_ord_red_crit_fam.Red_Inf_\_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 simp 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_Inf_\_q q0 (fst ` N)" using i1_in to_F_i1_in unfolding labeled_ord_red_crit_fam.Red_Inf_\_q_def no_labels.Red_Inf_\_q_def \_Inf_L_q_def labeled_ord_red_crit_fam.\_set_q_def no_labels.\_set_q_def \_F_L_q_def by force show "\1 \ {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_Inf_\_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_Inf_\_q q (fst ` N)} \ labeled_ord_red_crit_fam.Red_Inf_\_q q N" proof fix q0 \1 assume i1_in: "\1 \ {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_Inf_\_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 simp have concl_swap: "fst (concl_of \1) = concl_of (to_F \1)" unfolding concl_of_def to_F_def by simp then have "((\_Inf_L_q q0 \1) \ None \ the (\_Inf_L_q q0 \1) \ Red_Inf_q q0 (labeled_ord_red_crit_fam.\_set_q q0 N)) \ ((\_Inf_L_q q0 \1 = None) \ \_F_L_q q0 (concl_of \1) \ (labeled_ord_red_crit_fam.\_set_q q0 N \ Red_F_q q0 (labeled_ord_red_crit_fam.\_set_q q0 N)))" using i1_in unfolding no_labels.Red_Inf_\_q_def \_Inf_L_q_def labeled_ord_red_crit_fam.\_set_q_def no_labels.\_set_q_def \_F_L_q_def by auto then show "\1 \ labeled_ord_red_crit_fam.Red_Inf_\_q q0 N" using i1_in2 unfolding labeled_ord_red_crit_fam.Red_Inf_\_q_def by blast qed qed then have "\ \ labeled_ord_red_crit_fam.Red_Inf_\_q q N" if "q \ Q" for q using that to_F_in2 i_in unfolding labeled_ord_red_crit_fam.Red_Inf_\_q_def no_labels.Red_Inf_\_q_def \_Inf_L_q_def labeled_ord_red_crit_fam.\_set_q_def no_labels.\_set_q_def \_F_L_q_def by auto then show "\ \ labeled_ord_red_crit_fam.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q N" unfolding labeled_ord_red_crit_fam.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q_def by blast qed ultimately show "\ \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_Inf_Q N \ to_F \ \ no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` N)" by argo qed (* lem:redundant-labeled-formulas *) 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) \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q N\ proof - note assms moreover have i: \C \ no_labels.Red_F_\_empty (fst ` N) \ (C, L) \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q 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.\_set_q q (fst ` N))" if "q \ Q" for q unfolding no_labels.Red_F_\_empty_q_def using that by blast have "no_labels.\_set_q q (fst ` N) = labeled_ord_red_crit_fam.\_set_q q N" for q unfolding no_labels.\_set_q_def labeled_ord_red_crit_fam.\_set_q_def \_F_L_q_def by simp then have "\_F_L_q q (C, L) \ Red_F_q q (labeled_ord_red_crit_fam.\_set_q q N)" if "q \ Q" for q using that g_in_red unfolding \_F_L_q_def by simp then show ?thesis unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q_def labeled_ord_red_crit_fam.Red_F_\_q_g_def by blast qed moreover have ii: \\C' \ fst ` N. C' \\ C \ (C, L) \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q 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 unfolding no_labels.\_set_q_def labeled_ord_red_crit_fam.\_set_q_def \_F_L_q_def using that by auto then have "(C, L) \ labeled_ord_red_crit_fam.Red_F_\_q_g q N" if "q \ Q" for q unfolding labeled_ord_red_crit_fam.Red_F_\_q_g_def using that c'_l'_in c'_l'_prec by blast then show ?thesis unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q_def by blast qed moreover have iii: \\(C', L') \ N. (L' \l L \ C' \\ C) \ (C, L) \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q 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) \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q 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 unfolding no_labels.\_set_q_def labeled_ord_red_crit_fam.\_set_q_def \_F_L_q_def using that by auto then have "(C, L) \ labeled_ord_red_crit_fam.Red_F_\_q_g q N" if "q \ Q" for q unfolding labeled_ord_red_crit_fam.Red_F_\_q_g_def using that c'_l'_in c'_l'_prec by blast then have ?thesis unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q_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 Architecture\ locale Given_Clause = Prover_Architecture_Basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_Inf_q Red_F_q \_F_q \_Inf_q Inf_FL Equiv_F Prec_F Prec_l 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_Inf_q :: "'q \ 'g set \ 'g inference set" and Red_F_q :: "'q \ 'g set \ 'g set" and \_F_q :: "'q \ 'f \ 'g set" and \_Inf_q :: "'q \ 'f inference \ 'g inference set option" and Inf_FL :: \('f \ 'l) inference set\ 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) + fixes active :: "'l" assumes inf_have_prems: "\F \ Inf_F \ prems_of \F \ []" and active_minimal: "l2 \ active \ active \l l2" and at_least_two_labels: "\l2. active \l l2" and inf_never_active: "\ \ Inf_FL \ snd (concl_of \) \ active" begin lemma labeled_inf_have_prems: "\ \ Inf_FL \ set (prems_of \) \ {}" using inf_have_prems Inf_FL_to_Inf_F by fastforce definition active_subset :: "('f \ 'l) set \ ('f \ 'l) set" where "active_subset M = {CL \ M. snd CL = active}" definition non_active_subset :: "('f \ 'l) set \ ('f \ 'l) set" where "non_active_subset M = {CL \ M. snd CL \ active}" inductive step :: "('f \ 'l) set \ ('f \ 'l) set \ bool" (infix "\GC" 50) where process: "N1 = N \ M \ N2 = N \ M' \ M \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q (N \ M') \ active_subset M' = {} \ N1 \GC N2" | - infer: "N1 = N \ {(C, L)} \ {(C, L)} \ N = {} \ N2 = N \ {(C, active)} \ M \ L \ active \ + infer: "N1 = N \ {(C, L)} \ N2 = N \ {(C, active)} \ M \ L \ active \ active_subset M = {} \ no_labels.Non_ground.Inf_from2 (fst ` (active_subset N)) {C} \ no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N \ {(C, active)} \ M)) \ N1 \GC N2" abbreviation derive :: "('f \ 'l) set \ ('f \ 'l) set \ bool" (infix "\RedL" 50) where "derive \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive" lemma one_step_equiv: "N1 \GC N2 \ N1 \RedL 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 \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q (N \ M')" and active_empty: "active_subset M' = {}" have "N1 - N2 \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q N2" using n1_is n2_is m_red by auto then show "labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive N1 N2" unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.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 - empty_inter: "{(C, L)} \ N = {}" 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)} \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q N2" using red_labeled_clauses by blast - moreover have "(C, L) \ M \ N1 - N2 = {(C, L)}" using n1_is n2_is empty_inter not_active by auto - moreover have "(C, L) \ M \ N1 - N2 = {}" using n1_is n2_is by auto + moreover have "N1 - N2 = {} \ N1 - N2 = {(C, L)}" using n1_is n2_is by blast ultimately have "N1 - N2 \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q N2" using empty_red_f_equiv[of N2] by blast then show "labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive N1 N2" unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive.simps by blast qed abbreviation fair :: "('f \ 'l) set llist \ bool" where "fair \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.fair" (* lem:gc-derivations-are-red-derivations *) lemma gc_to_red: "chain (\GC) D \ chain (\RedL) D" using one_step_equiv Lazy_List_Chain.chain_mono by blast lemma (in-) all_ex_finite_set: "(\(j::nat)\{0..(n::nat). P j n) \ (\n1 n2. \j\{0.. P j n2 \ n1 = n2) \ finite {n. \j \ {0.. nat \ bool" assume allj_exn: "\j\{0..n. P j n" and uniq_n: "\n1 n2. \j\{0.. P j n2 \ n1 = n2" have "{n. \j \ {0..((\j. {n. P j n}) ` {0..j\{0.. finite {n. \j \ {0..j. {n. P j n}"] by simp have "\j\{0..!n. P j n" using allj_exn uniq_n by blast then have "\j\{0..j \ {0..GC) D" and non_empty: "llength D > 0" and init_state: "active_subset (lnth D 0) = {}" and final_state: "non_active_subset (Liminf_llist D) = {}" shows "fair D" unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.fair_def proof fix \ assume i_in: "\ \ with_labels.Inf_from (Liminf_llist D)" have i_in_inf_fl: "\ \ Inf_FL" using i_in unfolding with_labels.Inf_from_def by blast have "Liminf_llist D = active_subset (Liminf_llist D)" using final_state unfolding non_active_subset_def active_subset_def by blast then have i_in2: "\ \ with_labels.Inf_from (active_subset (Liminf_llist D))" 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 with_labels.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..nj. enat (Suc nj) < llength D \ (prems_of \)!j \ active_subset (lnth D nj) \ (\k. k > nj \ enat k < llength D \ (prems_of \)!j \ active_subset (lnth D k)))" proof clarify fix j assume j_in: "j \ {0..)!j" using i_in2 unfolding m_def with_labels.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 D" using j_in i_in unfolding m_def with_labels.Inf_from_def by force then obtain nj where nj_is: "enat nj < llength D" and c_in2: "(C, active) \ \ (lnth D ` {k. nj \ k \ enat k < llength D})" unfolding Liminf_llist_def using init_state by blast then have c_in3: "\k. k \ nj \ enat k < llength D \ (C, active) \ (lnth D k)" by blast have nj_pos: "nj > 0" using init_state c_in2 nj_is unfolding active_subset_def by fastforce obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength D \ (C, active) \ \ (lnth D ` {k. nj \ k \ enat k < llength D}))" by blast then have in_allk: "\k. k \ nj_min \ enat k < llength D \ (C, active) \ (lnth D 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 D" using nj_min_is by (smt LeastI_ex \\thesis. (\nj. \enat nj < llength D; (C, active) \ \ (lnth D ` {k. nj \ k \ enat k < llength D})\ \ thesis) \ thesis\) have "nj_min > 0" using nj_is c_in2 nj_pos nj_min_is by (metis (mono_tags, lifting) Collect_empty_eq \(C, active) \ Liminf_llist D\ \Liminf_llist D = active_subset (Liminf_llist D)\ \\k\nj_min. enat k < llength D \ (C, active) \ lnth D k\ active_subset_def init_state linorder_not_less mem_Collect_eq non_empty zero_enat_def) 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 D" using HOL.no_atp(15)[OF njm_smaller_D njm_prec_njm_enat] . have njm_prec_all_suc: "\k>njm_prec. enat k < llength D \ (C, active) \ lnth D k" using nj_prec_is in_allk by simp have notin_njm_prec: "(C, active) \ lnth D njm_prec" proof (rule ccontr) assume "\ (C, active) \ lnth D njm_prec" then have absurd_hyp: "(C, active) \ lnth D njm_prec" by simp have prec_smaller: "enat njm_prec < llength D" using nj_min_is nj_prec_is by (smt LeastI_ex Suc_leD \\thesis. (\nj. \enat nj < llength D; (C, active) \ \ (lnth D ` {k. nj \ k \ enat k < llength D})\ \ thesis) \ thesis\ enat_ord_simps(1) le_eq_less_or_eq le_less_trans) have "(C, active) \ \ (lnth D ` {k. njm_prec \ k \ enat k < llength D})" proof - { fix k assume k_in: "njm_prec \ k \ enat k < llength D" have "k = njm_prec \ (C, active) \ lnth D k" using absurd_hyp by simp moreover have "njm_prec < k \ (C, active) \ lnth D k" using nj_prec_is in_allk k_in by simp ultimately have "(C, active) \ lnth D k" using k_in by fastforce } then show "(C, active) \ \ (lnth D ` {k. njm_prec \ k \ enat k < llength D})" by blast qed then have "enat njm_prec < llength D \ (C, active) \ \ (lnth D ` {k. njm_prec \ k \ enat k < llength D})" 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 D njm_prec)" unfolding active_subset_def by blast then show "\nj. enat (Suc nj) < llength D \ (prems_of \)!j \ active_subset (lnth D nj) \ (\k. k > nj \ enat k < llength D \ (prems_of \)!j \ active_subset (lnth D 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.. (prems_of \)!j \ active_subset (lnth D nj) \ (\k. k > nj \ enat k < llength D \ (prems_of \)!j \ active_subset (lnth D k)))}" then have nj_not_empty: "nj_set \ {}" proof - have zero_in: "0 \ {0.. ! 0 \ active_subset (lnth D n0)" and "\k>n0. enat k < llength D \ prems_of \ ! 0 \ active_subset (lnth D 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) (* the n below in the n-1 from the pen-and-paper proof *) 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..)!j0 \ active_subset (lnth D n)" and j0_allin: "(\k. k > n \ enat k < llength D \ (prems_of \)!j0 \ active_subset (lnth D 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 with_labels.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 D (Suc n))" using C0_is j0_allin suc_n_length by (simp add: active_subset_def) have C0_notin: "(C0, active) \ (lnth D n)" using C0_is j0_notin unfolding active_subset_def by simp have step_n: "lnth D n \GC lnth D (Suc n)" using deriv chain_lnth_rel n_in unfolding nj_set_def by blast - have "\N C L M. (lnth D n = N \ {(C, L)} \ {(C, L)} \ N = {} \ + have "\N C L M. (lnth D n = N \ {(C, L)} \ lnth D (Suc n) = N \ {(C, active)} \ M \ L \ active \ active_subset M = {} \ no_labels.Non_ground.Inf_from2 (fst ` (active_subset N)) {C} \ no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N \ {(C, active)} \ M)))" proof - have proc_or_infer: "(\N1 N M N2 M'. lnth D n = N1 \ lnth D (Suc n) = N2 \ N1 = N \ M \ N2 = N \ M' \ M \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q (N \ M') \ active_subset M' = {}) \ (\N1 N C L N2 M. lnth D n = N1 \ lnth D (Suc n) = N2 \ N1 = N \ {(C, L)} \ - {(C, L)} \ N = {} \ N2 = N \ {(C, active)} \ M \ - L \ active \ active_subset M = {} \ + N2 = N \ {(C, active)} \ M \ L \ active \ active_subset M = {} \ no_labels.Non_ground.Inf_from2 (fst ` (active_subset N)) {C} \ no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N \ {(C, active)} \ M)))" using step.simps[of "lnth D n" "lnth D (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.Non_ground.Inf_from2 (fst ` (active_subset N)) {C0} \ no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N \ {(C0, active)} \ M))" and nth_d_is: "lnth D n = N \ {(C0, L)}" and suc_nth_d_is: "lnth D (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.. (prems_of \)!j \ (prems_of \)!j0 \ (prems_of \)!j \ (active_subset N)" for j proof - fix j assume j_in: "j \ {0..)!j \ (prems_of \)!j0" obtain nj where nj_len: "enat (Suc nj) < llength D" and nj_prems: "(prems_of \)!j \ active_subset (lnth D nj)" and nj_greater: "(\k. k > nj \ enat k < llength D \ (prems_of \)!j \ active_subset (lnth D 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 D n" "lnth D (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 D 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 "\ \ with_labels.Inf_from2 (active_subset N) {(C0, active)}" using i_in_inf_fl unfolding with_labels.Inf_from2_def with_labels.Inf_from_def by blast then have "to_F \ \ no_labels.Non_ground.Inf_from2 (fst ` (active_subset N)) {C0}" unfolding to_F_def with_labels.Inf_from2_def with_labels.Inf_from_def no_labels.Non_ground.Inf_from2_def no_labels.Non_ground.Inf_from_def using Inf_FL_to_Inf_F by force then have "to_F \ \ no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (lnth D (Suc n)))" using suc_nth_d_is inf_from_subs by fastforce then have "\q \ Q. (\_Inf_q q (to_F \) \ None \ the (\_Inf_q q (to_F \)) \ Red_Inf_q q (\ (\_F_q q ` (fst ` (lnth D (Suc n)))))) \ (\_Inf_q q (to_F \) = None \ \_F_q q (concl_of (to_F \)) \ (\ (\_F_q q ` (fst ` (lnth D (Suc n))))) \ Red_F_q q (\ (\_F_q q ` (fst ` (lnth D (Suc n))))))" unfolding to_F_def no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q_def no_labels.Red_Inf_\_q_def no_labels.\_set_q_def by fastforce then have "\ \ with_labels.Red_Inf_Q (lnth D (Suc n))" unfolding to_F_def with_labels.Red_Inf_Q_def Red_Inf_\_L_q_def \_Inf_L_q_def \_set_L_q_def \_F_L_q_def using i_in_inf_fl by auto then show "\ \ labeled_ord_red_crit_fam.empty_ord_lifted_calc_w_red_crit_family.inter_red_crit_calculus.Sup_Red_Inf_llist D" unfolding labeled_ord_red_crit_fam.empty_ord_lifted_calc_w_red_crit_family.inter_red_crit_calculus.Sup_Red_Inf_llist_def using red_inf_equiv2 suc_n_length by auto qed (* thm:gc-completeness *) theorem gc_complete: assumes deriv: "chain (\GC) D" and not_empty_d: "llength D > 0" and init_state: "active_subset (lnth D 0) = {}" and final_state: "non_active_subset (Liminf_llist D) = {}" and b_in: "B \ Bot_F" and bot_entailed: "no_labels.entails_\_Q (fst ` (lnth D 0)) {B}" shows "\i. enat i < llength D \ (\BL\ Bot_FL. BL \ (lnth D i))" proof - have labeled_b_in: "(B, active) \ Bot_FL" unfolding Bot_FL_def using b_in by simp have not_empty_d2: "\ lnull D" using not_empty_d by force have labeled_bot_entailed: "entails_\_L_Q (lnth D 0) {(B, active)}" using labeled_entailment_lifting bot_entailed by fastforce have "fair D" using gc_fair[OF deriv not_empty_d init_state final_state] . then have "\i \ {i. enat i < llength D}. \BL\Bot_FL. BL \ lnth D i" using stat_ref_calc.dynamic_refutational_complete labeled_b_in not_empty_d2 gc_to_red[OF deriv] labeled_bot_entailed entail_equiv unfolding dynamic_refutational_complete_calculus_def dynamic_refutational_complete_calculus_axioms_def by blast then show ?thesis by blast qed end subsection \Lazy Given Clause Architecture\ locale Lazy_Given_Clause = Prover_Architecture_Basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_Inf_q Red_F_q \_F_q \_Inf_q Inf_FL Equiv_F Prec_F Prec_l 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_Inf_q :: "'q \ 'g set \ 'g inference set" and Red_F_q :: "'q \ 'g set \ 'g set" and \_F_q :: "'q \ 'f \ 'g set" and \_Inf_q :: "'q \ 'f inference \ 'g inference set option" and Inf_FL :: \('f \ 'l) inference set\ 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) + fixes active :: "'l" assumes active_minimal: "l2 \ active \ active \l l2" and at_least_two_labels: "\l2. active \l l2" and inf_never_active: "\ \ Inf_FL \ snd (concl_of \) \ active" begin definition active_subset :: "('f \ 'l) set \ ('f \ 'l) set" where "active_subset M = {CL \ M. snd CL = active}" definition non_active_subset :: "('f \ 'l) set \ ('f \ 'l) set" where "non_active_subset M = {CL \ M. snd CL \ active}" 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 \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q (N \ M') \ active_subset M' = {} \ (T, N1) \LGC (T, N2)" | - schedule_infer: "T2 = T1 \ T' \ N1 = N \ {(C, L)} \ {(C, L)} \ N = {} \ N2 = N \ {(C, active)} \ + schedule_infer: "T2 = T1 \ T' \ N1 = N \ {(C, L)} \ N2 = N \ {(C, active)} \ L \ active \ T' = no_labels.Non_ground.Inf_from2 (fst ` (active_subset N)) {C} \ (T1, N1) \LGC (T2, N2)" | - compute_infer: "T1 = T2 \ {\} \ T2 \ {\} = {} \ N2 = N1 \ M \ active_subset M = {} \ + compute_infer: "T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N1 \ M)) \ (T1, N1) \LGC (T2, N2)" | - delete_orphans: "T1 = T2 \ T' \ T2 \ T' = {} \ + delete_orphans: "T1 = T2 \ T' \ T' \ no_labels.Non_ground.Inf_from (fst ` (active_subset N)) = {} \ (T1, N) \LGC (T2, N)" abbreviation derive :: "('f \ 'l) set \ ('f \ 'l) set \ bool" (infix "\RedL" 50) where "derive \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive" lemma premise_free_inf_always_from: "\ \ Inf_F \ length (prems_of \) = 0 \ \ \ no_labels.Non_ground.Inf_from N" unfolding no_labels.Non_ground.Inf_from_def by simp lemma one_step_equiv: "(T1, N1) \LGC (T2, N2) \ N1 \RedL 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 \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q (N \ M')" have "N1 - N2 \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q N2" using n1_is n2_is m_red by auto then show "N1 \RedL N2" unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.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)} \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q N2" using red_labeled_clauses by blast then have "N1 - N2 \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q N2" using empty_red_f_equiv[of N2] using n1_is n2_is by blast then show "N1 \RedL N2" unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive.simps by blast next fix M assume n2_is: "N2 = N1 \ M" have "N1 - N2 \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q N2" using n2_is by blast then show "N1 \RedL N2" unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive.simps by blast next assume n2_is: "N2 = N1" have "N1 - N2 \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.Red_F_Q N2" using n2_is by blast then show "N1 \RedL N2" unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.derive.simps by blast qed abbreviation fair :: "('f \ 'l) set llist \ bool" where "fair \ labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.fair" (* lem:lgc-derivations-are-red-derivations *) lemma lgc_to_red: "chain (\LGC) D \ chain (\RedL) (lmap snd D)" using one_step_equiv Lazy_List_Chain.chain_mono by (smt chain_lmap prod.collapse) (* lem:fair-lgc-derivations *) lemma lgc_fair: assumes deriv: "chain (\LGC) D" and non_empty: "llength D > 0" and init_state: "active_subset (snd (lnth D 0)) = {}" and final_state: "non_active_subset (Liminf_llist (lmap snd D)) = {}" and no_prems_init_active: "\\ \ Inf_F. length (prems_of \) = 0 \ \ \ (fst (lnth D 0))" and final_schedule: "Liminf_llist (lmap fst D) = {}" shows "fair (lmap snd D)" unfolding labeled_ord_red_crit_fam.lifted_calc_w_red_crit_family.inter_red_crit_calculus.fair_def proof fix \ assume i_in: "\ \ with_labels.Inf_from (Liminf_llist (lmap snd D))" have i_in_inf_fl: "\ \ Inf_FL" using i_in unfolding with_labels.Inf_from_def by blast have "Liminf_llist (lmap snd D) = active_subset (Liminf_llist (lmap snd D))" using final_state unfolding non_active_subset_def active_subset_def by blast then have i_in2: "\ \ with_labels.Inf_from (active_subset (Liminf_llist (lmap snd D)))" 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 with_labels.Inf_from_def to_F_def by blast have exist_nj: "\j \ {0..nj. enat (Suc nj) < llength D \ (prems_of \)!j \ active_subset (snd (lnth D nj)) \ (\k. k > nj \ enat k < llength D \ (prems_of \)!j \ active_subset (snd (lnth D k))))" proof clarify fix j assume j_in: "j \ {0..)!j" using i_in2 unfolding m_def with_labels.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 D)" using j_in i_in unfolding m_def with_labels.Inf_from_def by force then obtain nj where nj_is: "enat nj < llength D" and c_in2: "(C, active) \ \ (snd ` (lnth D ` {k. nj \ k \ enat k < llength D}))" unfolding Liminf_llist_def using init_state by fastforce then have c_in3: "\k. k \ nj \ enat k < llength D \ (C, active) \ snd (lnth D k)" by blast have nj_pos: "nj > 0" using init_state c_in2 nj_is unfolding active_subset_def by fastforce obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength D \ (C, active) \ \ (snd ` (lnth D ` {k. nj \ k \ enat k < llength D})))" by blast then have in_allk: "\k. k \ nj_min \ enat k < llength D \ (C, active) \ snd (lnth D k)" using c_in3 nj_is c_in2 INT_E LeastI_ex by (smt INT_iff INT_simps(10) c_is image_eqI mem_Collect_eq) have njm_smaller_D: "enat nj_min < llength D" using nj_min_is by (smt LeastI_ex \\thesis. (\nj. \enat nj < llength D; (C, active) \ \ (snd ` (lnth D ` {k. nj \ k \ enat k < llength D}))\ \ thesis) \ thesis\) have "nj_min > 0" using nj_is c_in2 nj_pos nj_min_is by (metis (mono_tags, lifting) active_subset_def emptyE in_allk init_state mem_Collect_eq non_empty not_less snd_conv zero_enat_def) 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 D" using HOL.no_atp(15)[OF njm_smaller_D njm_prec_njm_enat] . have njm_prec_all_suc: "\k>njm_prec. enat k < llength D \ (C, active) \ snd (lnth D k)" using nj_prec_is in_allk by simp have notin_njm_prec: "(C, active) \ snd (lnth D njm_prec)" proof (rule ccontr) assume "\ (C, active) \ snd (lnth D njm_prec)" then have absurd_hyp: "(C, active) \ snd (lnth D njm_prec)" by simp have prec_smaller: "enat njm_prec < llength D" using nj_min_is nj_prec_is by (smt LeastI_ex Suc_leD \\thesis. (\nj. \enat nj < llength D; (C, active) \ \ (snd ` (lnth D ` {k. nj \ k \ enat k < llength D}))\ \ thesis) \ thesis\ enat_ord_simps(1) le_eq_less_or_eq le_less_trans) have "(C, active) \ \ (snd ` (lnth D ` {k. njm_prec \ k \ enat k < llength D}))" proof - { fix k assume k_in: "njm_prec \ k \ enat k < llength D" have "k = njm_prec \ (C, active) \ snd (lnth D k)" using absurd_hyp by simp moreover have "njm_prec < k \ (C, active) \ snd (lnth D k)" using nj_prec_is in_allk k_in by simp ultimately have "(C, active) \ snd (lnth D k)" using k_in by fastforce } then show "(C, active) \ \ (snd ` (lnth D ` {k. njm_prec \ k \ enat k < llength D}))" by blast qed then have "enat njm_prec < llength D \ (C, active) \ \ (snd ` (lnth D ` {k. njm_prec \ k \ enat k < llength D}))" 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 D njm_prec))" unfolding active_subset_def by blast then show "\nj. enat (Suc nj) < llength D \ (prems_of \)!j \ active_subset (snd (lnth D nj)) \ (\k. k > nj \ enat k < llength D \ (prems_of \)!j \ active_subset (snd (lnth D 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.. (prems_of \)!j \ active_subset (snd (lnth D nj)) \ (\k. k > nj \ enat k < llength D \ (prems_of \)!j \ active_subset (snd (lnth D k))))}" { assume m_null: "m = 0" then have "enat 0 < llength D \ to_F \ \ fst (lnth D 0)" using no_prems_init_active i_in_F non_empty m_def_F zero_enat_def by auto then have "\n. enat n < llength D \ to_F \ \ fst (lnth D n)" by blast } moreover { assume m_pos: "m > 0" have nj_not_empty: "nj_set \ {}" proof - have zero_in: "0 \ {0.. ! 0 \ active_subset (snd (lnth D n0))" and "\k>n0. enat k < llength D \ prems_of \ ! 0 \ active_subset (snd (lnth D 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..)!j0 \ active_subset (snd (lnth D n))" and j0_allin: "(\k. k > n \ enat k < llength D \ (prems_of \)!j0 \ active_subset (snd (lnth D 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 with_labels.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 D (Suc n)))" using C0_is j0_allin suc_n_length by (simp add: active_subset_def) have C0_notin: "(C0, active) \ (snd (lnth D n))" using C0_is j0_notin unfolding active_subset_def by simp have step_n: "lnth D n \LGC lnth D (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 D n = (T1, N1) \ lnth D (Suc n) = (T2, N2) \ - T2 = T1 \ T' \ N1 = N \ {(C, L)} \ {(C, L)} \ N = {} \ N2 = N \ {(C, active)} \ L \ active \ + T2 = T1 \ T' \ N1 = N \ {(C, L)} \ N2 = N \ {(C, active)} \ L \ active \ T' = no_labels.Non_ground.Inf_from2 (fst ` active_subset N) {C}" using step.simps[of "lnth D n" "lnth D (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 D n = (T1, N1)" and suc_nth_d_is: "lnth D (Suc n) = (T2, N2)" and t2_is: "T2 = T1 \ T'" and - n1_is: "N1 = N \ {(C0, L)}" "{(C0, L)} \ N = {}" "N2 = N \ {(C0, active)}" and + n1_is: "N1 = N \ {(C0, L)}" "N2 = N \ {(C0, active)}" and l_not_active: "L \ active" and tp_is: "T' = no_labels.Non_ground.Inf_from2 (fst ` active_subset N) {C0}" using C0_in C0_notin j0_in C0_is using active_subset_def by fastforce have "j \ {0.. (prems_of \)!j \ (prems_of \)!j0 \ (prems_of \)!j \ (active_subset N)" for j proof - fix j assume j_in: "j \ {0..)!j \ (prems_of \)!j0" obtain nj where nj_len: "enat (Suc nj) < llength D" and nj_prems: "(prems_of \)!j \ active_subset (snd (lnth D nj))" and nj_greater: "(\k. k > nj \ enat k < llength D \ (prems_of \)!j \ active_subset (snd (lnth D 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 D n" "lnth D (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 D 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 "\ \ with_labels.Inf_from2 (active_subset N) {(C0, active)}" using i_in_inf_fl prems_i_active unfolding with_labels.Inf_from2_def with_labels.Inf_from_def by blast then have "to_F \ \ no_labels.Non_ground.Inf_from2 (fst ` (active_subset N)) {C0}" unfolding to_F_def with_labels.Inf_from2_def with_labels.Inf_from_def no_labels.Non_ground.Inf_from2_def no_labels.Non_ground.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.. (\k. k > n \ enat k < llength D \ (prems_of \)!j \ active_subset (snd (lnth D k)))" for j proof (cases "j = j0") case True assume "j = j0" then show "(\k. k > n \ enat k < llength D \ (prems_of \)!j \ active_subset (snd (lnth D k)))" using j0_allin by simp next case False assume j_in: "j \ {0.. j0" obtain nj where nj_len: "enat (Suc nj) < llength D" and nj_prems: "(prems_of \)!j \ active_subset (snd (lnth D nj))" and nj_greater: "(\k. k > nj \ enat k < llength D \ (prems_of \)!j \ active_subset (snd (lnth D 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 D \ (prems_of \)!j \ active_subset (snd (lnth D k)))" using nj_greater n_bigger by auto qed then have allj_allk: "(\c\ set (prems_of \). (\k. k > n \ enat k < llength D \ c \ active_subset (snd (lnth D 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 D \ to_F \ \ fst (lnth D (Suc n)) \ (\c\ set (prems_of \). snd c = active) \ (\c\ set (prems_of \). (\k. k > n \ enat k < llength D \ c \ active_subset (snd (lnth D 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 D \ to_F \ \ fst (lnth D n) \ (\c\ set (prems_of \). snd c = active) \ (\c\ set (prems_of \). (\k. k \ n \ enat k < llength D \ c \ active_subset (snd (lnth D k))))" by auto } ultimately obtain n T2 N2 where i_in_suc_n: "to_F \ \ fst (lnth D n)" and all_prems_active_after: "m > 0 \ (\c\ set (prems_of \). (\k. k \ n \ enat k < llength D \ c \ active_subset (snd (lnth D k))))" and suc_n_length: "enat n < llength D" and suc_nth_d_is: "lnth D 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 D \ to_F \ \ (fst (lnth D p)) \ to_F \ \ (fst (lnth D (Suc p)))" proof (rule ccontr) assume contra: "\ (\p\n. enat (Suc p) < llength D \ to_F \ \ (fst (lnth D p)) \ to_F \ \ (fst (lnth D (Suc p))))" then have i_in_suc: "p0 \ n \ enat (Suc p0) < llength D \ to_F \ \ (fst (lnth D p0)) \ to_F \ \ (fst (lnth D (Suc p0)))" for p0 by blast have "p0 \ n \ enat p0 < llength D \ to_F \ \ (fst (lnth D 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 D \ to_F \ \ fst (lnth D p0)" and sucsuc_smaller_d: "enat (Suc p0) < llength D" have suc_p_bigger_n: "n \ p0" using p_bigger_n by simp have suc_smaller_d: "enat p0 < llength D" using sucsuc_smaller_d Suc_ile_eq dual_order.strict_implies_order by blast then have "to_F \ \ fst (lnth D 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 D \ to_F \ \ (fst (lnth D j))" by presburger have "llength (lmap fst D) = llength D" by force then have "to_F \ \ \ (lnth (lmap fst D) ` {j. n \ j \ enat j < llength (lmap fst D)})" using i_in_all_bigger_n using Suc_le_D by auto then have "to_F \ \ Liminf_llist (lmap fst D)" 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 D" and i_in_p: "to_F \ \ (fst (lnth D p))" and i_notin_suc_p: "to_F \ \ (fst (lnth D (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 D p \LGC lnth D (Suc p)" using deriv p_smaller_d chain_lnth_rel by blast then have "\T1 T2 \ N2 N1 M. lnth D p = (T1, N1) \ lnth D (Suc p) = (T2, N2) \ - T1 = T2 \ {\} \ T2 \ {\} = {} \ N2 = N1 \ M \ active_subset M = {} \ + T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N1 \ M))" proof - have ci_or_do: "(\T1 T2 \ N2 N1 M. lnth D p = (T1, N1) \ lnth D (Suc p) = (T2, N2) \ - T1 = T2 \ {\} \ T2 \ {\} = {} \ N2 = N1 \ M \ active_subset M = {} \ + T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N1 \ M))) \ (\T1 T2 T' N. lnth D p = (T1, N) \ lnth D (Suc p) = (T2, N) \ - T1 = T2 \ T' \ T2 \ T' = {} \ + T1 = T2 \ T' \ T' \ no_labels.Non_ground.Inf_from (fst ` active_subset N) = {})" - using step.simps[of "lnth D p" "lnth D (Suc p)"] step_p i_in_p i_notin_suc_p - by fastforce + using step.simps[of "lnth D p" "lnth D (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.. (prems_of (to_F \))!j \ (fst ` (active_subset (snd (lnth D p))))" for j proof - fix j assume m_pos: "m > 0" and j_in: "j \ {0..)!j \ (active_subset (snd (lnth D 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 D p))))" by blast then show "(prems_of (to_F \))!j \ (fst ` (active_subset (snd (lnth D 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.Non_ground.Inf_from (fst ` active_subset (snd (lnth D p)))" using i_in_F unfolding no_labels.Non_ground.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 D p = (T1, N1) \ lnth D (Suc p) = (T2, N2) \ - T1 = T2 \ {\} \ T2 \ {\} = {} \ N2 = N1 \ M \ active_subset M = {} \ + T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (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 D p = (T1, N1) \ lnth D (Suc p) = (T2, N2) \ - T1 = T2 \ {\} \ T2 \ {\} = {} \ N2 = N1 \ M \ active_subset M = {} \ + T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (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 D p = (T1p, N1p)" and suc_p_is: "lnth D (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.empty_ord_lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (N1p \ Mp))" using i_in_p i_notin_suc_p by fastforce have "to_F \ \ no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q (fst ` (snd (lnth D (Suc p))))" using i_in_red_inf suc_p_is n2p_is by fastforce then have "\q \ Q. (\_Inf_q q (to_F \) \ None \ the (\_Inf_q q (to_F \)) \ Red_Inf_q q (\ (\_F_q q ` (fst ` (snd (lnth D (Suc p))))))) \ (\_Inf_q q (to_F \) = None \ \_F_q q (concl_of (to_F \)) \ (\ (\_F_q q ` (fst ` (snd (lnth D (Suc p)))))) \ Red_F_q q (\ (\_F_q q ` (fst ` (snd (lnth D (Suc p)))))))" unfolding to_F_def no_labels.lifted_calc_w_red_crit_family.Red_Inf_Q_def no_labels.Red_Inf_\_q_def no_labels.\_set_q_def by fastforce then have "\ \ with_labels.Red_Inf_Q (snd (lnth D (Suc p)))" unfolding to_F_def with_labels.Red_Inf_Q_def Red_Inf_\_L_q_def \_Inf_L_q_def \_set_L_q_def \_F_L_q_def using i_in_inf_fl by auto then show "\ \ labeled_ord_red_crit_fam.empty_ord_lifted_calc_w_red_crit_family.inter_red_crit_calculus.Sup_Red_Inf_llist (lmap snd D)" unfolding labeled_ord_red_crit_fam.empty_ord_lifted_calc_w_red_crit_family.inter_red_crit_calculus.Sup_Red_Inf_llist_def using red_inf_equiv2 suc_n_length p_smaller_d by auto qed (* thm:lgc-completeness *) theorem lgc_complete: assumes deriv: "chain (\LGC) D" and not_empty_d: "llength D > 0" and init_state: "active_subset (snd (lnth D 0)) = {}" and final_state: "non_active_subset (Liminf_llist (lmap snd D)) = {}" and no_prems_init_active: "\\ \ Inf_F. length (prems_of \) = 0 \ \ \ fst (lnth D 0)" and final_schedule: "Liminf_llist (lmap fst D) = {}" and b_in: "B \ Bot_F" and bot_entailed: "no_labels.entails_\_Q (fst ` (snd (lnth D 0))) {B}" shows "\i. enat i < llength D \ (\BL \ Bot_FL. BL \ snd (lnth D i))" proof - have labeled_b_in: "(B, active) \ Bot_FL" unfolding Bot_FL_def using b_in by simp have not_empty_d2: "\ lnull (lmap snd D)" using not_empty_d by force have simp_snd_lmap: "lnth (lmap snd D) 0 = snd (lnth D 0)" using lnth_lmap[of 0 D snd] not_empty_d by (simp add: zero_enat_def) have labeled_bot_entailed: "entails_\_L_Q (snd (lnth D 0)) {(B, active)}" using labeled_entailment_lifting bot_entailed by fastforce have "fair (lmap snd D)" using lgc_fair[OF deriv not_empty_d init_state final_state no_prems_init_active final_schedule] . then have "\i \ {i. enat i < llength D}. \BL\Bot_FL. BL \ (snd (lnth D i))" using stat_ref_calc.dynamic_refutational_complete labeled_b_in not_empty_d2 lgc_to_red[OF deriv] labeled_bot_entailed entail_equiv simp_snd_lmap unfolding dynamic_refutational_complete_calculus_def dynamic_refutational_complete_calculus_axioms_def by (metis (mono_tags, lifting) llength_lmap lnth_lmap mem_Collect_eq) then show ?thesis by blast qed end end