diff --git a/thys/Saturation_Framework/Calculus.thy b/thys/Saturation_Framework/Calculus.thy --- a/thys/Saturation_Framework/Calculus.thy +++ b/thys/Saturation_Framework/Calculus.thy @@ -1,409 +1,409 @@ (* Title: Calculi Based on a Redundancy Criterion * Author: Sophie Tourret , 2018-2020 *) section \Calculi Based on a Redundancy Criterion\ text \This section introduces the most basic notions upon which the framework is built: consequence relations and inference systems. It also defines the notion of a family of consequence relations and of redundancy criteria. This corresponds to sections 2.1 and 2.2 of the report.\ theory Calculus imports Ordered_Resolution_Prover.Lazy_List_Liminf Ordered_Resolution_Prover.Lazy_List_Chain begin subsection \Consequence Relations\ locale consequence_relation = fixes Bot :: "'f set" and entails :: "'f set \ 'f set \ bool" (infix "\" 50) assumes bot_not_empty: "Bot \ {}" and bot_entails_all: "B \ Bot \ {B} \ N1" and subset_entailed: "N2 \ N1 \ N1 \ N2" and all_formulas_entailed: "(\C \ N2. N1 \ {C}) \ N1 \ N2" and entails_trans[trans]: "N1 \ N2 \ N2 \ N3 \ N1 \ N3" begin lemma entail_set_all_formulas: "N1 \ N2 \ (\C \ N2. N1 \ {C})" by (meson all_formulas_entailed empty_subsetI insert_subset subset_entailed entails_trans) lemma entail_union: "N \ N1 \ N \ N2 \ N \ N1 \ N2" using entail_set_all_formulas[of N N1] entail_set_all_formulas[of N N2] entail_set_all_formulas[of N "N1 \ N2"] by blast lemma entail_unions: "(\i \ I. N \ Ni i) \ N \ \ (Ni ` I)" using entail_set_all_formulas[of N "\ (Ni ` I)"] entail_set_all_formulas[of N] Complete_Lattices.UN_ball_bex_simps(2)[of Ni I "\C. N \ {C}", symmetric] by meson lemma entail_all_bot: "(\B \ Bot. N \ {B}) \ (\B' \ Bot. N \ {B'})" using bot_entails_all entails_trans by blast lemma entails_trans_strong: "N1 \ N2 \ N1 \ N2 \ N3 \ N1 \ N3" by (meson entail_union entails_trans order_refl subset_entailed) end subsection \Families of Consequence Relations\ locale consequence_relation_family = fixes Bot :: "'f set" and Q :: "'q set" and entails_q :: "'q \ ('f set \ 'f set \ bool)" assumes Q_nonempty: "Q \ {}" and q_cons_rel: "\q \ Q. consequence_relation Bot (entails_q q)" begin lemma bot_not_empty: "Bot \ {}" using Q_nonempty consequence_relation.bot_not_empty consequence_relation_family.q_cons_rel consequence_relation_family_axioms by blast -definition entails_Q :: "'f set \ 'f set \ bool" (infix "\Q" 50) where +definition entails :: "'f set \ 'f set \ bool" (infix "\Q" 50) where "N1 \Q N2 \ (\q \ Q. entails_q q N1 N2)" (* lem:intersection-of-conseq-rel *) -lemma intersect_cons_rel_family: "consequence_relation Bot entails_Q" - unfolding consequence_relation_def entails_Q_def +lemma intersect_cons_rel_family: "consequence_relation Bot entails" + unfolding consequence_relation_def entails_def by (intro conjI bot_not_empty) (metis consequence_relation_def q_cons_rel)+ end subsection \Inference Systems\ datatype 'f inference = Infer (prems_of: "'f list") (concl_of: "'f") locale inference_system = fixes Inf :: \'f inference set\ begin definition Inf_from :: "'f set \ 'f inference set" where "Inf_from N = {\ \ Inf. set (prems_of \) \ N}" definition Inf_from2 :: "'f set \ 'f set \ 'f inference set" where "Inf_from2 N M = Inf_from (N \ M) - Inf_from (N - M)" lemma Inf_if_Inf_from: "\ \ Inf_from N \ \ \ Inf" unfolding Inf_from_def by simp lemma Inf_if_Inf_from2: "\ \ Inf_from2 N M \ \ \ Inf" unfolding Inf_from2_def Inf_from_def by simp lemma Inf_from2_alt: "Inf_from2 N M = {\ \ Inf. \ \ Inf_from (N \ M) \ set (prems_of \) \ M \ {}}" unfolding Inf_from_def Inf_from2_def by auto lemma Inf_from_mono: "N \ N' \ Inf_from N \ Inf_from N'" unfolding Inf_from_def by auto lemma Inf_from2_mono: "N \ N' \ M \ M' \ Inf_from2 N M \ Inf_from2 N' M'" unfolding Inf_from2_alt using Inf_from_mono[of "N \ M" "N' \ M'"] by auto end subsection \Families of Inference Systems\ locale inference_system_family = fixes Q :: "'q set" and Inf_q :: "'q \ 'f inference set" assumes Q_nonempty: "Q \ {}" begin definition Inf_from_q :: "'q \ 'f set \ 'f inference set" where "Inf_from_q q = inference_system.Inf_from (Inf_q q)" definition Inf_from2_q :: "'q \ 'f set \ 'f set \ 'f inference set" where "Inf_from2_q q = inference_system.Inf_from2 (Inf_q q)" lemma Inf_from2_q_alt: "Inf_from2_q q N M = {\ \ Inf_q q. \ \ Inf_from_q q (N \ M) \ set (prems_of \) \ M \ {}}" unfolding Inf_from_q_def Inf_from2_q_def inference_system.Inf_from2_alt by auto end subsection \Calculi Based on a Single Redundancy Criterion\ locale calculus = inference_system Inf + consequence_relation Bot entails for Bot :: "'f set" and Inf :: \'f inference set\ and entails :: "'f set \ 'f set \ bool" (infix "\" 50) + fixes - Red_Inf :: "'f set \ 'f inference set" and + Red_I :: "'f set \ 'f inference set" and Red_F :: "'f set \ 'f set" assumes - Red_Inf_to_Inf: "Red_Inf N \ Inf" and + Red_I_to_Inf: "Red_I N \ Inf" and Red_F_Bot: "B \ Bot \ N \ {B} \ N - Red_F N \ {B}" and Red_F_of_subset: "N \ N' \ Red_F N \ Red_F N'" and - Red_Inf_of_subset: "N \ N' \ Red_Inf N \ Red_Inf N'" and + Red_I_of_subset: "N \ N' \ Red_I N \ Red_I N'" and Red_F_of_Red_F_subset: "N' \ Red_F N \ Red_F N \ Red_F (N - N')" and - Red_Inf_of_Red_F_subset: "N' \ Red_F N \ Red_Inf N \ Red_Inf (N - N')" and - Red_Inf_of_Inf_to_N: "\ \ Inf \ concl_of \ \ N \ \ \ Red_Inf N" + Red_I_of_Red_F_subset: "N' \ Red_F N \ Red_I N \ Red_I (N - N')" and + Red_I_of_Inf_to_N: "\ \ Inf \ concl_of \ \ N \ \ \ Red_I N" begin -lemma Red_Inf_of_Inf_to_N_subset: "{\ \ Inf. concl_of \ \ N} \ Red_Inf N" - using Red_Inf_of_Inf_to_N by blast +lemma Red_I_of_Inf_to_N_subset: "{\ \ Inf. concl_of \ \ N} \ Red_I N" + using Red_I_of_Inf_to_N by blast (* lem:red-concl-implies-red-inf *) lemma red_concl_to_red_inf: assumes i_in: "\ \ Inf" and concl: "concl_of \ \ Red_F N" - shows "\ \ Red_Inf N" + shows "\ \ Red_I N" proof - - have "\ \ Red_Inf (Red_F N)" by (simp add: Red_Inf_of_Inf_to_N i_in concl) - then have i_in_Red: "\ \ Red_Inf (N \ Red_F N)" by (simp add: Red_Inf_of_Inf_to_N concl i_in) + have "\ \ Red_I (Red_F N)" by (simp add: Red_I_of_Inf_to_N i_in concl) + then have i_in_Red: "\ \ Red_I (N \ Red_F N)" by (simp add: Red_I_of_Inf_to_N concl i_in) have red_n_subs: "Red_F N \ Red_F (N \ Red_F N)" by (simp add: Red_F_of_subset) - then have "\ \ Red_Inf ((N \ Red_F N) - (Red_F N - N))" using Red_Inf_of_Red_F_subset i_in_Red + then have "\ \ Red_I ((N \ Red_F N) - (Red_F N - N))" using Red_I_of_Red_F_subset i_in_Red by (meson Diff_subset subsetCE subset_trans) then show ?thesis by (metis Diff_cancel Diff_subset Un_Diff Un_Diff_cancel contra_subsetD - calculus.Red_Inf_of_subset calculus_axioms sup_bot.right_neutral) + calculus.Red_I_of_subset calculus_axioms sup_bot.right_neutral) qed definition saturated :: "'f set \ bool" where - "saturated N \ Inf_from N \ Red_Inf N" + "saturated N \ Inf_from N \ Red_I N" definition reduc_saturated :: "'f set \ bool" where - "reduc_saturated N \ Inf_from (N - Red_F N) \ Red_Inf N" + "reduc_saturated N \ Inf_from (N - Red_F N) \ Red_I N" -lemma Red_Inf_without_red_F: - "Red_Inf (N - Red_F N) = Red_Inf N" - using Red_Inf_of_subset [of "N - Red_F N" N] - and Red_Inf_of_Red_F_subset [of "Red_F N" N] by blast +lemma Red_I_without_red_F: + "Red_I (N - Red_F N) = Red_I N" + using Red_I_of_subset [of "N - Red_F N" N] + and Red_I_of_Red_F_subset [of "Red_F N" N] by blast lemma saturated_without_red_F: assumes saturated: "saturated N" shows "saturated (N - Red_F N)" proof - have "Inf_from (N - Red_F N) \ Inf_from N" unfolding Inf_from_def by auto - also have "Inf_from N \ Red_Inf N" using saturated unfolding saturated_def by auto - also have "Red_Inf N \ Red_Inf (N - Red_F N)" using Red_Inf_of_Red_F_subset by auto - finally have "Inf_from (N - Red_F N) \ Red_Inf (N - Red_F N)" by auto + also have "Inf_from N \ Red_I N" using saturated unfolding saturated_def by auto + also have "Red_I N \ Red_I (N - Red_F N)" using Red_I_of_Red_F_subset by auto + finally have "Inf_from (N - Red_F N) \ Red_I (N - Red_F N)" by auto then show ?thesis unfolding saturated_def by auto qed definition fair :: "'f set llist \ bool" where - "fair D \ Inf_from (Liminf_llist D) \ Sup_llist (lmap Red_Inf D)" + "fair D \ Inf_from (Liminf_llist D) \ Sup_llist (lmap Red_I D)" inductive "derive" :: "'f set \ 'f set \ bool" (infix "\Red" 50) where derive: "M - N \ Red_F N \ M \Red N" lemma gt_Max_notin: \finite A \ A \ {} \ x > Max A \ x \ A\ by auto lemma equiv_Sup_Liminf: assumes in_Sup: "C \ Sup_llist D" and not_in_Liminf: "C \ Liminf_llist D" shows "\i \ {i. enat (Suc i) < llength D}. C \ lnth D i - lnth D (Suc i)" proof - obtain i where C_D_i: "C \ Sup_upto_llist D (enat i)" and "enat i < llength D" using elem_Sup_llist_imp_Sup_upto_llist in_Sup by fast then obtain j where j: "j \ i \ enat j < llength D \ C \ lnth D j" using not_in_Liminf unfolding Sup_upto_llist_def chain_def Liminf_llist_def by auto obtain k where k: "C \ lnth D k" "enat k < llength D" "k \ i" using C_D_i unfolding Sup_upto_llist_def by auto let ?S = "{i. i < j \ i \ k \ C \ lnth D i}" define l where "l = Max ?S" have \k \ {i. i < j \ k \ i \ C \ lnth D i}\ using k j by (auto simp: order.order_iff_strict) then have nempty: "{i. i < j \ k \ i \ C \ lnth D i} \ {}" by auto then have l_prop: "l < j \ l \ k \ C \ lnth D l" using Max_in[of ?S, OF _ nempty] unfolding l_def by auto then have "C \ lnth D l - lnth D (Suc l)" using j gt_Max_notin[OF _ nempty, of "Suc l"] unfolding l_def[symmetric] by (auto intro: Suc_lessI) then show ?thesis proof (rule bexI[of _ l]) show "l \ {i. enat (Suc i) < llength D}" using l_prop j by (clarify, metis Suc_leI dual_order.order_iff_strict enat_ord_simps(2) less_trans) qed qed (* lem:nonpersistent-is-redundant *) lemma Red_in_Sup: assumes deriv: "chain (\Red) D" shows "Sup_llist D - Liminf_llist D \ Red_F (Sup_llist D)" proof fix C assume C_in_subset: "C \ Sup_llist D - Liminf_llist D" { fix C i assume in_ith_elem: "C \ lnth D i - lnth D (Suc i)" and i: "enat (Suc i) < llength D" have "lnth D i \Red lnth D (Suc i)" using i deriv in_ith_elem chain_lnth_rel by auto then have "C \ Red_F (lnth D (Suc i))" using in_ith_elem derive.cases by blast then have "C \ Red_F (Sup_llist D)" using Red_F_of_subset by (meson contra_subsetD i lnth_subset_Sup_llist) } then show "C \ Red_F (Sup_llist D)" using equiv_Sup_Liminf[of C] C_in_subset by fast qed (* lem:redundant-remains-redundant-during-run 1/2 *) -lemma Red_Inf_subset_Liminf: +lemma Red_I_subset_Liminf: assumes deriv: \chain (\Red) D\ and i: \enat i < llength D\ - shows \Red_Inf (lnth D i) \ Red_Inf (Liminf_llist D)\ + shows \Red_I (lnth D i) \ Red_I (Liminf_llist D)\ proof - - have Sup_in_diff: \Red_Inf (Sup_llist D) \ Red_Inf (Sup_llist D - (Sup_llist D - Liminf_llist D))\ - using Red_Inf_of_Red_F_subset[OF Red_in_Sup] deriv by auto + have Sup_in_diff: \Red_I (Sup_llist D) \ Red_I (Sup_llist D - (Sup_llist D - Liminf_llist D))\ + using Red_I_of_Red_F_subset[OF Red_in_Sup] deriv by auto also have \Sup_llist D - (Sup_llist D - Liminf_llist D) = Liminf_llist D\ by (simp add: Liminf_llist_subset_Sup_llist double_diff) - then have Red_Inf_Sup_in_Liminf: \Red_Inf (Sup_llist D) \ Red_Inf (Liminf_llist D)\ + then have Red_I_Sup_in_Liminf: \Red_I (Sup_llist D) \ Red_I (Liminf_llist D)\ using Sup_in_diff by auto have \lnth D i \ Sup_llist D\ unfolding Sup_llist_def using i by blast - then have "Red_Inf (lnth D i) \ Red_Inf (Sup_llist D)" using Red_Inf_of_subset + then have "Red_I (lnth D i) \ Red_I (Sup_llist D)" using Red_I_of_subset unfolding Sup_llist_def by auto - then show ?thesis using Red_Inf_Sup_in_Liminf by auto + then show ?thesis using Red_I_Sup_in_Liminf by auto qed (* lem:redundant-remains-redundant-during-run 2/2 *) lemma Red_F_subset_Liminf: assumes deriv: \chain (\Red) D\ and i: \enat i < llength D\ shows \Red_F (lnth D i) \ Red_F (Liminf_llist D)\ proof - have Sup_in_diff: \Red_F (Sup_llist D) \ Red_F (Sup_llist D - (Sup_llist D - Liminf_llist D))\ using Red_F_of_Red_F_subset[OF Red_in_Sup] deriv by auto also have \Sup_llist D - (Sup_llist D - Liminf_llist D) = Liminf_llist D\ by (simp add: Liminf_llist_subset_Sup_llist double_diff) then have Red_F_Sup_in_Liminf: \Red_F (Sup_llist D) \ Red_F (Liminf_llist D)\ using Sup_in_diff by auto have \lnth D i \ Sup_llist D\ unfolding Sup_llist_def using i by blast then have "Red_F (lnth D i) \ Red_F (Sup_llist D)" using Red_F_of_subset unfolding Sup_llist_def by auto then show ?thesis using Red_F_Sup_in_Liminf by auto qed (* lem:N-i-is-persistent-or-redundant *) lemma i_in_Liminf_or_Red_F: assumes deriv: \chain (\Red) D\ and i: \enat i < llength D\ shows \lnth D i \ Red_F (Liminf_llist D) \ Liminf_llist D\ proof (rule,rule) fix C assume C: \C \ lnth D i\ and C_not_Liminf: \C \ Liminf_llist D\ have \C \ Sup_llist D\ unfolding Sup_llist_def using C i by auto then obtain j where j: \C \ lnth D j - lnth D (Suc j)\ \enat (Suc j) < llength D\ using equiv_Sup_Liminf[of C D] C_not_Liminf by auto then have \C \ Red_F (lnth D (Suc j))\ using deriv by (meson chain_lnth_rel contra_subsetD derive.cases) then show \C \ Red_F (Liminf_llist D)\ using Red_F_subset_Liminf[of D "Suc j"] deriv j(2) by blast qed (* lem:fairness-implies-saturation *) lemma fair_implies_Liminf_saturated: assumes deriv: \chain (\Red) D\ and fair: \fair D\ shows \saturated (Liminf_llist D)\ unfolding saturated_def proof fix \ assume \: \\ \ Inf_from (Liminf_llist D)\ - have \\ \ Sup_llist (lmap Red_Inf D)\ using fair \ unfolding fair_def by auto - then obtain i where i: \enat i < llength D\ \\ \ Red_Inf (lnth D i)\ + have \\ \ Sup_llist (lmap Red_I D)\ using fair \ unfolding fair_def by auto + then obtain i where i: \enat i < llength D\ \\ \ Red_I (lnth D i)\ unfolding Sup_llist_def by auto - then show \\ \ Red_Inf (Liminf_llist D)\ - using deriv i_in_Liminf_or_Red_F[of D i] Red_Inf_subset_Liminf by blast + then show \\ \ Red_I (Liminf_llist D)\ + using deriv i_in_Liminf_or_Red_F[of D i] Red_I_subset_Liminf by blast qed end locale statically_complete_calculus = calculus + assumes statically_complete: "B \ Bot \ saturated N \ N \ {B} \ \B'\Bot. B' \ N" begin lemma dynamically__complete_Liminf: fixes B D assumes bot_elem: \B \ Bot\ and deriv: \chain (\Red) D\ and fair: \fair D\ and unsat: \lhd D \ {B}\ shows \\B'\Bot. B' \ Liminf_llist D\ proof - note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]] have non_empty: \\ lnull D\ using chain_not_lnull[OF deriv] . have subs: \lhd D \ Sup_llist D\ using lhd_subset_Sup_llist[of D] non_empty by (simp add: lhd_conv_lnth) have \Sup_llist D \ {B}\ using unsat subset_entailed[OF subs] entails_trans[of "Sup_llist D" "lhd D"] by auto then have Sup_no_Red: \Sup_llist D - Red_F (Sup_llist D) \ {B}\ using bot_elem Red_F_Bot by auto have Sup_no_Red_in_Liminf: \Sup_llist D - Red_F (Sup_llist D) \ Liminf_llist D\ using deriv Red_in_Sup by auto have Liminf_entails_Bot: \Liminf_llist D \ {B}\ using Sup_no_Red subset_entailed[OF Sup_no_Red_in_Liminf] entails_trans by blast have \saturated (Liminf_llist D)\ using deriv fair fair_implies_Liminf_saturated unfolding saturated_def by auto then show ?thesis using bot_elem statically_complete Liminf_entails_Bot by auto qed end locale dynamically_complete_calculus = calculus + assumes dynamically__complete: "B \ Bot \ chain (\Red) D \ fair D \ lhd D \ {B} \ \i \ {i. enat i < llength D}. \B'\Bot. B' \ lnth D i" begin (* lem:dynamic-ref-compl-implies-static *) sublocale statically_complete_calculus proof fix B N assume bot_elem: \B \ Bot\ and saturated_N: "saturated N" and refut_N: "N \ {B}" define D where "D = LCons N LNil" have[simp]: \\ lnull D\ by (auto simp: D_def) have deriv_D: \chain (\Red) D\ by (simp add: chain.chain_singleton D_def) have liminf_is_N: "Liminf_llist D = N" by (simp add: D_def Liminf_llist_LCons) have head_D: "N = lhd D" by (simp add: D_def) - have "Sup_llist (lmap Red_Inf D) = Red_Inf N" by (simp add: D_def) + have "Sup_llist (lmap Red_I D) = Red_I N" by (simp add: D_def) then have fair_D: "fair D" using saturated_N by (simp add: fair_def saturated_def liminf_is_N) obtain i B' where B'_is_bot: \B' \ Bot\ and B'_in: "B' \ lnth D i" and \i < llength D\ using dynamically__complete[of B D] bot_elem fair_D head_D saturated_N deriv_D refut_N by auto then have "i = 0" by (auto simp: D_def enat_0_iff) show \\B'\Bot. B' \ N\ using B'_is_bot B'_in unfolding \i = 0\ head_D[symmetric] D_def by auto qed end (* lem:static-ref-compl-implies-dynamic *) sublocale statically_complete_calculus \ dynamically_complete_calculus proof fix B D assume \B \ Bot\ and \chain (\Red) D\ and \fair D\ and \lhd D \ {B}\ then have \\B'\Bot. B' \ Liminf_llist D\ by (rule dynamically__complete_Liminf) then show \\i\{i. enat i < llength D}. \B'\Bot. B' \ lnth D i\ unfolding Liminf_llist_def by auto qed end diff --git a/thys/Saturation_Framework/Calculus_Variations.thy b/thys/Saturation_Framework/Calculus_Variations.thy --- a/thys/Saturation_Framework/Calculus_Variations.thy +++ b/thys/Saturation_Framework/Calculus_Variations.thy @@ -1,435 +1,435 @@ (* Title: Variations on a Theme * Author: Sophie Tourret , 2018-2020 *) section \Variations on a Theme\ text \In this section, section 2.4 of the report is covered, demonstrating that various notions of redundancy are equivalent.\ theory Calculus_Variations imports Calculus begin -locale reduced_calculus = calculus Bot Inf entails Red_Inf Red_F +locale reduced_calculus = calculus Bot Inf entails Red_I Red_F for Bot :: "'f set" and Inf :: \'f inference set\ and entails :: "'f set \ 'f set \ bool" (infix "\" 50) and - Red_Inf :: "'f set \ 'f inference set" and + Red_I :: "'f set \ 'f inference set" and Red_F :: "'f set \ 'f set" + assumes - inf_in_red_inf: "Inf_from2 UNIV (Red_F N) \ Red_Inf N" + inf_in_red_inf: "Inf_from2 UNIV (Red_F N) \ Red_I N" begin (* lem:reduced-rc-implies-sat-equiv-reduced-sat *) lemma sat_eq_reduc_sat: "saturated N \ reduc_saturated N" proof fix N assume "saturated N" then show "reduc_saturated N" - using Red_Inf_without_red_F saturated_without_red_F + using Red_I_without_red_F saturated_without_red_F unfolding saturated_def reduc_saturated_def by blast next fix N assume red_sat_n: "reduc_saturated N" show "saturated N" unfolding saturated_def using red_sat_n inf_in_red_inf unfolding reduc_saturated_def Inf_from_def Inf_from2_def by blast qed end locale reducedly_statically_complete_calculus = calculus + assumes reducedly_statically_complete: "B \ Bot \ reduc_saturated N \ N \ {B} \ \B'\Bot. B' \ N" locale reducedly_statically_complete_reduced_calculus = reduced_calculus + assumes reducedly_statically_complete: "B \ Bot \ reduc_saturated N \ N \ {B} \ \B'\Bot. B' \ N" begin sublocale reducedly_statically_complete_calculus by (simp add: calculus_axioms reducedly_statically_complete reducedly_statically_complete_calculus_axioms.intro reducedly_statically_complete_calculus_def) (* cor:reduced-rc-implies-st-ref-comp-equiv-reduced-st-ref-comp 1/2 *) sublocale statically_complete_calculus proof fix B N assume bot_elem: \B \ Bot\ and saturated_N: "saturated N" and refut_N: "N \ {B}" have reduc_saturated_N: "reduc_saturated N" using saturated_N sat_eq_reduc_sat by blast show "\B'\Bot. B' \ N" using reducedly_statically_complete[OF bot_elem reduc_saturated_N refut_N] . qed end context reduced_calculus begin (* cor:reduced-rc-implies-st-ref-comp-equiv-reduced-st-ref-comp 2/2 *) lemma stat_ref_comp_imp_red_stat_ref_comp: - "statically_complete_calculus Bot Inf entails Red_Inf Red_F \ - reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F" + "statically_complete_calculus Bot Inf entails Red_I Red_F \ + reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F" proof fix B N assume - stat_ref_comp: "statically_complete_calculus Bot Inf (\) Red_Inf Red_F" and + stat_ref_comp: "statically_complete_calculus Bot Inf (\) Red_I Red_F" and bot_elem: \B \ Bot\ and saturated_N: "reduc_saturated N" and refut_N: "N \ {B}" have reduc_saturated_N: "saturated N" using saturated_N sat_eq_reduc_sat by blast show "\B'\Bot. B' \ N" using statically_complete_calculus.statically_complete[OF stat_ref_comp bot_elem reduc_saturated_N refut_N] . qed end context calculus begin -definition Red_Red_Inf :: "'f set \ 'f inference set" where - "Red_Red_Inf N = Red_Inf N \ Inf_from2 UNIV (Red_F N)" +definition Red_Red_I :: "'f set \ 'f inference set" where + "Red_Red_I N = Red_I N \ Inf_from2 UNIV (Red_F N)" -lemma reduced_calc_is_calc: "calculus Bot Inf entails Red_Red_Inf Red_F" +lemma reduced_calc_is_calc: "calculus Bot Inf entails Red_Red_I Red_F" proof fix N - show "Red_Red_Inf N \ Inf" - unfolding Red_Red_Inf_def Inf_from2_def Inf_from_def using Red_Inf_to_Inf by auto + show "Red_Red_I N \ Inf" + unfolding Red_Red_I_def Inf_from2_def Inf_from_def using Red_I_to_Inf by auto next fix B N assume b_in: "B \ Bot" and n_entails: "N \ {B}" show "N - Red_F N \ {B}" by (simp add: Red_F_Bot b_in n_entails) next fix N N' :: "'f set" assume "N \ N'" then show "Red_F N \ Red_F N'" by (simp add: Red_F_of_subset) next fix N N' :: "'f set" assume n_in: "N \ N'" then have "Inf_from (UNIV - (Red_F N')) \ Inf_from (UNIV - (Red_F N))" using Red_F_of_subset[OF n_in] unfolding Inf_from_def by auto then have "Inf_from2 UNIV (Red_F N) \ Inf_from2 UNIV (Red_F N')" unfolding Inf_from2_def by auto - then show "Red_Red_Inf N \ Red_Red_Inf N'" - unfolding Red_Red_Inf_def using Red_Inf_of_subset[OF n_in] by blast + then show "Red_Red_I N \ Red_Red_I N'" + unfolding Red_Red_I_def using Red_I_of_subset[OF n_in] by blast next fix N N' :: "'f set" assume "N' \ Red_F N" then show "Red_F N \ Red_F (N - N')" by (simp add: Red_F_of_Red_F_subset) next fix N N' :: "'f set" assume np_subs: "N' \ Red_F N" have "Red_F N \ Red_F (N - N')" by (simp add: Red_F_of_Red_F_subset np_subs) then have "Inf_from (UNIV - (Red_F (N - N'))) \ Inf_from (UNIV - (Red_F N))" by (metis Diff_subset Red_F_of_subset eq_iff) then have "Inf_from2 UNIV (Red_F N) \ Inf_from2 UNIV (Red_F (N - N'))" unfolding Inf_from2_def by auto - then show "Red_Red_Inf N \ Red_Red_Inf (N - N')" - unfolding Red_Red_Inf_def using Red_Inf_of_Red_F_subset[OF np_subs] by blast + then show "Red_Red_I N \ Red_Red_I (N - N')" + unfolding Red_Red_I_def using Red_I_of_Red_F_subset[OF np_subs] by blast next fix \ N assume "\ \ Inf" "concl_of \ \ N" - then show "\ \ Red_Red_Inf N" - by (simp add: Red_Inf_of_Inf_to_N Red_Red_Inf_def) + then show "\ \ Red_Red_I N" + by (simp add: Red_I_of_Inf_to_N Red_Red_I_def) qed -lemma inf_subs_reduced_red_inf: "Inf_from2 UNIV (Red_F N) \ Red_Red_Inf N" - unfolding Red_Red_Inf_def by simp +lemma inf_subs_reduced_red_inf: "Inf_from2 UNIV (Red_F N) \ Red_Red_I N" + unfolding Red_Red_I_def by simp (* lem:red'-is-reduced-redcrit *) text \The following is a lemma and not a sublocale as was previously used in similar cases. Here, a sublocale cannot be used because it would create an infinitely descending chain of sublocales. \ -lemma reduc_calc: "reduced_calculus Bot Inf entails Red_Red_Inf Red_F" +lemma reduc_calc: "reduced_calculus Bot Inf entails Red_Red_I Red_F" using inf_subs_reduced_red_inf reduced_calc_is_calc by (simp add: reduced_calculus.intro reduced_calculus_axioms_def) -interpretation reduc_calc: reduced_calculus Bot Inf entails Red_Red_Inf Red_F +interpretation reduc_calc: reduced_calculus Bot Inf entails Red_Red_I Red_F by (fact reduc_calc) (* lem:saturation-red-vs-red'-1 *) lemma sat_imp_red_calc_sat: "saturated N \ reduc_calc.saturated N" - unfolding saturated_def reduc_calc.saturated_def Red_Red_Inf_def by blast + unfolding saturated_def reduc_calc.saturated_def Red_Red_I_def by blast (* lem:saturation-red-vs-red'-2 1/2 (i) \ (ii) *) lemma red_sat_eq_red_calc_sat: "reduc_saturated N \ reduc_calc.saturated N" proof assume red_sat_n: "reduc_saturated N" show "reduc_calc.saturated N" unfolding reduc_calc.saturated_def proof fix \ assume i_in: "\ \ Inf_from N" - show "\ \ Red_Red_Inf N" + show "\ \ Red_Red_I N" using i_in red_sat_n - unfolding reduc_saturated_def Inf_from2_def Inf_from_def Red_Red_Inf_def by blast + unfolding reduc_saturated_def Inf_from2_def Inf_from_def Red_Red_I_def by blast qed next assume red_sat_n: "reduc_calc.saturated N" show "reduc_saturated N" unfolding reduc_saturated_def proof fix \ assume i_in: "\ \ Inf_from (N - Red_F N)" - show "\ \ Red_Inf N" + show "\ \ Red_I N" using i_in red_sat_n - unfolding Inf_from_def reduc_calc.saturated_def Red_Red_Inf_def Inf_from2_def by blast + unfolding Inf_from_def reduc_calc.saturated_def Red_Red_I_def Inf_from2_def by blast qed qed (* lem:saturation-red-vs-red'-2 2/2 (i) \ (iii) *) lemma red_sat_eq_sat: "reduc_saturated N \ saturated (N - Red_F N)" - unfolding reduc_saturated_def saturated_def by (simp add: Red_Inf_without_red_F) + unfolding reduc_saturated_def saturated_def by (simp add: Red_I_without_red_F) (* thm:reduced-stat-ref-compl 1/3 (i) \ (iii) *) -theorem stat_is_stat_red: "statically_complete_calculus Bot Inf entails Red_Inf Red_F \ - statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" +theorem stat_is_stat_red: "statically_complete_calculus Bot Inf entails Red_I Red_F \ + statically_complete_calculus Bot Inf entails Red_Red_I Red_F" proof assume - stat_ref1: "statically_complete_calculus Bot Inf entails Red_Inf Red_F" - show "statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + stat_ref1: "statically_complete_calculus Bot Inf entails Red_I Red_F" + show "statically_complete_calculus Bot Inf entails Red_Red_I Red_F" using reduc_calc.calculus_axioms unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def proof show "\B N. B \ Bot \ reduc_calc.saturated N \ N \ {B} \ (\B'\Bot. B' \ N)" proof (clarify) fix B N assume b_in: "B \ Bot" and n_sat: "reduc_calc.saturated N" and n_imp_b: "N \ {B}" have "saturated (N - Red_F N)" using red_sat_eq_red_calc_sat[of N] red_sat_eq_sat[of N] n_sat by blast moreover have "(N - Red_F N) \ {B}" using n_imp_b b_in by (simp add: reduc_calc.Red_F_Bot) ultimately show "\B'\Bot. B'\ N" using stat_ref1 by (meson DiffD1 b_in statically_complete_calculus.statically_complete) qed qed next assume - stat_ref3: "statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" - show "statically_complete_calculus Bot Inf entails Red_Inf Red_F" + stat_ref3: "statically_complete_calculus Bot Inf entails Red_Red_I Red_F" + show "statically_complete_calculus Bot Inf entails Red_I Red_F" unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def using calculus_axioms proof show "\B N. B \ Bot \ saturated N \ N \ {B} \ (\B'\Bot. B' \ N)" proof clarify fix B N assume b_in: "B \ Bot" and n_sat: "saturated N" and n_imp_b: "N \ {B}" then show "\B'\ Bot. B' \ N" using stat_ref3 sat_imp_red_calc_sat[OF n_sat] by (meson statically_complete_calculus.statically_complete) qed qed qed (* thm:reduced-stat-ref-compl 2/3 (iv) \ (iii) *) theorem red_stat_red_is_stat_red: - "reducedly_statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F \ - statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + "reducedly_statically_complete_calculus Bot Inf entails Red_Red_I Red_F \ + statically_complete_calculus Bot Inf entails Red_Red_I Red_F" using reduc_calc.stat_ref_comp_imp_red_stat_ref_comp by (metis reduc_calc.sat_eq_reduc_sat reducedly_statically_complete_calculus.axioms(2) reducedly_statically_complete_calculus_axioms_def reduced_calc_is_calc statically_complete_calculus.intro statically_complete_calculus_axioms.intro) (* thm:reduced-stat-ref-compl 3/3 (ii) \ (iii) *) theorem red_stat_is_stat_red: - "reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F \ - statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + "reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F \ + statically_complete_calculus Bot Inf entails Red_Red_I Red_F" using reduc_calc.calculus_axioms calculus_axioms red_sat_eq_red_calc_sat unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def reducedly_statically_complete_calculus_def reducedly_statically_complete_calculus_axioms_def by blast lemma sup_red_f_in_red_liminf: "chain derive D \ Sup_llist (lmap Red_F D) \ Red_F (Liminf_llist D)" proof fix N assume deriv: "chain derive D" and n_in_sup: "N \ Sup_llist (lmap Red_F D)" obtain i0 where i_smaller: "enat i0 < llength D" and n_in: "N \ Red_F (lnth D i0)" using n_in_sup by (metis Sup_llist_imp_exists_index llength_lmap lnth_lmap) have "Red_F (lnth D i0) \ Red_F (Liminf_llist D)" using i_smaller by (simp add: deriv Red_F_subset_Liminf) then show "N \ Red_F (Liminf_llist D)" using n_in by fast qed lemma sup_red_inf_in_red_liminf: - "chain derive D \ Sup_llist (lmap Red_Inf D) \ Red_Inf (Liminf_llist D)" + "chain derive D \ Sup_llist (lmap Red_I D) \ Red_I (Liminf_llist D)" proof fix \ assume deriv: "chain derive D" and - i_in_sup: "\ \ Sup_llist (lmap Red_Inf D)" - obtain i0 where i_smaller: "enat i0 < llength D" and n_in: "\ \ Red_Inf (lnth D i0)" + i_in_sup: "\ \ Sup_llist (lmap Red_I D)" + obtain i0 where i_smaller: "enat i0 < llength D" and n_in: "\ \ Red_I (lnth D i0)" using i_in_sup unfolding Sup_llist_def by auto - have "Red_Inf (lnth D i0) \ Red_Inf (Liminf_llist D)" - using i_smaller by (simp add: deriv Red_Inf_subset_Liminf) - then show "\ \ Red_Inf (Liminf_llist D)" + have "Red_I (lnth D i0) \ Red_I (Liminf_llist D)" + using i_smaller by (simp add: deriv Red_I_subset_Liminf) + then show "\ \ Red_I (Liminf_llist D)" using n_in by fast qed definition reduc_fair :: "'f set llist \ bool" where "reduc_fair D \ - Inf_from (Liminf_llist D - Sup_llist (lmap Red_F D)) \ Sup_llist (lmap Red_Inf D)" + Inf_from (Liminf_llist D - Sup_llist (lmap Red_F D)) \ Sup_llist (lmap Red_I D)" (* lem:red-fairness-implies-red-saturation *) lemma reduc_fair_imp_Liminf_reduc_sat: "chain derive D \ reduc_fair D \ reduc_saturated (Liminf_llist D)" unfolding reduc_saturated_def proof - fix D assume deriv: "chain derive D" and red_fair: "reduc_fair D" have "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) \ Inf_from (Liminf_llist D - Sup_llist (lmap Red_F D))" using sup_red_f_in_red_liminf[OF deriv] unfolding Inf_from_def by blast - then have "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) \ Sup_llist (lmap Red_Inf D)" + then have "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) \ Sup_llist (lmap Red_I D)" using red_fair unfolding reduc_fair_def by simp - then show "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) \ Red_Inf (Liminf_llist D)" + then show "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) \ Red_I (Liminf_llist D)" using sup_red_inf_in_red_liminf[OF deriv] by fast qed end locale reducedly_dynamically_complete_calculus = calculus + assumes reducedly_dynamically__complete: "B \ Bot \ chain derive D \ reduc_fair D \ lhd D \ {B} \ \i \ {i. enat i < llength D}. \ B'\Bot. B' \ lnth D i" begin sublocale reducedly_statically_complete_calculus proof fix B N assume bot_elem: \B \ Bot\ and saturated_N: "reduc_saturated N" and refut_N: "N \ {B}" define D where "D = LCons N LNil" have[simp]: \\ lnull D\ by (auto simp: D_def) have deriv_D: \chain (\Red) D\ by (simp add: chain.chain_singleton D_def) have liminf_is_N: "Liminf_llist D = N" by (simp add: D_def Liminf_llist_LCons) have head_D: "N = lhd D" by (simp add: D_def) have "Sup_llist (lmap Red_F D) = Red_F N" by (simp add: D_def) - moreover have "Sup_llist (lmap Red_Inf D) = Red_Inf N" by (simp add: D_def) + moreover have "Sup_llist (lmap Red_I D) = Red_I N" by (simp add: D_def) ultimately have fair_D: "reduc_fair D" using saturated_N liminf_is_N unfolding reduc_fair_def reduc_saturated_def by (simp add: reduc_fair_def reduc_saturated_def liminf_is_N) obtain i B' where B'_is_bot: \B' \ Bot\ and B'_in: "B' \ lnth D i" and \i < llength D\ using reducedly_dynamically__complete[of B D] bot_elem fair_D head_D saturated_N deriv_D refut_N by auto then have "i = 0" by (auto simp: D_def enat_0_iff) show \\B'\Bot. B' \ N\ using B'_is_bot B'_in unfolding \i = 0\ head_D[symmetric] D_def by auto qed end sublocale reducedly_statically_complete_calculus \ reducedly_dynamically_complete_calculus proof fix B D assume bot_elem: \B \ Bot\ and deriv: \chain (\Red) D\ and fair: \reduc_fair D\ and unsat: \lhd D \ {B}\ have non_empty: \\ lnull D\ using chain_not_lnull[OF deriv] . have subs: \lhd D \ Sup_llist D\ using lhd_subset_Sup_llist[of D] non_empty by (simp add: lhd_conv_lnth) have \Sup_llist D \ {B}\ using unsat subset_entailed[OF subs] entails_trans[of "Sup_llist D" "lhd D"] by auto then have Sup_no_Red: \Sup_llist D - Red_F (Sup_llist D) \ {B}\ using bot_elem Red_F_Bot by auto have Sup_no_Red_in_Liminf: \Sup_llist D - Red_F (Sup_llist D) \ Liminf_llist D\ using deriv Red_in_Sup by auto have Liminf_entails_Bot: \Liminf_llist D \ {B}\ using Sup_no_Red subset_entailed[OF Sup_no_Red_in_Liminf] entails_trans by blast have \reduc_saturated (Liminf_llist D)\ using deriv fair reduc_fair_imp_Liminf_reduc_sat unfolding reduc_saturated_def by auto then have \\B'\Bot. B' \ Liminf_llist D\ using bot_elem reducedly_statically_complete Liminf_entails_Bot by auto then show \\i\{i. enat i < llength D}. \B'\Bot. B' \ lnth D i\ unfolding Liminf_llist_def by auto qed context calculus begin -lemma dyn_equiv_stat: "dynamically_complete_calculus Bot Inf entails Red_Inf Red_F = - statically_complete_calculus Bot Inf entails Red_Inf Red_F" +lemma dyn_equiv_stat: "dynamically_complete_calculus Bot Inf entails Red_I Red_F = + statically_complete_calculus Bot Inf entails Red_I Red_F" proof - assume "dynamically_complete_calculus Bot Inf entails Red_Inf Red_F" - then interpret dynamically_complete_calculus Bot Inf entails Red_Inf Red_F + assume "dynamically_complete_calculus Bot Inf entails Red_I Red_F" + then interpret dynamically_complete_calculus Bot Inf entails Red_I Red_F by simp - show "statically_complete_calculus Bot Inf entails Red_Inf Red_F" + show "statically_complete_calculus Bot Inf entails Red_I Red_F" by (simp add: statically_complete_calculus_axioms) next - assume "statically_complete_calculus Bot Inf entails Red_Inf Red_F" - then interpret statically_complete_calculus Bot Inf entails Red_Inf Red_F + assume "statically_complete_calculus Bot Inf entails Red_I Red_F" + then interpret statically_complete_calculus Bot Inf entails Red_I Red_F by simp - show "dynamically_complete_calculus Bot Inf entails Red_Inf Red_F" + show "dynamically_complete_calculus Bot Inf entails Red_I Red_F" by (simp add: dynamically_complete_calculus_axioms) qed lemma red_dyn_equiv_red_stat: - "reducedly_dynamically_complete_calculus Bot Inf entails Red_Inf Red_F = - reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F" + "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F = + reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F" proof - assume "reducedly_dynamically_complete_calculus Bot Inf entails Red_Inf Red_F" - then interpret reducedly_dynamically_complete_calculus Bot Inf entails Red_Inf Red_F + assume "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F" + then interpret reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F by simp - show "reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F" + show "reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F" by (simp add: reducedly_statically_complete_calculus_axioms) next - assume "reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F" - then interpret reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F + assume "reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F" + then interpret reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F by simp - show "reducedly_dynamically_complete_calculus Bot Inf entails Red_Inf Red_F" + show "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F" by (simp add: reducedly_dynamically_complete_calculus_axioms) qed -interpretation reduc_calc: reduced_calculus Bot Inf entails Red_Red_Inf Red_F +interpretation reduc_calc: reduced_calculus Bot Inf entails Red_Red_I Red_F by (fact reduc_calc) (* thm:reduced-dyn-ref-compl 1/3 (v) \ (vii) *) theorem dyn_ref_eq_dyn_ref_red: - "dynamically_complete_calculus Bot Inf entails Red_Inf Red_F \ - dynamically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + "dynamically_complete_calculus Bot Inf entails Red_I Red_F \ + dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F" using dyn_equiv_stat stat_is_stat_red reduc_calc.dyn_equiv_stat by meson (* thm:reduced-dyn-ref-compl 2/3 (viii) \ (vii) *) theorem red_dyn_ref_red_eq_dyn_ref_red: - "reducedly_dynamically_complete_calculus Bot Inf entails Red_Red_Inf Red_F \ - dynamically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + "reducedly_dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F \ + dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F" using red_dyn_equiv_red_stat dyn_equiv_stat red_stat_red_is_stat_red by (simp add: reduc_calc.dyn_equiv_stat reduc_calc.red_dyn_equiv_red_stat) (* thm:reduced-dyn-ref-compl 3/3 (vi) \ (vii) *) theorem red_dyn_ref_eq_dyn_ref_red: - "reducedly_dynamically_complete_calculus Bot Inf entails Red_Inf Red_F \ - dynamically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + "reducedly_dynamically_complete_calculus Bot Inf entails Red_I Red_F \ + dynamically_complete_calculus Bot Inf entails Red_Red_I Red_F" using red_dyn_equiv_red_stat dyn_equiv_stat red_stat_is_stat_red reduc_calc.dyn_equiv_stat reduc_calc.red_dyn_equiv_red_stat by blast end end diff --git a/thys/Saturation_Framework/Given_Clause_Architectures.thy b/thys/Saturation_Framework/Given_Clause_Architectures.thy --- a/thys/Saturation_Framework/Given_Clause_Architectures.thy +++ b/thys/Saturation_Framework/Given_Clause_Architectures.thy @@ -1,1175 +1,1175 @@ (* Title: Given Clause Prover Architectures * Author: Sophie Tourret , 2019-2020 *) 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_Inf_q Red_F_q \_F_q \_Inf_q Inf_FL + entails_q Inf_G_q Red_I_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_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 \_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) 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 inf_never_active: "\ \ Inf_FL \ snd (concl_of \) \ active" and static_ref_comp: "statically_complete_calculus Bot_F Inf_F (\\\) - no_labels.Red_Inf_\_Q no_labels.Red_F_\_empty" + no_labels.Red_I_\ no_labels.Red_F_\_empty" 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 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_Inf_Q Red_F_Q +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_Inf_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q) (\g. Prec_FL)" + (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q) (\g. Prec_FL)" proof - have "tiebreaker_lifting 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 Cl Cl'. False)" + (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q) (\g Cl Cl'. False)" 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) + then have "standard_lifting Bot_FL Inf_FL Bot_G (Inf_G_q q) (entails_q q) (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_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_Inf_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q) (\g. Prec_FL)" + (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_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_Inf_q Red_F_q +sublocale lifting_intersection Inf_FL Bot_G Q Inf_G_q entails_q Red_I_q Red_F_q Bot_FL \_F_L_q \_Inf_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 "\RedL" 50) -lemma std_Red_Inf_Q_eq: "std.Red_Inf_Q = Red_Inf_\_Q" - unfolding Red_Inf_\_q_def Red_Inf_\_L_q_def by simp +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_Q_eq: "std.Red_F_Q = Red_F_\_empty" +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_Inf_Q Red_F_Q - by unfold_locales (use statically_complete std_Red_Inf_Q_eq in auto) +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) (* lem:redundant-labeled-inferences *) lemma labeled_red_inf_eq_red_inf: assumes i_in: "\ \ Inf_FL" - shows "\ \ Red_Inf_Q N \ to_F \ \ no_labels.Red_Inf_\_Q (fst ` N)" + shows "\ \ Red_I N \ to_F \ \ no_labels.Red_I_\ (fst ` N)" proof - assume i_in2: "\ \ Red_Inf_Q N" - then have "X \ Red_Inf_\_q ` Q \ \ \ X N" for X - unfolding Red_Inf_Q_def by blast - obtain X0 where "X0 \ Red_Inf_\_q ` Q" + 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_Inf_\_q q0 N" 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_Inf_\_q q0 (fst ` N)" + have "Y0 (fst ` N) = no_labels.Red_I_\_q q0 (fst ` N)" unfolding y0_is proof - show "to_F ` X0 N \ no_labels.Red_Inf_\_q q0 (fst ` N)" + 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_Inf_\_q q0 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: "((\_Inf_L_q q0 \0_FL) \ None \ - the (\_Inf_L_q q0 \0_FL) \ Red_Inf_q q0 (\_set_q q0 N)) + the (\_Inf_L_q q0 \0_FL) \ Red_I_q q0 (\_set_q q0 N)) \ ((\_Inf_L_q q0 \0_FL = None) \ \_F_L_q q0 (concl_of \0_FL) \ \_set_q q0 N \ Red_F_q q0 (\_set_q q0 N))" - unfolding Red_Inf_\_q_def by blast + 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: "\_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))" + have "the (\_Inf_q q0 \0) \ Red_I_q q0 (no_labels.\_set_q q0 (fst ` N))" using subs1 i0_to_i0_FL not_none 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 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 + 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_Inf_\_q q0 (fst ` N) \ to_F ` X0 N" + show "no_labels.Red_I_\_q q0 (fst ` N) \ to_F ` X0 N" proof fix \0 - assume i0_in: "\0 \ no_labels.Red_Inf_\_q q0 (fst ` N)" + assume i0_in: "\0 \ no_labels.Red_I_\_q q0 (fst ` N)" then have i0_in2: "\0 \ Inf_F" - unfolding no_labels.Red_Inf_\_q_def by blast + 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 (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 (\_set_q q0 N)) + the (\_Inf_L_q q0 \0_FL) \ Red_I_q q0 (\_set_q q0 N)) \ ((\_Inf_L_q q0 \0_FL = None) \ \_F_L_q q0 (concl_of \0_FL) \ (\_set_q q0 N \ Red_F_q q0 (\_set_q q0 N)))" - using i0_in i0_to_i0_FL concl_swap unfolding no_labels.Red_Inf_\_q_def by simp - then have "\0_FL \ Red_Inf_\_q q0 N" - using i0_FL_in unfolding Red_Inf_\_q_def by simp + 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_Inf_\_q ` Q \ to_F \ \ Y (fst ` N)" for Y - using i_in2 no_labels.Red_Inf_Q_def std_Red_Inf_Q_eq red_inf_impl by force - then show "to_F \ \ no_labels.Red_Inf_\_Q (fst ` N)" - unfolding Red_Inf_Q_def no_labels.Red_Inf_\_Q_def by blast + 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_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.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 + 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_Inf_\_q q N = {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_Inf_\_q q (fst ` N)}" for q + 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_Inf_\_q q N \ {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_Inf_\_q q (fst ` N)}" + 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_Inf_\_q q0 N" + i1_in: "\1 \ Red_I_\_q q0 N" have i1_in2: "\1 \ Inf_FL" - using i1_in unfolding Red_Inf_\_q_def by blast + 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 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 Red_Inf_\_q_def no_labels.Red_Inf_\_q_def by force - show "\1 \ {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_Inf_\_q q0 (fst ` N)}" + 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_Inf_\_q q (fst ` N)} \ Red_Inf_\_q q N" + 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_Inf_\_q q0 (fst ` N)}" + 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 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 (\_set_q q0 N)) + then have "((\_Inf_L_q q0 \1) \ None \ the (\_Inf_L_q q0 \1) \ Red_I_q q0 (\_set_q q0 N)) \ (\_Inf_L_q q0 \1 = None \ \_F_L_q q0 (concl_of \1) \ \_set_q q0 N \ Red_F_q q0 (\_set_q q0 N))" - using i1_in unfolding no_labels.Red_Inf_\_q_def by auto - then show "\1 \ Red_Inf_\_q q0 N" - using i1_in2 unfolding Red_Inf_\_q_def by blast + 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_Inf_\_q q N" if "q \ Q" for q - using that to_F_in2 i_in unfolding Red_Inf_\_q_def no_labels.Red_Inf_\_q_def by auto - then show "\ \ Red_Inf_\_Q N" - unfolding Red_Inf_\_Q_def by blast + 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 (* 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) \ Red_F_Q N\ + shows \(C, L) \ Red_F N\ proof - note assms - moreover have i: \C \ no_labels.Red_F_\_empty (fst ` N) \ (C, L) \ Red_F_Q N\ + 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.\_set_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 (\_set_q q N)" if "q \ Q" for q using that g_in_red by simp then show ?thesis - unfolding Red_F_Q_def Red_F_\_q_g_def by blast + unfolding Red_F_def Red_F_\_q_def by blast qed - moreover have ii: \\C' \ fst ` N. C' \\ C \ (C, L) \ Red_F_Q N\ + 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_g q N" if "q \ Q" for q - unfolding Red_F_\_q_g_def using that c'_l'_in c'_l'_prec by blast + 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_Q_def by blast + unfolding Red_F_def by blast qed - moreover have iii: \\(C', L') \ N. L' \l L \ C' \\ C \ (C, L) \ Red_F_Q N\ + 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_Q N" if "C' \\ C" + 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_g q N" if "q \ Q" for q - unfolding Red_F_\_q_g_def using that c'_l'_in c'_l'_prec by blast + 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_Q_def by blast + 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_Inf_q +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 \_Inf_q Inf_FL 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_Inf_q :: "'q \ 'g set \ '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 \_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) 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 Inf_FL_to_Inf_F 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_Q (N \ M') \ + 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_from2 (fst ` (active_subset N)) {C} - \ no_labels.Red_Inf_Q (fst ` (N \ {(C, active)} \ M)) \ + \ no_labels.Red_I (fst ` (N \ {(C, active)} \ M)) \ N1 \GC N2" 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 \ Red_F_Q (N \ M')" and + m_red: "M \ Red_F (N \ M')" and active_empty: "active_subset M' = {}" - have "N1 - N2 \ Red_F_Q N2" + have "N1 - N2 \ Red_F N2" using n1_is n2_is m_red by auto then show "N1 \RedL 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_Q N2" + 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_Q N2" - using std_Red_F_Q_eq by blast + ultimately have "N1 - N2 \ Red_F N2" + using std_Red_F_eq by blast then show "N1 \RedL N2" unfolding derive.simps by blast qed (* 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 init_state: "active_subset (lhd D) = {}" and final_state: "passive_subset (Liminf_llist D) = {}" shows "fair D" unfolding fair_def proof fix \ assume i_in: "\ \ Inf_from (Liminf_llist D)" 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 D = active_subset (Liminf_llist D)" using final_state unfolding passive_subset_def active_subset_def by blast then have i_in2: "\ \ 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 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 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 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 lhd_is by force 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 lhd_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 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 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 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)} \ lnth D (Suc n) = N \ {(C, active)} \ M \ L \ active \ active_subset M = {} \ no_labels.Inf_from2 (fst ` (active_subset N)) {C} - \ no_labels.Red_Inf_Q (fst ` (N \ {(C, active)} \ M)))" + \ no_labels.Red_I (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 \ Red_F_Q (N \ M') \ active_subset M' = {}) \ + N2 = N \ M' \ M \ Red_F (N \ M') \ active_subset M' = {}) \ (\N1 N C L N2 M. lnth D n = N1 \ lnth D (Suc n) = N2 \ N1 = N \ {(C, L)} \ N2 = N \ {(C, active)} \ M \ L \ active \ active_subset M = {} \ no_labels.Inf_from2 (fst ` (active_subset N)) {C} \ - no_labels.Red_Inf_Q (fst ` (N \ {(C, active)} \ M)))" + no_labels.Red_I (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.Inf_from2 (fst ` (active_subset N)) {C0} - \ no_labels.Red_Inf_Q (fst ` (N \ {(C0, active)} \ M))" and + \ no_labels.Red_I (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 "\ \ Inf_from2 (active_subset N) {(C0, active)}" using i_in_inf_fl unfolding Inf_from2_def Inf_from_def by blast then have "to_F \ \ no_labels.Inf_from2 (fst ` (active_subset N)) {C0}" unfolding to_F_def Inf_from2_def Inf_from_def no_labels.Inf_from2_def no_labels.Inf_from_def using Inf_FL_to_Inf_F by force - then have "to_F \ \ no_labels.Red_Inf_Q (fst ` (lnth D (Suc n)))" + then have "to_F \ \ no_labels.Red_I (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)))) + the (\_Inf_q q (to_F \)) \ Red_I_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.Red_Inf_Q_def no_labels.Red_Inf_\_q_def by blast - then have "\ \ Red_Inf_\_Q (lnth D (Suc n))" - using i_in_inf_fl unfolding Red_Inf_\_Q_def Red_Inf_\_q_def by (simp add: to_F_def) - then show "\ \ Sup_llist (lmap Red_Inf_\_Q D)" + unfolding to_F_def no_labels.Red_I_def no_labels.Red_I_\_q_def by blast + then have "\ \ Red_I_\ (lnth D (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_\ D)" unfolding Sup_llist_def using suc_n_length by auto qed theorem gc_complete_Liminf: assumes deriv: "chain (\GC) D" and init_state: "active_subset (lhd D) = {}" and final_state: "passive_subset (Liminf_llist D) = {}" and b_in: "B \ Bot_F" and - bot_entailed: "no_labels.entails_\_Q (fst ` lhd D) {B}" + bot_entailed: "no_labels.entails_\ (fst ` lhd D) {B}" shows "\BL \ Bot_FL. BL \ Liminf_llist D" 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_Q (lhd D) {(B, active)}" + have labeled_bot_entailed: "entails_\_L (lhd D) {(B, active)}" using labeled_entailment_lifting bot_entailed lhd_is by fastforce have fair: "fair D" 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 (* thm:gc-completeness *) theorem gc_complete: assumes deriv: "chain (\GC) D" and init_state: "active_subset (lhd D) = {}" and final_state: "passive_subset (Liminf_llist D) = {}" and b_in: "B \ Bot_F" and - bot_entailed: "no_labels.entails_\_Q (fst ` lhd D) {B}" + bot_entailed: "no_labels.entails_\ (fst ` lhd D) {B}" shows "\i. enat i < llength D \ (\BL \ Bot_FL. BL \ lnth D i)" proof - note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]] have "\BL\Bot_FL. BL \ Liminf_llist D" 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_Inf_q +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 \_Inf_q Inf_FL 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_Inf_q :: "'q \ 'g set \ '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 \_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) 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_Q (N \ M') \ + 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_from2 (fst ` (active_subset N)) {C} \ (T1, N1) \LGC (T2, N2)" | compute_infer: "T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ - \ \ no_labels.Red_Inf_Q (fst ` (N1 \ M)) \ (T1, N1) \LGC (T2, N2)" | + \ \ no_labels.Red_I (fst ` (N1 \ M)) \ (T1, N1) \LGC (T2, N2)" | delete_orphans: "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 \ length (prems_of \) = 0 \ \ \ no_labels.Inf_from N" unfolding no_labels.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 \ Red_F_Q (N \ M')" - have "N1 - N2 \ Red_F_Q N2" + 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 \RedL 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_Q N2" + ultimately have "{(C, L)} \ Red_F N2" using red_labeled_clauses by blast - then have "N1 - N2 \ Red_F_Q N2" - using std_Red_F_Q_eq using n1_is n2_is by blast + then have "N1 - N2 \ Red_F N2" + using std_Red_F_eq using n1_is n2_is by blast then show "N1 \RedL N2" unfolding derive.simps by blast next fix M assume n2_is: "N2 = N1 \ M" - have "N1 - N2 \ Red_F_Q N2" + have "N1 - N2 \ Red_F N2" using n2_is by blast then show "N1 \RedL N2" unfolding derive.simps by blast next assume n2_is: "N2 = N1" - have "N1 - N2 \ Red_F_Q N2" + have "N1 - N2 \ Red_F N2" using n2_is by blast then show "N1 \RedL N2" unfolding derive.simps by blast qed (* 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 init_state: "active_subset (snd (lhd D)) = {}" and final_state: "passive_subset (Liminf_llist (lmap snd D)) = {}" and no_prems_init_active: "\\ \ Inf_F. length (prems_of \) = 0 \ \ \ fst (lhd D)" and final_schedule: "Liminf_llist (lmap fst D) = {}" shows "fair (lmap snd D)" unfolding fair_def proof fix \ assume i_in: "\ \ Inf_from (Liminf_llist (lmap snd D))" 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 D) = active_subset (Liminf_llist (lmap snd D))" using final_state unfolding passive_subset_def active_subset_def by blast then have i_in2: "\ \ 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 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 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 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 lhd_is 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 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 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 (lhd D)" using no_prems_init_active i_in_F m_def_F zero_enat_def chain_length_pos[OF deriv] by auto then have "\n. enat n < llength D \ to_F \ \ fst (lnth D n)" unfolding lhd_is 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 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)} \ N2 = N \ {(C, active)} \ L \ active \ T' = no_labels.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)}" "N2 = N \ {(C0, active)}" and l_not_active: "L \ active" and tp_is: "T' = no_labels.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 "\ \ Inf_from2 (active_subset N) {(C0, active)}" using i_in_inf_fl prems_i_active unfolding Inf_from2_def Inf_from_def by blast then have "to_F \ \ no_labels.Inf_from2 (fst ` (active_subset N)) {C0}" unfolding to_F_def Inf_from2_def Inf_from_def no_labels.Inf_from2_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.. (\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 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ - \ \ no_labels.Red_Inf_\_Q (fst ` (N1 \ M))" + \ \ no_labels.Red_I_\ (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 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ - \ \ no_labels.Red_Inf_\_Q (fst ` (N1 \ M))) \ + \ \ no_labels.Red_I_\ (fst ` (N1 \ M))) \ (\T1 T2 T' N. lnth D p = (T1, N) \ lnth D (Suc p) = (T2, N) \ T1 = T2 \ T' \ T' \ no_labels.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 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.Inf_from (fst ` active_subset (snd (lnth D 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 D p = (T1, N1) \ lnth D (Suc p) = (T2, N2) \ T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ - \ \ no_labels.Red_Inf_\_Q (fst ` (N1 \ 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 D p = (T1, N1) \ lnth D (Suc p) = (T2, N2) \ T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ - \ \ no_labels.Red_Inf_\_Q (fst ` (N1 \ 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 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.Red_Inf_\_Q + 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_Inf_Q (fst ` (snd (lnth D (Suc p))))" + have "to_F \ \ no_labels.Red_I (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))))) + the (\_Inf_q q (to_F \)) \ Red_I_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.Red_Inf_Q_def no_labels.Red_Inf_\_q_def by blast - then have "\ \ Red_Inf_\_Q (snd (lnth D (Suc p)))" - using i_in_inf_fl unfolding Red_Inf_\_Q_def Red_Inf_\_q_def by (simp add: to_F_def) - then show "\ \ Sup_llist (lmap Red_Inf_\_Q (lmap snd D))" + unfolding to_F_def no_labels.Red_I_def no_labels.Red_I_\_q_def by blast + then have "\ \ Red_I_\ (snd (lnth D (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 D))" unfolding Sup_llist_def using suc_n_length p_smaller_d by auto qed theorem lgc_complete_Liminf: assumes deriv: "chain (\LGC) D" and init_state: "active_subset (snd (lhd D)) = {}" and final_state: "passive_subset (Liminf_llist (lmap snd D)) = {}" and no_prems_init_active: "\\ \ Inf_F. length (prems_of \) = 0 \ \ \ fst (lhd D)" and final_schedule: "Liminf_llist (lmap fst D) = {}" and b_in: "B \ Bot_F" and - bot_entailed: "no_labels.entails_\_Q (fst ` snd (lhd D)) {B}" + bot_entailed: "no_labels.entails_\ (fst ` snd (lhd D)) {B}" shows "\BL \ Bot_FL. BL \ Liminf_llist (lmap snd D)" proof - have labeled_b_in: "(B, active) \ Bot_FL" using b_in by simp have simp_snd_lmap: "lhd (lmap snd D) = snd (lhd D)" by (rule llist.map_sel(1)[OF chain_not_lnull[OF deriv]]) - have labeled_bot_entailed: "entails_\_L_Q (snd (lhd D)) {(B, active)}" + have labeled_bot_entailed: "entails_\_L (snd (lhd D)) {(B, active)}" using labeled_entailment_lifting bot_entailed by fastforce have "fair (lmap snd D)" using lgc_fair[OF deriv init_state final_state no_prems_init_active 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_Inf_Q_eq + labeled_bot_entailed simp_snd_lmap std_Red_I_eq by presburger qed (* thm:lgc-completeness *) theorem lgc_complete: assumes deriv: "chain (\LGC) D" and init_state: "active_subset (snd (lhd D)) = {}" and final_state: "passive_subset (Liminf_llist (lmap snd D)) = {}" and no_prems_init_active: "\\ \ Inf_F. length (prems_of \) = 0 \ \ \ fst (lhd D)" and final_schedule: "Liminf_llist (lmap fst D) = {}" and b_in: "B \ Bot_F" and - bot_entailed: "no_labels.entails_\_Q (fst ` snd (lhd D)) {B}" + bot_entailed: "no_labels.entails_\ (fst ` snd (lhd D)) {B}" shows "\i. enat i < llength D \ (\BL \ Bot_FL. BL \ snd (lnth D i))" proof - have "\BL\Bot_FL. BL \ Liminf_llist (lmap snd D)" using assms by (rule lgc_complete_Liminf) then show ?thesis unfolding Liminf_llist_def by auto qed end end diff --git a/thys/Saturation_Framework/Intersection_Calculus.thy b/thys/Saturation_Framework/Intersection_Calculus.thy --- a/thys/Saturation_Framework/Intersection_Calculus.thy +++ b/thys/Saturation_Framework/Intersection_Calculus.thy @@ -1,240 +1,240 @@ (* Title: Calculi Based on the Intersection of Redundancy Criteria * Author: Sophie Tourret , 2018-2020 *) section \Calculi Based on the Intersection of Redundancy Criteria\ text \In this section, section 2.3 of the report is covered, on calculi equipped with a family of redundancy criteria.\ theory Intersection_Calculus imports Calculus Ordered_Resolution_Prover.Lazy_List_Liminf Ordered_Resolution_Prover.Lazy_List_Chain begin subsection \Calculi with a Family of Redundancy Criteria\ locale intersection_calculus = inference_system Inf + consequence_relation_family Bot Q entails_q for Bot :: "'f set" and Inf :: \'f inference set\ and Q :: "'q set" and entails_q :: "'q \ 'f set \ 'f set \ bool" + fixes - Red_Inf_q :: "'q \ 'f set \ 'f inference set" and + Red_I_q :: "'q \ 'f set \ 'f inference set" and Red_F_q :: "'q \ 'f set \ 'f set" assumes Q_nonempty: "Q \ {}" and - all_red_crit: "\q \ Q. calculus Bot Inf (entails_q q) (Red_Inf_q q) (Red_F_q q)" + all_red_crit: "\q \ Q. calculus Bot Inf (entails_q q) (Red_I_q q) (Red_F_q q)" begin -definition Red_Inf_Q :: "'f set \ 'f inference set" where - "Red_Inf_Q N = (\q \ Q. Red_Inf_q q N)" +definition Red_I :: "'f set \ 'f inference set" where + "Red_I N = (\q \ Q. Red_I_q q N)" -definition Red_F_Q :: "'f set \ 'f set" where - "Red_F_Q N = (\q \ Q. Red_F_q q N)" +definition Red_F :: "'f set \ 'f set" where + "Red_F N = (\q \ Q. Red_F_q q N)" (* lem:intersection-of-red-crit *) -sublocale calculus Bot Inf entails_Q Red_Inf_Q Red_F_Q +sublocale calculus Bot Inf entails Red_I Red_F unfolding calculus_def calculus_axioms_def proof (intro conjI) - show "consequence_relation Bot entails_Q" + show "consequence_relation Bot entails" using intersect_cons_rel_family . next - show "\N. Red_Inf_Q N \ Inf" - unfolding Red_Inf_Q_def + show "\N. Red_I N \ Inf" + unfolding Red_I_def proof fix N - show "(\q \ Q. Red_Inf_q q N) \ Inf" + show "(\q \ Q. Red_I_q q N) \ Inf" proof (intro Inter_subset) - fix Red_Infs - assume one_red_inf: "Red_Infs \ (\q. Red_Inf_q q N) ` Q" - show "Red_Infs \ Inf" - using one_red_inf all_red_crit calculus.Red_Inf_to_Inf by blast + fix Red_Is + assume one_red_inf: "Red_Is \ (\q. Red_I_q q N) ` Q" + show "Red_Is \ Inf" + using one_red_inf all_red_crit calculus.Red_I_to_Inf by blast next - show "(\q. Red_Inf_q q N) ` Q \ {}" + show "(\q. Red_I_q q N) ` Q \ {}" using Q_nonempty by blast qed qed next - show "\B N. B \ Bot \ N \Q {B} \ N - Red_F_Q N \Q {B}" + show "\B N. B \ Bot \ N \Q {B} \ N - Red_F N \Q {B}" proof (intro allI impI) fix B N assume B_in: "B \ Bot" and N_unsat: "N \Q {B}" - show "N - Red_F_Q N \Q {B}" unfolding entails_Q_def Red_F_Q_def + show "N - Red_F N \Q {B}" unfolding entails_def Red_F_def proof fix qi assume qi_in: "qi \ Q" define entails_qi (infix "\qi" 50) where "entails_qi = entails_q qi" have cons_rel_qi: "consequence_relation Bot entails_qi" unfolding entails_qi_def using qi_in all_red_crit calculus.axioms(1) by blast define Red_F_qi where "Red_F_qi = Red_F_q qi" - have red_qi_in_Q: "Red_F_Q N \ Red_F_qi N" - unfolding Red_F_Q_def Red_F_qi_def using qi_in image_iff by blast - then have "N - Red_F_qi N \ N - Red_F_Q N" by blast - then have entails_1: "N - Red_F_Q N \qi N - Red_F_qi N" + have red_qi_in: "Red_F N \ Red_F_qi N" + unfolding Red_F_def Red_F_qi_def using qi_in image_iff by blast + then have "N - Red_F_qi N \ N - Red_F N" by blast + then have entails_1: "N - Red_F N \qi N - Red_F_qi N" using qi_in all_red_crit unfolding calculus_def consequence_relation_def entails_qi_def by metis - have N_unsat_qi: "N \qi {B}" using qi_in N_unsat unfolding entails_qi_def entails_Q_def + have N_unsat_qi: "N \qi {B}" using qi_in N_unsat unfolding entails_qi_def entails_def by simp then have N_unsat_qi: "N - Red_F_qi N \qi {B}" using qi_in all_red_crit Red_F_qi_def calculus.Red_F_Bot[OF _ B_in] entails_qi_def by fastforce show "N - (\q \ Q. Red_F_q q N) \qi {B}" using consequence_relation.entails_trans[OF cons_rel_qi entails_1 N_unsat_qi] - unfolding Red_F_Q_def . + unfolding Red_F_def . qed qed next - show "\N1 N2. N1 \ N2 \ Red_F_Q N1 \ Red_F_Q N2" - proof (intro allI impI) - fix N1 :: "'f set" - and N2 :: "'f set" - assume - N1_in_N2: "N1 \ N2" - show "Red_F_Q N1 \ Red_F_Q N2" - proof - fix C - assume "C \ Red_F_Q N1" - then have "\qi \ Q. C \ Red_F_q qi N1" unfolding Red_F_Q_def by blast - then have "\qi \ Q. C \ Red_F_q qi N2" - using N1_in_N2 all_red_crit calculus.axioms(2) calculus.Red_F_of_subset by blast - then show "C \ Red_F_Q N2" unfolding Red_F_Q_def by blast - qed - qed -next - show "\N1 N2. N1 \ N2 \ Red_Inf_Q N1 \ Red_Inf_Q N2" + show "\N1 N2. N1 \ N2 \ Red_F N1 \ Red_F N2" proof (intro allI impI) fix N1 :: "'f set" and N2 :: "'f set" assume N1_in_N2: "N1 \ N2" - show "Red_Inf_Q N1 \ Red_Inf_Q N2" + show "Red_F N1 \ Red_F N2" proof - fix \ - assume "\ \ Red_Inf_Q N1" - then have "\qi \ Q. \ \ Red_Inf_q qi N1" unfolding Red_Inf_Q_def by blast - then have "\qi \ Q. \ \ Red_Inf_q qi N2" - using N1_in_N2 all_red_crit calculus.axioms(2) calculus.Red_Inf_of_subset by blast - then show "\ \ Red_Inf_Q N2" unfolding Red_Inf_Q_def by blast + fix C + assume "C \ Red_F N1" + then have "\qi \ Q. C \ Red_F_q qi N1" unfolding Red_F_def by blast + then have "\qi \ Q. C \ Red_F_q qi N2" + using N1_in_N2 all_red_crit calculus.axioms(2) calculus.Red_F_of_subset by blast + then show "C \ Red_F N2" unfolding Red_F_def by blast qed qed next - show "\N2 N1. N2 \ Red_F_Q N1 \ Red_F_Q N1 \ Red_F_Q (N1 - N2)" + show "\N1 N2. N1 \ N2 \ Red_I N1 \ Red_I N2" proof (intro allI impI) - fix N2 N1 - assume N2_in_Red_N1: "N2 \ Red_F_Q N1" - show "Red_F_Q N1 \ Red_F_Q (N1 - N2)" + fix N1 :: "'f set" + and N2 :: "'f set" + assume + N1_in_N2: "N1 \ N2" + show "Red_I N1 \ Red_I N2" proof - fix C - assume "C \ Red_F_Q N1" - then have "\qi \ Q. C \ Red_F_q qi N1" unfolding Red_F_Q_def by blast - moreover have "\qi \ Q. N2 \ Red_F_q qi N1" using N2_in_Red_N1 unfolding Red_F_Q_def by blast - ultimately have "\qi \ Q. C \ Red_F_q qi (N1 - N2)" - using all_red_crit calculus.axioms(2) calculus.Red_F_of_Red_F_subset - by blast - then show "C \ Red_F_Q (N1 - N2)" unfolding Red_F_Q_def by blast + fix \ + assume "\ \ Red_I N1" + then have "\qi \ Q. \ \ Red_I_q qi N1" unfolding Red_I_def by blast + then have "\qi \ Q. \ \ Red_I_q qi N2" + using N1_in_N2 all_red_crit calculus.axioms(2) calculus.Red_I_of_subset by blast + then show "\ \ Red_I N2" unfolding Red_I_def by blast qed qed next - show "\N2 N1. N2 \ Red_F_Q N1 \ Red_Inf_Q N1 \ Red_Inf_Q (N1 - N2)" + show "\N2 N1. N2 \ Red_F N1 \ Red_F N1 \ Red_F (N1 - N2)" proof (intro allI impI) fix N2 N1 - assume N2_in_Red_N1: "N2 \ Red_F_Q N1" - show "Red_Inf_Q N1 \ Red_Inf_Q (N1 - N2)" + assume N2_in_Red_N1: "N2 \ Red_F N1" + show "Red_F N1 \ Red_F (N1 - N2)" proof - fix \ - assume "\ \ Red_Inf_Q N1" - then have "\qi \ Q. \ \ Red_Inf_q qi N1" unfolding Red_Inf_Q_def by blast - moreover have "\qi \ Q. N2 \ Red_F_q qi N1" using N2_in_Red_N1 unfolding Red_F_Q_def by blast - ultimately have "\qi \ Q. \ \ Red_Inf_q qi (N1 - N2)" - using all_red_crit calculus.axioms(2) calculus.Red_Inf_of_Red_F_subset by blast - then show "\ \ Red_Inf_Q (N1 - N2)" unfolding Red_Inf_Q_def by blast + fix C + assume "C \ Red_F N1" + then have "\qi \ Q. C \ Red_F_q qi N1" unfolding Red_F_def by blast + moreover have "\qi \ Q. N2 \ Red_F_q qi N1" using N2_in_Red_N1 unfolding Red_F_def by blast + ultimately have "\qi \ Q. C \ Red_F_q qi (N1 - N2)" + using all_red_crit calculus.axioms(2) calculus.Red_F_of_Red_F_subset + by blast + then show "C \ Red_F (N1 - N2)" unfolding Red_F_def by blast qed qed next - show "\\ N. \ \ Inf \ concl_of \ \ N \ \ \ Red_Inf_Q N" + show "\N2 N1. N2 \ Red_F N1 \ Red_I N1 \ Red_I (N1 - N2)" + proof (intro allI impI) + fix N2 N1 + assume N2_in_Red_N1: "N2 \ Red_F N1" + show "Red_I N1 \ Red_I (N1 - N2)" + proof + fix \ + assume "\ \ Red_I N1" + then have "\qi \ Q. \ \ Red_I_q qi N1" unfolding Red_I_def by blast + moreover have "\qi \ Q. N2 \ Red_F_q qi N1" using N2_in_Red_N1 unfolding Red_F_def by blast + ultimately have "\qi \ Q. \ \ Red_I_q qi (N1 - N2)" + using all_red_crit calculus.axioms(2) calculus.Red_I_of_Red_F_subset by blast + then show "\ \ Red_I (N1 - N2)" unfolding Red_I_def by blast + qed + qed +next + show "\\ N. \ \ Inf \ concl_of \ \ N \ \ \ Red_I N" proof (intro allI impI) fix \ N assume i_in: "\ \ Inf" and concl_in: "concl_of \ \ N" - then have "\qi \ Q. \ \ Red_Inf_q qi N" - using all_red_crit calculus.axioms(2) calculus.Red_Inf_of_Inf_to_N by blast - then show "\ \ Red_Inf_Q N" unfolding Red_Inf_Q_def by blast + then have "\qi \ Q. \ \ Red_I_q qi N" + using all_red_crit calculus.axioms(2) calculus.Red_I_of_Inf_to_N by blast + then show "\ \ Red_I N" unfolding Red_I_def by blast qed qed (* lem:satur-wrt-intersection-of-red *) -lemma sat_int_to_sat_q: "calculus.saturated Inf Red_Inf_Q N \ - (\qi \ Q. calculus.saturated Inf (Red_Inf_q qi) N)" for N +lemma sat_int_to_sat_q: "calculus.saturated Inf Red_I N \ + (\qi \ Q. calculus.saturated Inf (Red_I_q qi) N)" for N proof fix N - assume inter_sat: "calculus.saturated Inf Red_Inf_Q N" - show "\qi \ Q. calculus.saturated Inf (Red_Inf_q qi) N" + assume inter_sat: "calculus.saturated Inf Red_I N" + show "\qi \ Q. calculus.saturated Inf (Red_I_q qi) N" proof fix qi assume qi_in: "qi \ Q" - then interpret one: calculus Bot Inf "entails_q qi" "Red_Inf_q qi" "Red_F_q qi" + then interpret one: calculus Bot Inf "entails_q qi" "Red_I_q qi" "Red_F_q qi" by (metis all_red_crit) show "one.saturated N" using qi_in inter_sat - unfolding one.saturated_def saturated_def Red_Inf_Q_def by blast + unfolding one.saturated_def saturated_def Red_I_def by blast qed next fix N - assume all_sat: "\qi \ Q. calculus.saturated Inf (Red_Inf_q qi) N" + assume all_sat: "\qi \ Q. calculus.saturated Inf (Red_I_q qi) N" show "saturated N" - unfolding saturated_def Red_Inf_Q_def + unfolding saturated_def Red_I_def proof fix \ assume \_in: "\ \ Inf_from N" - have "\Red_Inf_qi \ Red_Inf_q ` Q. \ \ Red_Inf_qi N" + have "\Red_I_qi \ Red_I_q ` Q. \ \ Red_I_qi N" proof - fix Red_Inf_qi - assume red_inf_in: "Red_Inf_qi \ Red_Inf_q ` Q" + fix Red_I_qi + assume red_inf_in: "Red_I_qi \ Red_I_q ` Q" then obtain qi where qi_in: "qi \ Q" and - red_inf_qi_def: "Red_Inf_qi = Red_Inf_q qi" by blast - then interpret one: calculus Bot Inf "entails_q qi" "Red_Inf_q qi" "Red_F_q qi" + red_inf_qi_def: "Red_I_qi = Red_I_q qi" by blast + then interpret one: calculus Bot Inf "entails_q qi" "Red_I_q qi" "Red_F_q qi" by (metis all_red_crit) have "one.saturated N" using qi_in all_sat red_inf_qi_def by blast - then show "\ \ Red_Inf_qi N" unfolding one.saturated_def using \_in red_inf_qi_def by blast + then show "\ \ Red_I_qi N" unfolding one.saturated_def using \_in red_inf_qi_def by blast qed - then show "\ \ (\q \ Q. Red_Inf_q q N)" by blast + then show "\ \ (\q \ Q. Red_I_q q N)" by blast qed qed (* lem:checking-static-ref-compl-for-intersections *) lemma stat_ref_comp_from_bot_in_sat: - "(\N. calculus.saturated Inf Red_Inf_Q N \ (\B \ Bot. B \ N) \ + "(\N. calculus.saturated Inf Red_I N \ (\B \ Bot. B \ N) \ (\B \ Bot. \qi \ Q. \ entails_q qi N {B})) \ - statically_complete_calculus Bot Inf entails_Q Red_Inf_Q Red_F_Q" + statically_complete_calculus Bot Inf entails Red_I Red_F" proof (rule ccontr) assume - N_saturated: "\N. (calculus.saturated Inf Red_Inf_Q N \ (\B \ Bot. B \ N)) \ + N_saturated: "\N. (calculus.saturated Inf Red_I N \ (\B \ Bot. B \ N)) \ (\B \ Bot. \qi \ Q. \ entails_q qi N {B})" and - no_stat_ref_comp: "\ statically_complete_calculus Bot Inf (\Q) Red_Inf_Q Red_F_Q" + no_stat_ref_comp: "\ statically_complete_calculus Bot Inf (\Q) Red_I Red_F" obtain N1 B1 where B1_in: - "B1 \ Bot" and N1_saturated: "calculus.saturated Inf Red_Inf_Q N1" and + "B1 \ Bot" and N1_saturated: "calculus.saturated Inf Red_I N1" and N1_unsat: "N1 \Q {B1}" and no_B_in_N1: "\B \ Bot. B \ N1" using no_stat_ref_comp by (metis calculus_axioms statically_complete_calculus.intro statically_complete_calculus_axioms.intro) obtain B2 qi where qi_in: "qi \ Q" and no_qi: "\ entails_q qi N1 {B2}" using N_saturated N1_saturated no_B_in_N1 by auto have "N1 \Q {B2}" using N1_unsat B1_in intersect_cons_rel_family unfolding consequence_relation_def by metis - then have "entails_q qi N1 {B2}" unfolding entails_Q_def using qi_in by blast + then have "entails_q qi N1 {B2}" unfolding entails_def using qi_in by blast then show False using no_qi by simp qed end end diff --git a/thys/Saturation_Framework/Labeled_Lifting_to_Non_Ground_Calculi.thy b/thys/Saturation_Framework/Labeled_Lifting_to_Non_Ground_Calculi.thy --- a/thys/Saturation_Framework/Labeled_Lifting_to_Non_Ground_Calculi.thy +++ b/thys/Saturation_Framework/Labeled_Lifting_to_Non_Ground_Calculi.thy @@ -1,363 +1,363 @@ (* Title: Labeled Lifting to Non-Ground Calculi * Author: Sophie Tourret , 2019-2020 *) section \Labeled Lifting to Non-Ground Calculi\ text \This section formalizes the extension of the lifting results to labeled calculi. This corresponds to section 3.4 of the report.\ theory Labeled_Lifting_to_Non_Ground_Calculi imports Lifting_to_Non_Ground_Calculi begin subsection \Labeled Lifting with a Family of Tiebreaker Orderings\ locale labeled_tiebreaking_lifting = no_labels: tiebreaker_lifting Bot_F Inf_F - Bot_G entails_G Inf_G Red_Inf_G Red_F_G \_F \_Inf Prec_F + Bot_G entails_G Inf_G Red_I_G Red_F_G \_F \_Inf Prec_F for Bot_F :: "'f set" and Inf_F :: "'f inference set" and Bot_G :: "'g set" and entails_G :: "'g set \ 'g set \ bool" (infix "\G" 50) and Inf_G :: "'g inference set" and - Red_Inf_G :: "'g set \ 'g inference set" and + Red_I_G :: "'g set \ 'g inference set" and Red_F_G :: "'g set \ 'g set" and \_F :: "'f \ 'g set" and \_Inf :: "'f inference \ 'g inference set option" and Prec_F :: "'g \ 'f \ 'f \ bool" (infix "\" 50) + fixes Inf_FL :: \('f \ 'l) inference set\ assumes Inf_F_to_Inf_FL: \\\<^sub>F \ Inf_F \ length (Ll :: 'l list) = length (prems_of \\<^sub>F) \ \L0. Infer (zip (prems_of \\<^sub>F) Ll) (concl_of \\<^sub>F, L0) \ Inf_FL\ and Inf_FL_to_Inf_F: \\\<^sub>F\<^sub>L \ Inf_FL \ Infer (map fst (prems_of \\<^sub>F\<^sub>L)) (fst (concl_of \\<^sub>F\<^sub>L)) \ Inf_F\ begin definition to_F :: \('f \ 'l) inference \ 'f inference\ where \to_F \\<^sub>F\<^sub>L = Infer (map fst (prems_of \\<^sub>F\<^sub>L)) (fst (concl_of \\<^sub>F\<^sub>L))\ abbreviation Bot_FL :: \('f \ 'l) set\ where \Bot_FL \ Bot_F \ UNIV\ abbreviation \_F_L :: \('f \ 'l) \ 'g set\ where \\_F_L CL \ \_F (fst CL)\ abbreviation \_Inf_L :: \('f \ 'l) inference \ 'g inference set option\ where \\_Inf_L \\<^sub>F\<^sub>L \ \_Inf (to_F \\<^sub>F\<^sub>L)\ (* lem:labeled-grounding-function *) -sublocale standard_lifting Bot_FL Inf_FL Bot_G Inf_G "(\G)" Red_Inf_G Red_F_G \_F_L \_Inf_L +sublocale standard_lifting Bot_FL Inf_FL Bot_G Inf_G "(\G)" Red_I_G Red_F_G \_F_L \_Inf_L proof show "Bot_FL \ {}" using no_labels.Bot_F_not_empty by simp next show "B \ Bot_FL \ \_F_L B \ {}" for B using no_labels.Bot_map_not_empty by auto next show "B \ Bot_FL \ \_F_L B \ Bot_G" for B using no_labels.Bot_map by force next fix CL show "\_F_L CL \ Bot_G \ {} \ CL \ Bot_FL" using no_labels.Bot_cond by (metis SigmaE UNIV_I UNIV_Times_UNIV mem_Sigma_iff prod.sel(1)) next fix \ assume i_in: \\ \ Inf_FL\ and ground_not_none: \\_Inf_L \ \ None\ - then show "the (\_Inf_L \) \ Red_Inf_G (\_F_L (concl_of \))" + then show "the (\_Inf_L \) \ Red_I_G (\_F_L (concl_of \))" unfolding to_F_def using no_labels.inf_map Inf_FL_to_Inf_F by fastforce qed -sublocale tiebreaker_lifting Bot_FL Inf_FL Bot_G entails_G Inf_G Red_Inf_G Red_F_G \_F_L \_Inf_L +sublocale tiebreaker_lifting Bot_FL Inf_FL Bot_G entails_G Inf_G Red_I_G Red_F_G \_F_L \_Inf_L "\g Cl Cl'. False" by unfold_locales simp+ notation entails_\ (infix "\\L" 50) (* lem:labeled-consequence *) lemma labeled_entailment_lifting: "NL1 \\L NL2 \ fst ` NL1 \\ fst ` NL2" by simp -lemma red_inf_impl: "\ \ Red_Inf_\ NL \ to_F \ \ no_labels.Red_Inf_\ (fst ` NL)" - unfolding Red_Inf_\_def no_labels.Red_Inf_\_def using Inf_FL_to_Inf_F by (auto simp: to_F_def) +lemma red_inf_impl: "\ \ Red_I_\ NL \ to_F \ \ no_labels.Red_I_\ (fst ` NL)" + unfolding Red_I_\_def no_labels.Red_I_\_def using Inf_FL_to_Inf_F by (auto simp: to_F_def) (* lem:labeled-saturation *) lemma labeled_saturation_lifting: "saturated NL \ no_labels.saturated (fst ` NL)" unfolding saturated_def no_labels.saturated_def Inf_from_def no_labels.Inf_from_def proof clarify fix \ assume - subs_Red_Inf: "{\ \ Inf_FL. set (prems_of \) \ NL} \ Red_Inf_\ NL" and + subs_Red_I: "{\ \ Inf_FL. set (prems_of \) \ NL} \ Red_I_\ NL" and i_in: "\ \ Inf_F" and i_prems: "set (prems_of \) \ fst ` NL" define Lli where "Lli i = (SOME x. ((prems_of \)!i,x) \ NL)" for i have [simp]:"((prems_of \)!i,Lli i) \ NL" if "i < length (prems_of \)" for i using that i_prems unfolding Lli_def by (metis nth_mem someI_ex DomainE Domain_fst subset_eq) define Ll where "Ll = map Lli [0..)]" have Ll_length: "length Ll = length (prems_of \)" unfolding Ll_def by auto have subs_NL: "set (zip (prems_of \) Ll) \ NL" unfolding Ll_def by (auto simp:in_set_zip) obtain L0 where L0: "Infer (zip (prems_of \) Ll) (concl_of \, L0) \ Inf_FL" using Inf_F_to_Inf_FL[OF i_in Ll_length] .. define \_FL where "\_FL = Infer (zip (prems_of \) Ll) (concl_of \, L0)" then have "set (prems_of \_FL) \ NL" using subs_NL by simp then have "\_FL \ {\ \ Inf_FL. set (prems_of \) \ NL}" unfolding \_FL_def using L0 by blast - then have "\_FL \ Red_Inf_\ NL" using subs_Red_Inf by fast + then have "\_FL \ Red_I_\ NL" using subs_Red_I by fast moreover have "\ = to_F \_FL" unfolding to_F_def \_FL_def using Ll_length by (cases \) auto - ultimately show "\ \ no_labels.Red_Inf_\ (fst ` NL)" by (auto intro: red_inf_impl) + ultimately show "\ \ no_labels.Red_I_\ (fst ` NL)" by (auto intro: red_inf_impl) qed (* lem:labeled-static-ref-compl *) lemma stat_ref_comp_to_labeled_sta_ref_comp: assumes static: - "statically_complete_calculus Bot_F Inf_F (\\) no_labels.Red_Inf_\ no_labels.Red_F_\" - shows "statically_complete_calculus Bot_FL Inf_FL (\\L) Red_Inf_\ Red_F_\" + "statically_complete_calculus Bot_F Inf_F (\\) no_labels.Red_I_\ no_labels.Red_F_\" + shows "statically_complete_calculus Bot_FL Inf_FL (\\L) Red_I_\ Red_F_\" proof fix Bl :: \'f \ 'l\ and Nl :: \('f \ 'l) set\ assume Bl_in: \Bl \ Bot_FL\ and Nl_sat: \saturated Nl\ and Nl_entails_Bl: \Nl \\L {Bl}\ define B where "B = fst Bl" have B_in: "B \ Bot_F" using Bl_in B_def SigmaE by force define N where "N = fst ` Nl" have N_sat: "no_labels.saturated N" using N_def Nl_sat labeled_saturation_lifting by blast have N_entails_B: "N \\ {B}" using Nl_entails_Bl unfolding labeled_entailment_lifting N_def B_def by force have "\B' \ Bot_F. B' \ N" using B_in N_sat N_entails_B using static[unfolded statically_complete_calculus_def statically_complete_calculus_axioms_def] by blast then obtain B' where in_Bot: "B' \ Bot_F" and in_N: "B' \ N" by force then have "B' \ fst ` Bot_FL" by fastforce obtain Bl' where in_Nl: "Bl' \ Nl" and fst_Bl': "fst Bl' = B'" using in_N unfolding N_def by blast have "Bl' \ Bot_FL" using fst_Bl' in_Bot vimage_fst by fastforce then show \\Bl'\Bot_FL. Bl' \ Nl\ using in_Nl by blast qed end subsection \Labeled Lifting with a Family of Redundancy Criteria\ locale labeled_lifting_intersection = no_labels: lifting_intersection Inf_F - Bot_G Q Inf_G_q entails_q Red_Inf_q Red_F_q Bot_F \_F_q \_Inf_q "\g Cl Cl'. False" + Bot_G Q Inf_G_q entails_q Red_I_q Red_F_q Bot_F \_F_q \_Inf_q "\g Cl Cl'. False" 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_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 \_Inf_q :: "'q \ 'f inference \ 'g inference set option" + fixes Inf_FL :: \('f \ 'l) inference set\ assumes Inf_F_to_Inf_FL: \\\<^sub>F \ Inf_F \ length (Ll :: 'l list) = length (prems_of \\<^sub>F) \ \L0. Infer (zip (prems_of \\<^sub>F) Ll) (concl_of \\<^sub>F, L0) \ Inf_FL\ and Inf_FL_to_Inf_F: \\\<^sub>F\<^sub>L \ Inf_FL \ Infer (map fst (prems_of \\<^sub>F\<^sub>L)) (fst (concl_of \\<^sub>F\<^sub>L)) \ Inf_F\ begin definition to_F :: \('f \ 'l) inference \ 'f inference\ where \to_F \\<^sub>F\<^sub>L = Infer (map fst (prems_of \\<^sub>F\<^sub>L)) (fst (concl_of \\<^sub>F\<^sub>L))\ abbreviation Bot_FL :: \('f \ 'l) set\ where \Bot_FL \ Bot_F \ UNIV\ abbreviation \_F_L_q :: \'q \ ('f \ 'l) \ 'g set\ where \\_F_L_q q CL \ \_F_q q (fst CL)\ abbreviation \_Inf_L_q :: \'q \ ('f \ 'l) inference \ 'g inference set option\ where \\_Inf_L_q q \\<^sub>F\<^sub>L \ \_Inf_q q (to_F \\<^sub>F\<^sub>L)\ abbreviation \_set_L_q :: "'q \ ('f \ 'l) set \ 'g set" where "\_set_L_q q N \ \ (\_F_L_q q ` N)" -definition Red_Inf_\_L_q :: "'q \ ('f \ 'l) set \ ('f \ 'l) inference set" where - "Red_Inf_\_L_q q N = {\ \ Inf_FL. (\_Inf_L_q q \ \ None \ the (\_Inf_L_q q \) \ Red_Inf_q q (\_set_L_q q N)) +definition Red_I_\_L_q :: "'q \ ('f \ 'l) set \ ('f \ 'l) inference set" where + "Red_I_\_L_q q N = {\ \ Inf_FL. (\_Inf_L_q q \ \ None \ the (\_Inf_L_q q \) \ Red_I_q q (\_set_L_q q N)) \ (\_Inf_L_q q \ = None \ \_F_L_q q (concl_of \) \ \_set_L_q q N \ Red_F_q q (\_set_L_q q N))}" -abbreviation Red_Inf_\_L_Q :: "('f \ 'l) set \ ('f \ 'l) inference set" where - "Red_Inf_\_L_Q N \ (\q \ Q. Red_Inf_\_L_q q N)" +abbreviation Red_I_\_L :: "('f \ 'l) set \ ('f \ 'l) inference set" where + "Red_I_\_L N \ (\q \ Q. Red_I_\_L_q q N)" abbreviation entails_\_L_q :: "'q \ ('f \ 'l) set \ ('f \ 'l) set \ bool" where "entails_\_L_q q N1 N2 \ entails_q q (\_set_L_q q N1) (\_set_L_q q N2)" lemma lifting_q: assumes "q \ Q" - shows "labeled_tiebreaking_lifting Bot_F Inf_F Bot_G (entails_q q) (Inf_G_q q) (Red_Inf_q q) + shows "labeled_tiebreaking_lifting Bot_F Inf_F Bot_G (entails_q q) (Inf_G_q q) (Red_I_q q) (Red_F_q q) (\_F_q q) (\_Inf_q q) (\g Cl Cl'. False) Inf_FL" using assms no_labels.standard_lifting_family Inf_F_to_Inf_FL Inf_FL_to_Inf_F by (simp add: labeled_tiebreaking_lifting_axioms_def labeled_tiebreaking_lifting_def) lemma lifted_q: assumes q_in: "q \ Q" - shows "standard_lifting Bot_FL Inf_FL Bot_G (Inf_G_q q) (entails_q q) (Red_Inf_q q) (Red_F_q q) + shows "standard_lifting Bot_FL Inf_FL Bot_G (Inf_G_q q) (entails_q q) (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q)" proof - interpret q_lifting: labeled_tiebreaking_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" - "Red_Inf_q q" "Red_F_q q" "\_F_q q" "\_Inf_q q" "\g Cl Cl'. False" Inf_FL + "Red_I_q q" "Red_F_q q" "\_F_q q" "\_Inf_q q" "\g Cl Cl'. False" Inf_FL using lifting_q[OF q_in] . have "\_Inf_L_q q = q_lifting.\_Inf_L" unfolding to_F_def q_lifting.to_F_def by simp then show ?thesis using q_lifting.standard_lifting_axioms by simp qed lemma ord_fam_lifted_q: assumes q_in: "q \ Q" - shows "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) (Red_Inf_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) (\_Inf_L_q q) (\g Cl Cl'. False)" proof - interpret standard_q_lifting: 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" + "Red_I_q q" "Red_F_q q" "\_F_L_q q" "\_Inf_L_q q" using lifted_q[OF q_in] . have "minimal_element (\Cl Cl'. False) UNIV" by (simp add: minimal_element.intro po_on_def transp_onI wfp_on_imp_irreflp_on) then show ?thesis using standard_q_lifting.standard_lifting_axioms by (simp add: tiebreaker_lifting_axioms_def tiebreaker_lifting_def) qed definition Red_F_\_empty_L_q :: "'q \ ('f \ 'l) set \ ('f \ 'l) set" where "Red_F_\_empty_L_q q N = {C. \D \ \_F_L_q q C. D \ Red_F_q q (\_set_L_q q N) \ (\E \ N. False \ D \ \_F_L_q q E)}" abbreviation Red_F_\_empty_L :: "('f \ 'l) set \ ('f \ 'l) set" where "Red_F_\_empty_L N \ (\q \ Q. Red_F_\_empty_L_q q N)" lemma all_lifted_red_crit: assumes q_in: "q \ Q" - shows "calculus Bot_FL Inf_FL (entails_\_L_q q) (Red_Inf_\_L_q q) (Red_F_\_empty_L_q q)" + shows "calculus Bot_FL Inf_FL (entails_\_L_q q) (Red_I_\_L_q q) (Red_F_\_empty_L_q q)" proof - interpret ord_q_lifting: tiebreaker_lifting 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 Cl Cl'. False" + "Inf_G_q q" "Red_I_q q" "Red_F_q q" "\_F_L_q q" "\_Inf_L_q q" "\g Cl Cl'. False" using ord_fam_lifted_q[OF q_in] . - have "Red_Inf_\_L_q q = ord_q_lifting.Red_Inf_\" - unfolding Red_Inf_\_L_q_def ord_q_lifting.Red_Inf_\_def by simp + have "Red_I_\_L_q q = ord_q_lifting.Red_I_\" + unfolding Red_I_\_L_q_def ord_q_lifting.Red_I_\_def by simp moreover have "Red_F_\_empty_L_q q = ord_q_lifting.Red_F_\" unfolding Red_F_\_empty_L_q_def ord_q_lifting.Red_F_\_def by simp ultimately show ?thesis using ord_q_lifting.calculus_axioms by argo qed lemma all_lifted_cons_rel: assumes q_in: "q \ Q" shows "consequence_relation Bot_FL (entails_\_L_q q)" using all_lifted_red_crit calculus_def q_in by blast sublocale consequence_relation_family Bot_FL Q entails_\_L_q using all_lifted_cons_rel by (simp add: consequence_relation_family.intro no_labels.Q_nonempty) -sublocale intersection_calculus Bot_FL Inf_FL Q entails_\_L_q Red_Inf_\_L_q Red_F_\_empty_L_q +sublocale intersection_calculus Bot_FL Inf_FL Q entails_\_L_q Red_I_\_L_q Red_F_\_empty_L_q using intersection_calculus.intro[OF consequence_relation_family_axioms] by (simp add: all_lifted_red_crit intersection_calculus_axioms_def no_labels.Q_nonempty) lemma in_Inf_FL_imp_to_F_in_Inf_F: "\ \ Inf_FL \ to_F \ \ Inf_F" by (simp add: Inf_FL_to_Inf_F to_F_def) lemma in_Inf_from_imp_to_F_in_Inf_from: "\ \ Inf_from N \ to_F \ \ no_labels.Inf_from (fst ` N)" unfolding Inf_from_def no_labels.Inf_from_def to_F_def by (auto intro: Inf_FL_to_Inf_F) -notation no_labels.entails_\_Q (infix "\\\" 50) +notation no_labels.entails_\ (infix "\\\" 50) -abbreviation entails_\_L_Q :: "('f \ 'l) set \ ('f \ 'l) set \ bool" (infix "\\\L" 50) where - "(\\\L) \ entails_Q" +abbreviation entails_\_L :: "('f \ 'l) set \ ('f \ 'l) set \ bool" (infix "\\\L" 50) where + "(\\\L) \ entails" -lemmas entails_\_L_Q_def = entails_Q_def +lemmas entails_\_L_def = entails_def (* lem:labeled-consequence-intersection *) lemma labeled_entailment_lifting: "NL1 \\\L NL2 \ fst ` NL1 \\\ fst ` NL2" - unfolding no_labels.entails_\_Q_def entails_\_L_Q_def by force + unfolding no_labels.entails_\_def entails_\_L_def by force -lemma red_inf_impl: "\ \ Red_Inf_Q NL \ to_F \ \ no_labels.Red_Inf_\_Q (fst ` NL)" - unfolding no_labels.Red_Inf_\_Q_def Red_Inf_Q_def +lemma red_inf_impl: "\ \ Red_I NL \ to_F \ \ no_labels.Red_I_\ (fst ` NL)" + unfolding no_labels.Red_I_\_def Red_I_def proof clarify fix X Xa q assume q_in: "q \ Q" and - i_in_inter: "\ \ (\q \ Q. Red_Inf_\_L_q q NL)" - have i_in_q: "\ \ Red_Inf_\_L_q q NL" using q_in i_in_inter image_eqI by blast - then have i_in: "\ \ Inf_FL" unfolding Red_Inf_\_L_q_def by blast + i_in_inter: "\ \ (\q \ Q. Red_I_\_L_q q NL)" + have i_in_q: "\ \ Red_I_\_L_q q NL" using q_in i_in_inter image_eqI by blast + then have i_in: "\ \ Inf_FL" unfolding Red_I_\_L_q_def by blast have to_F_in: "to_F \ \ Inf_F" unfolding to_F_def using Inf_FL_to_Inf_F[OF i_in] . have rephrase1: "(\CL\NL. \_F_q q (fst CL)) = (\ (\_F_q q ` fst ` NL))" by blast have rephrase2: "fst (concl_of \) = concl_of (to_F \)" unfolding concl_of_def to_F_def by simp - have subs_red: "(\_Inf_L_q q \ \ None \ the (\_Inf_L_q q \) \ Red_Inf_q q (\_set_L_q q NL)) + have subs_red: "(\_Inf_L_q q \ \ None \ the (\_Inf_L_q q \) \ Red_I_q q (\_set_L_q q NL)) \ (\_Inf_L_q q \ = None \ \_F_L_q q (concl_of \) \ \_set_L_q q NL \ Red_F_q q (\_set_L_q q NL))" - using i_in_q unfolding Red_Inf_\_L_q_def by blast + using i_in_q unfolding Red_I_\_L_q_def by blast then have to_F_subs_red: "(\_Inf_q q (to_F \) \ None \ - the (\_Inf_q q (to_F \)) \ Red_Inf_q q (no_labels.\_set_q q (fst ` NL))) + the (\_Inf_q q (to_F \)) \ Red_I_q q (no_labels.\_set_q q (fst ` NL))) \ (\_Inf_q q (to_F \) = None \ \_F_q q (concl_of (to_F \)) \ no_labels.\_set_q q (fst ` NL) \ Red_F_q q (no_labels.\_set_q q (fst ` NL)))" using rephrase1 rephrase2 by metis - then show "to_F \ \ no_labels.Red_Inf_\_q q (fst ` NL)" - using to_F_in unfolding no_labels.Red_Inf_\_q_def by simp + then show "to_F \ \ no_labels.Red_I_\_q q (fst ` NL)" + using to_F_in unfolding no_labels.Red_I_\_q_def by simp qed (* lem:labeled-saturation-intersection *) lemma labeled_family_saturation_lifting: "saturated NL \ no_labels.saturated (fst ` NL)" unfolding saturated_def no_labels.saturated_def Inf_from_def no_labels.Inf_from_def proof clarify fix \F assume - labeled_sat: "{\ \ Inf_FL. set (prems_of \) \ NL} \ Red_Inf_Q NL" and + labeled_sat: "{\ \ Inf_FL. set (prems_of \) \ NL} \ Red_I NL" and iF_in: "\F \ Inf_F" and iF_prems: "set (prems_of \F) \ fst ` NL" define Lli where "Lli i = (SOME x. ((prems_of \F)!i,x) \ NL)" for i have [simp]:"((prems_of \F)!i,Lli i) \ NL" if "i < length (prems_of \F)" for i using that iF_prems nth_mem someI_ex unfolding Lli_def by (metis DomainE Domain_fst subset_eq) define Ll where "Ll = map Lli [0..F)]" have Ll_length: "length Ll = length (prems_of \F)" unfolding Ll_def by auto have subs_NL: "set (zip (prems_of \F) Ll) \ NL" unfolding Ll_def by (auto simp:in_set_zip) obtain L0 where L0: "Infer (zip (prems_of \F) Ll) (concl_of \F, L0) \ Inf_FL" using Inf_F_to_Inf_FL[OF iF_in Ll_length] .. define \FL where "\FL = Infer (zip (prems_of \F) Ll) (concl_of \F, L0)" then have "set (prems_of \FL) \ NL" using subs_NL by simp then have "\FL \ {\ \ Inf_FL. set (prems_of \) \ NL}" unfolding \FL_def using L0 by blast - then have "\FL \ Red_Inf_Q NL" using labeled_sat by fast + then have "\FL \ Red_I NL" using labeled_sat by fast moreover have "\F = to_F \FL" unfolding to_F_def \FL_def using Ll_length by (cases \F) auto - ultimately show "\F \ no_labels.Red_Inf_\_Q (fst ` NL)" + ultimately show "\F \ no_labels.Red_I_\ (fst ` NL)" by (auto intro: red_inf_impl) qed (* thm:labeled-static-ref-compl-intersection *) theorem labeled_static_ref: - assumes calc: "statically_complete_calculus Bot_F Inf_F (\\\) no_labels.Red_Inf_\_Q + assumes calc: "statically_complete_calculus Bot_F Inf_F (\\\) no_labels.Red_I_\ no_labels.Red_F_\_empty" - shows "statically_complete_calculus Bot_FL Inf_FL (\\\L) Red_Inf_Q Red_F_Q" + shows "statically_complete_calculus Bot_FL Inf_FL (\\\L) Red_I Red_F" proof fix Bl :: \'f \ 'l\ and Nl :: \('f \ 'l) set\ assume Bl_in: \Bl \ Bot_FL\ and Nl_sat: \saturated Nl\ and Nl_entails_Bl: \Nl \\\L {Bl}\ define B where "B = fst Bl" have B_in: "B \ Bot_F" using Bl_in B_def SigmaE by force define N where "N = fst ` Nl" have N_sat: "no_labels.saturated N" using N_def Nl_sat labeled_family_saturation_lifting by blast have N_entails_B: "N \\\ {B}" using Nl_entails_Bl unfolding labeled_entailment_lifting N_def B_def by force have "\B' \ Bot_F. B' \ N" using B_in N_sat N_entails_B calc[unfolded statically_complete_calculus_def statically_complete_calculus_axioms_def] by blast then obtain B' where in_Bot: "B' \ Bot_F" and in_N: "B' \ N" by force then have "B' \ fst ` Bot_FL" by fastforce obtain Bl' where in_Nl: "Bl' \ Nl" and fst_Bl': "fst Bl' = B'" using in_N unfolding N_def by blast have "Bl' \ Bot_FL" using fst_Bl' in_Bot vimage_fst by fastforce then show \\Bl'\Bot_FL. Bl' \ Nl\ using in_Nl by blast qed end end diff --git a/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy b/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy --- a/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy +++ b/thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy @@ -1,758 +1,758 @@ (* Title: Lifting to Non-Ground Calculi * Author: Sophie Tourret , 2018-2020 *) section \Lifting to Non-ground Calculi\ text \The section 3.1 to 3.3 of the report are covered by the current section. Various forms of lifting are proven correct. These allow to obtain the dynamic refutational completeness of a non-ground calculus from the static refutational completeness of its ground counterpart.\ theory Lifting_to_Non_Ground_Calculi imports Intersection_Calculus Calculus_Variations Well_Quasi_Orders.Minimal_Elements begin subsection \Standard Lifting\ locale standard_lifting = inference_system Inf_F + - ground: calculus Bot_G Inf_G entails_G Red_Inf_G Red_F_G + ground: calculus Bot_G Inf_G entails_G Red_I_G Red_F_G for Bot_F :: \'f set\ and Inf_F :: \'f inference set\ and Bot_G :: \'g set\ and Inf_G :: \'g inference set\ and entails_G :: \'g set \ 'g set \ bool\ (infix "\G" 50) and - Red_Inf_G :: \'g set \ 'g inference set\ and + Red_I_G :: \'g set \ 'g inference set\ and Red_F_G :: \'g set \ 'g set\ + fixes \_F :: \'f \ 'g set\ and \_Inf :: \'f inference \ 'g inference set option\ assumes Bot_F_not_empty: "Bot_F \ {}" and Bot_map_not_empty: \B \ Bot_F \ \_F B \ {}\ and Bot_map: \B \ Bot_F \ \_F B \ Bot_G\ and Bot_cond: \\_F C \ Bot_G \ {} \ C \ Bot_F\ and - inf_map: \\ \ Inf_F \ \_Inf \ \ None \ the (\_Inf \) \ Red_Inf_G (\_F (concl_of \))\ + inf_map: \\ \ Inf_F \ \_Inf \ \ None \ the (\_Inf \) \ Red_I_G (\_F (concl_of \))\ begin abbreviation \_set :: \'f set \ 'g set\ where \\_set N \ \ (\_F ` N)\ lemma \_subset: \N1 \ N2 \ \_set N1 \ \_set N2\ by auto abbreviation entails_\ :: \'f set \ 'f set \ bool\ (infix "\\" 50) where \N1 \\ N2 \ \_set N1 \G \_set N2\ lemma subs_Bot_G_entails: assumes not_empty: \sB \ {}\ and in_bot: \sB \ Bot_G\ shows \sB \G N\ proof - have \\B. B \ sB\ using not_empty by auto then obtain B where B_in: \B \ sB\ by auto then have r_trans: \{B} \G N\ using ground.bot_entails_all in_bot by auto have l_trans: \sB \G {B}\ using B_in ground.subset_entailed by auto then show ?thesis using r_trans ground.entails_trans[of sB "{B}"] by auto qed (* lem:derived-consequence-relation *) sublocale consequence_relation Bot_F entails_\ proof show "Bot_F \ {}" using Bot_F_not_empty . next show \B\Bot_F \ {B} \\ N\ for B N proof - assume \B \ Bot_F\ then show \{B} \\ N\ using Bot_map ground.bot_entails_all[of _ "\_set N"] subs_Bot_G_entails Bot_map_not_empty by auto qed next fix N1 N2 :: \'f set\ assume \N2 \ N1\ then show \N1 \\ N2\ using \_subset ground.subset_entailed by auto next fix N1 N2 assume N1_entails_C: \\C \ N2. N1 \\ {C}\ show \N1 \\ N2\ using ground.all_formulas_entailed N1_entails_C by (smt UN_E UN_I ground.entail_set_all_formulas singletonI) next fix N1 N2 N3 assume \N1 \\ N2\ and \N2 \\ N3\ then show \N1 \\ N3\ using ground.entails_trans by blast qed end subsection \Strong Standard Lifting\ (* rmk:strong-standard-lifting *) locale strong_standard_lifting = inference_system Inf_F + - ground: calculus Bot_G Inf_G entails_G Red_Inf_G Red_F_G + ground: calculus Bot_G Inf_G entails_G Red_I_G Red_F_G for Bot_F :: \'f set\ and Inf_F :: \'f inference set\ and Bot_G :: \'g set\ and Inf_G :: \'g inference set\ and entails_G :: \'g set \ 'g set \ bool\ (infix "\G" 50) and - Red_Inf_G :: \'g set \ 'g inference set\ and + Red_I_G :: \'g set \ 'g inference set\ and Red_F_G :: \'g set \ 'g set\ + fixes \_F :: \'f \ 'g set\ and \_Inf :: \'f inference \ 'g inference set option\ assumes Bot_F_not_empty: "Bot_F \ {}" and Bot_map_not_empty: \B \ Bot_F \ \_F B \ {}\ and Bot_map: \B \ Bot_F \ \_F B \ Bot_G\ and Bot_cond: \\_F C \ Bot_G \ {} \ C \ Bot_F\ and strong_inf_map: \\ \ Inf_F \ \_Inf \ \ None \ concl_of ` (the (\_Inf \)) \ (\_F (concl_of \))\ and inf_map_in_Inf: \\ \ Inf_F \ \_Inf \ \ None \ the (\_Inf \) \ Inf_G\ begin -sublocale standard_lifting Bot_F Inf_F Bot_G Inf_G "(\G)" Red_Inf_G Red_F_G \_F \_Inf +sublocale standard_lifting Bot_F Inf_F Bot_G Inf_G "(\G)" Red_I_G Red_F_G \_F \_Inf proof show "Bot_F \ {}" using Bot_F_not_empty . next fix B assume b_in: "B \ Bot_F" show "\_F B \ {}" using Bot_map_not_empty[OF b_in] . next fix B assume b_in: "B \ Bot_F" show "\_F B \ Bot_G" using Bot_map[OF b_in] . next show "\C. \_F C \ Bot_G \ {} \ C \ Bot_F" using Bot_cond . next fix \ assume i_in: "\ \ Inf_F" and some_g: "\_Inf \ \ None" - show "the (\_Inf \) \ Red_Inf_G (\_F (concl_of \))" + show "the (\_Inf \) \ Red_I_G (\_F (concl_of \))" proof fix \G assume ig_in1: "\G \ the (\_Inf \)" then have ig_in2: "\G \ Inf_G" using inf_map_in_Inf[OF i_in some_g] by blast - show "\G \ Red_Inf_G (\_F (concl_of \))" - using strong_inf_map[OF i_in some_g] ground.Red_Inf_of_Inf_to_N[OF ig_in2] + show "\G \ Red_I_G (\_F (concl_of \))" + using strong_inf_map[OF i_in some_g] ground.Red_I_of_Inf_to_N[OF ig_in2] ig_in1 by blast qed qed end subsection \Lifting with a Family of Tiebreaker Orderings\ locale tiebreaker_lifting = - standard_lifting Bot_F Inf_F Bot_G Inf_G entails_G Red_Inf_G Red_F_G \_F \_Inf + standard_lifting Bot_F Inf_F Bot_G Inf_G entails_G Red_I_G Red_F_G \_F \_Inf for Bot_F :: \'f set\ and Inf_F :: \'f inference set\ and Bot_G :: \'g set\ and entails_G :: \'g set \ 'g set \ bool\ (infix "\G" 50) and Inf_G :: \'g inference set\ and - Red_Inf_G :: \'g set \ 'g inference set\ and + Red_I_G :: \'g set \ 'g inference set\ and Red_F_G :: \'g set \ 'g set\ and \_F :: "'f \ 'g set" and \_Inf :: "'f inference \ 'g inference set option" + fixes Prec_F_g :: \'g \ 'f \ 'f \ bool\ assumes all_wf: "minimal_element (Prec_F_g g) UNIV" begin -definition Red_Inf_\ :: "'f set \ 'f inference set" where - \Red_Inf_\ N = {\ \ Inf_F. (\_Inf \ \ None \ the (\_Inf \) \ Red_Inf_G (\_set N)) +definition Red_I_\ :: "'f set \ 'f inference set" where + \Red_I_\ N = {\ \ Inf_F. (\_Inf \ \ None \ the (\_Inf \) \ Red_I_G (\_set N)) \ (\_Inf \ = None \ \_F (concl_of \) \ \_set N \ Red_F_G (\_set N))}\ definition Red_F_\ :: "'f set \ 'f set" where \Red_F_\ N = {C. \D \ \_F C. D \ Red_F_G (\_set N) \ (\E \ N. Prec_F_g D E C \ D \ \_F E)}\ lemma Prec_trans: assumes \Prec_F_g D A B\ and \Prec_F_g D B C\ shows \Prec_F_g D A C\ using minimal_element.po assms unfolding po_on_def transp_on_def by (smt UNIV_I all_wf) lemma prop_nested_in_set: "D \ P C \ C \ {C. \D \ P C. A D \ B C D} \ A D \ B C D" by blast (* lem:wolog-C'-nonredundant *) lemma Red_F_\_equiv_def: \Red_F_\ N = {C. \Di \ \_F C. Di \ Red_F_G (\_set N) \ (\E \ (N - Red_F_\ N). Prec_F_g Di E C \ Di \ \_F E)}\ proof (rule; clarsimp) fix C D assume C_in: \C \ Red_F_\ N\ and D_in: \D \ \_F C\ and not_sec_case: \\E \ N - Red_F_\ N. Prec_F_g D E C \ D \ \_F E\ have C_in_unfolded: "C \ {C. \Di \ \_F C. Di \ Red_F_G (\_set N) \ (\E\N. Prec_F_g Di E C \ Di \ \_F E)}" using C_in unfolding Red_F_\_def . have neg_not_sec_case: \\ (\E\N - Red_F_\ N. Prec_F_g D E C \ D \ \_F E)\ using not_sec_case by clarsimp have unfol_C_D: \D \ Red_F_G (\_set N) \ (\E\N. Prec_F_g D E C \ D \ \_F E)\ using prop_nested_in_set[of D \_F C "\x. x \ Red_F_G (\ (\_F ` N))" "\x y. \E \ N. Prec_F_g y E x \ y \ \_F E", OF D_in C_in_unfolded] by blast show \D \ Red_F_G (\_set N)\ proof (rule ccontr) assume contrad: \D \ Red_F_G (\_set N)\ have non_empty: \\E\N. Prec_F_g D E C \ D \ \_F E\ using contrad unfol_C_D by auto define B where \B = {E \ N. Prec_F_g D E C \ D \ \_F E}\ then have B_non_empty: \B \ {}\ using non_empty by auto interpret minimal_element "Prec_F_g D" UNIV using all_wf[of D] . obtain F :: 'f where F: \F = min_elt B\ by auto then have D_in_F: \D \ \_F F\ unfolding B_def using non_empty by (smt Sup_UNIV Sup_upper UNIV_I contra_subsetD empty_iff empty_subsetI mem_Collect_eq min_elt_mem unfol_C_D) have F_prec: \Prec_F_g D F C\ using F min_elt_mem[of B, OF _ B_non_empty] unfolding B_def by auto have F_not_in: \F \ Red_F_\ N\ proof assume F_in: \F \ Red_F_\ N\ have unfol_F_D: \D \ Red_F_G (\_set N) \ (\G\N. Prec_F_g D G F \ D \ \_F G)\ using F_in D_in_F unfolding Red_F_\_def by auto then have \\G\N. Prec_F_g D G F \ D \ \_F G\ using contrad D_in unfolding Red_F_\_def by auto then obtain G where G_in: \G \ N\ and G_prec: \Prec_F_g D G F\ and G_map: \D \ \_F G\ by auto have \Prec_F_g D G C\ using G_prec F_prec Prec_trans by blast then have \G \ B\ unfolding B_def using G_in G_map by auto then show \False\ using F G_prec min_elt_minimal[of B G, OF _ B_non_empty] by auto qed have \F \ N\ using F by (metis B_def B_non_empty mem_Collect_eq min_elt_mem top_greatest) then have \F \ N - Red_F_\ N\ using F_not_in by auto then show \False\ using D_in_F neg_not_sec_case F_prec by blast qed next fix C assume only_if: \\D\\_F C. D \ Red_F_G (\_set N) \ (\E\N - Red_F_\ N. Prec_F_g D E C \ D \ \_F E)\ show \C \ Red_F_\ N\ unfolding Red_F_\_def using only_if by auto qed (* lem:lifting-main-technical *) lemma not_red_map_in_map_not_red: \\_set N - Red_F_G (\_set N) \ \_set (N - Red_F_\ N)\ proof fix D assume D_hyp: \D \ \_set N - Red_F_G (\_set N)\ interpret minimal_element "Prec_F_g D" UNIV using all_wf[of D] . have D_in: \D \ \_set N\ using D_hyp by blast have D_not_in: \D \ Red_F_G (\_set N)\ using D_hyp by blast have exist_C: \\C. C \ N \ D \ \_F C\ using D_in by auto define B where \B = {C \ N. D \ \_F C}\ obtain C where C: \C = min_elt B\ by auto have C_in_N: \C \ N\ using exist_C by (metis B_def C empty_iff mem_Collect_eq min_elt_mem top_greatest) have D_in_C: \D \ \_F C\ using exist_C by (metis B_def C empty_iff mem_Collect_eq min_elt_mem top_greatest) have C_not_in: \C \ Red_F_\ N\ proof assume C_in: \C \ Red_F_\ N\ have \D \ Red_F_G (\_set N) \ (\E\N. Prec_F_g D E C \ D \ \_F E)\ using C_in D_in_C unfolding Red_F_\_def by auto then show \False\ proof assume \D \ Red_F_G (\_set N)\ then show \False\ using D_not_in by simp next assume \\E\N. Prec_F_g D E C \ D \ \_F E\ then show \False\ using C by (metis (no_types, lifting) B_def UNIV_I empty_iff mem_Collect_eq min_elt_minimal top_greatest) qed qed show \D \ \_set (N - Red_F_\ N)\ using D_in_C C_not_in C_in_N by blast qed (* lem:nonredundant-entails-redundant *) lemma Red_F_Bot_F: \B \ Bot_F \ N \\ {B} \ N - Red_F_\ N \\ {B}\ proof - fix B N assume B_in: \B \ Bot_F\ and N_entails: \N \\ {B}\ then have to_bot: \\_set N - Red_F_G (\_set N) \G \_F B\ using ground.Red_F_Bot Bot_map by (smt cSup_singleton ground.entail_set_all_formulas image_insert image_is_empty subsetCE) have from_f: \\_set (N - Red_F_\ N) \G \_set N - Red_F_G (\_set N)\ using ground.subset_entailed[OF not_red_map_in_map_not_red] by blast then have \\_set (N - Red_F_\ N) \G \_F B\ using to_bot ground.entails_trans by blast then show \N - Red_F_\ N \\ {B}\ using Bot_map by simp qed (* lem:redundancy-monotonic-addition 1/2 *) lemma Red_F_of_subset_F: \N \ N' \ Red_F_\ N \ Red_F_\ N'\ using ground.Red_F_of_subset unfolding Red_F_\_def by clarsimp (meson \_subset subsetD) (* lem:redundancy-monotonic-addition 2/2 *) -lemma Red_Inf_of_subset_F: \N \ N' \ Red_Inf_\ N \ Red_Inf_\ N'\ - using Collect_mono \_subset subset_iff ground.Red_Inf_of_subset unfolding Red_Inf_\_def +lemma Red_I_of_subset_F: \N \ N' \ Red_I_\ N \ Red_I_\ N'\ + using Collect_mono \_subset subset_iff ground.Red_I_of_subset unfolding Red_I_\_def by (smt ground.Red_F_of_subset Un_iff) (* lem:redundancy-monotonic-deletion-forms *) lemma Red_F_of_Red_F_subset_F: \N' \ Red_F_\ N \ Red_F_\ N \ Red_F_\ (N - N')\ proof fix N N' C assume N'_in_Red_F_N: \N' \ Red_F_\ N\ and C_in_red_F_N: \C \ Red_F_\ N\ have lem8: \\D \ \_F C. D \ Red_F_G (\_set N) \ (\E \ (N - Red_F_\ N). Prec_F_g D E C \ D \ \_F E)\ using Red_F_\_equiv_def C_in_red_F_N by blast show \C \ Red_F_\ (N - N')\ unfolding Red_F_\_def proof (rule,rule) fix D assume \D \ \_F C\ then have \D \ Red_F_G (\_set N) \ (\E \ (N - Red_F_\ N). Prec_F_g D E C \ D \ \_F E)\ using lem8 by auto then show \D \ Red_F_G (\_set (N - N')) \ (\E\N - N'. Prec_F_g D E C \ D \ \_F E)\ proof assume \D \ Red_F_G (\_set N)\ then have \D \ Red_F_G (\_set N - Red_F_G (\_set N))\ using ground.Red_F_of_Red_F_subset[of "Red_F_G (\_set N)" "\_set N"] by auto then have \D \ Red_F_G (\_set (N - Red_F_\ N))\ using ground.Red_F_of_subset[OF not_red_map_in_map_not_red[of N]] by auto then have \D \ Red_F_G (\_set (N - N'))\ using N'_in_Red_F_N \_subset[of "N - Red_F_\ N" "N - N'"] by (smt DiffE DiffI ground.Red_F_of_subset subsetCE subsetI) then show ?thesis by blast next assume \\E\N - Red_F_\ N. Prec_F_g D E C \ D \ \_F E\ then obtain E where E_in: \E\N - Red_F_\ N\ and E_prec_C: \Prec_F_g D E C\ and D_in: \D \ \_F E\ by auto have \E \ N - N'\ using E_in N'_in_Red_F_N by blast then show ?thesis using E_prec_C D_in by blast qed qed qed (* lem:redundancy-monotonic-deletion-infs *) -lemma Red_Inf_of_Red_F_subset_F: \N' \ Red_F_\ N \ Red_Inf_\ N \ Red_Inf_\ (N - N') \ +lemma Red_I_of_Red_F_subset_F: \N' \ Red_F_\ N \ Red_I_\ N \ Red_I_\ (N - N') \ proof fix N N' \ assume N'_in_Red_F_N: \N' \ Red_F_\ N\ and - i_in_Red_Inf_N: \\ \ Red_Inf_\ N\ - have i_in: \\ \ Inf_F\ using i_in_Red_Inf_N unfolding Red_Inf_\_def by blast + i_in_Red_I_N: \\ \ Red_I_\ N\ + have i_in: \\ \ Inf_F\ using i_in_Red_I_N unfolding Red_I_\_def by blast { assume not_none: "\_Inf \ \ None" - have \\\' \ the (\_Inf \). \' \ Red_Inf_G (\_set N)\ - using not_none i_in_Red_Inf_N unfolding Red_Inf_\_def by auto - then have \\\' \ the (\_Inf \). \' \ Red_Inf_G (\_set N - Red_F_G (\_set N))\ - using not_none ground.Red_Inf_of_Red_F_subset by blast - then have ip_in_Red_Inf_G: \\\' \ the (\_Inf \). \' \ Red_Inf_G (\_set (N - Red_F_\ N))\ - using not_none ground.Red_Inf_of_subset[OF not_red_map_in_map_not_red[of N]] by auto - then have not_none_in: \\\' \ the (\_Inf \). \' \ Red_Inf_G (\_set (N - N'))\ + have \\\' \ the (\_Inf \). \' \ Red_I_G (\_set N)\ + using not_none i_in_Red_I_N unfolding Red_I_\_def by auto + then have \\\' \ the (\_Inf \). \' \ Red_I_G (\_set N - Red_F_G (\_set N))\ + using not_none ground.Red_I_of_Red_F_subset by blast + then have ip_in_Red_I_G: \\\' \ the (\_Inf \). \' \ Red_I_G (\_set (N - Red_F_\ N))\ + using not_none ground.Red_I_of_subset[OF not_red_map_in_map_not_red[of N]] by auto + then have not_none_in: \\\' \ the (\_Inf \). \' \ Red_I_G (\_set (N - N'))\ using not_none N'_in_Red_F_N - by (meson Diff_mono ground.Red_Inf_of_subset \_subset subset_iff subset_refl) - then have "the (\_Inf \) \ Red_Inf_G (\_set (N - N'))" by blast + by (meson Diff_mono ground.Red_I_of_subset \_subset subset_iff subset_refl) + then have "the (\_Inf \) \ Red_I_G (\_set (N - N'))" by blast } moreover { assume none: "\_Inf \ = None" have ground_concl_subs: "\_F (concl_of \) \ (\_set N \ Red_F_G (\_set N))" - using none i_in_Red_Inf_N unfolding Red_Inf_\_def by blast + using none i_in_Red_I_N unfolding Red_I_\_def by blast then have d_in_imp12: "D \ \_F (concl_of \) \ D \ \_set N - Red_F_G (\_set N) \ D \ Red_F_G (\_set N)" by blast have d_in_imp1: "D \ \_set N - Red_F_G (\_set N) \ D \ \_set (N - N')" using not_red_map_in_map_not_red N'_in_Red_F_N by blast have d_in_imp_d_in: "D \ Red_F_G (\_set N) \ D \ Red_F_G (\_set N - Red_F_G (\_set N))" using ground.Red_F_of_Red_F_subset[of "Red_F_G (\_set N)" "\_set N"] by blast have g_subs1: "\_set N - Red_F_G (\_set N) \ \_set (N - Red_F_\ N)" using not_red_map_in_map_not_red unfolding Red_F_\_def by auto have g_subs2: "\_set (N - Red_F_\ N) \ \_set (N - N')" using N'_in_Red_F_N by blast have d_in_imp2: "D \ Red_F_G (\_set N) \ D \ Red_F_G (\_set (N - N'))" using ground.Red_F_of_subset ground.Red_F_of_subset[OF g_subs1] ground.Red_F_of_subset[OF g_subs2] d_in_imp_d_in by blast have "\_F (concl_of \) \ (\_set (N - N') \ Red_F_G (\_set (N - N')))" using d_in_imp12 d_in_imp1 d_in_imp2 by (smt ground.Red_F_of_Red_F_subset ground.Red_F_of_subset UnCI UnE Un_Diff_cancel2 ground_concl_subs g_subs1 g_subs2 subset_iff) } - ultimately show \\ \ Red_Inf_\ (N - N')\ using i_in unfolding Red_Inf_\_def by auto + ultimately show \\ \ Red_I_\ (N - N')\ using i_in unfolding Red_I_\_def by auto qed (* lem:concl-contained-implies-red-inf *) -lemma Red_Inf_of_Inf_to_N_F: +lemma Red_I_of_Inf_to_N_F: assumes i_in: \\ \ Inf_F\ and concl_i_in: \concl_of \ \ N\ shows - \\ \ Red_Inf_\ N \ + \\ \ Red_I_\ N \ proof - - have \\ \ Inf_F \ \_Inf \ \ None \ the (\_Inf \) \ Red_Inf_G (\_F (concl_of \))\ using inf_map by simp - moreover have \Red_Inf_G (\_F (concl_of \)) \ Red_Inf_G (\_set N)\ - using concl_i_in ground.Red_Inf_of_subset by blast + have \\ \ Inf_F \ \_Inf \ \ None \ the (\_Inf \) \ Red_I_G (\_F (concl_of \))\ using inf_map by simp + moreover have \Red_I_G (\_F (concl_of \)) \ Red_I_G (\_set N)\ + using concl_i_in ground.Red_I_of_subset by blast moreover have "\ \ Inf_F \ \_Inf \ = None \ concl_of \ \ N \ \_F (concl_of \) \ \_set N" by blast - ultimately show ?thesis using i_in concl_i_in unfolding Red_Inf_\_def by auto + ultimately show ?thesis using i_in concl_i_in unfolding Red_I_\_def by auto qed (* thm:FRedsqsubset-is-red-crit and also thm:lifted-red-crit if ordering empty *) -sublocale calculus Bot_F Inf_F entails_\ Red_Inf_\ Red_F_\ +sublocale calculus Bot_F Inf_F entails_\ Red_I_\ Red_F_\ proof fix B N N' \ - show \Red_Inf_\ N \ Inf_F\ unfolding Red_Inf_\_def by blast + show \Red_I_\ N \ Inf_F\ unfolding Red_I_\_def by blast show \B \ Bot_F \ N \\ {B} \ N - Red_F_\ N \\ {B}\ using Red_F_Bot_F by simp show \N \ N' \ Red_F_\ N \ Red_F_\ N'\ using Red_F_of_subset_F by simp - show \N \ N' \ Red_Inf_\ N \ Red_Inf_\ N'\ using Red_Inf_of_subset_F by simp + show \N \ N' \ Red_I_\ N \ Red_I_\ N'\ using Red_I_of_subset_F by simp show \N' \ Red_F_\ N \ Red_F_\ N \ Red_F_\ (N - N')\ using Red_F_of_Red_F_subset_F by simp - show \N' \ Red_F_\ N \ Red_Inf_\ N \ Red_Inf_\ (N - N')\ using Red_Inf_of_Red_F_subset_F by simp - show \\ \ Inf_F \ concl_of \ \ N \ \ \ Red_Inf_\ N\ using Red_Inf_of_Inf_to_N_F by simp + show \N' \ Red_F_\ N \ Red_I_\ N \ Red_I_\ (N - N')\ using Red_I_of_Red_F_subset_F by simp + show \\ \ Inf_F \ concl_of \ \ N \ \ \ Red_I_\ N\ using Red_I_of_Inf_to_N_F by simp qed lemma grounded_inf_in_ground_inf: "\ \ Inf_F \ \_Inf \ \ None \ the (\_Inf \) \ Inf_G" - using inf_map ground.Red_Inf_to_Inf by blast + using inf_map ground.Red_I_to_Inf by blast abbreviation ground_Inf_redundant :: "'f set \ bool" where "ground_Inf_redundant N \ ground.Inf_from (\_set N) - \ {\. \\'\ Inf_from N. \_Inf \' \ None \ \ \ the (\_Inf \')} \ Red_Inf_G (\_set N)" + \ {\. \\'\ Inf_from N. \_Inf \' \ None \ \ \ the (\_Inf \')} \ Red_I_G (\_set N)" lemma sat_inf_imp_ground_red: assumes "saturated N" and "\' \ Inf_from N" and "\_Inf \' \ None \ \ \ the (\_Inf \')" - shows "\ \ Red_Inf_G (\_set N)" - using assms Red_Inf_\_def unfolding saturated_def by auto + shows "\ \ Red_I_G (\_set N)" + using assms Red_I_\_def unfolding saturated_def by auto (* lem:sat-wrt-finf *) lemma sat_imp_ground_sat: "saturated N \ ground_Inf_redundant N \ ground.saturated (\_set N)" unfolding ground.saturated_def using sat_inf_imp_ground_red by auto (* thm:finf-complete *) theorem stat_ref_comp_to_non_ground: assumes - stat_ref_G: "statically_complete_calculus Bot_G Inf_G entails_G Red_Inf_G Red_F_G" and + stat_ref_G: "statically_complete_calculus Bot_G Inf_G entails_G Red_I_G Red_F_G" and sat_n_imp: "\N. saturated N \ ground_Inf_redundant N" shows - "statically_complete_calculus Bot_F Inf_F entails_\ Red_Inf_\ Red_F_\" + "statically_complete_calculus Bot_F Inf_F entails_\ Red_I_\ Red_F_\" proof fix B N assume b_in: "B \ Bot_F" and sat_n: "saturated N" and n_entails_bot: "N \\ {B}" have ground_n_entails: "\_set N \G \_F B" using n_entails_bot by simp then obtain BG where bg_in1: "BG \ \_F B" using Bot_map_not_empty[OF b_in] by blast then have bg_in: "BG \ Bot_G" using Bot_map[OF b_in] by blast have ground_n_entails_bot: "\_set N \G {BG}" using ground_n_entails bg_in1 ground.entail_set_all_formulas by blast have "ground.Inf_from (\_set N) \ - {\. \\'\ Inf_from N. \_Inf \' \ None \ \ \ the (\_Inf \')} \ Red_Inf_G (\_set N)" + {\. \\'\ Inf_from N. \_Inf \' \ None \ \ \ the (\_Inf \')} \ Red_I_G (\_set N)" using sat_n_imp[OF sat_n] . have "ground.saturated (\_set N)" using sat_imp_ground_sat[OF sat_n sat_n_imp[OF sat_n]] . then have "\BG'\Bot_G. BG' \ (\_set N)" using stat_ref_G ground.calculus_axioms bg_in ground_n_entails_bot unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def by blast then show "\B'\ Bot_F. B' \ N" using bg_in Bot_cond Bot_map_not_empty Bot_cond by blast qed end lemma wf_empty_rel: "minimal_element (\_ _. False) UNIV" by (simp add: minimal_element.intro po_on_def transp_onI wfp_on_imp_irreflp_on) lemma any_to_empty_order_lifting: - "tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G \_F - \_Inf Prec_F_g \ tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G + "tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G \_F + \_Inf Prec_F_g \ tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G \_F \_Inf (\g C C'. False)" proof - - fix Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G \_F \_Inf Prec_F_g - assume lift: "tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G + fix Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G \_F \_Inf Prec_F_g + assume lift: "tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G \_F \_Inf Prec_F_g" then interpret lift_g: - tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G \_F + tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G \_F \_Inf Prec_F_g by auto - show "tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G Red_F_G + show "tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G \_F \_Inf (\g C C'. False)" by (simp add: wf_empty_rel lift_g.standard_lifting_axioms tiebreaker_lifting_axioms.intro tiebreaker_lifting_def) qed lemma po_on_empty_rel[simp]: "po_on (\_ _. False) UNIV" unfolding po_on_def irreflp_on_def transp_on_def by auto locale lifting_equivalence_with_empty_order = - any_order_lifting: tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G + any_order_lifting: tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G \_F \_Inf Prec_F_g + - empty_order_lifting: tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_Inf_G + empty_order_lifting: tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G \_F \_Inf "\g C C'. False" for \_F :: \'f \ 'g set\ and \_Inf :: \'f inference \ 'g inference set option\ and Bot_F :: \'f set\ and Inf_F :: \'f inference set\ and Bot_G :: \'g set\ and Inf_G :: \'g inference set\ and entails_G :: \'g set \ 'g set \ bool\ (infix "\G" 50) and - Red_Inf_G :: \'g set \ 'g inference set\ and + Red_I_G :: \'g set \ 'g inference set\ and Red_F_G :: \'g set \ 'g set\ and Prec_F_g :: \'g \ 'f \ 'f \ bool\ sublocale tiebreaker_lifting \ lifting_equivalence_with_empty_order by unfold_locales simp+ context lifting_equivalence_with_empty_order begin (* lem:saturation-indep-of-sqsubset *) lemma saturated_empty_order_equiv_saturated: "any_order_lifting.saturated N = empty_order_lifting.saturated N" by (rule refl) (* lem:static-ref-compl-indep-of-sqsubset *) lemma static_empty_order_equiv_static: "statically_complete_calculus Bot_F Inf_F any_order_lifting.entails_\ - empty_order_lifting.Red_Inf_\ empty_order_lifting.Red_F_\ = + empty_order_lifting.Red_I_\ empty_order_lifting.Red_F_\ = statically_complete_calculus Bot_F Inf_F any_order_lifting.entails_\ - any_order_lifting.Red_Inf_\ any_order_lifting.Red_F_\" + any_order_lifting.Red_I_\ any_order_lifting.Red_F_\" unfolding statically_complete_calculus_def by (rule iffI) (standard,(standard)[],simp)+ (* thm:FRedsqsubset-is-dyn-ref-compl *) theorem static_to_dynamic: "statically_complete_calculus Bot_F Inf_F - any_order_lifting.entails_\ empty_order_lifting.Red_Inf_\ empty_order_lifting.Red_F_\ = + any_order_lifting.entails_\ empty_order_lifting.Red_I_\ empty_order_lifting.Red_F_\ = dynamically_complete_calculus Bot_F Inf_F - any_order_lifting.entails_\ any_order_lifting.Red_Inf_\ any_order_lifting.Red_F_\ " + any_order_lifting.entails_\ any_order_lifting.Red_I_\ any_order_lifting.Red_F_\ " using any_order_lifting.dyn_equiv_stat static_empty_order_equiv_static by blast end subsection \Lifting with a Family of Redundancy Criteria\ locale lifting_intersection = inference_system Inf_F + ground: inference_system_family Q Inf_G_q + ground: consequence_relation_family Bot_G Q entails_q for Inf_F :: "'f inference set" and Bot_G :: "'g set" and Q :: "'q set" and Inf_G_q :: \'q \ 'g inference set\ and entails_q :: "'q \ 'g set \ 'g set \ bool" and - Red_Inf_q :: "'q \ 'g set \ 'g inference set" and + Red_I_q :: "'q \ 'g set \ 'g inference set" and Red_F_q :: "'q \ 'g set \ 'g set" + fixes Bot_F :: "'f set" and \_F_q :: "'q \ 'f \ 'g set" and \_Inf_q :: "'q \ 'f inference \ 'g inference set option" and Prec_F_g :: "'g \ 'f \ 'f \ bool" assumes standard_lifting_family: - "\q \ Q. tiebreaker_lifting Bot_F Inf_F Bot_G (entails_q q) (Inf_G_q q) (Red_Inf_q q) + "\q \ Q. tiebreaker_lifting Bot_F Inf_F Bot_G (entails_q q) (Inf_G_q q) (Red_I_q q) (Red_F_q q) (\_F_q q) (\_Inf_q q) Prec_F_g" begin abbreviation \_set_q :: "'q \ 'f set \ 'g set" where "\_set_q q N \ \ (\_F_q q ` N)" -definition Red_Inf_\_q :: "'q \ 'f set \ 'f inference set" where - "Red_Inf_\_q q N = {\ \ Inf_F. (\_Inf_q q \ \ None \ the (\_Inf_q q \) \ Red_Inf_q q (\_set_q q N)) +definition Red_I_\_q :: "'q \ 'f set \ 'f inference set" where + "Red_I_\_q q N = {\ \ Inf_F. (\_Inf_q q \ \ None \ the (\_Inf_q q \) \ Red_I_q q (\_set_q q N)) \ (\_Inf_q q \ = None \ \_F_q q (concl_of \) \ (\_set_q q N \ Red_F_q q (\_set_q q N)))}" definition Red_F_\_empty_q :: "'q \ 'f set \ 'f set" where "Red_F_\_empty_q q N = {C. \D \ \_F_q q C. D \ Red_F_q q (\_set_q q N)}" -definition Red_F_\_q_g :: "'q \ 'f set \ 'f set" where - "Red_F_\_q_g q N = +definition Red_F_\_q :: "'q \ 'f set \ 'f set" where + "Red_F_\_q q N = {C. \D \ \_F_q q C. D \ Red_F_q q (\_set_q q N) \ (\E \ N. Prec_F_g D E C \ D \ \_F_q q E)}" abbreviation entails_\_q :: "'q \ 'f set \ 'f set \ bool" where "entails_\_q q N1 N2 \ entails_q q (\_set_q q N1) (\_set_q q N2)" lemma red_crit_lifting_family: assumes q_in: "q \ Q" - shows "calculus Bot_F Inf_F (entails_\_q q) (Red_Inf_\_q q) (Red_F_\_q_g q)" + shows "calculus Bot_F Inf_F (entails_\_q q) (Red_I_\_q q) (Red_F_\_q q)" proof - interpret wf_lift: - tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_Inf_q q" + tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_I_q q" "Red_F_q q" "\_F_q q" "\_Inf_q q" Prec_F_g using standard_lifting_family q_in by metis - have "Red_Inf_\_q q = wf_lift.Red_Inf_\" - unfolding Red_Inf_\_q_def wf_lift.Red_Inf_\_def by blast - moreover have "Red_F_\_q_g q = wf_lift.Red_F_\" - unfolding Red_F_\_q_g_def wf_lift.Red_F_\_def by blast + have "Red_I_\_q q = wf_lift.Red_I_\" + unfolding Red_I_\_q_def wf_lift.Red_I_\_def by blast + moreover have "Red_F_\_q q = wf_lift.Red_F_\" + unfolding Red_F_\_q_def wf_lift.Red_F_\_def by blast ultimately show ?thesis using wf_lift.calculus_axioms by simp qed lemma red_crit_lifting_family_empty_ord: assumes q_in: "q \ Q" - shows "calculus Bot_F Inf_F (entails_\_q q) (Red_Inf_\_q q) (Red_F_\_empty_q q)" + shows "calculus Bot_F Inf_F (entails_\_q q) (Red_I_\_q q) (Red_F_\_empty_q q)" proof - interpret wf_lift: - tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_Inf_q q" + tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_I_q q" "Red_F_q q" "\_F_q q" "\_Inf_q q" Prec_F_g using standard_lifting_family q_in by metis - have "Red_Inf_\_q q = wf_lift.Red_Inf_\" - unfolding Red_Inf_\_q_def wf_lift.Red_Inf_\_def by blast + have "Red_I_\_q q = wf_lift.Red_I_\" + unfolding Red_I_\_q_def wf_lift.Red_I_\_def by blast moreover have "Red_F_\_empty_q q = wf_lift.empty_order_lifting.Red_F_\" unfolding Red_F_\_empty_q_def wf_lift.empty_order_lifting.Red_F_\_def by blast ultimately show ?thesis using wf_lift.empty_order_lifting.calculus_axioms by simp qed sublocale consequence_relation_family Bot_F Q entails_\_q proof (unfold_locales; (intro ballI)?) show "Q \ {}" by (rule ground.Q_nonempty) next fix qi assume qi_in: "qi \ Q" interpret lift: tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q qi" "Inf_G_q qi" - "Red_Inf_q qi" "Red_F_q qi" "\_F_q qi" "\_Inf_q qi" Prec_F_g + "Red_I_q qi" "Red_F_q qi" "\_F_q qi" "\_Inf_q qi" Prec_F_g using qi_in by (metis standard_lifting_family) show "consequence_relation Bot_F (entails_\_q qi)" by unfold_locales qed -sublocale intersection_calculus Bot_F Inf_F Q entails_\_q Red_Inf_\_q Red_F_\_q_g +sublocale intersection_calculus Bot_F Inf_F Q entails_\_q Red_I_\_q Red_F_\_q by unfold_locales (auto simp: Q_nonempty red_crit_lifting_family) -abbreviation entails_\_Q :: "'f set \ 'f set \ bool" (infix "\\\" 50) where - "(\\\) \ entails_Q" - -abbreviation Red_Inf_\_Q :: "'f set \ 'f inference set" where - "Red_Inf_\_Q \ Red_Inf_Q" +abbreviation entails_\ :: "'f set \ 'f set \ bool" (infix "\\\" 50) where + "(\\\) \ entails" -abbreviation Red_F_\_Q :: "'f set \ 'f set" where - "Red_F_\_Q \ Red_F_Q" +abbreviation Red_I_\ :: "'f set \ 'f inference set" where + "Red_I_\ \ Red_I" -lemmas entails_\_Q_def = entails_Q_def -lemmas Red_Inf_\_Q_def = Red_Inf_Q_def -lemmas Red_F_\_Q_def = Red_F_Q_def +abbreviation Red_F_\ :: "'f set \ 'f set" where + "Red_F_\ \ Red_F" -sublocale empty_ord: intersection_calculus Bot_F Inf_F Q entails_\_q Red_Inf_\_q +lemmas entails_\_def = entails_def +lemmas Red_I_\_def = Red_I_def +lemmas Red_F_\_def = Red_F_def + +sublocale empty_ord: intersection_calculus Bot_F Inf_F Q entails_\_q Red_I_\_q Red_F_\_empty_q by unfold_locales (auto simp: Q_nonempty red_crit_lifting_family_empty_ord) abbreviation Red_F_\_empty :: "'f set \ 'f set" where - "Red_F_\_empty \ empty_ord.Red_F_Q" + "Red_F_\_empty \ empty_ord.Red_F" -lemmas Red_F_\_empty_def = empty_ord.Red_F_Q_def +lemmas Red_F_\_empty_def = empty_ord.Red_F_def lemma sat_inf_imp_ground_red_fam_inter: assumes sat_n: "saturated N" and i'_in: "\' \ Inf_from N" and q_in: "q \ Q" and grounding: "\_Inf_q q \' \ None \ \ \ the (\_Inf_q q \')" - shows "\ \ Red_Inf_q q (\_set_q q N)" + shows "\ \ Red_I_q q (\_set_q q N)" proof - - have "\' \ Red_Inf_\_q q N" + have "\' \ Red_I_\_q q N" using sat_n i'_in q_in all_red_crit calculus.saturated_def sat_int_to_sat_q by blast - then have "the (\_Inf_q q \') \ Red_Inf_q q (\_set_q q N)" - by (simp add: Red_Inf_\_q_def grounding) + then have "the (\_Inf_q q \') \ Red_I_q q (\_set_q q N)" + by (simp add: Red_I_\_q_def grounding) then show ?thesis using grounding by blast qed abbreviation ground_Inf_redundant :: "'q \ 'f set \ bool" where "ground_Inf_redundant q N \ ground.Inf_from_q q (\_set_q q N) - \ {\. \\'\ Inf_from N. \_Inf_q q \' \ None \ \ \ the (\_Inf_q q \')} \ Red_Inf_q q (\_set_q q N)" + \ {\. \\'\ Inf_from N. \_Inf_q q \' \ None \ \ \ the (\_Inf_q q \')} \ Red_I_q q (\_set_q q N)" abbreviation ground_saturated :: "'q \ 'f set \ bool" where - "ground_saturated q N \ ground.Inf_from_q q (\_set_q q N) \ Red_Inf_q q (\_set_q q N)" + "ground_saturated q N \ ground.Inf_from_q q (\_set_q q N) \ Red_I_q q (\_set_q q N)" lemma sat_imp_ground_sat_fam_inter: "saturated N \ q \ Q \ ground_Inf_redundant q N \ ground_saturated q N" using sat_inf_imp_ground_red_fam_inter by auto (* thm:intersect-finf-complete *) theorem stat_ref_comp_to_non_ground_fam_inter: assumes stat_ref_G: - "\q \ Q. statically_complete_calculus Bot_G (Inf_G_q q) (entails_q q) (Red_Inf_q q) + "\q \ Q. statically_complete_calculus Bot_G (Inf_G_q q) (entails_q q) (Red_I_q q) (Red_F_q q)" and sat_n_imp: "\N. saturated N \ \q \ Q. ground_Inf_redundant q N" shows - "statically_complete_calculus Bot_F Inf_F entails_\_Q Red_Inf_\_Q Red_F_\_empty" + "statically_complete_calculus Bot_F Inf_F entails_\ Red_I_\ Red_F_\_empty" using empty_ord.calculus_axioms unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def proof (standard, clarify) fix B N assume b_in: "B \ Bot_F" and sat_n: "saturated N" and entails_bot: "N \\\ {B}" then obtain q where q_in: "q \ Q" and inf_subs: "ground.Inf_from_q q (\_set_q q N) \ {\. \\'\ Inf_from N. \_Inf_q q \' \ None \ \ \ the (\_Inf_q q \')} - \ Red_Inf_q q (\_set_q q N)" + \ Red_I_q q (\_set_q q N)" using sat_n_imp[of N] by blast - interpret q_calc: calculus Bot_F Inf_F "entails_\_q q" "Red_Inf_\_q q" "Red_F_\_q_g q" + interpret q_calc: calculus Bot_F Inf_F "entails_\_q q" "Red_I_\_q q" "Red_F_\_q q" using all_red_crit[rule_format, OF q_in] . have n_q_sat: "q_calc.saturated N" using q_in sat_int_to_sat_q sat_n by simp interpret lifted_q_calc: - tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_Inf_q q" + tiebreaker_lifting Bot_F Inf_F Bot_G "entails_q q" "Inf_G_q q" "Red_I_q q" "Red_F_q q" "\_F_q q" "\_Inf_q q" using q_in by (simp add: standard_lifting_family) have n_lift_sat: "lifted_q_calc.empty_order_lifting.saturated N" - using n_q_sat unfolding Red_Inf_\_q_def lifted_q_calc.empty_order_lifting.Red_Inf_\_def + using n_q_sat unfolding Red_I_\_q_def lifted_q_calc.empty_order_lifting.Red_I_\_def lifted_q_calc.saturated_def q_calc.saturated_def by auto have ground_sat_n: "lifted_q_calc.ground.saturated (\_set_q q N)" by (rule lifted_q_calc.sat_imp_ground_sat[OF n_lift_sat]) (use n_lift_sat inf_subs ground.Inf_from_q_def in auto) have ground_n_entails_bot: "entails_\_q q N {B}" - using q_in entails_bot unfolding entails_\_Q_def by simp - interpret statically_complete_calculus Bot_G "Inf_G_q q" "entails_q q" "Red_Inf_q q" + using q_in entails_bot unfolding entails_\_def by simp + interpret statically_complete_calculus Bot_G "Inf_G_q q" "entails_q q" "Red_I_q q" "Red_F_q q" using stat_ref_G[rule_format, OF q_in] . obtain BG where bg_in: "BG \ \_F_q q B" using lifted_q_calc.Bot_map_not_empty[OF b_in] by blast then have "BG \ Bot_G" using lifted_q_calc.Bot_map[OF b_in] by blast then have "\BG'\Bot_G. BG' \ \_set_q q N" using ground_sat_n ground_n_entails_bot statically_complete[of BG, OF _ ground_sat_n] bg_in lifted_q_calc.ground.entail_set_all_formulas[of "\_set_q q N" "\_set_q q {B}"] by simp then show "\B'\ Bot_F. B' \ N" using lifted_q_calc.Bot_cond by blast qed (* lem:intersect-saturation-indep-of-sqsubset *) lemma sat_eq_sat_empty_order: "saturated N = empty_ord.saturated N" by (rule refl) (* lem:intersect-static-ref-compl-indep-of-sqsubset *) lemma static_empty_ord_inter_equiv_static_inter: - "statically_complete_calculus Bot_F Inf_F entails_Q Red_Inf_Q Red_F_Q = - statically_complete_calculus Bot_F Inf_F entails_Q Red_Inf_Q Red_F_\_empty" + "statically_complete_calculus Bot_F Inf_F entails Red_I Red_F = + statically_complete_calculus Bot_F Inf_F entails Red_I Red_F_\_empty" unfolding statically_complete_calculus_def by (simp add: empty_ord.calculus_axioms calculus_axioms) (* thm:intersect-static-ref-compl-is-dyn-ref-compl-with-order *) theorem stat_eq_dyn_ref_comp_fam_inter: "statically_complete_calculus Bot_F Inf_F - entails_Q Red_Inf_Q Red_F_\_empty = - dynamically_complete_calculus Bot_F Inf_F entails_Q Red_Inf_Q Red_F_Q" + entails Red_I Red_F_\_empty = + dynamically_complete_calculus Bot_F Inf_F entails Red_I Red_F" using dyn_equiv_stat static_empty_ord_inter_equiv_static_inter by blast end end