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 :: "'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" 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)" +definition Inf_between :: "'f set \ 'f set \ 'f inference set" where + "Inf_between 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_if_Inf_between: "\ \ Inf_between N M \ \ \ Inf" + unfolding Inf_between_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_between_alt: + "Inf_between N M = {\ \ Inf. \ \ Inf_from (N \ M) \ set (prems_of \) \ M \ {}}" + unfolding Inf_from_def Inf_between_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 +lemma Inf_between_mono: "N \ N' \ M \ M' \ Inf_between N M \ Inf_between N' M'" + unfolding Inf_between_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)" +definition Inf_between_q :: "'q \ 'f set \ 'f set \ 'f inference set" where + "Inf_between_q q = inference_system.Inf_between (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 +lemma Inf_between_q_alt: + "Inf_between_q q N M = {\ \ Inf_q q. \ \ Inf_from_q q (N \ M) \ set (prems_of \) \ M \ {}}" + unfolding Inf_from_q_def Inf_between_q_def inference_system.Inf_between_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_I :: "'f set \ 'f inference set" and Red_F :: "'f set \ 'f set" assumes 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_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_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_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_I N" proof - 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_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_I_of_subset calculus_axioms sup_bot.right_neutral) qed definition saturated :: "'f set \ bool" where "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_I N" 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_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_I D)" + "fair Ns \ Inf_from (Liminf_llist Ns) \ Sup_llist (lmap Red_I Ns)" 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" + in_Sup: "C \ Sup_llist Ns" and + not_in_Liminf: "C \ Liminf_llist Ns" shows - "\i \ {i. enat (Suc i) < llength D}. C \ lnth D i - lnth D (Suc i)" + "\i \ {i. enat (Suc i) < llength Ns}. C \ lnth Ns i - lnth Ns (Suc i)" proof - - obtain i where C_D_i: "C \ Sup_upto_llist D (enat i)" and "enat i < llength D" + obtain i where C_D_i: "C \ Sup_upto_llist Ns (enat i)" and "enat i < llength Ns" 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" + then obtain j where j: "j \ i \ enat j < llength Ns \ C \ lnth Ns 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 + obtain k where k: "C \ lnth Ns k" "enat k < llength Ns" "k \ i" using C_D_i unfolding Sup_upto_llist_def by auto - let ?S = "{i. i < j \ i \ k \ C \ lnth D i}" + let ?S = "{i. i < j \ i \ k \ C \ lnth Ns 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] + have \k \ {i. i < j \ k \ i \ C \ lnth Ns i}\ using k j by (auto simp: order.order_iff_strict) + then have nempty: "{i. i < j \ k \ i \ C \ lnth Ns i} \ {}" by auto + then have l_prop: "l < j \ l \ k \ C \ lnth Ns 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"] + then have "C \ lnth Ns l - lnth Ns (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}" + show "l \ {i. enat (Suc i) < llength Ns}" 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)" + assumes deriv: "chain (\Red) Ns" + shows "Sup_llist Ns - Liminf_llist Ns \ Red_F (Sup_llist Ns)" proof fix C - assume C_in_subset: "C \ Sup_llist D - Liminf_llist D" + assume C_in_subset: "C \ Sup_llist Ns - Liminf_llist Ns" { 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 + in_ith_elem: "C \ lnth Ns i - lnth Ns (Suc i)" and + i: "enat (Suc i) < llength Ns" + have "lnth Ns i \Red lnth Ns (Suc i)" using i deriv in_ith_elem chain_lnth_rel by auto + then have "C \ Red_F (lnth Ns (Suc i))" using in_ith_elem derive.cases by blast + then have "C \ Red_F (Sup_llist Ns)" 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 + then show "C \ Red_F (Sup_llist Ns)" using equiv_Sup_Liminf[of C] C_in_subset by fast qed (* lem:redundant-remains-redundant-during-run 1/2 *) lemma Red_I_subset_Liminf: - assumes deriv: \chain (\Red) D\ and - i: \enat i < llength D\ - shows \Red_I (lnth D i) \ Red_I (Liminf_llist D)\ + assumes deriv: \chain (\Red) Ns\ and + i: \enat i < llength Ns\ + shows \Red_I (lnth Ns i) \ Red_I (Liminf_llist Ns)\ proof - - have Sup_in_diff: \Red_I (Sup_llist D) \ Red_I (Sup_llist D - (Sup_llist D - Liminf_llist D))\ + have Sup_in_diff: \Red_I (Sup_llist Ns) \ Red_I (Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns))\ 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\ + also have \Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns) = Liminf_llist Ns\ by (simp add: Liminf_llist_subset_Sup_llist double_diff) - then have Red_I_Sup_in_Liminf: \Red_I (Sup_llist D) \ Red_I (Liminf_llist D)\ + then have Red_I_Sup_in_Liminf: \Red_I (Sup_llist Ns) \ Red_I (Liminf_llist Ns)\ using Sup_in_diff by auto - have \lnth D i \ Sup_llist D\ unfolding Sup_llist_def using i by blast - then have "Red_I (lnth D i) \ Red_I (Sup_llist D)" using Red_I_of_subset + have \lnth Ns i \ Sup_llist Ns\ unfolding Sup_llist_def using i by blast + then have "Red_I (lnth Ns i) \ Red_I (Sup_llist Ns)" using Red_I_of_subset unfolding Sup_llist_def 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)\ + assumes deriv: \chain (\Red) Ns\ and + i: \enat i < llength Ns\ + shows \Red_F (lnth Ns i) \ Red_F (Liminf_llist Ns)\ proof - - have Sup_in_diff: \Red_F (Sup_llist D) \ Red_F (Sup_llist D - (Sup_llist D - Liminf_llist D))\ + have Sup_in_diff: \Red_F (Sup_llist Ns) \ Red_F (Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns))\ 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\ + also have \Sup_llist Ns - (Sup_llist Ns - Liminf_llist Ns) = Liminf_llist Ns\ 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)\ + then have Red_F_Sup_in_Liminf: \Red_F (Sup_llist Ns) \ Red_F (Liminf_llist Ns)\ 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 + have \lnth Ns i \ Sup_llist Ns\ unfolding Sup_llist_def using i by blast + then have "Red_F (lnth Ns i) \ Red_F (Sup_llist Ns)" 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\ + deriv: \chain (\Red) Ns\ and + i: \enat i < llength Ns\ + shows \lnth Ns i \ Red_F (Liminf_llist Ns) \ Liminf_llist Ns\ 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))\ + assume C: \C \ lnth Ns i\ + and C_not_Liminf: \C \ Liminf_llist Ns\ + have \C \ Sup_llist Ns\ unfolding Sup_llist_def using C i by auto + then obtain j where j: \C \ lnth Ns j - lnth Ns (Suc j)\ \enat (Suc j) < llength Ns\ + using equiv_Sup_Liminf[of C Ns] C_not_Liminf by auto + then have \C \ Red_F (lnth Ns (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 + then show \C \ Red_F (Liminf_llist Ns)\ using Red_F_subset_Liminf[of Ns "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)\ + deriv: \chain (\Red) Ns\ and + fair: \fair Ns\ + shows \saturated (Liminf_llist Ns)\ unfolding saturated_def proof fix \ - assume \: \\ \ Inf_from (Liminf_llist D)\ - 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)\ + assume \: \\ \ Inf_from (Liminf_llist Ns)\ + have \\ \ Sup_llist (lmap Red_I Ns)\ using fair \ unfolding fair_def by auto + then obtain i where i: \enat i < llength Ns\ \\ \ Red_I (lnth Ns i)\ unfolding Sup_llist_def by auto - then show \\ \ Red_I (Liminf_llist D)\ - using deriv i_in_Liminf_or_Red_F[of D i] Red_I_subset_Liminf by blast + then show \\ \ Red_I (Liminf_llist Ns)\ + using deriv i_in_Liminf_or_Red_F[of Ns 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 + fixes B Ns 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\ + deriv: \chain (\Red) Ns\ and + fair: \fair Ns\ and + unsat: \lhd Ns \ {B}\ + shows \\B'\Bot. B' \ Liminf_llist Ns\ 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}\ + have non_empty: \\ lnull Ns\ using chain_not_lnull[OF deriv] . + have subs: \lhd Ns \ Sup_llist Ns\ + using lhd_subset_Sup_llist[of Ns] non_empty by (simp add: lhd_conv_lnth) + have \Sup_llist Ns \ {B}\ + using unsat subset_entailed[OF subs] entails_trans[of "Sup_llist Ns" "lhd Ns"] by auto + then have Sup_no_Red: \Sup_llist Ns - Red_F (Sup_llist Ns) \ {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\ + have Sup_no_Red_in_Liminf: \Sup_llist Ns - Red_F (Sup_llist Ns) \ Liminf_llist Ns\ using deriv Red_in_Sup by auto - have Liminf_entails_Bot: \Liminf_llist D \ {B}\ + have Liminf_entails_Bot: \Liminf_llist Ns \ {B}\ using Sup_no_Red subset_entailed[OF Sup_no_Red_in_Liminf] entails_trans by blast - have \saturated (Liminf_llist D)\ + have \saturated (Liminf_llist Ns)\ 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" + dynamically_complete: "B \ Bot \ chain (\Red) Ns \ fair Ns \ lhd Ns \ {B} \ + \i \ {i. enat i < llength Ns}. \B'\Bot. B' \ lnth Ns 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_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 + define Ns where "Ns = LCons N LNil" + have[simp]: \\ lnull Ns\ by (auto simp: Ns_def) + have deriv_D: \chain (\Red) Ns\ by (simp add: chain.chain_singleton Ns_def) + have liminf_is_N: "Liminf_llist Ns = N" by (simp add: Ns_def Liminf_llist_LCons) + have head_D: "N = lhd Ns" by (simp add: Ns_def) + have "Sup_llist (lmap Red_I Ns) = Red_I N" by (simp add: Ns_def) + then have fair_D: "fair Ns" 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 Ns i" and \i < llength Ns\ + using dynamically_complete[of B Ns] 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) + by (auto simp: Ns_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 + using B'_is_bot B'_in unfolding \i = 0\ head_D[symmetric] Ns_def by auto qed end (* lem:static-ref-compl-implies-dynamic *) sublocale statically_complete_calculus \ dynamically_complete_calculus proof - fix B D + fix B Ns assume \B \ Bot\ and - \chain (\Red) D\ and - \fair D\ and - \lhd D \ {B}\ - then have \\B'\Bot. B' \ Liminf_llist D\ + \chain (\Red) Ns\ and + \fair Ns\ and + \lhd Ns \ {B}\ + then have \\B'\Bot. B' \ Liminf_llist Ns\ by (rule dynamically_complete_Liminf) - then show \\i\{i. enat i < llength D}. \B'\Bot. B' \ lnth D i\ + then show \\i\{i. enat i < llength Ns}. \B'\Bot. B' \ lnth Ns 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_I Red_F for Bot :: "'f set" and Inf :: \'f inference set\ and entails :: "'f set \ 'f set \ bool" (infix "\" 50) 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_I N" + inf_in_red_inf: "Inf_between 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_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 + using red_sat_n inf_in_red_inf unfolding reduc_saturated_def Inf_from_def Inf_between_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_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_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_I :: "'f set \ 'f inference set" where - "Red_Red_I N = Red_I N \ Inf_from2 UNIV (Red_F N)" + "Red_Red_I N = Red_I N \ Inf_between UNIV (Red_F N)" lemma reduced_calc_is_calc: "calculus Bot Inf entails Red_Red_I Red_F" proof fix N show "Red_Red_I N \ Inf" - unfolding Red_Red_I_def Inf_from2_def Inf_from_def using Red_I_to_Inf by auto + unfolding Red_Red_I_def Inf_between_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 have "Inf_between UNIV (Red_F N) \ Inf_between UNIV (Red_F N')" + unfolding Inf_between_def by auto 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 have "Inf_between UNIV (Red_F N) \ Inf_between UNIV (Red_F (N - N'))" + unfolding Inf_between_def by auto 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_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_I N" +lemma inf_subs_reduced_red_inf: "Inf_between 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_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_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_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_I N" using i_in red_sat_n - unfolding reduc_saturated_def Inf_from2_def Inf_from_def Red_Red_I_def by blast + unfolding reduc_saturated_def Inf_between_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_I N" using i_in red_sat_n - unfolding Inf_from_def reduc_calc.saturated_def Red_Red_I_def Inf_from2_def by blast + unfolding Inf_from_def reduc_calc.saturated_def Red_Red_I_def Inf_between_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_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_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_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_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_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_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)" + "chain derive Ns \ Sup_llist (lmap Red_F Ns) \ Red_F (Liminf_llist Ns)" 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)" + deriv: "chain derive Ns" and + n_in_sup: "N \ Sup_llist (lmap Red_F Ns)" + obtain i0 where i_smaller: "enat i0 < llength Ns" and n_in: "N \ Red_F (lnth Ns 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)" + have "Red_F (lnth Ns i0) \ Red_F (Liminf_llist Ns)" using i_smaller by (simp add: deriv Red_F_subset_Liminf) - then show "N \ Red_F (Liminf_llist D)" + then show "N \ Red_F (Liminf_llist Ns)" using n_in by fast qed lemma sup_red_inf_in_red_liminf: - "chain derive D \ Sup_llist (lmap Red_I D) \ Red_I (Liminf_llist D)" + "chain derive Ns \ Sup_llist (lmap Red_I Ns) \ Red_I (Liminf_llist Ns)" proof fix \ assume - deriv: "chain derive D" and - 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)" + deriv: "chain derive Ns" and + i_in_sup: "\ \ Sup_llist (lmap Red_I Ns)" + obtain i0 where i_smaller: "enat i0 < llength Ns" and n_in: "\ \ Red_I (lnth Ns i0)" using i_in_sup unfolding Sup_llist_def by auto - have "Red_I (lnth D i0) \ Red_I (Liminf_llist D)" + have "Red_I (lnth Ns i0) \ Red_I (Liminf_llist Ns)" using i_smaller by (simp add: deriv Red_I_subset_Liminf) - then show "\ \ Red_I (Liminf_llist D)" + then show "\ \ Red_I (Liminf_llist Ns)" 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_I D)" + "reduc_fair Ns \ + Inf_from (Liminf_llist Ns - Sup_llist (lmap Red_F Ns)) \ Sup_llist (lmap Red_I Ns)" (* lem:red-fairness-implies-red-saturation *) lemma reduc_fair_imp_Liminf_reduc_sat: - "chain derive D \ reduc_fair D \ reduc_saturated (Liminf_llist D)" + "chain derive Ns \ reduc_fair Ns \ reduc_saturated (Liminf_llist Ns)" unfolding reduc_saturated_def proof - - fix D + fix Ns 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))" + deriv: "chain derive Ns" and + red_fair: "reduc_fair Ns" + have "Inf_from (Liminf_llist Ns - Red_F (Liminf_llist Ns)) + \ Inf_from (Liminf_llist Ns - Sup_llist (lmap Red_F Ns))" 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_I D)" + then have "Inf_from (Liminf_llist Ns - Red_F (Liminf_llist Ns)) \ Sup_llist (lmap Red_I Ns)" using red_fair unfolding reduc_fair_def by simp - then show "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) \ Red_I (Liminf_llist D)" + then show "Inf_from (Liminf_llist Ns - Red_F (Liminf_llist Ns)) \ Red_I (Liminf_llist Ns)" 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" + reducedly_dynamically_complete: "B \ Bot \ chain derive Ns \ reduc_fair Ns \ + lhd Ns \ {B} \ \i \ {i. enat i < llength Ns}. \ B'\Bot. B' \ lnth Ns 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_I D) = Red_I N" by (simp add: D_def) - ultimately have fair_D: "reduc_fair D" + define Ns where "Ns = LCons N LNil" + have[simp]: \\ lnull Ns\ by (auto simp: Ns_def) + have deriv_D: \chain (\Red) Ns\ by (simp add: chain.chain_singleton Ns_def) + have liminf_is_N: "Liminf_llist Ns = N" by (simp add: Ns_def Liminf_llist_LCons) + have head_D: "N = lhd Ns" by (simp add: Ns_def) + have "Sup_llist (lmap Red_F Ns) = Red_F N" by (simp add: Ns_def) + moreover have "Sup_llist (lmap Red_I Ns) = Red_I N" by (simp add: Ns_def) + ultimately have fair_D: "reduc_fair Ns" 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 + obtain i B' where B'_is_bot: \B' \ Bot\ and B'_in: "B' \ lnth Ns i" and \i < llength Ns\ + using reducedly_dynamically_complete[of B Ns] 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) + by (auto simp: Ns_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 + using B'_is_bot B'_in unfolding \i = 0\ head_D[symmetric] Ns_def by auto qed end sublocale reducedly_statically_complete_calculus \ reducedly_dynamically_complete_calculus proof - fix B D + fix B Ns 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}\ + deriv: \chain (\Red) Ns\ and + fair: \reduc_fair Ns\ and + unsat: \lhd Ns \ {B}\ + have non_empty: \\ lnull Ns\ using chain_not_lnull[OF deriv] . + have subs: \lhd Ns \ Sup_llist Ns\ + using lhd_subset_Sup_llist[of Ns] non_empty by (simp add: lhd_conv_lnth) + have \Sup_llist Ns \ {B}\ + using unsat subset_entailed[OF subs] entails_trans[of "Sup_llist Ns" "lhd Ns"] by auto + then have Sup_no_Red: \Sup_llist Ns - Red_F (Sup_llist Ns) \ {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\ + have Sup_no_Red_in_Liminf: \Sup_llist Ns - Red_F (Sup_llist Ns) \ Liminf_llist Ns\ using deriv Red_in_Sup by auto - have Liminf_entails_Bot: \Liminf_llist D \ {B}\ + have Liminf_entails_Bot: \Liminf_llist Ns \ {B}\ using Sup_no_Red subset_entailed[OF Sup_no_Red_in_Liminf] entails_trans by blast - have \reduc_saturated (Liminf_llist D)\ + have \reduc_saturated (Liminf_llist Ns)\ using deriv fair reduc_fair_imp_Liminf_reduc_sat unfolding reduc_saturated_def by auto - then have \\B'\Bot. B' \ Liminf_llist D\ + then have \\B'\Bot. B' \ Liminf_llist Ns\ 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\ + then show \\i\{i. enat i < llength Ns}. \B'\Bot. B' \ lnth Ns i\ unfolding Liminf_llist_def by auto qed context calculus begin 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_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_I Red_F" by (simp add: statically_complete_calculus_axioms) next 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_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_I Red_F = reducedly_statically_complete_calculus Bot Inf entails Red_I Red_F" proof 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_I Red_F" by (simp add: reducedly_statically_complete_calculus_axioms) next 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_I Red_F" by (simp add: reducedly_dynamically_complete_calculus_axioms) qed 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_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_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_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,1174 +1,1174 @@ (* 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_I_q Red_F_q \_F_q \_Inf_q Inf_FL + entails_q Inf_G_q Red_I_q Red_F_q \_F_q \_I_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_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 \_I_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_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_I Red_F using labeled_static_ref[OF static_ref_comp] . lemma labeled_tiebreaker_lifting: assumes q_in: "q \ Q" shows "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) - (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q) (\g. Prec_FL)" + (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_I_L_q q) (\g. Prec_FL)" proof - have "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) - (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q) (\g Cl Cl'. False)" + (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_I_L_q q) (\g Cl Cl'. False)" using ord_fam_lifted_q[OF q_in] . then have "standard_lifting 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)" + (Red_F_q q) (\_F_L_q q) (\_I_L_q q)" using lifted_q[OF q_in] by blast then show "tiebreaker_lifting Bot_FL Inf_FL Bot_G (entails_q q) (Inf_G_q q) - (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q) (\g. Prec_FL)" + (Red_I_q q) (Red_F_q q) (\_F_L_q q) (\_I_L_q q) (\g. Prec_FL)" using wf_prec_FL by (simp add: tiebreaker_lifting.intro tiebreaker_lifting_axioms.intro) qed sublocale lifting_intersection Inf_FL Bot_G Q Inf_G_q entails_q Red_I_q Red_F_q - Bot_FL \_F_L_q \_Inf_L_q "\g. Prec_FL" + Bot_FL \_F_L_q \_I_L_q "\g. Prec_FL" using labeled_tiebreaker_lifting unfolding lifting_intersection_def by (simp add: lifting_intersection_axioms.intro no_labels.ground.consequence_relation_family_axioms no_labels.ground.inference_system_family_axioms) notation derive (infix "\RedL" 50) lemma std_Red_I_eq: "std.Red_I = Red_I_\" unfolding Red_I_\_q_def Red_I_\_L_q_def by simp lemma std_Red_F_eq: "std.Red_F = Red_F_\_empty" unfolding Red_F_\_empty_q_def Red_F_\_empty_L_q_def by simp sublocale statically_complete_calculus Bot_FL Inf_FL "(\\\L)" Red_I Red_F by unfold_locales (use statically_complete std_Red_I_eq in auto) (* lem:redundant-labeled-inferences *) lemma labeled_red_inf_eq_red_inf: assumes i_in: "\ \ Inf_FL" shows "\ \ Red_I N \ to_F \ \ no_labels.Red_I_\ (fst ` N)" proof assume i_in2: "\ \ Red_I N" then have "X \ Red_I_\_q ` Q \ \ \ X N" for X unfolding Red_I_def by blast obtain X0 where "X0 \ Red_I_\_q ` Q" using Q_nonempty by blast then obtain q0 where x0_is: "X0 N = Red_I_\_q q0 N" by blast then obtain Y0 where y0_is: "Y0 (fst ` N) = to_F ` (X0 N)" by auto have "Y0 (fst ` N) = no_labels.Red_I_\_q q0 (fst ` N)" unfolding y0_is proof show "to_F ` X0 N \ no_labels.Red_I_\_q q0 (fst ` N)" proof fix \0 assume i0_in: "\0 \ to_F ` X0 N" then have i0_in2: "\0 \ to_F ` Red_I_\_q q0 N" using x0_is by argo then obtain \0_FL where i0_FL_in: "\0_FL \ Inf_FL" and i0_to_i0_FL: "\0 = to_F \0_FL" and - subs1: "((\_Inf_L_q q0 \0_FL) \ None \ - the (\_Inf_L_q q0 \0_FL) \ Red_I_q q0 (\_set_q q0 N)) - \ ((\_Inf_L_q q0 \0_FL = None) \ + subs1: "((\_I_L_q q0 \0_FL) \ None \ + the (\_I_L_q q0 \0_FL) \ Red_I_q q0 (\_set_q q0 N)) + \ ((\_I_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_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_I_q q0 (no_labels.\_set_q q0 (fst ` N))" + not_none: "\_I_q q0 \0 \ None" and + "the (\_I_q q0 \0) \ {}" + then obtain \1 where i1_in: "\1 \ the (\_I_q q0 \0)" by blast + have "the (\_I_q q0 \0) \ Red_I_q q0 (no_labels.\_set_q q0 (fst ` N))" using subs1 i0_to_i0_FL not_none by auto } moreover { assume - is_none: "\_Inf_q q0 \0 = None" + is_none: "\_I_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_I_\_q q0 (fst ` N)" unfolding no_labels.Red_I_\_q_def using i0_in3 by auto qed next show "no_labels.Red_I_\_q q0 (fst ` N) \ to_F ` X0 N" proof fix \0 assume i0_in: "\0 \ no_labels.Red_I_\_q q0 (fst ` N)" then have i0_in2: "\0 \ Inf_F" unfolding no_labels.Red_I_\_q_def by blast obtain \0_FL where i0_FL_in: "\0_FL \ Inf_FL" and i0_to_i0_FL: "\0 = to_F \0_FL" using Inf_F_to_Inf_FL[OF i0_in2] unfolding to_F_def by (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_I_q q0 (\_set_q q0 N)) - \ ((\_Inf_L_q q0 \0_FL = None) \ + have subs1: "((\_I_L_q q0 \0_FL) \ None \ + the (\_I_L_q q0 \0_FL) \ Red_I_q q0 (\_set_q q0 N)) + \ ((\_I_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_I_\_q_def by simp then have "\0_FL \ Red_I_\_q q0 N" using i0_FL_in unfolding Red_I_\_q_def by simp then show "\0 \ to_F ` X0 N" using x0_is i0_to_i0_FL i0_in2 by blast qed qed then have "Y \ no_labels.Red_I_\_q ` Q \ to_F \ \ Y (fst ` N)" for Y using i_in2 no_labels.Red_I_def std_Red_I_eq red_inf_impl by force then show "to_F \ \ no_labels.Red_I_\ (fst ` N)" unfolding Red_I_def no_labels.Red_I_\_def by blast next assume to_F_in: "to_F \ \ no_labels.Red_I_\ (fst ` N)" have imp_to_F: "X \ no_labels.Red_I_\_q ` Q \ to_F \ \ X (fst ` N)" for X using to_F_in unfolding no_labels.Red_I_\_def by blast then have to_F_in2: "to_F \ \ no_labels.Red_I_\_q q (fst ` N)" if "q \ Q" for q using that by auto have "Red_I_\_q q N = {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_I_\_q q (fst ` N)}" for q proof show "Red_I_\_q q N \ {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_I_\_q q (fst ` N)}" proof fix q0 \1 assume i1_in: "\1 \ Red_I_\_q q0 N" have i1_in2: "\1 \ Inf_FL" using i1_in unfolding Red_I_\_q_def by blast then have to_F_i1_in: "to_F \1 \ Inf_F" using Inf_FL_to_Inf_F unfolding to_F_def by 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_I_\_q q0 (fst ` N)" using i1_in to_F_i1_in unfolding Red_I_\_q_def no_labels.Red_I_\_q_def by force show "\1 \ {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_I_\_q q0 (fst ` N)}" using i1_in2 i1_to_F_in by blast qed next show "{\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_I_\_q q (fst ` N)} \ Red_I_\_q q N" proof fix q0 \1 assume i1_in: "\1 \ {\0_FL \ Inf_FL. to_F \0_FL \ no_labels.Red_I_\_q q0 (fst ` N)}" then have i1_in2: "\1 \ Inf_FL" by blast then have to_F_i1_in: "to_F \1 \ Inf_F" using Inf_FL_to_Inf_F unfolding to_F_def by 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_I_q q0 (\_set_q q0 N)) - \ (\_Inf_L_q q0 \1 = None \ + then have "((\_I_L_q q0 \1) \ None \ the (\_I_L_q q0 \1) \ Red_I_q q0 (\_set_q q0 N)) + \ (\_I_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_I_\_q_def by auto then show "\1 \ Red_I_\_q q0 N" using i1_in2 unfolding Red_I_\_q_def by blast qed qed then have "\ \ Red_I_\_q q N" if "q \ Q" for q using that to_F_in2 i_in unfolding Red_I_\_q_def no_labels.Red_I_\_q_def by auto then show "\ \ Red_I_\ N" unfolding Red_I_\_def by blast qed (* 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 N\ proof - note assms moreover have i: \C \ no_labels.Red_F_\_empty (fst ` N) \ (C, L) \ Red_F N\ proof - assume "C \ no_labels.Red_F_\_empty (fst ` N)" then have "C \ no_labels.Red_F_\_empty_q q (fst ` N)" if "q \ Q" for q unfolding no_labels.Red_F_\_empty_def using that by fast then have g_in_red: "\_F_q q C \ Red_F_q q (no_labels.\_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_def Red_F_\_q_def by blast qed moreover have ii: \\C' \ fst ` N. C' \\ C \ (C, L) \ Red_F N\ proof - assume "\C' \ fst ` N. C' \\ C" then obtain C' where c'_in: "C' \ fst ` N" and c_prec_c': "C' \\ C" by blast obtain L' where c'_l'_in: "(C', L') \ N" using c'_in by auto have c'_l'_prec: "(C', L') \ (C, L)" using c_prec_c' unfolding Prec_FL_def by simp have c_in_c'_g: "\_F_q q C \ \_F_q q C'" if "q \ Q" for q using prec_F_grounding[OF that c_prec_c'] by presburger then have "\_F_L_q q (C, L) \ \_F_L_q q (C', L')" if "q \ Q" for q using that by auto then have "(C, L) \ Red_F_\_q q N" if "q \ Q" for q unfolding Red_F_\_q_def using that c'_l'_in c'_l'_prec by blast then show ?thesis unfolding Red_F_def by blast qed moreover have iii: \\(C', L') \ N. L' \l L \ C' \\ C \ (C, L) \ Red_F N\ proof - assume "\(C', L') \ N. L' \l L \ C' \\ C" then obtain C' L' where c'_l'_in: "(C', L') \ N" and l'_sub_l: "L' \l L" and c'_sub_c: "C' \\ C" by fast have "(C, L) \ Red_F N" if "C' \\ C" using that c'_l'_in ii by fastforce moreover { assume equiv_c_c': "C \ C'" then have equiv_c'_c: "C' \ C" using equiv_equiv_F by (simp add: equivp_symp) then have c'_l'_prec: "(C', L') \ (C, L)" using l'_sub_l unfolding Prec_FL_def by simp have "\_F_q q C = \_F_q q C'" if "q \ Q" for q using that equiv_F_grounding equiv_c_c' equiv_c'_c by (simp add: set_eq_subset) then have "\_F_L_q q (C, L) = \_F_L_q q (C', L')" if "q \ Q" for q using that by auto then have "(C, L) \ Red_F_\_q q N" if "q \ Q" for q unfolding Red_F_\_q_def using that c'_l'_in c'_l'_prec by blast then have ?thesis unfolding Red_F_def by blast } ultimately show ?thesis using c'_sub_c equiv_equiv_F equivp_symp by fastforce qed ultimately show ?thesis by blast qed end subsection \Given Clause Procedure\ locale given_clause = given_clause_basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q - Red_F_q \_F_q \_Inf_q Inf_FL Equiv_F Prec_F Prec_l active + Red_F_q \_F_q \_I_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_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 + \_I_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 (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.Inf_between (fst ` (active_subset N)) {C} \ no_labels.Red_I (fst ` (N \ {(C, active)} \ M)) \ N1 \GC N2" lemma one_step_equiv: "N1 \GC N2 \ N1 \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 (N \ M')" and active_empty: "active_subset M' = {}" have "N1 - N2 \ Red_F N2" using n1_is n2_is m_red by auto then show "N1 \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 N2" using red_labeled_clauses by blast moreover have "N1 - N2 = {} \ N1 - N2 = {(C, L)}" using n1_is n2_is by blast ultimately have "N1 - N2 \ Red_F N2" using std_Red_F_eq by blast then show "N1 \RedL N2" unfolding derive.simps by blast qed (* lem:gc-derivations-are-red-derivations *) -lemma gc_to_red: "chain (\GC) D \ chain (\RedL) D" +lemma gc_to_red: "chain (\GC) Ns \ chain (\RedL) Ns" 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" + deriv: "chain (\GC) Ns" and + init_state: "active_subset (lhd Ns) = {}" and + final_state: "passive_subset (Liminf_llist Ns) = {}" + shows "fair Ns" unfolding fair_def proof fix \ - assume i_in: "\ \ Inf_from (Liminf_llist D)" + assume i_in: "\ \ Inf_from (Liminf_llist Ns)" note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]] have i_in_inf_fl: "\ \ Inf_FL" using i_in unfolding Inf_from_def by blast - have "Liminf_llist D = active_subset (Liminf_llist D)" + have "Liminf_llist Ns = active_subset (Liminf_llist Ns)" using final_state unfolding passive_subset_def active_subset_def by blast - then have i_in2: "\ \ Inf_from (active_subset (Liminf_llist D))" using i_in by simp + then have i_in2: "\ \ Inf_from (active_subset (Liminf_llist Ns))" using i_in by simp define m where "m = length (prems_of \)" then have m_def_F: "m = length (prems_of (to_F \))" unfolding to_F_def by simp have i_in_F: "to_F \ \ Inf_F" using i_in Inf_FL_to_Inf_F unfolding Inf_from_def to_F_def by blast then have m_pos: "m > 0" using m_def_F using inf_have_prems by blast - have exist_nj: "\j \ {0..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)))" + have exist_nj: "\j \ {0..nj. enat (Suc nj) < llength Ns \ + prems_of \ ! j \ active_subset (lnth Ns nj) \ + (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (lnth Ns k)))" proof clarify fix j assume j_in: "j \ {0.. ! 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" + then have "(C, active) \ Liminf_llist Ns" using j_in i_in unfolding m_def Inf_from_def by force - then obtain nj where nj_is: "enat nj < llength D" and - c_in2: "(C, active) \ \ (lnth D ` {k. nj \ k \ enat k < llength D})" + then obtain nj where nj_is: "enat nj < llength Ns" and + c_in2: "(C, active) \ \ (lnth Ns ` {k. nj \ k \ enat k < llength Ns})" unfolding Liminf_llist_def using init_state by blast - then have c_in3: "\k. k \ nj \ enat k < llength D \ (C, active) \ lnth D k" by blast + then have c_in3: "\k. k \ nj \ enat k < llength Ns \ (C, active) \ lnth Ns k" by blast have nj_pos: "nj > 0" using init_state c_in2 nj_is unfolding active_subset_def lhd_is by force - obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength 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)" + obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength Ns \ + (C, active) \ \ (lnth Ns ` {k. nj \ k \ enat k < llength Ns}))" by blast + then have in_allk: "\k. k \ nj_min \ enat k < llength Ns \ (C, active) \ (lnth Ns k)" using c_in3 nj_is c_in2 by (metis (mono_tags, lifting) INT_E LeastI_ex mem_Collect_eq) - have njm_smaller_D: "enat nj_min < llength D" + have njm_smaller_D: "enat nj_min < llength Ns" 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\) + by (smt LeastI_ex \\thesis. (\nj. \enat nj < llength Ns; + (C, active) \ \ (lnth Ns ` {k. nj \ k \ enat k < llength Ns})\ \ thesis) \ thesis\) have "nj_min > 0" using nj_is c_in2 nj_pos nj_min_is lhd_is - by (metis (mono_tags, lifting) Collect_empty_eq \(C, active) \ Liminf_llist 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 + by (metis (mono_tags, lifting) Collect_empty_eq \(C, active) \ Liminf_llist Ns\ + \Liminf_llist Ns = active_subset (Liminf_llist Ns)\ + \\k\nj_min. enat k < llength Ns \ (C, active) \ lnth Ns k\ active_subset_def init_state linorder_not_less mem_Collect_eq zero_enat_def chain_length_pos[OF deriv]) then obtain njm_prec where nj_prec_is: "Suc njm_prec = nj_min" using gr0_conv_Suc by auto then have njm_prec_njm: "njm_prec < nj_min" by blast then have njm_prec_njm_enat: "enat njm_prec < enat nj_min" by simp - have njm_prec_smaller_d: "njm_prec < llength D" + have njm_prec_smaller_d: "njm_prec < llength Ns" 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" + have njm_prec_all_suc: "\k>njm_prec. enat k < llength Ns \ (C, active) \ lnth Ns k" using nj_prec_is in_allk by simp - have notin_njm_prec: "(C, active) \ lnth D njm_prec" + have notin_njm_prec: "(C, active) \ lnth Ns 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\ + assume "\ (C, active) \ lnth Ns njm_prec" + then have absurd_hyp: "(C, active) \ lnth Ns njm_prec" by simp + have prec_smaller: "enat njm_prec < llength Ns" using nj_min_is nj_prec_is + by (smt LeastI_ex Suc_leD \\thesis. (\nj. \enat nj < llength Ns; + (C, active) \ \ (lnth Ns ` {k. nj \ k \ enat k < llength Ns})\ \ thesis) \ thesis\ enat_ord_simps(1) le_eq_less_or_eq le_less_trans) - have "(C, active) \ \ (lnth D ` {k. njm_prec \ k \ enat k < llength D})" + have "(C, active) \ \ (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns})" proof - { fix k - assume k_in: "njm_prec \ k \ enat k < llength 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" + assume k_in: "njm_prec \ k \ enat k < llength Ns" + have "k = njm_prec \ (C, active) \ lnth Ns k" using absurd_hyp by simp + moreover have "njm_prec < k \ (C, active) \ lnth Ns k" using nj_prec_is in_allk k_in by simp - ultimately have "(C, active) \ lnth D k" using k_in by fastforce + ultimately have "(C, active) \ lnth Ns k" using k_in by fastforce } - then show "(C, active) \ \ (lnth D ` {k. njm_prec \ k \ enat k < llength D})" by blast + then show "(C, active) \ \ (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns})" by blast qed - then have "enat njm_prec < llength D \ - (C, active) \ \ (lnth D ` {k. njm_prec \ k \ enat k < llength D})" + then have "enat njm_prec < llength Ns \ + (C, active) \ \ (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns})" using prec_smaller by blast then show False using nj_min_is nj_prec_is Orderings.wellorder_class.not_less_Least njm_prec_njm by blast qed - then have notin_active_subs_njm_prec: "(C, active) \ active_subset (lnth D njm_prec)" + then have notin_active_subs_njm_prec: "(C, active) \ active_subset (lnth Ns njm_prec)" unfolding active_subset_def by blast - then show "\nj. enat (Suc nj) < llength D \ prems_of \ ! j \ active_subset (lnth D nj) \ - (\k. k > nj \ enat k < llength D \ prems_of \ ! j \ active_subset (lnth D k))" + then show "\nj. enat (Suc nj) < llength Ns \ prems_of \ ! j \ active_subset (lnth Ns nj) \ + (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (lnth Ns k))" using c_is njm_prec_all_suc njm_prec_smaller_d by (metis (mono_tags, lifting) active_subset_def mem_Collect_eq nj_prec_is njm_smaller_D snd_conv) qed - define nj_set where "nj_set = {nj. (\j\{0.. - prems_of \ ! j \ active_subset (lnth D nj) \ - (\k. k > nj \ enat k < llength D \ prems_of \ ! j \ active_subset (lnth D k)))}" + define nj_set where "nj_set = {nj. (\j\{0.. + prems_of \ ! j \ active_subset (lnth Ns nj) \ + (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (lnth Ns k)))}" then have nj_not_empty: "nj_set \ {}" proof - have zero_in: "0 \ {0.. ! 0 \ active_subset (lnth D n0)" and - "\k>n0. enat k < llength D \ prems_of \ ! 0 \ active_subset (lnth D k)" + then obtain n0 where "enat (Suc n0) < llength Ns" and + "prems_of \ ! 0 \ active_subset (lnth Ns n0)" and + "\k>n0. enat k < llength Ns \ prems_of \ ! 0 \ active_subset (lnth Ns k)" using exist_nj by fast then have "n0 \ nj_set" unfolding nj_set_def using zero_in by blast then show "nj_set \ {}" by auto qed have nj_finite: "finite nj_set" using all_ex_finite_set[OF exist_nj] by (metis (no_types, lifting) Suc_ile_eq dual_order.strict_implies_order linorder_neqE_nat nj_set_def) (* 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))" + then obtain j0 where j0_in: "j0 \ {0.. ! j0 \ active_subset (lnth Ns n)" and + j0_allin: "(\k. k > n \ enat k < llength Ns \ prems_of \ ! j0 \ active_subset (lnth Ns k))" unfolding nj_set_def by blast obtain C0 where C0_is: "prems_of \ ! j0 = (C0, active)" using j0_in using i_in2 unfolding m_def Inf_from_def active_subset_def by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv) then have C0_prems_i: "(C0, active) \ set (prems_of \)" using in_set_conv_nth j0_in m_def by force - have C0_in: "(C0, active) \ (lnth D (Suc n))" + have C0_in: "(C0, active) \ (lnth Ns (Suc n))" using C0_is j0_allin suc_n_length by (simp add: active_subset_def) - have C0_notin: "(C0, active) \ (lnth D n)" using C0_is j0_notin unfolding active_subset_def by simp - have step_n: "lnth D n \GC lnth D (Suc n)" + have C0_notin: "(C0, active) \ (lnth Ns n)" using C0_is j0_notin unfolding active_subset_def by simp + have step_n: "lnth Ns n \GC lnth Ns (Suc n)" using deriv chain_lnth_rel n_in unfolding nj_set_def by blast - have "\N C L M. (lnth 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} + have "\N C L M. (lnth Ns n = N \ {(C, L)} \ + lnth Ns (Suc n) = N \ {(C, active)} \ M \ L \ active \ active_subset M = {} \ + no_labels.Inf_between (fst ` (active_subset N)) {C} \ no_labels.Red_I (fst ` (N \ {(C, active)} \ M)))" proof - - have proc_or_infer: "(\N1 N M N2 M'. lnth D n = N1 \ lnth D (Suc n) = N2 \ N1 = N \ M \ + have proc_or_infer: "(\N1 N M N2 M'. lnth Ns n = N1 \ lnth Ns (Suc n) = N2 \ N1 = N \ M \ N2 = N \ M' \ M \ Red_F (N \ M') \ active_subset M' = {}) \ - (\N1 N C L N2 M. lnth D n = N1 \ lnth D (Suc n) = N2 \ N1 = N \ {(C, L)} \ + (\N1 N C L N2 M. lnth Ns n = N1 \ lnth Ns (Suc n) = N2 \ N1 = N \ {(C, L)} \ N2 = N \ {(C, active)} \ M \ L \ active \ active_subset M = {} \ - no_labels.Inf_from2 (fst ` (active_subset N)) {C} \ + no_labels.Inf_between (fst ` (active_subset N)) {C} \ no_labels.Red_I (fst ` (N \ {(C, active)} \ M)))" - using step.simps[of "lnth D n" "lnth D (Suc n)"] step_n by blast + using step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n by blast show ?thesis using C0_in C0_notin proc_or_infer j0_in C0_is by (smt Un_iff active_subset_def mem_Collect_eq snd_conv sup_bot.right_neutral) qed then obtain N M L where inf_from_subs: - "no_labels.Inf_from2 (fst ` (active_subset N)) {C0} + "no_labels.Inf_between (fst ` (active_subset N)) {C0} \ 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 + nth_d_is: "lnth Ns n = N \ {(C0, L)}" and + suc_nth_d_is: "lnth Ns (Suc n) = N \ {(C0, active)} \ M" and l_not_active: "L \ active" using C0_in C0_notin j0_in C0_is using active_subset_def by fastforce have "j \ {0.. 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))" + obtain nj where nj_len: "enat (Suc nj) < llength Ns" and + nj_prems: "prems_of \ ! j \ active_subset (lnth Ns nj)" and + nj_greater: "(\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (lnth Ns k))" using exist_nj j_in by blast then have "nj \ nj_set" unfolding nj_set_def using j_in by blast moreover have "nj \ n" proof (rule ccontr) assume "\ nj \ n" then have "prems_of \ ! j = (C0, active)" - using C0_in C0_notin step.simps[of "lnth D n" "lnth D (Suc n)"] step_n + using C0_in C0_notin step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n by (smt Un_iff nth_d_is suc_nth_d_is l_not_active active_subset_def insertCI insertE lessI mem_Collect_eq nj_greater nj_prems snd_conv suc_n_length) then show False using j_not_j0 C0_is by simp qed ultimately have "nj < n" using n_bigger by force - then have "prems_of \ ! j \ (active_subset (lnth D n))" + then have "prems_of \ ! j \ (active_subset (lnth Ns n))" using nj_greater n_in Suc_ile_eq dual_order.strict_implies_order unfolding nj_set_def by blast then show "prems_of \ ! j \ (active_subset N)" using nth_d_is l_not_active unfolding active_subset_def by force qed then have "set (prems_of \) \ active_subset N \ {(C0, active)}" using C0_prems_i C0_is m_def by (metis Un_iff atLeast0LessThan in_set_conv_nth insertCI lessThan_iff subrelI) moreover have "\ (set (prems_of \) \ active_subset N - {(C0, active)})" using C0_prems_i by blast - ultimately have "\ \ Inf_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 + ultimately have "\ \ Inf_between (active_subset N) {(C0, active)}" + using i_in_inf_fl unfolding Inf_between_def Inf_from_def by blast + then have "to_F \ \ no_labels.Inf_between (fst ` (active_subset N)) {C0}" + unfolding to_F_def Inf_between_def Inf_from_def + no_labels.Inf_between_def no_labels.Inf_from_def using Inf_FL_to_Inf_F by force - then have "to_F \ \ no_labels.Red_I (fst ` (lnth D (Suc n)))" + then have "to_F \ \ no_labels.Red_I (fst ` (lnth Ns (Suc n)))" using suc_nth_d_is inf_from_subs by fastforce - then have "\q \ Q. (\_Inf_q q (to_F \) \ None \ - 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))))" + then have "\q \ Q. (\_I_q q (to_F \) \ None \ + the (\_I_q q (to_F \)) \ Red_I_q q (\ (\_F_q q ` fst ` lnth Ns (Suc n)))) + \ (\_I_q q (to_F \) = None \ + \_F_q q (concl_of (to_F \)) \ \ (\_F_q q ` fst ` lnth Ns (Suc n)) \ + Red_F_q q (\ (\_F_q q ` fst ` lnth Ns (Suc n))))" unfolding to_F_def no_labels.Red_I_def no_labels.Red_I_\_q_def by blast - then have "\ \ Red_I_\ (lnth D (Suc n))" + then have "\ \ Red_I_\ (lnth Ns (Suc n))" using i_in_inf_fl unfolding Red_I_\_def Red_I_\_q_def by (simp add: to_F_def) - then show "\ \ Sup_llist (lmap Red_I_\ D)" + then show "\ \ Sup_llist (lmap Red_I_\ Ns)" unfolding Sup_llist_def using suc_n_length by auto qed theorem gc_complete_Liminf: assumes - deriv: "chain (\GC) D" and - init_state: "active_subset (lhd D) = {}" and - final_state: "passive_subset (Liminf_llist D) = {}" and + deriv: "chain (\GC) Ns" and + init_state: "active_subset (lhd Ns) = {}" and + final_state: "passive_subset (Liminf_llist Ns) = {}" and b_in: "B \ Bot_F" and - bot_entailed: "no_labels.entails_\ (fst ` lhd D) {B}" - shows "\BL \ Bot_FL. BL \ Liminf_llist D" + bot_entailed: "no_labels.entails_\ (fst ` lhd Ns) {B}" + shows "\BL \ Bot_FL. BL \ Liminf_llist Ns" proof - note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]] have labeled_b_in: "(B, active) \ Bot_FL" using b_in by simp - have labeled_bot_entailed: "entails_\_L (lhd D) {(B, active)}" + have labeled_bot_entailed: "entails_\_L (lhd Ns) {(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] . + have fair: "fair Ns" using gc_fair[OF deriv init_state final_state] . then show ?thesis using dynamically_complete_Liminf[OF labeled_b_in gc_to_red[OF deriv] fair labeled_bot_entailed] by blast qed (* 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 + deriv: "chain (\GC) Ns" and + init_state: "active_subset (lhd Ns) = {}" and + final_state: "passive_subset (Liminf_llist Ns) = {}" and b_in: "B \ Bot_F" and - bot_entailed: "no_labels.entails_\ (fst ` lhd D) {B}" - shows "\i. enat i < llength D \ (\BL \ Bot_FL. BL \ lnth D i)" + bot_entailed: "no_labels.entails_\ (fst ` lhd Ns) {B}" + shows "\i. enat i < llength Ns \ (\BL \ Bot_FL. BL \ lnth Ns i)" proof - note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]] - have "\BL\Bot_FL. BL \ Liminf_llist D" + have "\BL\Bot_FL. BL \ Liminf_llist Ns" using assms by (rule gc_complete_Liminf) then show ?thesis unfolding Liminf_llist_def by auto qed end subsection \Lazy Given Clause Procedure\ locale lazy_given_clause = given_clause_basis Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q - Red_F_q \_F_q \_Inf_q Inf_FL Equiv_F Prec_F Prec_l active + Red_F_q \_F_q \_I_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_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 + \_I_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 (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} \ + L \ active \ T' = no_labels.Inf_between (fst ` (active_subset N)) {C} \ (T1, N1) \LGC (T2, N2)" | compute_infer: "T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.Red_I (fst ` (N1 \ M)) \ (T1, N1) \LGC (T2, N2)" | delete_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 \ prems_of \ = [] \ \ \ no_labels.Inf_from N" unfolding no_labels.Inf_from_def by simp lemma one_step_equiv: "(T1, N1) \LGC (T2, N2) \ N1 \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 (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 N2" using red_labeled_clauses by blast then have "N1 - N2 \ Red_F N2" using std_Red_F_eq using n1_is n2_is by blast then show "N1 \RedL N2" unfolding derive.simps by blast next fix M assume n2_is: "N2 = N1 \ M" have "N1 - N2 \ Red_F N2" using n2_is by blast then show "N1 \RedL N2" unfolding derive.simps by blast next assume n2_is: "N2 = N1" have "N1 - N2 \ Red_F N2" using n2_is by blast then show "N1 \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)" +lemma lgc_to_red: "chain (\LGC) Ns \ chain (\RedL) (lmap snd Ns)" 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. prems_of \ = [] \ \ \ fst (lhd D)" and - final_schedule: "Liminf_llist (lmap fst D) = {}" - shows "fair (lmap snd D)" + deriv: "chain (\LGC) Ns" and + init_state: "active_subset (snd (lhd Ns)) = {}" and + final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and + no_prems_init_active: "\\ \ Inf_F. prems_of \ = [] \ \ \ fst (lhd Ns)" and + final_schedule: "Liminf_llist (lmap fst Ns) = {}" + shows "fair (lmap snd Ns)" unfolding fair_def proof fix \ - assume i_in: "\ \ Inf_from (Liminf_llist (lmap snd D))" + assume i_in: "\ \ Inf_from (Liminf_llist (lmap snd Ns))" note lhd_is = lhd_conv_lnth[OF chain_not_lnull[OF deriv]] have i_in_inf_fl: "\ \ Inf_FL" using i_in unfolding Inf_from_def by blast - have "Liminf_llist (lmap snd D) = active_subset (Liminf_llist (lmap snd D))" + have "Liminf_llist (lmap snd Ns) = active_subset (Liminf_llist (lmap snd Ns))" using final_state unfolding passive_subset_def active_subset_def by blast - then have i_in2: "\ \ Inf_from (active_subset (Liminf_llist (lmap snd D)))" + then have i_in2: "\ \ Inf_from (active_subset (Liminf_llist (lmap snd Ns)))" using i_in by simp define m where "m = length (prems_of \)" then have m_def_F: "m = length (prems_of (to_F \))" unfolding to_F_def by simp have i_in_F: "to_F \ \ Inf_F" using i_in Inf_FL_to_Inf_F unfolding Inf_from_def to_F_def by blast - have exist_nj: "\j \ {0..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))))" + have exist_nj: "\j \ {0..nj. enat (Suc nj) < llength Ns \ + prems_of \ ! j \ active_subset (snd (lnth Ns nj)) \ + (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns k))))" proof clarify fix j assume j_in: "j \ {0.. ! 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)" + then have "(C, active) \ Liminf_llist (lmap snd Ns)" using j_in i_in unfolding m_def Inf_from_def by force - then obtain nj where nj_is: "enat nj < llength D" and - c_in2: "(C, active) \ \ (snd ` (lnth D ` {k. nj \ k \ enat k < llength D}))" + then obtain nj where nj_is: "enat nj < llength Ns" and + c_in2: "(C, active) \ \ (snd ` (lnth Ns ` {k. nj \ k \ enat k < llength Ns}))" unfolding Liminf_llist_def using init_state by fastforce - then have c_in3: "\k. k \ nj \ enat k < llength D \ (C, active) \ snd (lnth D k)" by blast + then have c_in3: "\k. k \ nj \ enat k < llength Ns \ (C, active) \ snd (lnth Ns k)" by blast have nj_pos: "nj > 0" using init_state c_in2 nj_is unfolding active_subset_def lhd_is by fastforce - obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength 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)" + obtain nj_min where nj_min_is: "nj_min = (LEAST nj. enat nj < llength Ns \ + (C, active) \ \ (snd ` (lnth Ns ` {k. nj \ k \ enat k < llength Ns})))" by blast + then have in_allk: "\k. k \ nj_min \ enat k < llength Ns \ (C, active) \ snd (lnth Ns k)" using c_in3 nj_is c_in2 INT_E LeastI_ex by (smt INT_iff INT_simps(10) c_is image_eqI mem_Collect_eq) - have njm_smaller_D: "enat nj_min < llength D" + have njm_smaller_D: "enat nj_min < llength Ns" 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\) + by (smt LeastI_ex \\thesis. (\nj. \enat nj < llength Ns; + (C, active) \ \ (snd ` (lnth Ns ` {k. nj \ k \ enat k < llength Ns}))\ \ thesis) \ thesis\) have "nj_min > 0" using nj_is c_in2 nj_pos nj_min_is lhd_is by (metis (mono_tags, lifting) active_subset_def emptyE in_allk init_state mem_Collect_eq not_less snd_conv zero_enat_def chain_length_pos[OF deriv]) then obtain njm_prec where nj_prec_is: "Suc njm_prec = nj_min" using gr0_conv_Suc by auto then have njm_prec_njm: "njm_prec < nj_min" by blast then have njm_prec_njm_enat: "enat njm_prec < enat nj_min" by simp - have njm_prec_smaller_d: "njm_prec < llength 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)" + have njm_prec_smaller_d: "njm_prec < llength Ns" + using HOL.no_atp(15)[OF njm_smaller_D njm_prec_njm_enat] . + have njm_prec_all_suc: "\k>njm_prec. enat k < llength Ns \ (C, active) \ snd (lnth Ns k)" using nj_prec_is in_allk by simp - have notin_njm_prec: "(C, active) \ snd (lnth D njm_prec)" + have notin_njm_prec: "(C, active) \ snd (lnth Ns 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\ + assume "\ (C, active) \ snd (lnth Ns njm_prec)" + then have absurd_hyp: "(C, active) \ snd (lnth Ns njm_prec)" by simp + have prec_smaller: "enat njm_prec < llength Ns" using nj_min_is nj_prec_is + by (smt LeastI_ex Suc_leD \\thesis. (\nj. \enat nj < llength Ns; + (C, active) \ \ (snd ` (lnth Ns ` {k. nj \ k \ enat k < llength Ns}))\ \ thesis) \ thesis\ enat_ord_simps(1) le_eq_less_or_eq le_less_trans) - have "(C, active) \ \ (snd ` (lnth D ` {k. njm_prec \ k \ enat k < llength D}))" + have "(C, active) \ \ (snd ` (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns}))" proof - { fix k - assume k_in: "njm_prec \ k \ enat k < llength 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)" + assume k_in: "njm_prec \ k \ enat k < llength Ns" + have "k = njm_prec \ (C, active) \ snd (lnth Ns k)" using absurd_hyp by simp + moreover have "njm_prec < k \ (C, active) \ snd (lnth Ns k)" using nj_prec_is in_allk k_in by simp - ultimately have "(C, active) \ snd (lnth D k)" using k_in by fastforce + ultimately have "(C, active) \ snd (lnth Ns k)" using k_in by fastforce } - then show "(C, active) \ \ (snd ` (lnth D ` {k. njm_prec \ k \ enat k < llength D}))" + then show "(C, active) \ \ (snd ` (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns}))" by blast qed - then have "enat njm_prec < llength D \ - (C, active) \ \ (snd ` (lnth D ` {k. njm_prec \ k \ enat k < llength D}))" + then have "enat njm_prec < llength Ns \ + (C, active) \ \ (snd ` (lnth Ns ` {k. njm_prec \ k \ enat k < llength Ns}))" using prec_smaller by blast then show False using nj_min_is nj_prec_is Orderings.wellorder_class.not_less_Least njm_prec_njm by blast qed - then have notin_active_subs_njm_prec: "(C, active) \ active_subset (snd (lnth D njm_prec))" + then have notin_active_subs_njm_prec: "(C, active) \ active_subset (snd (lnth Ns njm_prec))" unfolding active_subset_def by blast - then show "\nj. enat (Suc nj) < llength 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)))" + then show "\nj. enat (Suc nj) < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns nj)) \ + (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns k)))" using c_is njm_prec_all_suc njm_prec_smaller_d by (metis (mono_tags, lifting) active_subset_def mem_Collect_eq nj_prec_is njm_smaller_D snd_conv) qed - define nj_set where "nj_set = {nj. (\j\{0.. - 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))))}" + define nj_set where "nj_set = {nj. (\j\{0.. + prems_of \ ! j \ active_subset (snd (lnth Ns nj)) \ + (\k. k > nj \ enat k < llength Ns \ prems_of \ ! j \ active_subset (snd (lnth Ns k))))}" { assume m_null: "m = 0" - then have "enat 0 < llength D \ to_F \ \ fst (lhd D)" + then have "enat 0 < llength Ns \ to_F \ \ fst (lhd Ns)" 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)" + then have "\n. enat n < llength Ns \ to_F \ \ fst (lnth Ns n)" unfolding lhd_is by blast } moreover { assume m_pos: "m > 0" have nj_not_empty: "nj_set \ {}" proof - have zero_in: "0 \ {0.. ! 0 \ active_subset (snd (lnth D n0))" and - "\k>n0. enat k < llength D \ prems_of \ ! 0 \ active_subset (snd (lnth D k))" + then obtain n0 where "enat (Suc n0) < llength Ns" and + "prems_of \ ! 0 \ active_subset (snd (lnth Ns n0))" and + "\k>n0. enat k < llength Ns \ prems_of \ ! 0 \ active_subset (snd (lnth Ns k))" using exist_nj by fast then have "n0 \ nj_set" unfolding nj_set_def using zero_in by blast then show "nj_set \ {}" by auto qed have nj_finite: "finite nj_set" using all_ex_finite_set[OF exist_nj] by (metis (no_types, lifting) Suc_ile_eq dual_order.strict_implies_order linorder_neqE_nat nj_set_def) have "\n \ nj_set. \nj \ nj_set. nj \ n" using nj_not_empty nj_finite using Max_ge Max_in by blast then obtain n where n_in: "n \ nj_set" and n_bigger: "\nj \ nj_set. nj \ n" by blast - then obtain j0 where j0_in: "j0 \ {0.. ! 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)))" + then obtain j0 where j0_in: "j0 \ {0.. ! j0 \ active_subset (snd (lnth Ns n))" and + j0_allin: "(\k. k > n \ enat k < llength Ns \ + prems_of \ ! j0 \ active_subset (snd (lnth Ns k)))" unfolding nj_set_def by blast obtain C0 where C0_is: "prems_of \ ! j0 = (C0, active)" using j0_in i_in2 unfolding m_def Inf_from_def active_subset_def by (smt Collect_mem_eq Collect_mono_iff atLeastLessThan_iff nth_mem old.prod.exhaust snd_conv) then have C0_prems_i: "(C0, active) \ set (prems_of \)" using in_set_conv_nth j0_in m_def by force - have C0_in: "(C0, active) \ (snd (lnth D (Suc n)))" + have C0_in: "(C0, active) \ (snd (lnth Ns (Suc n)))" using C0_is j0_allin suc_n_length by (simp add: active_subset_def) - have C0_notin: "(C0, active) \ (snd (lnth D n))" + have C0_notin: "(C0, active) \ (snd (lnth Ns n))" using C0_is j0_notin unfolding active_subset_def by simp - have step_n: "lnth D n \LGC lnth D (Suc n)" + have step_n: "lnth Ns n \LGC lnth Ns (Suc n)" using deriv chain_lnth_rel n_in unfolding nj_set_def by blast - have is_scheduled: "\T2 T1 T' N1 N C L N2. lnth D n = (T1, N1) \ lnth D (Suc n) = (T2, N2) \ + have is_scheduled: "\T2 T1 T' N1 N C L N2. lnth Ns n = (T1, N1) \ lnth Ns (Suc n) = (T2, N2) \ T2 = T1 \ T' \ N1 = N \ {(C, L)} \ N2 = N \ {(C, active)} \ L \ active \ - T' = no_labels.Inf_from2 (fst ` active_subset N) {C}" - using step.simps[of "lnth D n" "lnth D (Suc n)"] step_n C0_in C0_notin + T' = no_labels.Inf_between (fst ` active_subset N) {C}" + using step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n C0_in C0_notin unfolding active_subset_def by fastforce - then obtain T2 T1 T' N1 N L N2 where nth_d_is: "lnth D n = (T1, N1)" and - suc_nth_d_is: "lnth D (Suc n) = (T2, N2)" and t2_is: "T2 = T1 \ T'" and + then obtain T2 T1 T' N1 N L N2 where nth_d_is: "lnth Ns n = (T1, N1)" and + suc_nth_d_is: "lnth Ns (Suc n) = (T2, N2)" and t2_is: "T2 = T1 \ T'" and n1_is: "N1 = N \ {(C0, L)}" "N2 = N \ {(C0, active)}" and l_not_active: "L \ active" and - tp_is: "T' = no_labels.Inf_from2 (fst ` active_subset N) {C0}" + tp_is: "T' = no_labels.Inf_between (fst ` active_subset N) {C0}" using C0_in C0_notin j0_in C0_is using active_subset_def by fastforce have "j \ {0.. 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)))" + obtain nj where nj_len: "enat (Suc nj) < llength Ns" and + nj_prems: "prems_of \ ! j \ active_subset (snd (lnth Ns nj))" and + nj_greater: "(\k. k > nj \ enat k < llength Ns \ + prems_of \ ! j \ active_subset (snd (lnth Ns k)))" using exist_nj j_in by blast then have "nj \ nj_set" unfolding nj_set_def using j_in by blast moreover have "nj \ n" proof (rule ccontr) assume "\ nj \ n" then have "prems_of \ ! j = (C0, active)" - using C0_in C0_notin step.simps[of "lnth D n" "lnth D (Suc n)"] step_n + using C0_in C0_notin step.simps[of "lnth Ns n" "lnth Ns (Suc n)"] step_n active_subset_def is_scheduled nj_greater nj_prems suc_n_length by auto then show False using j_not_j0 C0_is by simp qed ultimately have "nj < n" using n_bigger by force - then have "prems_of \ ! j \ (active_subset (snd (lnth D n)))" + then have "prems_of \ ! j \ (active_subset (snd (lnth Ns n)))" using nj_greater n_in Suc_ile_eq dual_order.strict_implies_order unfolding nj_set_def by blast then show "prems_of \ ! j \ (active_subset N)" using nth_d_is l_not_active n1_is unfolding active_subset_def by force qed then have prems_i_active: "set (prems_of \) \ active_subset N \ {(C0, active)}" using C0_prems_i C0_is m_def by (metis Un_iff atLeast0LessThan in_set_conv_nth insertCI lessThan_iff subrelI) moreover have "\ (set (prems_of \) \ active_subset N - {(C0, active)})" using C0_prems_i by blast - ultimately have "\ \ Inf_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 + ultimately have "\ \ Inf_between (active_subset N) {(C0, active)}" + using i_in_inf_fl prems_i_active unfolding Inf_between_def Inf_from_def by blast + then have "to_F \ \ no_labels.Inf_between (fst ` (active_subset N)) {C0}" + unfolding to_F_def Inf_between_def Inf_from_def + no_labels.Inf_between_def no_labels.Inf_from_def using Inf_FL_to_Inf_F by force then have i_in_t2: "to_F \ \ T2" using tp_is t2_is by simp - have "j \ {0.. (\k. k > n \ enat k < llength D \ - prems_of \ ! j \ active_subset (snd (lnth D k)))" for j + have "j \ {0.. (\k. k > n \ enat k < llength Ns \ + prems_of \ ! j \ active_subset (snd (lnth Ns k)))" for j proof (cases "j = j0") case True assume "j = j0" - then show "(\k. k > n \ enat k < llength D \ - prems_of \ ! j \ active_subset (snd (lnth D k)))" using j0_allin by simp + then show "(\k. k > n \ enat k < llength Ns \ + prems_of \ ! j \ active_subset (snd (lnth Ns k)))" using j0_allin by simp next case False assume j_in: "j \ {0.. 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)))" + obtain nj where nj_len: "enat (Suc nj) < llength Ns" and + nj_prems: "prems_of \ ! j \ active_subset (snd (lnth Ns nj))" and + nj_greater: "(\k. k > nj \ enat k < llength Ns \ + prems_of \ ! j \ active_subset (snd (lnth Ns k)))" using exist_nj j_in by blast then have "nj \ nj_set" unfolding nj_set_def using j_in by blast - then show "(\k. k > n \ enat k < llength D \ - prems_of \ ! j \ active_subset (snd (lnth D k)))" + then show "(\k. k > n \ enat k < llength Ns \ + prems_of \ ! j \ active_subset (snd (lnth Ns k)))" using nj_greater n_bigger by auto qed - then have allj_allk: "(\c\ set (prems_of \). (\k. k > n \ enat k < llength D \ - c \ active_subset (snd (lnth D k))))" + then have allj_allk: "(\c\ set (prems_of \). (\k. k > n \ enat k < llength Ns \ + c \ active_subset (snd (lnth Ns k))))" using m_def by (metis atLeast0LessThan in_set_conv_nth lessThan_iff) have "\c\ set (prems_of \). snd c = active" using prems_i_active unfolding active_subset_def by auto - then have ex_n_i_in: "\n. enat (Suc n) < llength D \ to_F \ \ fst (lnth D (Suc n)) \ + then have ex_n_i_in: "\n. enat (Suc n) < llength Ns \ to_F \ \ fst (lnth Ns (Suc n)) \ (\c\ set (prems_of \). snd c = active) \ - (\c\ set (prems_of \). (\k. k > n \ enat k < llength D \ - c \ active_subset (snd (lnth D k))))" + (\c\ set (prems_of \). (\k. k > n \ enat k < llength Ns \ + c \ active_subset (snd (lnth Ns k))))" using allj_allk i_in_t2 suc_nth_d_is fstI n_in nj_set_def by auto - then have "\n. enat n < llength D \ to_F \ \ fst (lnth D n) \ + then have "\n. enat n < llength Ns \ to_F \ \ fst (lnth Ns n) \ (\c\ set (prems_of \). snd c = active) \ (\c\ set (prems_of \). (\k. k \ n \ - enat k < llength D \ c \ active_subset (snd (lnth D k))))" + enat k < llength Ns \ c \ active_subset (snd (lnth Ns k))))" by auto } - ultimately obtain n T2 N2 where i_in_suc_n: "to_F \ \ fst (lnth 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)" + ultimately obtain n T2 N2 where i_in_suc_n: "to_F \ \ fst (lnth Ns n)" and + all_prems_active_after: "m > 0 \ (\c\ set (prems_of \). (\k. k \ n \ enat k < llength Ns \ + c \ active_subset (snd (lnth Ns k))))" and + suc_n_length: "enat n < llength Ns" and suc_nth_d_is: "lnth Ns n = (T2, N2)" by (metis less_antisym old.prod.exhaust zero_less_Suc) then have i_in_t2: "to_F \ \ T2" by simp - have "\p\n. enat (Suc p) < llength D \ to_F \ \ (fst (lnth D p)) \ to_F \ \ (fst (lnth D (Suc p)))" + have "\p\n. enat (Suc p) < llength Ns \ to_F \ \ (fst (lnth Ns p)) \ to_F \ \ (fst (lnth Ns (Suc p)))" proof (rule ccontr) assume - contra: "\ (\p\n. enat (Suc p) < llength 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 + contra: "\ (\p\n. enat (Suc p) < llength Ns \ to_F \ \ (fst (lnth Ns p)) \ + to_F \ \ (fst (lnth Ns (Suc p))))" + then have i_in_suc: "p0 \ n \ enat (Suc p0) < llength Ns \ to_F \ \ (fst (lnth Ns p0)) \ + to_F \ \ (fst (lnth Ns (Suc p0)))" for p0 by blast - have "p0 \ n \ enat p0 < llength D \ to_F \ \ (fst (lnth D p0))" for p0 + have "p0 \ n \ enat p0 < llength Ns \ to_F \ \ (fst (lnth Ns p0))" for p0 proof (induction rule: nat_induct_at_least) case base then show ?case using i_in_t2 suc_nth_d_is by simp next case (Suc p0) assume p_bigger_n: "n \ p0" and - induct_hyp: "enat p0 < llength D \ to_F \ \ fst (lnth D p0)" and - sucsuc_smaller_d: "enat (Suc p0) < llength D" + induct_hyp: "enat p0 < llength Ns \ to_F \ \ fst (lnth Ns p0)" and + sucsuc_smaller_d: "enat (Suc p0) < llength Ns" have suc_p_bigger_n: "n \ p0" using p_bigger_n by simp - have suc_smaller_d: "enat p0 < llength D" + have suc_smaller_d: "enat p0 < llength Ns" using sucsuc_smaller_d Suc_ile_eq dual_order.strict_implies_order by blast - then have "to_F \ \ fst (lnth D p0)" using induct_hyp by blast + then have "to_F \ \ fst (lnth Ns p0)" using induct_hyp by blast then show ?case using i_in_suc[OF suc_p_bigger_n sucsuc_smaller_d] by blast qed - then have i_in_all_bigger_n: "\j. j \ n \ enat j < llength D \ to_F \ \ (fst (lnth D j))" + then have i_in_all_bigger_n: "\j. j \ n \ enat j < llength Ns \ to_F \ \ (fst (lnth Ns j))" by presburger - have "llength (lmap fst D) = llength D" by force - then have "to_F \ \ \ (lnth (lmap fst D) ` {j. n \ j \ enat j < llength (lmap fst D)})" + have "llength (lmap fst Ns) = llength Ns" by force + then have "to_F \ \ \ (lnth (lmap fst Ns) ` {j. n \ j \ enat j < llength (lmap fst Ns)})" using i_in_all_bigger_n using Suc_le_D by auto - then have "to_F \ \ Liminf_llist (lmap fst D)" + then have "to_F \ \ Liminf_llist (lmap fst Ns)" unfolding Liminf_llist_def using suc_n_length by auto then show False using final_schedule by fast qed - then obtain p where p_greater_n: "p \ n" and p_smaller_d: "enat (Suc p) < llength D" and - i_in_p: "to_F \ \ (fst (lnth D p))" and i_notin_suc_p: "to_F \ \ (fst (lnth D (Suc p)))" + then obtain p where p_greater_n: "p \ n" and p_smaller_d: "enat (Suc p) < llength Ns" and + i_in_p: "to_F \ \ (fst (lnth Ns p))" and i_notin_suc_p: "to_F \ \ (fst (lnth Ns (Suc p)))" by blast have p_neq_n: "Suc p \ n" using i_notin_suc_p i_in_suc_n by blast - have step_p: "lnth 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) \ + have step_p: "lnth Ns p \LGC lnth Ns (Suc p)" using deriv p_smaller_d chain_lnth_rel by blast + then have "\T1 T2 \ N2 N1 M. lnth Ns p = (T1, N1) \ lnth Ns (Suc p) = (T2, N2) \ T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.Red_I_\ (fst ` (N1 \ M))" proof - - have ci_or_do: "(\T1 T2 \ N2 N1 M. lnth D p = (T1, N1) \ lnth D (Suc p) = (T2, N2) \ + have ci_or_do: "(\T1 T2 \ N2 N1 M. lnth Ns p = (T1, N1) \ lnth Ns (Suc p) = (T2, N2) \ T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.Red_I_\ (fst ` (N1 \ M))) \ - (\T1 T2 T' N. lnth D p = (T1, N) \ lnth D (Suc p) = (T2, N) \ + (\T1 T2 T' N. lnth Ns p = (T1, N) \ lnth Ns (Suc p) = (T2, N) \ T1 = T2 \ T' \ T' \ no_labels.Inf_from (fst ` active_subset N) = {})" - using step.simps[of "lnth D p" "lnth D (Suc p)"] step_p i_in_p i_notin_suc_p by fastforce + using step.simps[of "lnth Ns p" "lnth Ns (Suc p)"] step_p i_in_p i_notin_suc_p by fastforce then have p_greater_n_strict: "n < Suc p" using suc_nth_d_is p_greater_n i_in_t2 i_notin_suc_p le_eq_less_or_eq by force - have "m > 0 \ j \ {0.. prems_of (to_F \) ! j \ fst ` active_subset (snd (lnth D p))" + have "m > 0 \ j \ {0.. prems_of (to_F \) ! j \ fst ` active_subset (snd (lnth Ns p))" for j proof - fix j assume m_pos: "m > 0" and j_in: "j \ {0.. ! j \ (active_subset (snd (lnth D p)))" + then have "prems_of \ ! j \ (active_subset (snd (lnth Ns p)))" using all_prems_active_after[OF m_pos] p_smaller_d m_def p_greater_n p_neq_n by (meson Suc_ile_eq atLeastLessThan_iff dual_order.strict_implies_order nth_mem p_greater_n_strict) - then have "fst (prems_of \ ! j) \ fst ` active_subset (snd (lnth D p))" + then have "fst (prems_of \ ! j) \ fst ` active_subset (snd (lnth Ns p))" by blast - then show "prems_of (to_F \) ! j \ fst ` active_subset (snd (lnth D p))" + then show "prems_of (to_F \) ! j \ fst ` active_subset (snd (lnth Ns p))" unfolding to_F_def using j_in m_def by simp qed then have prems_i_active_p: "m > 0 \ - to_F \ \ no_labels.Inf_from (fst ` active_subset (snd (lnth D p)))" + to_F \ \ no_labels.Inf_from (fst ` active_subset (snd (lnth Ns p)))" using i_in_F unfolding no_labels.Inf_from_def by (smt atLeast0LessThan in_set_conv_nth lessThan_iff m_def_F mem_Collect_eq subsetI) - have "m = 0 \ (\T1 T2 \ N2 N1 M. lnth D p = (T1, N1) \ lnth D (Suc p) = (T2, N2) \ + have "m = 0 \ (\T1 T2 \ N2 N1 M. lnth Ns p = (T1, N1) \ lnth Ns (Suc p) = (T2, N2) \ T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.Red_I_\ (fst ` (N1 \ M)))" using ci_or_do premise_free_inf_always_from[of "to_F \" "fst ` active_subset _", OF i_in_F] m_def i_in_p i_notin_suc_p m_def_F by auto - then show "(\T1 T2 \ N2 N1 M. lnth D p = (T1, N1) \ lnth D (Suc p) = (T2, N2) \ + then show "(\T1 T2 \ N2 N1 M. lnth Ns p = (T1, N1) \ lnth Ns (Suc p) = (T2, N2) \ T1 = T2 \ {\} \ N2 = N1 \ M \ active_subset M = {} \ \ \ no_labels.Red_I_\ (fst ` (N1 \ M)))" using ci_or_do i_in_p i_notin_suc_p prems_i_active_p unfolding active_subset_def by force qed - then obtain T1p T2p N1p N2p Mp where "lnth D p = (T1p, N1p)" and - suc_p_is: "lnth D (Suc p) = (T2p, N2p)" and "T1p = T2p \ {to_F \}" and "T2p \ {to_F \} = {}" and + then obtain T1p T2p N1p N2p Mp where "lnth Ns p = (T1p, N1p)" and + suc_p_is: "lnth Ns (Suc p) = (T2p, N2p)" and "T1p = T2p \ {to_F \}" and "T2p \ {to_F \} = {}" and n2p_is: "N2p = N1p \ Mp"and "active_subset Mp = {}" and i_in_red_inf: "to_F \ \ no_labels.Red_I_\ (fst ` (N1p \ Mp))" using i_in_p i_notin_suc_p by fastforce - have "to_F \ \ no_labels.Red_I (fst ` (snd (lnth D (Suc p))))" + have "to_F \ \ no_labels.Red_I (fst ` (snd (lnth Ns (Suc p))))" using i_in_red_inf suc_p_is n2p_is by fastforce - then have "\q \ Q. (\_Inf_q q (to_F \) \ None \ - 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)))))" + then have "\q \ Q. (\_I_q q (to_F \) \ None \ + the (\_I_q q (to_F \)) \ Red_I_q q (\ (\_F_q q ` fst ` snd (lnth Ns (Suc p))))) + \ (\_I_q q (to_F \) = None \ + \_F_q q (concl_of (to_F \)) \ \ (\_F_q q ` fst ` snd (lnth Ns (Suc p))) \ + Red_F_q q (\ (\_F_q q ` fst ` snd (lnth Ns (Suc p)))))" unfolding to_F_def no_labels.Red_I_def no_labels.Red_I_\_q_def by blast - then have "\ \ Red_I_\ (snd (lnth D (Suc p)))" + then have "\ \ Red_I_\ (snd (lnth Ns (Suc p)))" using i_in_inf_fl unfolding Red_I_\_def Red_I_\_q_def by (simp add: to_F_def) - then show "\ \ Sup_llist (lmap Red_I_\ (lmap snd D))" + then show "\ \ Sup_llist (lmap Red_I_\ (lmap snd Ns))" unfolding Sup_llist_def using suc_n_length p_smaller_d by auto qed theorem lgc_complete_Liminf: assumes - deriv: "chain (\LGC) 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. prems_of \ = [] \ \ \ fst (lhd D)" and - final_schedule: "Liminf_llist (lmap fst D) = {}" and + deriv: "chain (\LGC) Ns" and + init_state: "active_subset (snd (lhd Ns)) = {}" and + final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and + no_prems_init_active: "\\ \ Inf_F. prems_of \ = [] \ \ \ fst (lhd Ns)" and + final_schedule: "Liminf_llist (lmap fst Ns) = {}" and b_in: "B \ Bot_F" and - bot_entailed: "no_labels.entails_\ (fst ` snd (lhd D)) {B}" - shows "\BL \ Bot_FL. BL \ Liminf_llist (lmap snd D)" + bot_entailed: "no_labels.entails_\ (fst ` snd (lhd Ns)) {B}" + shows "\BL \ Bot_FL. BL \ Liminf_llist (lmap snd Ns)" proof - have labeled_b_in: "(B, active) \ Bot_FL" using b_in by simp - have simp_snd_lmap: "lhd (lmap snd D) = snd (lhd D)" + have simp_snd_lmap: "lhd (lmap snd Ns) = snd (lhd Ns)" by (rule llist.map_sel(1)[OF chain_not_lnull[OF deriv]]) - have labeled_bot_entailed: "entails_\_L (snd (lhd D)) {(B, active)}" + have labeled_bot_entailed: "entails_\_L (snd (lhd Ns)) {(B, active)}" using labeled_entailment_lifting bot_entailed by fastforce - have "fair (lmap snd D)" + have "fair (lmap snd Ns)" 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_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. prems_of \ = [] \ \ \ fst (lhd D)" and - final_schedule: "Liminf_llist (lmap fst D) = {}" and + deriv: "chain (\LGC) Ns" and + init_state: "active_subset (snd (lhd Ns)) = {}" and + final_state: "passive_subset (Liminf_llist (lmap snd Ns)) = {}" and + no_prems_init_active: "\\ \ Inf_F. prems_of \ = [] \ \ \ fst (lhd Ns)" and + final_schedule: "Liminf_llist (lmap fst Ns) = {}" and b_in: "B \ Bot_F" and - bot_entailed: "no_labels.entails_\ (fst ` snd (lhd D)) {B}" - shows "\i. enat i < llength D \ (\BL \ Bot_FL. BL \ snd (lnth D i))" + bot_entailed: "no_labels.entails_\ (fst ` snd (lhd Ns)) {B}" + shows "\i. enat i < llength Ns \ (\BL \ Bot_FL. BL \ snd (lnth Ns i))" proof - - have "\BL\Bot_FL. BL \ Liminf_llist (lmap snd D)" + have "\BL\Bot_FL. BL \ Liminf_llist (lmap snd Ns)" using assms by (rule lgc_complete_Liminf) then show ?thesis unfolding Liminf_llist_def by auto qed end end 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_I_G Red_F_G \_F \_Inf Prec_F + Bot_G entails_G Inf_G Red_I_G Red_F_G \_F \_I 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_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 + \_I :: "'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)\ +abbreviation \_I_L :: \('f \ 'l) inference \ 'g inference set option\ where + \\_I_L \\<^sub>F\<^sub>L \ \_I (to_F \\<^sub>F\<^sub>L)\ (* lem:labeled-grounding-function *) -sublocale standard_lifting Bot_FL Inf_FL Bot_G Inf_G "(\G)" Red_I_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 \_I_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_I_G (\_F_L (concl_of \))" + ground_not_none: \\_I_L \ \ None\ + then show "the (\_I_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_I_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 \_I_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_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_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_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_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_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_I_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 \_I_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_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" + \_I_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 \_I_L_q :: \'q \ ('f \ 'l) inference \ 'g inference set option\ where + \\_I_L_q q \\<^sub>F\<^sub>L \ \_I_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_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))}" + "Red_I_\_L_q q N = {\ \ Inf_FL. (\_I_L_q q \ \ None \ the (\_I_L_q q \) \ Red_I_q q (\_set_L_q q N)) + \ (\_I_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_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_I_q q) - (Red_F_q q) (\_F_q q) (\_Inf_q q) (\g Cl Cl'. False) Inf_FL" + (Red_F_q q) (\_F_q q) (\_I_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_I_q q) (Red_F_q q) - (\_F_L_q q) (\_Inf_L_q q)" + (\_F_L_q q) (\_I_L_q q)" proof - interpret q_lifting: 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 + "Red_I_q q" "Red_F_q q" "\_F_q q" "\_I_q q" "\g Cl Cl'. False" Inf_FL using lifting_q[OF q_in] . - have "\_Inf_L_q q = q_lifting.\_Inf_L" + have "\_I_L_q q = q_lifting.\_I_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_I_q q) - (Red_F_q q) (\_F_L_q q) (\_Inf_L_q q) (\g Cl Cl'. False)" + (Red_F_q q) (\_F_L_q q) (\_I_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_I_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" "\_I_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_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_I_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" "\_I_L_q q" "\g Cl Cl'. False" using ord_fam_lifted_q[OF q_in] . 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_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_\ (infix "\\\" 50) abbreviation entails_\_L :: "('f \ 'l) set \ ('f \ 'l) set \ bool" (infix "\\\L" 50) where "(\\\L) \ entails" 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_\_def entails_\_L_def by force 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_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_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))" + have subs_red: "(\_I_L_q q \ \ None \ the (\_I_L_q q \) \ Red_I_q q (\_set_L_q q NL)) + \ (\_I_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_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_I_q q (no_labels.\_set_q q (fst ` NL))) - \ (\_Inf_q q (to_F \) = None \ + then have to_F_subs_red: "(\_I_q q (to_F \) \ None \ + the (\_I_q q (to_F \)) \ Red_I_q q (no_labels.\_set_q q (fst ` NL))) + \ (\_I_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_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_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_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_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_I_\ no_labels.Red_F_\_empty" 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_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_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\ + \_I :: \'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_I_G (\_F (concl_of \))\ + inf_map: \\ \ Inf_F \ \_I \ \ None \ the (\_I \) \ 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_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_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\ + \_I :: \'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\ + strong_inf_map: \\ \ Inf_F \ \_I \ \ None \ concl_of ` (the (\_I \)) \ (\_F (concl_of \))\ and + inf_map_in_Inf: \\ \ Inf_F \ \_I \ \ None \ the (\_I \) \ Inf_G\ begin -sublocale standard_lifting Bot_F Inf_F Bot_G Inf_G "(\G)" Red_I_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 \_I 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_I_G (\_F (concl_of \))" + some_g: "\_I \ \ None" + show "the (\_I \) \ Red_I_G (\_F (concl_of \))" proof fix \G - assume ig_in1: "\G \ the (\_Inf \)" + assume ig_in1: "\G \ the (\_I \)" then have ig_in2: "\G \ Inf_G" using inf_map_in_Inf[OF i_in some_g] by blast 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_I_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 \_I 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_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" + \_I :: "'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_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))}\ + \Red_I_\ N = {\ \ Inf_F. (\_I \ \ None \ the (\_I \) \ Red_I_G (\_set N)) + \ (\_I \ = 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_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_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_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_I_G (\_set N)\ + assume not_none: "\_I \ \ None" + have \\\' \ the (\_I \). \' \ 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))\ + then have \\\' \ the (\_I \). \' \ 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))\ + then have ip_in_Red_I_G: \\\' \ the (\_I \). \' \ 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'))\ + then have not_none_in: \\\' \ the (\_I \). \' \ Red_I_G (\_set (N - N'))\ using not_none N'_in_Red_F_N 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 + then have "the (\_I \) \ Red_I_G (\_set (N - N'))" by blast } moreover { - assume none: "\_Inf \ = None" + assume none: "\_I \ = None" have ground_concl_subs: "\_F (concl_of \) \ (\_set N \ Red_F_G (\_set N))" 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_I_\ (N - N')\ using i_in unfolding Red_I_\_def by auto qed (* lem:concl-contained-implies-red-inf *) lemma Red_I_of_Inf_to_N_F: assumes i_in: \\ \ Inf_F\ and concl_i_in: \concl_of \ \ N\ shows \\ \ Red_I_\ N \ proof - - have \\ \ Inf_F \ \_Inf \ \ None \ the (\_Inf \) \ Red_I_G (\_F (concl_of \))\ using inf_map by simp + have \\ \ Inf_F \ \_I \ \ None \ the (\_I \) \ 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" + moreover have "\ \ Inf_F \ \_I \ = None \ concl_of \ \ N \ \_F (concl_of \) \ \_set N" by blast 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_I_\ Red_F_\ proof fix B N N' \ 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_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_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" +lemma grounded_inf_in_ground_inf: "\ \ Inf_F \ \_I \ \ None \ the (\_I \) \ Inf_G" 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_I_G (\_set N)" + \ {\. \\'\ Inf_from N. \_I \' \ None \ \ \ the (\_I \')} \ Red_I_G (\_set N)" lemma sat_inf_imp_ground_red: assumes "saturated N" and "\' \ Inf_from N" and - "\_Inf \' \ None \ \ \ the (\_Inf \')" + "\_I \' \ None \ \ \ the (\_I \')" 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_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_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_I_G (\_set N)" + {\. \\'\ Inf_from N. \_I \' \ None \ \ \ the (\_I \')} \ 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_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)" + \_I Prec_F_g \ tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G + Red_F_G \_F \_I (\g C C'. False)" proof - - fix Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G \_F \_Inf Prec_F_g + fix Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G \_F \_I 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" + Red_F_G \_F \_I Prec_F_g" then interpret lift_g: tiebreaker_lifting Bot_F Inf_F Bot_G entails_G Inf_G Red_I_G Red_F_G \_F - \_Inf Prec_F_g + \_I Prec_F_g by auto 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)" + \_F \_I (\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_I_G - Red_F_G \_F \_Inf Prec_F_g + + Red_F_G \_F \_I Prec_F_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" + Red_F_G \_F \_I "\g C C'. False" for \_F :: \'f \ 'g set\ and - \_Inf :: \'f inference \ 'g inference set option\ and + \_I :: \'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_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_I_\ empty_order_lifting.Red_F_\ = statically_complete_calculus Bot_F Inf_F any_order_lifting.entails_\ 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_I_\ empty_order_lifting.Red_F_\ = dynamically_complete_calculus Bot_F Inf_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_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 + \_I_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_I_q q) - (Red_F_q q) (\_F_q q) (\_Inf_q q) Prec_F_g" + (Red_F_q q) (\_F_q q) (\_I_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_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)))}" + "Red_I_\_q q N = {\ \ Inf_F. (\_I_q q \ \ None \ the (\_I_q q \) \ Red_I_q q (\_set_q q N)) + \ (\_I_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 :: "'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_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_I_q q" - "Red_F_q q" "\_F_q q" "\_Inf_q q" Prec_F_g + "Red_F_q q" "\_F_q q" "\_I_q q" Prec_F_g using standard_lifting_family q_in by metis 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_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_I_q q" - "Red_F_q q" "\_F_q q" "\_Inf_q q" Prec_F_g + "Red_F_q q" "\_F_q q" "\_I_q q" Prec_F_g using standard_lifting_family q_in by metis 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_I_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" "\_I_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_I_\_q Red_F_\_q by unfold_locales (auto simp: Q_nonempty red_crit_lifting_family) abbreviation entails_\ :: "'f set \ 'f set \ bool" (infix "\\\" 50) where "(\\\) \ entails" abbreviation Red_I_\ :: "'f set \ 'f inference set" where "Red_I_\ \ Red_I" abbreviation Red_F_\ :: "'f set \ 'f set" where "Red_F_\ \ Red_F" 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" 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 \')" + grounding: "\_I_q q \' \ None \ \ \ the (\_I_q q \')" shows "\ \ Red_I_q q (\_set_q q N)" proof - 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_I_q q (\_set_q q N)" + then have "the (\_I_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_I_q q (\_set_q q N)" + \ {\. \\'\ Inf_from N. \_I_q q \' \ None \ \ \ the (\_I_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_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_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_\ 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 \')} + {\. \\'\ Inf_from N. \_I_q q \' \ None \ \ \ the (\_I_q q \')} \ 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_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_I_q q" - "Red_F_q q" "\_F_q q" "\_Inf_q q" + "Red_F_q q" "\_F_q q" "\_I_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_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_\_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 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 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 diff --git a/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy b/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy --- a/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy +++ b/thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy @@ -1,1151 +1,1151 @@ (* Title: Application of the Saturation Framework to Bachmair and Ganzinger's RP Author: Sophie Tourret , 2018-2020 Author: Jasmin Blanchette , 2020 *) section \Application of the Saturation Framework to Bachmair and Ganzinger's \textsf{RP}\ theory FO_Ordered_Resolution_Prover_Revisited imports Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover Saturation_Framework.Given_Clause_Architectures Clausal_Calculus Soundness begin text \The main results about Bachmair and Ganzinger's \textsf{RP} prover, as established in Section 4.3 of their \emph{Handbook} chapter and formalized by Schlichtkrull et al., are re-proved here using the saturation framework of Waldmann et al.\ subsection \Setup\ no_notation true_lit (infix "\l" 50) no_notation true_cls (infix "\" 50) no_notation true_clss (infix "\s" 50) no_notation true_cls_mset (infix "\m" 50) hide_type (open) Inference_System.inference hide_const (open) Inference_System.Infer Inference_System.main_prem_of Inference_System.side_prems_of Inference_System.prems_of Inference_System.concl_of Inference_System.concls_of Inference_System.infer_from type_synonym 'a old_inference = "'a Inference_System.inference" abbreviation "old_Infer \ Inference_System.Infer" abbreviation "old_side_prems_of \ Inference_System.side_prems_of" abbreviation "old_main_prem_of \ Inference_System.main_prem_of" abbreviation "old_concl_of \ Inference_System.concl_of" abbreviation "old_prems_of \ Inference_System.prems_of" abbreviation "old_concls_of \ Inference_System.concls_of" abbreviation "old_infer_from \ Inference_System.infer_from" lemmas old_infer_from_def = Inference_System.infer_from_def subsection \Library\ lemma set_zip_replicate_right[simp]: "set (zip xs (replicate (length xs) y)) = (\x. (x, y)) ` set xs" by (induct xs) auto subsection \Ground Layer\ context FO_resolution_prover begin interpretation gr: ground_resolution_with_selection "S_M S M" using selection_axioms by unfold_locales (fact S_M_selects_subseteq S_M_selects_neg_lits)+ definition G_Inf :: "'a clause set \ 'a clause inference set" where "G_Inf M = {Infer (CAs @ [DA]) E |CAs DA AAs As E. gr.ord_resolve M CAs DA AAs As E}" lemma G_Inf_have_prems: "\ \ G_Inf M \ prems_of \ \ []" unfolding G_Inf_def by auto lemma G_Inf_reductive: "\ \ G_Inf M \ concl_of \ < main_prem_of \" unfolding G_Inf_def by (auto dest: gr.ord_resolve_reductive) interpretation G: sound_inference_system "G_Inf M" "{{#}}" "(\e)" proof fix \ assume i_in: "\ \ G_Inf M" moreover { fix I assume I_ent_prems: "I \s set (prems_of \)" obtain CAs AAs As where the_inf: "gr.ord_resolve M CAs (main_prem_of \) AAs As (concl_of \)" and CAs: "CAs = side_prems_of \" using i_in unfolding G_Inf_def by auto then have "I \ concl_of \" using gr.ord_resolve_sound[of M CAs "main_prem_of \" AAs As "concl_of \" I] by (metis I_ent_prems G_Inf_have_prems i_in insert_is_Un set_mset_mset set_prems_of true_clss_insert true_clss_set_mset) } ultimately show "set (inference.prems_of \) \e {concl_of \}" by simp qed interpretation G: clausal_counterex_reducing_inference_system "G_Inf M" "gr.INTERP M" proof fix N D assume "{#} \ N" and "D \ N" and "\ gr.INTERP M N \ D" and "\C. C \ N \ \ gr.INTERP M N \ C \ D \ C" then obtain CAs AAs As E where cas_in: "set CAs \ N" and n_mod_cas: "gr.INTERP M N \m mset CAs" and ca_prod: "\CA. CA \ set CAs \ gr.production M N CA \ {}" and e_res: "gr.ord_resolve M CAs D AAs As E" and n_nmod_e: "\ gr.INTERP M N \ E" and e_lt_d: "E < D" using gr.ord_resolve_counterex_reducing by blast define \ where "\ = Infer (CAs @ [D]) E" have "\ \ G_Inf M" unfolding \_def G_Inf_def using e_res by auto moreover have "prems_of \ \ []" unfolding \_def by simp moreover have "main_prem_of \ = D" unfolding \_def by simp moreover have "set (side_prems_of \) \ N" unfolding \_def using cas_in by simp moreover have "gr.INTERP M N \s set (side_prems_of \)" unfolding \_def using n_mod_cas ca_prod by (simp add: gr.productive_imp_INTERP true_clss_def) moreover have "\ gr.INTERP M N \ concl_of \" unfolding \_def using n_nmod_e by simp moreover have "concl_of \ < D" unfolding \_def using e_lt_d by simp ultimately show "\\ \ G_Inf M. prems_of \ \ [] \ main_prem_of \ = D \ set (side_prems_of \) \ N \ gr.INTERP M N \s set (side_prems_of \) \ \ gr.INTERP M N \ concl_of \ \ concl_of \ < D" by blast qed interpretation G: clausal_counterex_reducing_calculus_with_standard_redundancy "G_Inf M" "gr.INTERP M" by (unfold_locales, fact G_Inf_have_prems, fact G_Inf_reductive) interpretation G: statically_complete_calculus "{{#}}" "G_Inf M" "(\e)" "G.Red_I M" G.Red_F by unfold_locales (use G.clausal_saturated_complete in blast) subsection \First-Order Layer\ abbreviation \_F :: \'a clause \ 'a clause set\ where \\_F \ grounding_of_cls\ abbreviation \_Fs :: \'a clause set \ 'a clause set\ where \\_Fs \ grounding_of_clss\ lemmas \_F_def = grounding_of_cls_def lemmas \_Fs_def = grounding_of_clss_def -definition \_Inf :: \'a clause set \ 'a clause inference \ 'a clause inference set\ where - \\_Inf M \ = {Infer (prems_of \ \\cl \s) (concl_of \ \ \) |\ \s. +definition \_I :: \'a clause set \ 'a clause inference \ 'a clause inference set\ where + \\_I M \ = {Infer (prems_of \ \\cl \s) (concl_of \ \ \) |\ \s. is_ground_subst_list \s \ is_ground_subst \ \ Infer (prems_of \ \\cl \s) (concl_of \ \ \) \ G_Inf M}\ abbreviation - \_Inf_opt :: \'a clause set \ 'a clause inference \ 'a clause inference set option\ + \_I_opt :: \'a clause set \ 'a clause inference \ 'a clause inference set option\ where - \\_Inf_opt M \ \ Some (\_Inf M \)\ + \\_I_opt M \ \ Some (\_I M \)\ definition F_Inf :: "'a clause inference set" where "F_Inf = {Infer (CAs @ [DA]) E | CAs DA AAs As \ E. ord_resolve_rename S CAs DA AAs As \ E}" lemma F_Inf_have_prems: "\ \ F_Inf \ prems_of \ \ []" unfolding F_Inf_def by force interpretation F: lifting_intersection F_Inf "{{#}}" UNIV G_Inf "\N. (\e)" G.Red_I "\N. G.Red_F" - "{{#}}" "\N. \_F" \_Inf_opt "\D C C'. False" + "{{#}}" "\N. \_F" \_I_opt "\D C C'. False" proof (unfold_locales; (intro ballI)?) show "UNIV \ {}" by (rule UNIV_not_empty) next show "consequence_relation {{#}} (\e)" by (fact consequence_relation_axioms) next show "\M. tiebreaker_lifting {{#}} F_Inf {{#}} (\e) (G_Inf M) (G.Red_I M) - G.Red_F \_F (\_Inf_opt M) (\D C C'. False)" + G.Red_F \_F (\_I_opt M) (\D C C'. False)" proof fix M \ assume \_in: "\ \ F_Inf" - show "the (\_Inf_opt M \) \ G.Red_I M (\_F (concl_of \))" + show "the (\_I_opt M \) \ G.Red_I M (\_F (concl_of \))" unfolding option.sel proof fix \' - assume \'_in: "\' \ \_Inf M \" + assume \'_in: "\' \ \_I M \" then obtain \ \s where \': "\' = Infer (prems_of \ \\cl \s) (concl_of \ \ \)" and \s_gr: "is_ground_subst_list \s" and \_gr: "is_ground_subst \" and \_infer: "Infer (prems_of \ \\cl \s) (concl_of \ \ \) \ G_Inf M" - unfolding \_Inf_def by blast + unfolding \_I_def by blast let ?DD1 = "{concl_of \ \ \}" show "\' \ G.Red_I M (\_F (concl_of \))" unfolding G.Red_I_def G.redundant_infer_def mem_Collect_eq using \' \_gr \_infer by (metis inference.sel(2) G_Inf_reductive empty_iff ground_subst_ground_cls grounding_of_cls_ground insert_iff subst_cls_eq_grounding_of_cls_subset_eq true_clss_union) qed qed (auto simp: \_F_def ex_ground_subst) qed notation F.entails_\ (infix "\\e" 50) lemma F_entails_\_iff: "N1 \\e N2 \ \ (\_F ` N1) \e \ (\_F ` N2)" unfolding F.entails_\_def by simp lemma true_Union_grounding_of_cls_iff_true_all_interps_ground_substs: "I \s (\C \ N. {C \ \ |\. is_ground_subst \}) \ (\\. is_ground_subst \ \ I \s N \cs \)" unfolding true_clss_def subst_clss_def by blast interpretation F: sound_inference_system F_Inf "{{#}}" "(\\e)" proof fix \ assume i_in: "\ \ F_Inf" moreover { fix I \ assume I_entails_prems: "\\. is_ground_subst \ \ I \s set (prems_of \) \cs \" and \_gr: "is_ground_subst \" obtain CAs AAs As \ where the_inf: "ord_resolve_rename S CAs (main_prem_of \) AAs As \ (concl_of \)" and CAs: "CAs = side_prems_of \" using i_in unfolding F_Inf_def by auto have prems: "mset (prems_of \) = mset (side_prems_of \) + {#main_prem_of \#}" by (metis (no_types) F_Inf_have_prems[OF i_in] add.right_neutral append_Cons append_Nil2 append_butlast_last_id mset.simps(2) mset_rev mset_single_iff_right rev_append rev_is_Nil_conv union_mset_add_mset_right) have "I \ concl_of \ \ \" using ord_resolve_rename_sound[OF the_inf, of I \, OF _ \_gr] unfolding CAs prems[symmetric] using I_entails_prems by (metis set_mset_mset set_mset_subst_cls_mset_subst_clss true_clss_set_mset) } ultimately show "set (inference.prems_of \) \\e {concl_of \}" unfolding F.entails_\_def \_F_def true_Union_grounding_of_cls_iff_true_all_interps_ground_substs by auto qed lemma G_Inf_overapproximates_F_Inf: - "\\<^sub>0 \ G.Inf_from M (\ (\_F ` M)) \ \\. \ \ F.Inf_from M \ \\<^sub>0 \ \_Inf M \" + "\\<^sub>0 \ G.Inf_from M (\ (\_F ` M)) \ \\. \ \ F.Inf_from M \ \\<^sub>0 \ \_I M \" proof - assume \\<^sub>0_in: "\\<^sub>0 \ G.Inf_from M (\ (\_F ` M))" have prems_\\<^sub>0_in: "set (prems_of \\<^sub>0) \ \ (\_F ` M)" using \\<^sub>0_in unfolding G.Inf_from_def by simp note \\<^sub>0_G_Inf = G.Inf_if_Inf_from[OF \\<^sub>0_in] then obtain CAs DA AAs As E where gr_res: \gr.ord_resolve M CAs DA AAs As E\ and \\<^sub>0_is: \\\<^sub>0 = Infer (CAs @ [DA]) E\ unfolding G_Inf_def by auto have CAs_in: \set CAs \ set (prems_of \\<^sub>0)\ by (simp add: \\<^sub>0_is subsetI) then have ground_CAs: \is_ground_cls_list CAs\ using prems_\\<^sub>0_in union_grounding_of_cls_ground is_ground_cls_list_def is_ground_clss_def by auto have DA_in: \DA \ set (prems_of \\<^sub>0)\ using \\<^sub>0_is by simp then have ground_DA: \is_ground_cls DA\ using prems_\\<^sub>0_in union_grounding_of_cls_ground is_ground_clss_def by auto obtain \ where grounded_res: \ord_resolve (S_M S M) CAs DA AAs As \ E\ using ground_ord_resolve_imp_ord_resolve[OF ground_DA ground_CAs gr.ground_resolution_with_selection_axioms gr_res] by auto have prems_ground: \{DA} \ set CAs \ \_Fs M\ using prems_\\<^sub>0_in CAs_in DA_in unfolding \_Fs_def by fast obtain \s \ \2 CAs0 DA0 AAs0 As0 E0 \ where ground_n: "is_ground_subst \" and ground_ns: "is_ground_subst_list \s" and ground_n2: "is_ground_subst \2" and ngr_res: "ord_resolve_rename S CAs0 DA0 AAs0 As0 \ E0" and CAs0_is: "CAs0 \\cl \s = CAs" and DA0_is: "DA0 \ \ = DA" and E0_is: "E0 \ \2 = E" and prems_in: "{DA0} \ set CAs0 \ M" and len_CAs0: "length CAs0 = length CAs" and len_ns: "length \s = length CAs" using ord_resolve_rename_lifting[OF _ grounded_res selection_axioms prems_ground] sel_stable by smt have "length CAs0 = length \s" using len_CAs0 len_ns by simp then have \\<^sub>0_is': "\\<^sub>0 = Infer ((CAs0 @ [DA0]) \\cl (\s @ [\])) (E0 \ \2)" unfolding \\<^sub>0_is by (auto simp: CAs0_is[symmetric] DA0_is[symmetric] E0_is[symmetric]) define \ :: "'a clause inference" where "\ = Infer (CAs0 @ [DA0]) E0" have i_F_Inf: \\ \ F_Inf\ unfolding \_def F_Inf_def using ngr_res by auto have "\\ \s. \\<^sub>0 = Infer ((CAs0 @ [DA0]) \\cl \s) (E0 \ \) \ is_ground_subst_list \s \ is_ground_subst \ \ Infer ((CAs0 @ [DA0]) \\cl \s) (E0 \ \) \ G_Inf M" by (rule exI[of _ \2], rule exI[of _ "\s @ [\]"], use ground_ns in \auto intro: ground_n ground_n2 \\<^sub>0_G_Inf[unfolded \\<^sub>0_is'] simp: \\<^sub>0_is' is_ground_subst_list_def\) - then have \\\<^sub>0 \ \_Inf M \\ - unfolding \_Inf_def \_def CAs0_is[symmetric] DA0_is[symmetric] E0_is[symmetric] by simp + then have \\\<^sub>0 \ \_I M \\ + unfolding \_I_def \_def CAs0_is[symmetric] DA0_is[symmetric] E0_is[symmetric] by simp moreover have \\ \ F.Inf_from M\ using prems_in i_F_Inf unfolding F.Inf_from_def \_def by simp ultimately show ?thesis by blast qed interpretation F: statically_complete_calculus "{{#}}" F_Inf "(\\e)" F.Red_I_\ F.Red_F_\_empty proof (rule F.stat_ref_comp_to_non_ground_fam_inter; clarsimp; (intro exI)?) show "\M. statically_complete_calculus {{#}} (G_Inf M) (\e) (G.Red_I M) G.Red_F" by (fact G.statically_complete_calculus_axioms) next fix N assume "F.saturated N" - show "F.ground.Inf_from_q N (\ (\_F ` N)) \ {\. \\' \ F.Inf_from N. \ \ \_Inf N \'} + show "F.ground.Inf_from_q N (\ (\_F ` N)) \ {\. \\' \ F.Inf_from N. \ \ \_I N \'} \ G.Red_I N (\ (\_F ` N))" - using G_Inf_overapproximates_F_Inf unfolding F.ground.Inf_from_q_def \_Inf_def by fastforce + using G_Inf_overapproximates_F_Inf unfolding F.ground.Inf_from_q_def \_I_def by fastforce qed subsection \Labeled First-Order Layer (or Given Clause Layer)\ datatype label = New | Processed | Old definition FL_Infer_of :: "'a clause inference \ ('a clause \ label) inference set" where "FL_Infer_of \ = {Infer Cls (D, New) |Cls D. \ = Infer (map fst Cls) D}" definition FL_Inf :: "('a clause \ label) inference set" where "FL_Inf = (\\ \ F_Inf. FL_Infer_of \)" abbreviation F_Equiv :: "'a clause \ 'a clause \ bool" (infix "\" 50) where "C \ D \ generalizes C D \ generalizes D C" abbreviation F_Prec :: "'a clause \ 'a clause \ bool" (infix "\\" 50) where "C \\ D \ strictly_generalizes C D" fun L_Prec :: "label \ label \ bool" (infix "\l" 50) where "Old \l l \ l \ Old" | "Processed \l l \ l = New" | "New \l l \ False" lemma irrefl_L_Prec: "\ l \l l" by (cases l) auto lemma trans_L_Prec: "l1 \l l2 \ l2 \l l3 \ l1 \l l3" by (cases l1; cases l2; cases l3) auto lemma wf_L_Prec: "wfP (\l)" by (metis L_Prec.elims(2) L_Prec.simps(3) not_accp_down wfP_accp_iff) interpretation FL: given_clause "{{#}}" F_Inf "{{#}}" UNIV "\N. (\e)" G_Inf G.Red_I - "\N. G.Red_F" "\N. \_F" \_Inf_opt FL_Inf "(\)" "(\\)" "(\l)" Old + "\N. G.Red_F" "\N. \_F" \_I_opt FL_Inf "(\)" "(\\)" "(\l)" Old proof (unfold_locales; (intro ballI)?) show "equivp (\)" unfolding equivp_def by (meson generalizes_refl generalizes_trans) next show "po_on (\\) UNIV" unfolding po_on_def irreflp_on_def transp_on_def using strictly_generalizes_irrefl strictly_generalizes_trans by auto next show "wfp_on (\\) UNIV" unfolding wfp_on_UNIV by (metis wf_strictly_generalizes) next show "po_on (\l) UNIV" unfolding po_on_def irreflp_on_def transp_on_def using irrefl_L_Prec trans_L_Prec by blast next show "wfp_on (\l) UNIV" unfolding wfp_on_UNIV by (rule wf_L_Prec) next fix C1 D1 C2 D2 assume "C1 \ D1" "C2 \ D2" "C1 \\ C2" then show "D1 \\ D2" by (smt antisym size_mset_mono size_subst strictly_generalizes_def generalizes_def generalizes_trans) next fix N C1 C2 assume "C1 \ C2" then show "\_F C1 \ \_F C2" unfolding generalizes_def \_F_def by clarsimp (metis is_ground_comp_subst subst_cls_comp_subst) next fix N C2 C1 assume "C2 \\ C1" then show "\_F C1 \ \_F C2" unfolding strictly_generalizes_def generalizes_def \_F_def by clarsimp (metis is_ground_comp_subst subst_cls_comp_subst) next show "\l. L_Prec Old l" using L_Prec.simps(1) by blast qed (auto simp: FL_Inf_def FL_Infer_of_def F_Inf_have_prems) notation FL.Prec_FL (infix "\" 50) notation FL.entails_\_L (infix "\\Le" 50) notation FL.derive (infix "\RedL" 50) notation FL.step (infix "\GC" 50) lemma FL_Red_F_eq: "FL.Red_F N = {C. \D \ \_F (fst C). D \ G.Red_F (\ (\_F ` fst ` N)) \ (\E \ N. E \ C \ D \ \_F (fst E))}" unfolding FL.Red_F_def FL.Red_F_\_q_def by auto lemma mem_FL_Red_F_because_G_Red_F: "(\D \ \_F (fst Cl). D \ G.Red_F (\ (\_F ` fst ` N))) \ Cl \ FL.Red_F N" unfolding FL_Red_F_eq by auto lemma mem_FL_Red_F_because_Prec_FL: "(\D \ \_F (fst Cl). \El \ N. El \ Cl \ D \ \_F (fst El)) \ Cl \ FL.Red_F N" unfolding FL_Red_F_eq by auto interpretation FL: compact_consequence_relation FL.Bot_FL "(\\Le)" proof fix CCl assume unsat: "CCl \\Le FL.Bot_FL" let ?bot = "({#}, undefined)" have "CCl \\Le {?bot}" using unsat by (metis (lifting) FL.entail_set_all_formulas UNIV_I insertI1 mem_Sigma_iff) then have "\ satisfiable (\CL \ CCl. \_F (fst CL))" unfolding FL.labeled_entailment_lifting F_entails_\_iff by auto then obtain DD where d_sub: "DD \ (\Cl \ CCl. \_F (fst Cl))" and d_fin: "finite DD" and d_unsat: "\I. \ I \s DD" unfolding clausal_logic_compact[of "\CL \ CCl. \_F (fst CL)"] by blast define CCl' :: "('a clause \ label) set" where "CCl' = {SOME Cl. Cl \ CCl \ D \ \_F (fst Cl) |D. D \ DD}" have ex_in_cl: "\Cl. Cl \ CCl \ D \ \_F (fst Cl)" if "D \ DD" for D using that d_sub by blast then have d_sub': "DD \ (\Cl \ CCl'. \_F (fst Cl))" using ex_in_cl unfolding CCl'_def by clarsimp (metis (lifting) eq_fst_iff ex_in_cl someI_ex) have "CCl' \ CCl" unfolding CCl'_def using someI_ex[OF ex_in_cl] by blast moreover have "finite CCl'" unfolding CCl'_def using d_fin by simp moreover have "CCl' \\Le FL.Bot_FL" unfolding CCl'_def using d_unsat ex_in_cl d_sub' CCl'_def by (metis (no_types, lifting) FL.entails_\_L_def subsetD true_clss_def) ultimately show "\CCl' \ CCl. finite CCl' \ CCl' \\Le FL.Bot_FL" by blast qed interpretation FL: refutationally_compact_calculus FL.Bot_FL FL_Inf "(\\Le)" FL.Red_I FL.Red_F .. subsection \\textsf{RP} Layer\ interpretation sq: selection "S_Q Sts" unfolding S_Q_def using S_M_selects_subseteq S_M_selects_neg_lits selection_axioms by unfold_locales auto interpretation gd: ground_resolution_with_selection "S_Q Sts" by unfold_locales interpretation src: standard_redundancy_criterion_reductive "gd.ord_\ Sts" by unfold_locales interpretation src: standard_redundancy_criterion_counterex_reducing "gd.ord_\ Sts" "ground_resolution_with_selection.INTERP (S_Q Sts)" by unfold_locales definition lclss_of_state :: "'a state \ ('a clause \ label) set" where "lclss_of_state St = (\C. (C, New)) ` N_of_state St \ (\C. (C, Processed)) ` P_of_state St \ (\C. (C, Old)) ` Q_of_state St" lemma image_hd_lclss_of_state[simp]: "fst ` lclss_of_state St = clss_of_state St" unfolding lclss_of_state_def by (auto simp: image_Un image_comp) lemma insert_lclss_of_state[simp]: "insert (C, New) (lclss_of_state (N, P, Q)) = lclss_of_state (N \ {C}, P, Q)" "insert (C, Processed) (lclss_of_state (N, P, Q)) = lclss_of_state (N, P \ {C}, Q)" "insert (C, Old) (lclss_of_state (N, P, Q)) = lclss_of_state (N, P, Q \ {C})" unfolding lclss_of_state_def image_def by auto lemma union_lclss_of_state[simp]: "lclss_of_state (N1, P1, Q1) \ lclss_of_state (N2, P2, Q2) = lclss_of_state (N1 \ N2, P1 \ P2, Q1 \ Q2)" unfolding lclss_of_state_def by auto lemma mem_lclss_of_state[simp]: "(C, New) \ lclss_of_state (N, P, Q) \ C \ N" "(C, Processed) \ lclss_of_state (N, P, Q) \ C \ P" "(C, Old) \ lclss_of_state (N, P, Q) \ C \ Q" unfolding lclss_of_state_def image_def by auto lemma lclss_Liminf_commute: "Liminf_llist (lmap lclss_of_state Sts) = lclss_of_state (Liminf_state Sts)" proof - have \Liminf_llist (lmap lclss_of_state Sts) = (\C. (C, New)) ` Liminf_llist (lmap N_of_state Sts) \ (\C. (C, Processed)) ` Liminf_llist (lmap P_of_state Sts) \ (\C. (C, Old)) ` Liminf_llist (lmap Q_of_state Sts)\ proof - have \inj_on (\C. (C, Old)) (Sup_llist (lmap Q_of_state Sts))\ by (meson Pair_inject inj_onI) moreover have \inj_on (\C. (C, Processed)) (Sup_llist (lmap P_of_state Sts))\ by (meson Pair_inject inj_onI) moreover have \inj_on (\C. (C, New)) (Sup_llist (lmap N_of_state Sts))\ by (meson Pair_inject inj_onI) moreover have \ \x\lset Sts. \Y\lset Sts. ((\C. (C, New)) ` N_of_state x \ (\C. (C, Processed)) ` P_of_state x) \ (\C. (C, Old)) ` Q_of_state Y = {}\ by auto moreover have \ \x\lset Sts. \Y\lset Sts. (\C. (C, New)) ` N_of_state x \ (\C. (C, Processed)) ` P_of_state Y = {}\ by auto ultimately show ?thesis unfolding lclss_of_state_def[abs_def] using Liminf_llist_lmap_union Liminf_llist_lmap_image by (smt llist.map_cong) qed then show ?thesis unfolding lclss_of_state_def Liminf_state_def by auto qed lemma GC_tautology_step: assumes tauto: "Neg A \# C" "Pos A \# C" shows "lclss_of_state (N \ {C}, P, Q) \GC lclss_of_state (N, P, Q)" proof - have c\_red: "C\ \ G.Red_F (\D \ N'. \_F (fst D))" if in_g: "C\ \ \_F C" for N' :: "('a clause \ label) set" and C\ proof - obtain \ where "C\ = C \ \" using in_g unfolding \_F_def by blast then have compl_lits: "Neg (A \a \) \# C\" "Pos (A \a \) \# C\" using tauto Neg_Melem_subst_atm_subst_cls Pos_Melem_subst_atm_subst_cls by auto then have "{} \e {C\}" unfolding true_clss_def true_cls_def true_lit_def if_distrib_fun by (metis literal.disc literal.sel singletonD) then show ?thesis unfolding G.Red_F_def by auto qed show ?thesis proof (rule FL.step.process[of _ "lclss_of_state (N, P, Q)" "{(C, New)}" _ "{}"]) show \lclss_of_state (N \ {C}, P, Q) = lclss_of_state (N, P, Q) \ {(C, New)}\ unfolding lclss_of_state_def by auto next show \lclss_of_state (N, P, Q) = lclss_of_state (N, P, Q) \ {}\ unfolding lclss_of_state_def by auto next show \{(C, New)} \ FL.Red_F_\ (lclss_of_state (N, P, Q) \ {})\ using mem_FL_Red_F_because_G_Red_F c\_red[of _ "lclss_of_state (N, P, Q)"] unfolding lclss_of_state_def by auto next show \FL.active_subset {} = {}\ unfolding FL.active_subset_def by auto qed qed lemma GC_subsumption_step: assumes d_in: "Dl \ N" and d_sub_c: "strictly_subsumes (fst Dl) (fst Cl) \ subsumes (fst Dl) (fst Cl) \ snd Dl \l snd Cl" shows "N \ {Cl} \GC N" proof - have d_sub'_c: "Cl \ FL.Red_F {Dl} \ Dl \ Cl" proof (cases "size (fst Dl) = size (fst Cl)") case True assume sizes_eq: \size (fst Dl) = size (fst Cl)\ have \size (fst Dl) = size (fst Cl) \ strictly_subsumes (fst Dl) (fst Cl) \ subsumes (fst Dl) (fst Cl) \ snd Dl \l snd Cl \ Dl \ Cl\ unfolding FL.Prec_FL_def unfolding generalizes_def strictly_generalizes_def strictly_subsumes_def subsumes_def by (metis size_subst subset_mset.order_refl subseteq_mset_size_eql) then have "Dl \ Cl" using sizes_eq d_sub_c by auto then show ?thesis by (rule disjI2) next case False then have d_ssub_c: "strictly_subsumes (fst Dl) (fst Cl)" using d_sub_c unfolding strictly_subsumes_def subsumes_def by (metis size_subst strict_subset_subst_strictly_subsumes strictly_subsumes_antisym subset_mset.antisym_conv2) have "Cl \ FL.Red_F {Dl}" proof (rule mem_FL_Red_F_because_G_Red_F) show \\D\\_F (fst Cl). D \ G.Red_F (\ (\_F ` fst ` {Dl}))\ using d_ssub_c unfolding G.Red_F_def strictly_subsumes_def subsumes_def \_F_def proof clarsimp fix \ \' assume fst_not_in: \\\. \ fst Cl \ \ \# fst Dl\ and fst_in: \fst Dl \ \ \# fst Cl\ and gr_sig: \is_ground_subst \'\ have \{fst Dl \ \ \ \'} \ {fst Dl \ \ |\. is_ground_subst \}\ using gr_sig by (metis (mono_tags, lifting) is_ground_comp_subst mem_Collect_eq singletonD subsetI subst_cls_comp_subst) moreover have \\I. I \s {fst Dl \ \ \ \'} \ I \ fst Cl \ \'\ using fst_in by (meson subst_cls_mono_mset true_clss_insert true_clss_subclause) moreover have \\D\{fst Dl \ \ \ \'}. D < fst Cl \ \'\ using fst_not_in fst_in gr_sig proof clarify show \\\. \ fst Cl \ \ \# fst Dl \ fst Dl \ \ \# fst Cl \ is_ground_subst \' \ fst Dl \ \ \ \' < fst Cl \ \'\ by (metis False size_subst subset_imp_less_mset subset_mset.le_less subst_subset_mono) qed ultimately show \\DD\{fst Dl \ \ |\. is_ground_subst \}. (\I. I \s DD \ I \ fst Cl \ \') \ (\D\DD. D < fst Cl \ \')\ by blast qed qed then show ?thesis by (rule disjI1) qed show ?thesis proof (rule FL.step.process[of _ N "{Cl}" _ "{}"], simp+) show \Cl \ FL.Red_F_\ N\ using d_sub'_c unfolding FL_Red_F_eq proof - have \\D. D \ \_F (fst Cl) \ \E\N. E \ Cl \ D \ \_F (fst E) \ \D\\_F (fst Cl). D \ G.Red_F (\_F (fst Dl)) \ Dl \ Cl \ D \ \_F (fst Dl) \ D \ G.Red_F (\a\N. \_F (fst a))\ by (metis (no_types, lifting) G.Red_F_of_subset SUP_upper d_in subset_iff) moreover have \\D. D \ \_F (fst Cl) \ \E\N. E \ Cl \ D \ \_F (fst E) \ Dl \ Cl \ D \ G.Red_F (\a\N. \_F (fst a))\ by (smt FL.Prec_FL_def FL.equiv_F_grounding FL.prec_F_grounding UNIV_witness d_in in_mono) ultimately show \Cl \ {C. \D\\_F (fst C). D \ G.Red_F (\ (\_F ` fst ` {Dl})) \ (\E\{Dl}. E \ C \ D \ \_F (fst E))} \ Dl \ Cl \ Cl \ {C. \D\\_F (fst C). D \ G.Red_F (\ (\_F ` fst ` N)) \ (\E\N. E \ C \ D \ \_F (fst E))}\ by auto qed next show \FL.active_subset {} = {}\ unfolding FL.active_subset_def by simp qed qed lemma GC_reduction_step: assumes young: "snd Dl \ Old" and d_sub_c: "fst Dl \# fst Cl" shows "N \ {Cl} \GC N \ {Dl}" proof (rule FL.step.process[of _ N "{Cl}" _ "{Dl}"]) have "Cl \ FL.Red_F {Dl}" proof (rule mem_FL_Red_F_because_G_Red_F) show \\D\\_F (fst Cl). D \ G.Red_F (\ (\_F ` fst ` {Dl}))\ using d_sub_c unfolding G.Red_F_def strictly_subsumes_def subsumes_def \_F_def proof clarsimp fix \ assume fst_not_in: \\ fst Cl \# fst Dl\ and fst_in: \fst Dl \# fst Cl\ and gr_sig: \is_ground_subst \\ have \{fst Dl \ \} \ {fst Dl \ \ |\. is_ground_subst \}\ using gr_sig by blast moreover have \fst Dl \ \ < fst Cl \ \\ using subst_subset_mono[OF d_sub_c, of \] gr_sig by (simp add: subset_imp_less_mset) moreover have \\I. I \ fst Dl \ \ \ I \ fst Cl \ \\ using subst_subset_mono[OF d_sub_c] true_clss_subclause by fast ultimately show \\DD\{fst Dl \ \ |\. is_ground_subst \}. (\I. I \s DD \ I \ fst Cl \ \) \ (\D\DD. D < fst Cl \ \)\ by blast qed qed then show "{Cl} \ FL.Red_F (N \ {Dl})" using FL.Red_F_of_subset by blast qed (auto simp: FL.active_subset_def young) lemma GC_processing_step: "N \ {(C, New)} \GC N \ {(C, Processed)}" proof (rule FL.step.process[of _ N "{(C, New)}" _ "{(C, Processed)}"]) have "(C, New) \ FL.Red_F {(C, Processed)}" by (rule mem_FL_Red_F_because_Prec_FL) (simp add: FL.Prec_FL_def generalizes_refl) then show "{(C, New)} \ FL.Red_F (N \ {(C, Processed)})" using FL.Red_F_of_subset by blast qed (auto simp: FL.active_subset_def) lemma old_inferences_between_eq_new_inferences_between: "old_concl_of ` inference_system.inferences_between (ord_FO_\ S) N C = - concl_of ` F.Inf_from2 N {C}" (is "?rp = ?f") + concl_of ` F.Inf_between N {C}" (is "?rp = ?f") proof (intro set_eqI iffI) fix E assume e_in: "E \ old_concl_of ` inference_system.inferences_between (ord_FO_\ S) N C" obtain CAs DA AAs As \ where e_res: "ord_resolve_rename S CAs DA AAs As \ E" and cd_sub: "set CAs \ {DA} \ N \ {C}" and c_in: "C \ set CAs \ {DA}" using e_in unfolding inference_system.inferences_between_def infer_from_def ord_FO_\_def by auto - show "E \ concl_of ` F.Inf_from2 N {C}" - unfolding F.Inf_from2_alt F.Inf_from_def + show "E \ concl_of ` F.Inf_between N {C}" + unfolding F.Inf_between_alt F.Inf_from_def proof - have \Infer (CAs @ [DA]) E \ F_Inf \ set (prems_of (Infer (CAs @ [DA]) E)) \ insert C N \ C \ set (prems_of (Infer (CAs @ [DA]) E)) \ E = concl_of (Infer (CAs @ [DA]) E)\ using e_res cd_sub c_in F_Inf_def by auto then show \E \ concl_of ` {\ \ F_Inf. \ \ {\ \ F_Inf. set (prems_of \) \ N \ {C}} \ set (prems_of \) \ {C} \ {}}\ by (smt Un_insert_right boolean_algebra_cancel.sup0 disjoint_insert(2) mem_Collect_eq image_def) qed next fix E - assume e_in: "E \ concl_of ` F.Inf_from2 N {C}" + assume e_in: "E \ concl_of ` F.Inf_between N {C}" obtain CAs DA AAs As \ where e_res: "ord_resolve_rename S CAs DA AAs As \ E" and cd_sub: "set CAs \ {DA} \ N \ {C}" and c_in: "C \ set CAs \ {DA}" - using e_in unfolding F.Inf_from2_alt F.Inf_from_def F_Inf_def inference_system.Inf_from2_alt + using e_in unfolding F.Inf_between_alt F.Inf_from_def F_Inf_def inference_system.Inf_between_alt inference_system.Inf_from_def by (auto simp: image_def Bex_def) show "E \ old_concl_of ` inference_system.inferences_between (ord_FO_\ S) N C" unfolding inference_system.inferences_between_def infer_from_def ord_FO_\_def using e_res cd_sub c_in by (clarsimp simp: image_def Bex_def, rule_tac x = "old_Infer (mset CAs) DA E" in exI, auto) qed lemma GC_inference_step: assumes young: "l \ Old" and no_active: "FL.active_subset M = {}" and m_sup: "fst ` M \ old_concl_of ` inference_system.inferences_between (ord_FO_\ S) (fst ` FL.active_subset N) C" shows "N \ {(C, l)} \GC N \ {(C, Old)} \ M" proof (rule FL.step.infer[of _ N C l _ M]) - have m_sup': "fst ` M \ concl_of ` F.Inf_from2 (fst ` FL.active_subset N) {C}" + have m_sup': "fst ` M \ concl_of ` F.Inf_between (fst ` FL.active_subset N) {C}" using m_sup unfolding old_inferences_between_eq_new_inferences_between . - show "F.Inf_from2 (fst ` FL.active_subset N) {C} \ F.Red_I (fst ` (N \ {(C, Old)} \ M))" + show "F.Inf_between (fst ` FL.active_subset N) {C} \ F.Red_I (fst ` (N \ {(C, Old)} \ M))" proof fix \ - assume \_in_if2: "\ \ F.Inf_from2 (fst ` FL.active_subset N) {C}" + assume \_in_if2: "\ \ F.Inf_between (fst ` FL.active_subset N) {C}" - note \_in = F.Inf_if_Inf_from2[OF \_in_if2] + note \_in = F.Inf_if_Inf_between[OF \_in_if2] have "concl_of \ \ fst ` M" - using m_sup' \_in_if2 m_sup' by (auto simp: image_def Collect_mono_iff F.Inf_from2_alt) + using m_sup' \_in_if2 m_sup' by (auto simp: image_def Collect_mono_iff F.Inf_between_alt) then have "concl_of \ \ fst ` (N \ {(C, Old)} \ M)" by auto then show "\ \ F.Red_I_\ (fst ` (N \ {(C, Old)} \ M))" by (rule F.Red_I_of_Inf_to_N[OF \_in]) qed qed (use young no_active in auto) lemma RP_step_imp_GC_step: "St \ St' \ lclss_of_state St \GC lclss_of_state St'" proof (induction rule: RP.induct) case (tautology_deletion A C N P Q) then show ?case by (rule GC_tautology_step) next case (forward_subsumption D P Q C N) note d_in = this(1) and d_sub_c = this(2) show ?case proof (cases "D \ P") case True then show ?thesis using GC_subsumption_step[of "(D, Processed)" "lclss_of_state (N, P, Q)" "(C, New)"] d_sub_c by auto next case False then have "D \ Q" using d_in by simp then show ?thesis using GC_subsumption_step[of "(D, Old)" "lclss_of_state (N, P, Q)" "(C, New)"] d_sub_c by auto qed next case (backward_subsumption_P D N C P Q) note d_in = this(1) and d_ssub_c = this(2) then show ?case using GC_subsumption_step[of "(D, New)" "lclss_of_state (N, P, Q)" "(C, Processed)"] d_ssub_c by auto next case (backward_subsumption_Q D N C P Q) note d_in = this(1) and d_ssub_c = this(2) then show ?case using GC_subsumption_step[of "(D, New)" "lclss_of_state (N, P, Q)" "(C, Old)"] d_ssub_c by auto next case (forward_reduction D L' P Q L \ C N) show ?case using GC_reduction_step[of "(C, New)" "(C + {#L#}, New)" "lclss_of_state (N, P, Q)"] by auto next case (backward_reduction_P D L' N L \ C P Q) show ?case using GC_reduction_step[of "(C, Processed)" "(C + {#L#}, Processed)" "lclss_of_state (N, P, Q)"] by auto next case (backward_reduction_Q D L' N L \ C P Q) show ?case using GC_reduction_step[of "(C, Processed)" "(C + {#L#}, Old)" "lclss_of_state (N, P, Q)"] by auto next case (clause_processing N C P Q) show ?case using GC_processing_step[of "lclss_of_state (N, P, Q)" C] by auto next case (inference_computation N Q C P) note n = this(1) show ?case proof - have \FL.active_subset (lclss_of_state (N, {}, {})) = {}\ unfolding n by (auto simp: FL.active_subset_def) moreover have \old_concls_of (inference_system.inferences_between (ord_FO_\ S) (fst ` FL.active_subset (lclss_of_state ({}, P, Q))) C) \ N\ unfolding n inference_system.inferences_between_def image_def mem_Collect_eq lclss_of_state_def infer_from_def by (auto simp: FL.active_subset_def) ultimately have \lclss_of_state ({}, insert C P, Q) \GC lclss_of_state (N, P, insert C Q)\ using GC_inference_step[of Processed "lclss_of_state (N, {}, {})" "lclss_of_state ({}, P, Q)" C, simplified] by blast then show ?case by (auto simp: FL.active_subset_def) qed qed lemma RP_derivation_imp_GC_derivation: "chain (\) Sts \ chain (\GC) (lmap lclss_of_state Sts)" using chain_lmap RP_step_imp_GC_step by blast lemma RP_step_imp_derive_step: "St \ St' \ lclss_of_state St \RedL lclss_of_state St'" by (rule FL.one_step_equiv) (rule RP_step_imp_GC_step) lemma RP_derivation_imp_derive_derivation: "chain (\) Sts \ chain (\RedL) (lmap lclss_of_state Sts)" using chain_lmap RP_step_imp_derive_step by blast theorem RP_sound_new_statement: assumes deriv: "chain (\) Sts" and bot_in: "{#} \ clss_of_state (Liminf_state Sts)" shows "clss_of_state (lhd Sts) \\e {{#}}" proof - have "clss_of_state (Liminf_state Sts) \\e {{#}}" using F.subset_entailed bot_in by auto then have "fst ` Liminf_llist (lmap lclss_of_state Sts) \\e {{#}}" by (metis image_hd_lclss_of_state lclss_Liminf_commute) then have "Liminf_llist (lmap lclss_of_state Sts) \\Le FL.Bot_FL" using FL.labeled_entailment_lifting by simp then have "lhd (lmap lclss_of_state Sts) \\Le FL.Bot_FL" proof - assume entails_lim: \FL.entails_\ (Liminf_llist (lmap lclss_of_state Sts)) ({{#}} \ UNIV)\ have \chain (\RedL) (lmap lclss_of_state Sts)\ using deriv RP_derivation_imp_derive_derivation by simp moreover have \chain FL.entails_\ (lmap lclss_of_state Sts)\ by (smt F_entails_\_iff FL.labeled_entailment_lifting RP_model chain_lmap deriv \_Fs_def image_hd_lclss_of_state) ultimately show \FL.entails_\ (lhd (lmap lclss_of_state Sts)) ({{#}} \ UNIV)\ using entails_lim FL.unsat_limit_iff by blast qed then have "lclss_of_state (lhd Sts) \\Le FL.Bot_FL" using chain_not_lnull deriv by fastforce then show ?thesis unfolding FL.entails_\_L_def F.entails_\_def lclss_of_state_def by auto qed theorem RP_saturated_if_fair_new_statement: assumes deriv: "chain (\) Sts" and init: "FL.active_subset (lclss_of_state (lhd Sts)) = {}" and final: "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}" shows "FL.saturated (Liminf_llist (lmap lclss_of_state Sts))" proof - note nnil = chain_not_lnull[OF deriv] have gc_deriv: "chain (\GC) (lmap lclss_of_state Sts)" by (rule RP_derivation_imp_GC_derivation[OF deriv]) show ?thesis using nnil init final FL.fair_implies_Liminf_saturated[OF FL.gc_to_red[OF gc_deriv] FL.gc_fair[OF gc_deriv]] by simp qed corollary RP_complete_if_fair_new_statement: assumes deriv: "chain (\) Sts" and init: "FL.active_subset (lclss_of_state (lhd Sts)) = {}" and final: "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}" and unsat: "grounding_of_state (lhd Sts) \e {{#}}" shows "{#} \ Q_of_state (Liminf_state Sts)" proof - note nnil = chain_not_lnull[OF deriv] note len = chain_length_pos[OF deriv] have gc_deriv: "chain (\GC) (lmap lclss_of_state Sts)" by (rule RP_derivation_imp_GC_derivation[OF deriv]) have hd_unsat: "fst ` lhd (lmap lclss_of_state Sts) \\e {{#}}" proof - have hd_lcls: "fst ` lhd (lmap lclss_of_state Sts) = lhd (lmap clss_of_state Sts)" using len zero_enat_def by auto show ?thesis unfolding hd_lcls F_entails_\_iff unfolding true_clss_def proof fix I show "Ball (\ (\_F ` lhd (lmap (\St. N_of_state St \ P_of_state St \ Q_of_state St) Sts))) ((\) I) \ Ball (\ (\_F ` {{#}})) ((\) I)" using unsat unfolding \_Fs_def by (metis (no_types, lifting) chain_length_pos gc_deriv gr.ex_min_counterex i0_less llength_eq_0 llength_lmap llength_lmap llist.map_sel(1) true_cls_empty true_clss_singleton) qed qed have "\BL \ {{#}} \ UNIV. BL \ Liminf_llist (lmap lclss_of_state Sts)" proof (rule FL.gc_complete_Liminf[OF gc_deriv,of "{#}"]) show \FL.active_subset (lhd (lmap lclss_of_state Sts)) = {}\ by (simp add: init nnil) next show \FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}\ using final by blast next show \{#} \ {{#}}\ by simp next show \fst ` lhd (lmap lclss_of_state Sts) \\e {{#}}\ using hd_unsat by blast qed then show ?thesis unfolding Liminf_state_def lclss_Liminf_commute using final[unfolded FL.passive_subset_def] Liminf_state_def lclss_Liminf_commute by fastforce qed subsection \Alternative Derivation of Previous \textsf{RP} Results\ lemma old_fair_imp_new_fair: assumes nnul: "\ lnull Sts" and fair: "fair_state_seq Sts" and empty_Q0: "Q_of_state (lhd Sts) = {}" shows "FL.active_subset (lclss_of_state (lhd Sts)) = {}" "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}" proof - show "FL.active_subset (lclss_of_state (lhd Sts)) = {}" using nnul empty_Q0 unfolding FL.active_subset_def by (cases Sts) auto next show "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}" using fair unfolding fair_state_seq_def FL.passive_subset_def proof assume \N_of_state (Liminf_state Sts) = {}\ and \P_of_state (Liminf_state Sts) = {}\ then show \{CL \ Liminf_llist (lmap lclss_of_state Sts). snd CL \ Old} = {}\ unfolding lclss_Liminf_commute lclss_of_state_def by auto qed qed lemma old_redundant_infer_iff: "src.redundant_infer N \ \ (\DD. DD \ N \ DD \ set_mset (old_side_prems_of \) \e {old_concl_of \} \ (\D \ DD. D < old_main_prem_of \))" (is "?lhs \ ?rhs") proof assume ?lhs then show ?rhs unfolding src.redundant_infer_def by auto next assume ?rhs then obtain DD0 where "DD0 \ N" and "DD0 \ set_mset (old_side_prems_of \) \e {old_concl_of \}" and "\D \ DD0. D < old_main_prem_of \" by blast then obtain DD where fin_dd: "finite DD" and dd_in: "DD \ N" and dd_un: "DD \ set_mset (old_side_prems_of \) \e {old_concl_of \}" and all_dd: "\D \ DD. D < old_main_prem_of \" using entails_concl_compact_union[of "{old_concl_of \}" DD0 "set_mset (old_side_prems_of \)"] by fast show ?lhs unfolding src.redundant_infer_def proof show \set_mset (mset_set DD) \ N \ (\I. I \m mset_set DD + old_side_prems_of \ \ I \ old_concl_of \) \ (\D. D \# mset_set DD \ D < old_main_prem_of \)\ using fin_dd dd_in dd_un all_dd by auto qed qed definition old_infer_of :: "'a clause inference \ 'a old_inference" where "old_infer_of \ = old_Infer (mset (side_prems_of \)) (main_prem_of \) (concl_of \)" lemma new_redundant_infer_imp_old_redundant_infer: "G.redundant_infer N \ \ src.redundant_infer N (old_infer_of \)" unfolding old_redundant_infer_iff G.redundant_infer_def old_infer_of_def by simp lemma saturated_imp_saturated_RP: assumes satur: "FL.saturated (Liminf_llist (lmap lclss_of_state Sts))" and no_passive: "FL.passive_subset (Liminf_llist (lmap lclss_of_state Sts)) = {}" shows "src.saturated_upto Sts (grounding_of_state (Liminf_state Sts))" proof - define Q where "Q = Liminf_llist (lmap Q_of_state Sts)" define Ql where "Ql = (\C. (C, Old)) ` Q" define G where "G = \ (\_F ` Q)" have limuls_eq: "Liminf_llist (lmap lclss_of_state Sts) = Ql" unfolding Ql_def Q_def using no_passive[unfolded FL.passive_subset_def] proof (simp) (* Sledgehammer-generated *) assume a1: "\a b. (a, b) \ Liminf_llist (lmap lclss_of_state Sts) \ b = Old" obtain mm :: "'a literal multiset set \ 'a literal multiset" where f2: "\M. {} = M \ mm M \ M" by (metis (no_types) equals0I) have f3: "\ps. Liminf_llist (lmap lclss_of_state ps) = lclss_of_state (Liminf_llist (lmap N_of_state ps), Liminf_llist (lmap P_of_state ps), Liminf_llist (lmap Q_of_state ps))" using Liminf_state_def lclss_Liminf_commute by presburger then have f4: "Liminf_llist (lmap P_of_state Sts) = {}" using f2 a1 by (metis (no_types) label.simps(5) mem_lclss_of_state(2)) have "Liminf_llist (lmap N_of_state Sts) = {}" using f3 f2 a1 by (metis (no_types) label.simps(3) mem_lclss_of_state(1)) then show "Liminf_llist (lmap lclss_of_state Sts) = (\m. (m, Old)) ` Liminf_llist (lmap Q_of_state Sts)" using f4 f3 by (simp add: lclss_of_state_def) qed have clst_eq: "clss_of_state (Liminf_state Sts) = Q" proof - (* Sledgehammer-generated *) have f1: "Q_of_state (Liminf_state Sts) = Q" using Liminf_state_def Q_def Q_of_state.simps by presburger then have f2: "Ql \ ((\m. (m, New)) ` N_of_state (Liminf_state Sts) \ (\m. (m, Processed)) ` P_of_state (Liminf_state Sts)) = lclss_of_state (Liminf_state Sts)" by (simp add: Ql_def lclss_of_state_def sup_commute) have f3: "lclss_of_state ({}, {}, Q_of_state (Liminf_state Sts)) = {} \ Ql" using f1 by (simp add: Ql_def lclss_of_state_def) have "Ql = (\m. (m, New)) ` N_of_state (Liminf_state Sts) \ (\m. (m, Processed)) ` P_of_state (Liminf_state Sts) \ (Ql \ {})" using f1 lclss_Liminf_commute lclss_of_state_def limuls_eq by auto then have "clss_of_state (Liminf_state Sts) = fst ` lclss_of_state ({}, {}, Q_of_state (Liminf_state Sts))" using f3 f2 by (simp add: sup_commute) then show ?thesis unfolding Q_def by (simp add: Liminf_state_def) qed have gflimuls_eq: "(\Cl \ Ql. \_F (fst Cl)) = G" unfolding Ql_def G_def by auto have "gd.inferences_from Sts G \ src.Ri Sts G" proof fix \ assume \_inf: "\ \ gd.inferences_from Sts G" obtain \ where \_inff: "\ \ G.Inf_from Q G" and \: "\ = old_infer_of \" using \_inf unfolding gd.inferences_from_def old_infer_from_def G.Inf_from_def old_infer_of_def proof (atomize_elim, clarify) assume g_is: \\ \ gd.ord_\ Sts\ and prems_in: \set_mset (old_side_prems_of \ + {#old_main_prem_of \#}) \ G\ obtain CAs DA AAs As E where main_in: \DA \ G\ and side_in: \set CAs \ G\ and g_is2: \\ = old_Infer (mset CAs) DA E\ and ord_res: \gd.ord_resolve Sts CAs DA AAs As E\ using g_is prems_in unfolding gd.ord_\_def by auto define \_\ where "\_\ = Infer (CAs @ [DA]) E" then have \\_\ \ G_Inf Q\ using Q_of_state.simps g_is g_is2 ord_res Liminf_state_def S_Q_def unfolding gd.ord_\_def G_Inf_def Q_def by auto moreover have \set (prems_of \_\) \ G\ using g_is2 prems_in unfolding \_\_def by simp moreover have \\ = old_Infer (mset (side_prems_of \_\)) (main_prem_of \_\) (concl_of \_\)\ using g_is2 unfolding \_\_def by simp ultimately show \\\. \ \ {\ \ G_Inf Q. set (prems_of \) \ G} \ \ = old_Infer (mset (side_prems_of \)) (main_prem_of \) (concl_of \)\ by blast qed obtain \' where \'_inff: "\' \ F.Inf_from Q" and - \_in_\': "\ \ \_Inf Q \'" + \_in_\': "\ \ \_I Q \'" using G_Inf_overapproximates_F_Inf \_inff unfolding G_def by blast note \'_inf = F.Inf_if_Inf_from[OF \'_inff] let ?olds = "replicate (length (prems_of \')) Old" obtain \'' and l0 where \'': "\'' = Infer (zip (prems_of \') ?olds) (concl_of \', l0)" and \''_inf: "\'' \ FL_Inf" using FL.Inf_F_to_Inf_FL[OF \'_inf, of ?olds, simplified] by blast have "set (prems_of \'') \ Ql" using \'_inff[unfolded F.Inf_from_def, simplified] unfolding \'' Ql_def by auto then have "\'' \ FL.Inf_from Ql" unfolding FL.Inf_from_def using \''_inf by simp moreover have "\' = FL.to_F \''" unfolding \'' unfolding FL.to_F_def by simp ultimately have "\ \ G.Red_I Q G" using \_in_\' FL.sat_inf_imp_ground_red_fam_inter[OF satur, unfolded limuls_eq gflimuls_eq, simplified] by blast then have "G.redundant_infer G \" unfolding G.Red_I_def by auto then have \_red: "src.redundant_infer G \" unfolding \ by (rule new_redundant_infer_imp_old_redundant_infer) moreover have "\ \ gd.ord_\ Sts" using \_inf gd.inferences_from_def by blast ultimately show "\ \ src.Ri Sts G" unfolding src.Ri_def by auto qed then show ?thesis unfolding G_def clst_eq src.saturated_upto_def by clarsimp (smt Diff_subset gd.inferences_from_mono subset_eq \_Fs_def) qed theorem RP_sound_old_statement: assumes deriv: "chain (\) Sts" and bot_in: "{#} \ clss_of_state (Liminf_state Sts)" shows "\ satisfiable (grounding_of_state (lhd Sts))" using RP_sound_new_statement[OF deriv bot_in] unfolding F_entails_\_iff \_Fs_def by simp text \The theorem below is stated differently than the original theorem in \textsf{RP}: The grounding of the limit might be a strict subset of the limit of the groundings. Because saturation is neither monotone nor antimonotone, the two results are incomparable. See also @{thm [source] grounding_of_state_Liminf_state_subseteq}.\ theorem RP_saturated_if_fair_old_statement_altered: assumes deriv: "chain (\) Sts" and fair: "fair_state_seq Sts" and empty_Q0: "Q_of_state (lhd Sts) = {}" shows "src.saturated_upto Sts (grounding_of_state (Liminf_state Sts))" proof - note fair' = old_fair_imp_new_fair[OF chain_not_lnull[OF deriv] fair empty_Q0] show ?thesis proof (rule saturated_imp_saturated_RP[OF _ fair'(2)], rule RP_saturated_if_fair_new_statement) show \chain (\) Sts\ by (rule deriv) qed (rule fair')+ qed corollary RP_complete_if_fair_old_statement: assumes deriv: "chain (\) Sts" and fair: "fair_state_seq Sts" and empty_Q0: "Q_of_state (lhd Sts) = {}" and unsat: "\ satisfiable (grounding_of_state (lhd Sts))" shows "{#} \ Q_of_state (Liminf_state Sts)" proof (rule RP_complete_if_fair_new_statement) show \chain (\) Sts\ by (rule deriv) next show \\_Fs (N_of_state (lhd Sts) \ P_of_state (lhd Sts) \ Q_of_state (lhd Sts)) \e {{#}}\ using unsat unfolding F_entails_\_iff by auto qed (rule old_fair_imp_new_fair[OF chain_not_lnull[OF deriv] fair empty_Q0])+ end end diff --git a/thys/Saturation_Framework_Extensions/Given_Clause_Architectures_Revisited.thy b/thys/Saturation_Framework_Extensions/Given_Clause_Architectures_Revisited.thy --- a/thys/Saturation_Framework_Extensions/Given_Clause_Architectures_Revisited.thy +++ b/thys/Saturation_Framework_Extensions/Given_Clause_Architectures_Revisited.thy @@ -1,500 +1,500 @@ (* Title: New Fairness Proofs for the Given Clause Prover Architectures Author: Jasmin Blanchette , 2020 *) section \New Fairness Proofs for the Given Clause Prover Architectures\ theory Given_Clause_Architectures_Revisited imports Saturation_Framework.Given_Clause_Architectures begin text \The given clause and lazy given clause procedures satisfy key invariants. This provides an alternative way to prove fairness and hence saturation of the limit.\ subsection \Given Clause Procedure\ context given_clause begin definition gc_invar :: "('f \ 'l) set llist \ enat \ bool" where "gc_invar Ns i \ Inf_from (active_subset (Liminf_upto_llist Ns i)) \ Sup_upto_llist (lmap Red_I_\ Ns) i" lemma gc_invar_infinity: assumes nnil: "\ lnull Ns" and invar: "\i. enat i < llength Ns \ gc_invar Ns (enat i)" shows "gc_invar Ns \" unfolding gc_invar_def proof (intro subsetI, unfold Liminf_upto_llist_infinity Sup_upto_llist_infinity) fix \ assume \_inff: "\ \ Inf_from (active_subset (Liminf_llist Ns))" define As where "As = lmap active_subset Ns" have act_ns: "active_subset (Liminf_llist Ns) = Liminf_llist As" unfolding As_def active_subset_def Liminf_set_filter_commute[symmetric] .. note \_inf = Inf_if_Inf_from[OF \_inff] note \_inff' = \_inff[unfolded act_ns] have "\ lnull As" unfolding As_def using nnil by auto moreover have "set (prems_of \) \ Liminf_llist As" using \_inff'[unfolded Inf_from_def] by simp ultimately obtain i where i_lt_as: "enat i < llength As" and prems_sub_ge_i: "set (prems_of \) \ (\j \ {j. i \ j \ enat j < llength As}. lnth As j)" using finite_subset_Liminf_llist_imp_exists_index by blast note i_lt_ns = i_lt_as[unfolded As_def, simplified] have "set (prems_of \) \ lnth As i" using prems_sub_ge_i i_lt_as by auto then have "\ \ Inf_from (active_subset (lnth Ns i))" using i_lt_as \_inf unfolding Inf_from_def As_def by auto then have "\ \ Sup_upto_llist (lmap Red_I_\ Ns) (enat i)" using nnil i_lt_ns invar[unfolded gc_invar_def] by auto then show "\ \ Sup_llist (lmap Red_I_\ Ns)" using Sup_upto_llist_subset_Sup_llist by fastforce qed lemma gc_invar_gc_init: assumes "\ lnull Ns" and "active_subset (lhd Ns) = {}" shows "gc_invar Ns 0" using assms labeled_inf_have_prems unfolding gc_invar_def Inf_from_def by auto lemma gc_invar_gc_step: assumes Si_lt: "enat (Suc i) < llength Ns" and invar: "gc_invar Ns i" and step: "lnth Ns i \GC lnth Ns (Suc i)" shows "gc_invar Ns (Suc i)" using step Si_lt invar proof cases have i_lt: "enat i < llength Ns" using Si_lt Suc_ile_eq order.strict_implies_order by blast have lim_i: "Liminf_upto_llist Ns (enat i) = lnth Ns i" using i_lt by auto have lim_Si: "Liminf_upto_llist Ns (enat (Suc i)) = lnth Ns (Suc i)" using Si_lt by auto { case (process N M M') note ni = this(1) and nSi = this(2) and m'_pas = this(4) have "Inf_from (active_subset (N \ M')) \ Inf_from (active_subset (N \ M))" using m'_pas by (metis active_subset_union boolean_algebra_cancel.sup0 Inf_from_mono subset_Un_eq sup_left_idem) also have "\ \ Sup_upto_llist (lmap Red_I_\ Ns) (enat i)" using invar unfolding gc_invar_def lim_i ni by auto also have "\ \ Sup_upto_llist (lmap Red_I_\ Ns) (enat (Suc i))" by simp finally show ?thesis unfolding gc_invar_def lim_Si nSi . next case (infer N C L M) note ni = this(1) and nSi = this(2) and l_pas = this(3) and m_pas = this(4) and inff_red = this(5) { fix \ assume \_inff: "\ \ Inf_from (active_subset (N \ {(C, active)} \ M))" have \_inf: "\ \ Inf_FL" using \_inff unfolding Inf_from_def by auto then have F\_inf: "to_F \ \ Inf_F" using Inf_FL_to_Inf_F[folded to_F_def] by fastforce have "\ \ Inf_from (active_subset N \ {(C, active)})" using \_inff m_pas by simp then have F\_inff: "to_F \ \ no_labels.Inf_from (fst ` (active_subset N \ {(C, active)}))" using F\_inf unfolding to_F_def Inf_from_def no_labels.Inf_from_def by auto have "\ \ Sup_upto_llist (lmap Red_I_\ Ns) (enat (Suc i))" - proof (cases "to_F \ \ no_labels.Inf_from2 (fst ` active_subset N) {C}") + proof (cases "to_F \ \ no_labels.Inf_between (fst ` active_subset N) {C}") case True then have "to_F \ \ no_labels.Red_I_\ (fst ` (N \ {(C, active)} \ M))" using inff_red by auto then have "\ \ Red_I_\ (N \ {(C, active)} \ M)" by (subst labeled_red_inf_eq_red_inf[OF \_inf]) then show ?thesis using Si_lt using nSi by auto next case False then have "to_F \ \ no_labels.Inf_from (fst ` active_subset N)" - using F\_inff unfolding no_labels.Inf_from_def no_labels.Inf_from2_def by auto + using F\_inff unfolding no_labels.Inf_from_def no_labels.Inf_between_def by auto then have "\ \ Inf_from (active_subset N)" using \_inf l_pas unfolding to_F_def Inf_from_def no_labels.Inf_from_def by clarsimp (smt \_inff[unfolded Inf_from_def] active_subset_def imageE image_subset_iff in_mono mem_Collect_eq prod.collapse) then show ?thesis using invar l_pas unfolding gc_invar_def lim_i ni by auto qed } then show ?thesis unfolding gc_invar_def lim_Si nSi by blast } qed lemma gc_invar_gc: assumes gc: "chain (\GC) Ns" and init: "active_subset (lhd Ns) = {}" and i_lt: "i < llength Ns" shows "gc_invar Ns i" using i_lt proof (induct i) case (enat i) then show ?case proof (induct i) case 0 then show ?case using gc_invar_gc_init[OF chain_not_lnull[OF gc] init] by (simp add: enat_0) next case (Suc i) note ih = this(1) and Si_lt = this(2) have i_lt: "enat i < llength Ns" using Si_lt Suc_ile_eq less_le by blast show ?case by (rule gc_invar_gc_step[OF Si_lt ih[OF i_lt] chain_lnth_rel[OF gc Si_lt]]) qed qed simp lemma gc_fair_new_proof: assumes gc: "chain (\GC) Ns" and init: "active_subset (lhd Ns) = {}" and lim: "passive_subset (Liminf_llist Ns) = {}" shows "fair Ns" unfolding fair_def proof - have "Inf_from (Liminf_llist Ns) \ Inf_from (active_subset (Liminf_llist Ns))" (is "?lhs \ _") using lim unfolding active_subset_def passive_subset_def by (metis (no_types, lifting) Inf_from_mono empty_Collect_eq mem_Collect_eq subsetI) also have "... \ Sup_llist (lmap Red_I_\ Ns)" (is "_ \ ?rhs") using gc_invar_infinity[OF chain_not_lnull[OF gc]] gc_invar_gc[OF gc init] unfolding gc_invar_def by fastforce finally show "?lhs \ ?rhs" . qed end subsection \Lazy Given Clause\ context lazy_given_clause begin definition from_F :: "'f inference \ ('f \ 'l) inference set" where "from_F \ = {\' \ Inf_FL. to_F \' = \}" definition lgc_invar :: "('f inference set \ ('f \ 'l) set) llist \ enat \ bool" where "lgc_invar TNs i \ Inf_from (active_subset (Liminf_upto_llist (lmap snd TNs) i)) \ \ (from_F ` Liminf_upto_llist (lmap fst TNs) i) \ Sup_upto_llist (lmap (Red_I_\ \ snd) TNs) i" lemma lgc_invar_infinity: assumes nnil: "\ lnull TNs" and invar: "\i. enat i < llength TNs \ lgc_invar TNs (enat i)" shows "lgc_invar TNs \" unfolding lgc_invar_def proof (intro subsetI, unfold Liminf_upto_llist_infinity Sup_upto_llist_infinity) fix \ assume \_inff: "\ \ Inf_from (active_subset (Liminf_llist (lmap snd TNs)))" define As where "As = lmap (active_subset \ snd) TNs" have act_ns: "active_subset (Liminf_llist (lmap snd TNs)) = Liminf_llist As" unfolding As_def active_subset_def Liminf_set_filter_commute[symmetric] llist.map_comp .. note \_inf = Inf_if_Inf_from[OF \_inff] note \_inff' = \_inff[unfolded act_ns] show "\ \ \ (from_F ` Liminf_llist (lmap fst TNs)) \ Sup_llist (lmap (Red_I_\ \ snd) TNs)" proof - { assume \_ni_lim: "\ \ \ (from_F ` Liminf_llist (lmap fst TNs))" have "\ lnull As" unfolding As_def using nnil by auto moreover have "set (prems_of \) \ Liminf_llist As" using \_inff'[unfolded Inf_from_def] by simp ultimately obtain i where i_lt_as: "enat i < llength As" and prems_sub_ge_i: "set (prems_of \) \ (\j \ {j. i \ j \ enat j < llength As}. lnth As j)" using finite_subset_Liminf_llist_imp_exists_index by blast have ts_nnil: "\ lnull (lmap fst TNs)" using As_def nnil by simp have F\_ni_lim: "to_F \ \ Liminf_llist (lmap fst TNs)" using \_inf \_ni_lim unfolding from_F_def by auto obtain i' where i_le_i': "i \ i'" and i'_lt_as: "enat i' < llength As" and F\_ni_i': "to_F \ \ lnth (lmap fst TNs) i'" using i_lt_as not_Liminf_llist_imp_exists_index[OF ts_nnil F\_ni_lim, of i] unfolding As_def by auto have \_ni_i': "\ \ \ (from_F ` fst (lnth TNs i'))" using F\_ni_i' i'_lt_as[unfolded As_def] unfolding from_F_def by auto have "set (prems_of \) \ (\j \ {j. i' \ j \ enat j < llength As}. lnth As j)" using prems_sub_ge_i i_le_i' by auto then have "set (prems_of \) \ lnth As i'" using i'_lt_as by auto then have "\ \ Inf_from (active_subset (snd (lnth TNs i')))" using i'_lt_as \_inf unfolding Inf_from_def As_def by auto then have \_in_i': "\ \ Sup_upto_llist (lmap (Red_I_\ \ snd) TNs) (enat i')" using \_ni_i' i'_lt_as[unfolded As_def] invar[unfolded lgc_invar_def] by auto then have "\ \ Sup_llist (lmap (Red_I_\ \ snd) TNs)" using Sup_upto_llist_subset_Sup_llist by fastforce } then show ?thesis by blast qed qed lemma lgc_invar_lgc_init: assumes nnil: "\ lnull TNs" and n_init: "active_subset (snd (lhd TNs)) = {}" and t_init: "\\ \ Inf_F. prems_of \ = [] \ \ \ fst (lhd TNs)" shows "lgc_invar TNs 0" unfolding lgc_invar_def proof - have "Inf_from (active_subset (Liminf_upto_llist (lmap snd TNs) 0)) = Inf_from {}" (is "?lhs = _") using nnil n_init by auto also have "... \ \ (from_F ` fst (lhd TNs))" using t_init Inf_FL_to_Inf_F unfolding Inf_from_def from_F_def to_F_def by force also have "... \ \ (from_F ` fst (lhd TNs)) \ Red_I_\ (snd (lhd TNs))" by fast also have "... = \ (from_F ` Liminf_upto_llist (lmap fst TNs) 0) \ Sup_upto_llist (lmap (Red_I_\ \ snd) TNs) 0" (is "_ = ?rhs") using nnil by auto finally show "?lhs \ ?rhs" . qed lemma lgc_invar_lgc_step: assumes Si_lt: "enat (Suc i) < llength TNs" and invar: "lgc_invar TNs i" and step: "lnth TNs i \LGC lnth TNs (Suc i)" shows "lgc_invar TNs (Suc i)" using step Si_lt invar proof cases let ?Sup_Red_i = "Sup_upto_llist (lmap (Red_I_\ \ snd) TNs) (enat i)" let ?Sup_Red_Si = "Sup_upto_llist (lmap (Red_I_\ \ snd) TNs) (enat (Suc i))" have i_lt: "enat i < llength TNs" using Si_lt Suc_ile_eq order.strict_implies_order by blast have lim_i: "Liminf_upto_llist (lmap fst TNs) (enat i) = lnth (lmap fst TNs) i" "Liminf_upto_llist (lmap snd TNs) (enat i) = lnth (lmap snd TNs) i" using i_lt by auto have lim_Si: "Liminf_upto_llist (lmap fst TNs) (enat (Suc i)) = lnth (lmap fst TNs) (Suc i)" "Liminf_upto_llist (lmap snd TNs) (enat (Suc i)) = lnth (lmap snd TNs) (Suc i)" using Si_lt by auto { case (process N1 N M N2 M' T) note tni = this(1) and tnSi = this(2) and n1 = this(3) and n2 = this(4) and m_red = this(5) and m'_pas = this(6) have ni: "lnth (lmap snd TNs) i = N \ M" by (simp add: i_lt n1 tni) have nSi: "lnth (lmap snd TNs) (Suc i) = N \ M'" by (simp add: Si_lt n2 tnSi) have ti: "lnth (lmap fst TNs) i = T" by (simp add: i_lt tni) have tSi: "lnth (lmap fst TNs) (Suc i) = T" by (simp add: Si_lt tnSi) have "Inf_from (active_subset (N \ M')) \ Inf_from (active_subset (N \ M))" using m'_pas by (metis active_subset_union boolean_algebra_cancel.sup0 Inf_from_mono subset_Un_eq sup_left_idem) also have "\ \ \ (from_F ` T) \ ?Sup_Red_i" using invar unfolding lgc_invar_def lim_i ni ti . also have "\ \ \ (from_F ` T) \ ?Sup_Red_Si" using Sup_upto_llist_mono by auto finally show ?thesis unfolding lgc_invar_def lim_Si nSi tSi . next case (schedule_infer T2 T1 T' N1 N C L N2) note tni = this(1) and tnSi = this(2) and t2 = this(3) and n1 = this(4) and n2 = this(5) and l_pas = this(6) and t' = this(7) have ni: "lnth (lmap snd TNs) i = N \ {(C, L)}" by (simp add: i_lt n1 tni) have nSi: "lnth (lmap snd TNs) (Suc i) = N \ {(C, active)}" by (simp add: Si_lt n2 tnSi) have ti: "lnth (lmap fst TNs) i = T1" by (simp add: i_lt tni) have tSi: "lnth (lmap fst TNs) (Suc i) = T1 \ T'" by (simp add: Si_lt t2 tnSi) { fix \ assume \_inff: "\ \ Inf_from (active_subset (N \ {(C, active)}))" have \_inf: "\ \ Inf_FL" using \_inff unfolding Inf_from_def by auto then have F\_inf: "to_F \ \ Inf_F" using Inf_FL_to_Inf_F[folded to_F_def] by fastforce have "\ \ \ (from_F ` (T1 \ T')) \ ?Sup_Red_Si" - proof (cases "to_F \ \ no_labels.Inf_from2 (fst ` active_subset N) {C}") + proof (cases "to_F \ \ no_labels.Inf_between (fst ` active_subset N) {C}") case True then have "\ \ \ (from_F ` (T1 \ T'))" unfolding t' from_F_def using \_inf by auto then show ?thesis by blast next case False moreover have "to_F \ \ no_labels.Inf_from (fst ` (active_subset N \ {(C, active)}))" using \_inff F\_inf unfolding to_F_def Inf_from_def no_labels.Inf_from_def by auto ultimately have "to_F \ \ no_labels.Inf_from (fst ` active_subset N)" - unfolding no_labels.Inf_from_def no_labels.Inf_from2_def by auto + unfolding no_labels.Inf_from_def no_labels.Inf_between_def by auto then have "\ \ Inf_from (active_subset N)" using \_inf unfolding to_F_def no_labels.Inf_from_def by clarsimp (smt Inf_from_def Un_insert_right \_inff active_subset_def boolean_algebra_cancel.sup0 imageE image_subset_iff insert_iff mem_Collect_eq prod.collapse snd_conv subset_iff) then have "\ \ \ (from_F ` (T1 \ T')) \ ?Sup_Red_i" using invar[unfolded lgc_invar_def] l_pas unfolding lim_i ni ti by auto then show ?thesis using Sup_upto_llist_mono by force qed } then show ?thesis unfolding lgc_invar_def lim_i lim_Si nSi tSi by fast next case (compute_infer T1 T2 \' N2 N1 M) note tni = this(1) and tnSi = this(2) and t1 = this(3) and n2 = this(4) and m_pas = this(5) and \'_red = this(6) have ni: "lnth (lmap snd TNs) i = N1" by (simp add: i_lt tni) have nSi: "lnth (lmap snd TNs) (Suc i) = N1 \ M" by (simp add: Si_lt n2 tnSi) have ti: "lnth (lmap fst TNs) i = T2 \ {\'}" by (simp add: i_lt t1 tni) have tSi: "lnth (lmap fst TNs) (Suc i) = T2" by (simp add: Si_lt tnSi) { fix \ assume \_inff: "\ \ Inf_from (active_subset (N1 \ M))" have \_bef: "\ \ \ (from_F ` (T2 \ {\'})) \ ?Sup_Red_i" using \_inff invar[unfolded lgc_invar_def lim_i ti ni] m_pas by auto have "\ \ \ (from_F ` T2) \ ?Sup_Red_Si" proof (cases "\ \ from_F \'") case \_in_\': True then have "\ \ Red_I_\ (N1 \ M)" using \'_red from_F_def labeled_red_inf_eq_red_inf by auto then have "\ \ ?Sup_Red_Si" using Si_lt by (simp add: n2 tnSi) then show ?thesis by auto next case False then show ?thesis using \_bef by auto qed } then show ?thesis unfolding lgc_invar_def lim_Si tSi nSi by blast next case (delete_orphans T1 T2 T' N) note tni = this(1) and tnSi = this(2) and t1 = this(3) and t'_orph = this(4) have ni: "lnth (lmap snd TNs) i = N" by (simp add: i_lt tni) have nSi: "lnth (lmap snd TNs) (Suc i) = N" by (simp add: Si_lt tnSi) have ti: "lnth (lmap fst TNs) i = T2 \ T'" by (simp add: i_lt t1 tni) have tSi: "lnth (lmap fst TNs) (Suc i) = T2" by (simp add: Si_lt tnSi) { fix \ assume \_inff: "\ \ Inf_from (active_subset N)" have "to_F \ \ T'" using t'_orph \_inff in_Inf_from_imp_to_F_in_Inf_from by blast hence "\ \ \ (from_F ` T')" unfolding from_F_def by auto then have "\ \ \ (from_F ` T2) \ ?Sup_Red_Si" using \_inff invar unfolding lgc_invar_def lim_i ni ti by auto } then show ?thesis unfolding lgc_invar_def lim_Si tSi nSi by blast } qed lemma lgc_invar_lgc: assumes lgc: "chain (\LGC) TNs" and n_init: "active_subset (snd (lhd TNs)) = {}" and t_init: "\\ \ Inf_F. prems_of \ = [] \ \ \ fst (lhd TNs)" and i_lt: "i < llength TNs" shows "lgc_invar TNs i" using i_lt proof (induct i) case (enat i) then show ?case proof (induct i) case 0 then show ?case using lgc_invar_lgc_init[OF chain_not_lnull[OF lgc] n_init t_init] by (simp add: enat_0) next case (Suc i) note ih = this(1) and Si_lt = this(2) have i_lt: "enat i < llength TNs" using Si_lt Suc_ile_eq less_le by blast show ?case by (rule lgc_invar_lgc_step[OF Si_lt ih[OF i_lt] chain_lnth_rel[OF lgc Si_lt]]) qed qed simp lemma lgc_fair_new_proof: assumes lgc: "chain (\LGC) TNs" and n_init: "active_subset (snd (lhd TNs)) = {}" and n_lim: "passive_subset (Liminf_llist (lmap snd TNs)) = {}" and t_init: "\\ \ Inf_F. prems_of \ = [] \ \ \ fst (lhd TNs)" and t_lim: "Liminf_llist (lmap fst TNs) = {}" shows "fair (lmap snd TNs)" unfolding fair_def llist.map_comp proof - have "Inf_from (Liminf_llist (lmap snd TNs)) \ Inf_from (active_subset (Liminf_llist (lmap snd TNs)))" (is "?lhs \ _") by (rule Inf_from_mono) (use n_lim passive_subset_def active_subset_def in blast) also have "... \ \ (from_F ` Liminf_upto_llist (lmap fst TNs) \) \ Sup_llist (lmap (Red_I_\ \ snd) TNs)" using lgc_invar_infinity[OF chain_not_lnull[OF lgc]] lgc_invar_lgc[OF lgc n_init t_init] unfolding lgc_invar_def by fastforce also have "... \ Sup_llist (lmap (Red_I_\ \ snd) TNs)" (is "_ \ ?rhs") using t_lim by auto finally show "?lhs \ ?rhs" . qed end end