diff --git a/thys/Saturation_Framework/Calculus_Variations.thy b/thys/Saturation_Framework/Calculus_Variations.thy new file mode 100644 --- /dev/null +++ b/thys/Saturation_Framework/Calculus_Variations.thy @@ -0,0 +1,435 @@ +(* Title: Variations on a Theme + * Author: Sophie Tourret , 2018-2020 *) + +section \Variations on a Theme\ + +text \In this section, section 2.4 of the report is covered, demonstrating + that various notions of redundancy are equivalent.\ + +theory Calculus_Variations + imports Calculus +begin + +locale reduced_calculus = calculus Bot Inf entails Red_Inf Red_F + for + Bot :: "'f set" and + Inf :: \'f inference set\ and + entails :: "'f set \ 'f set \ bool" (infix "\" 50) and + Red_Inf :: "'f set \ 'f inference set" and + Red_F :: "'f set \ 'f set" + + assumes + inf_in_red_inf: "Inf_from2 UNIV (Red_F N) \ Red_Inf N" +begin + +(* lem:reduced-rc-implies-sat-equiv-reduced-sat *) +lemma sat_eq_reduc_sat: "saturated N \ reduc_saturated N" +proof + fix N + assume "saturated N" + then show "reduc_saturated N" + using Red_Inf_without_red_F saturated_without_red_F + unfolding saturated_def reduc_saturated_def + by blast +next + fix N + assume red_sat_n: "reduc_saturated N" + show "saturated N" unfolding saturated_def + using red_sat_n inf_in_red_inf unfolding reduc_saturated_def Inf_from_def Inf_from2_def + by blast +qed + +end + +locale reducedly_statically_complete_calculus = calculus + + assumes reducedly_statically_complete: + "B \ Bot \ reduc_saturated N \ N \ {B} \ \B'\Bot. B' \ N" + +locale reducedly_statically_complete_reduced_calculus = reduced_calculus + + assumes reducedly_statically_complete: + "B \ Bot \ reduc_saturated N \ N \ {B} \ \B'\Bot. B' \ N" +begin + +sublocale reducedly_statically_complete_calculus + by (simp add: calculus_axioms reducedly_statically_complete + reducedly_statically_complete_calculus_axioms.intro + reducedly_statically_complete_calculus_def) + +(* cor:reduced-rc-implies-st-ref-comp-equiv-reduced-st-ref-comp 1/2 *) +sublocale statically_complete_calculus +proof + fix B N + assume + bot_elem: \B \ Bot\ and + saturated_N: "saturated N" and + refut_N: "N \ {B}" + have reduc_saturated_N: "reduc_saturated N" using saturated_N sat_eq_reduc_sat by blast + show "\B'\Bot. B' \ N" using reducedly_statically_complete[OF bot_elem reduc_saturated_N refut_N] . +qed + +end + +context reduced_calculus +begin + +(* cor:reduced-rc-implies-st-ref-comp-equiv-reduced-st-ref-comp 2/2 *) +lemma stat_ref_comp_imp_red_stat_ref_comp: + "statically_complete_calculus Bot Inf entails Red_Inf Red_F \ + reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F" +proof + fix B N + assume + stat_ref_comp: "statically_complete_calculus Bot Inf (\) Red_Inf Red_F" and + bot_elem: \B \ Bot\ and + saturated_N: "reduc_saturated N" and + refut_N: "N \ {B}" + have reduc_saturated_N: "saturated N" using saturated_N sat_eq_reduc_sat by blast + show "\B'\Bot. B' \ N" + using statically_complete_calculus.statically_complete[OF stat_ref_comp + bot_elem reduc_saturated_N refut_N] . +qed + +end + +context calculus +begin + +definition Red_Red_Inf :: "'f set \ 'f inference set" where + "Red_Red_Inf N = Red_Inf N \ Inf_from2 UNIV (Red_F N)" + +lemma reduced_calc_is_calc: "calculus Bot Inf entails Red_Red_Inf Red_F" +proof + fix N + show "Red_Red_Inf N \ Inf" + unfolding Red_Red_Inf_def Inf_from2_def Inf_from_def using Red_Inf_to_Inf by auto +next + fix B N + assume + b_in: "B \ Bot" and + n_entails: "N \ {B}" + show "N - Red_F N \ {B}" + by (simp add: Red_F_Bot b_in n_entails) +next + fix N N' :: "'f set" + assume "N \ N'" + then show "Red_F N \ Red_F N'" by (simp add: Red_F_of_subset) +next + fix N N' :: "'f set" + assume n_in: "N \ N'" + then have "Inf_from (UNIV - (Red_F N')) \ Inf_from (UNIV - (Red_F N))" + using Red_F_of_subset[OF n_in] unfolding Inf_from_def by auto + then have "Inf_from2 UNIV (Red_F N) \ Inf_from2 UNIV (Red_F N')" + unfolding Inf_from2_def by auto + then show "Red_Red_Inf N \ Red_Red_Inf N'" + unfolding Red_Red_Inf_def using Red_Inf_of_subset[OF n_in] by blast +next + fix N N' :: "'f set" + assume "N' \ Red_F N" + then show "Red_F N \ Red_F (N - N')" by (simp add: Red_F_of_Red_F_subset) +next + fix N N' :: "'f set" + assume np_subs: "N' \ Red_F N" + have "Red_F N \ Red_F (N - N')" by (simp add: Red_F_of_Red_F_subset np_subs) + then have "Inf_from (UNIV - (Red_F (N - N'))) \ Inf_from (UNIV - (Red_F N))" + by (metis Diff_subset Red_F_of_subset eq_iff) + then have "Inf_from2 UNIV (Red_F N) \ Inf_from2 UNIV (Red_F (N - N'))" + unfolding Inf_from2_def by auto + then show "Red_Red_Inf N \ Red_Red_Inf (N - N')" + unfolding Red_Red_Inf_def using Red_Inf_of_Red_F_subset[OF np_subs] by blast +next + fix \ N + assume "\ \ Inf" + "concl_of \ \ N" + then show "\ \ Red_Red_Inf N" + by (simp add: Red_Inf_of_Inf_to_N Red_Red_Inf_def) +qed + +lemma inf_subs_reduced_red_inf: "Inf_from2 UNIV (Red_F N) \ Red_Red_Inf N" + unfolding Red_Red_Inf_def by simp + +(* lem:red'-is-reduced-redcrit *) +text \The following is a lemma and not a sublocale as was previously used in similar cases. + Here, a sublocale cannot be used because it would create an infinitely descending + chain of sublocales. \ +lemma reduc_calc: "reduced_calculus Bot Inf entails Red_Red_Inf Red_F" + using inf_subs_reduced_red_inf reduced_calc_is_calc + by (simp add: reduced_calculus.intro reduced_calculus_axioms_def) + +interpretation reduc_calc: reduced_calculus Bot Inf entails Red_Red_Inf Red_F + by (fact reduc_calc) + +(* lem:saturation-red-vs-red'-1 *) +lemma sat_imp_red_calc_sat: "saturated N \ reduc_calc.saturated N" + unfolding saturated_def reduc_calc.saturated_def Red_Red_Inf_def by blast + +(* lem:saturation-red-vs-red'-2 1/2 (i) \ (ii) *) +lemma red_sat_eq_red_calc_sat: "reduc_saturated N \ reduc_calc.saturated N" +proof + assume red_sat_n: "reduc_saturated N" + show "reduc_calc.saturated N" + unfolding reduc_calc.saturated_def + proof + fix \ + assume i_in: "\ \ Inf_from N" + show "\ \ Red_Red_Inf N" + using i_in red_sat_n + unfolding reduc_saturated_def Inf_from2_def Inf_from_def Red_Red_Inf_def by blast + qed +next + assume red_sat_n: "reduc_calc.saturated N" + show "reduc_saturated N" + unfolding reduc_saturated_def + proof + fix \ + assume i_in: "\ \ Inf_from (N - Red_F N)" + show "\ \ Red_Inf N" + using i_in red_sat_n + unfolding Inf_from_def reduc_calc.saturated_def Red_Red_Inf_def Inf_from2_def by blast + qed +qed + +(* lem:saturation-red-vs-red'-2 2/2 (i) \ (iii) *) +lemma red_sat_eq_sat: "reduc_saturated N \ saturated (N - Red_F N)" + unfolding reduc_saturated_def saturated_def by (simp add: Red_Inf_without_red_F) + +(* thm:reduced-stat-ref-compl 1/3 (i) \ (iii) *) +theorem stat_is_stat_red: "statically_complete_calculus Bot Inf entails Red_Inf Red_F \ + statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" +proof + assume + stat_ref1: "statically_complete_calculus Bot Inf entails Red_Inf Red_F" + show "statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + using reduc_calc.calculus_axioms + unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def + proof + show "\B N. B \ Bot \ reduc_calc.saturated N \ N \ {B} \ (\B'\Bot. B' \ N)" + proof (clarify) + fix B N + assume + b_in: "B \ Bot" and + n_sat: "reduc_calc.saturated N" and + n_imp_b: "N \ {B}" + have "saturated (N - Red_F N)" using red_sat_eq_red_calc_sat[of N] red_sat_eq_sat[of N] n_sat by blast + moreover have "(N - Red_F N) \ {B}" using n_imp_b b_in by (simp add: reduc_calc.Red_F_Bot) + ultimately show "\B'\Bot. B'\ N" + using stat_ref1 by (meson DiffD1 b_in statically_complete_calculus.statically_complete) + qed + qed +next + assume + stat_ref3: "statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + show "statically_complete_calculus Bot Inf entails Red_Inf Red_F" + unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def + using calculus_axioms + proof + show "\B N. B \ Bot \ saturated N \ N \ {B} \ (\B'\Bot. B' \ N)" + proof clarify + fix B N + assume + b_in: "B \ Bot" and + n_sat: "saturated N" and + n_imp_b: "N \ {B}" + then show "\B'\ Bot. B' \ N" + using stat_ref3 sat_imp_red_calc_sat[OF n_sat] + by (meson statically_complete_calculus.statically_complete) + qed + qed +qed + +(* thm:reduced-stat-ref-compl 2/3 (iv) \ (iii) *) +theorem red_stat_red_is_stat_red: + "reducedly_statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F \ + statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + using reduc_calc.stat_ref_comp_imp_red_stat_ref_comp + by (metis reduc_calc.sat_eq_reduc_sat reducedly_statically_complete_calculus.axioms(2) + reducedly_statically_complete_calculus_axioms_def reduced_calc_is_calc + statically_complete_calculus.intro statically_complete_calculus_axioms.intro) + +(* thm:reduced-stat-ref-compl 3/3 (ii) \ (iii) *) +theorem red_stat_is_stat_red: + "reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F \ + statically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + using reduc_calc.calculus_axioms calculus_axioms red_sat_eq_red_calc_sat + unfolding statically_complete_calculus_def statically_complete_calculus_axioms_def + reducedly_statically_complete_calculus_def reducedly_statically_complete_calculus_axioms_def + by blast + +lemma sup_red_f_in_red_liminf: + "chain derive D \ Sup_llist (lmap Red_F D) \ Red_F (Liminf_llist D)" +proof + fix N + assume + deriv: "chain derive D" and + n_in_sup: "N \ Sup_llist (lmap Red_F D)" + obtain i0 where i_smaller: "enat i0 < llength D" and n_in: "N \ Red_F (lnth D i0)" + using n_in_sup by (metis Sup_llist_imp_exists_index llength_lmap lnth_lmap) + have "Red_F (lnth D i0) \ Red_F (Liminf_llist D)" + using i_smaller by (simp add: deriv Red_F_subset_Liminf) + then show "N \ Red_F (Liminf_llist D)" + using n_in by fast +qed + +lemma sup_red_inf_in_red_liminf: + "chain derive D \ Sup_llist (lmap Red_Inf D) \ Red_Inf (Liminf_llist D)" +proof + fix \ + assume + deriv: "chain derive D" and + i_in_sup: "\ \ Sup_llist (lmap Red_Inf D)" + obtain i0 where i_smaller: "enat i0 < llength D" and n_in: "\ \ Red_Inf (lnth D i0)" + using i_in_sup unfolding Sup_llist_def by auto + have "Red_Inf (lnth D i0) \ Red_Inf (Liminf_llist D)" + using i_smaller by (simp add: deriv Red_Inf_subset_Liminf) + then show "\ \ Red_Inf (Liminf_llist D)" + using n_in by fast +qed + +definition reduc_fair :: "'f set llist \ bool" where + "reduc_fair D \ + Inf_from (Liminf_llist D - Sup_llist (lmap Red_F D)) \ Sup_llist (lmap Red_Inf D)" + +(* lem:red-fairness-implies-red-saturation *) +lemma reduc_fair_imp_Liminf_reduc_sat: + "chain derive D \ reduc_fair D \ reduc_saturated (Liminf_llist D)" + unfolding reduc_saturated_def +proof - + fix D + assume + deriv: "chain derive D" and + red_fair: "reduc_fair D" + have "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) + \ Inf_from (Liminf_llist D - Sup_llist (lmap Red_F D))" + using sup_red_f_in_red_liminf[OF deriv] unfolding Inf_from_def by blast + then have "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) \ Sup_llist (lmap Red_Inf D)" + using red_fair unfolding reduc_fair_def by simp + then show "Inf_from (Liminf_llist D - Red_F (Liminf_llist D)) \ Red_Inf (Liminf_llist D)" + using sup_red_inf_in_red_liminf[OF deriv] by fast +qed + +end + +locale reducedly_dynamically_complete_calculus = calculus + + assumes + reducedly_dynamically__complete: "B \ Bot \ chain derive D \ reduc_fair D \ + lhd D \ {B} \ \i \ {i. enat i < llength D}. \ B'\Bot. B' \ lnth D i" +begin + +sublocale reducedly_statically_complete_calculus +proof + fix B N + assume + bot_elem: \B \ Bot\ and + saturated_N: "reduc_saturated N" and + refut_N: "N \ {B}" + define D where "D = LCons N LNil" + have[simp]: \\ lnull D\ by (auto simp: D_def) + have deriv_D: \chain (\Red) D\ by (simp add: chain.chain_singleton D_def) + have liminf_is_N: "Liminf_llist D = N" by (simp add: D_def Liminf_llist_LCons) + have head_D: "N = lhd D" by (simp add: D_def) + have "Sup_llist (lmap Red_F D) = Red_F N" by (simp add: D_def) + moreover have "Sup_llist (lmap Red_Inf D) = Red_Inf N" by (simp add: D_def) + ultimately have fair_D: "reduc_fair D" + using saturated_N liminf_is_N unfolding reduc_fair_def reduc_saturated_def + by (simp add: reduc_fair_def reduc_saturated_def liminf_is_N) + obtain i B' where B'_is_bot: \B' \ Bot\ and B'_in: "B' \ lnth D i" and \i < llength D\ + using reducedly_dynamically__complete[of B D] bot_elem fair_D head_D saturated_N deriv_D refut_N + by auto + then have "i = 0" + by (auto simp: D_def enat_0_iff) + show \\B'\Bot. B' \ N\ + using B'_is_bot B'_in unfolding \i = 0\ head_D[symmetric] D_def by auto +qed + +end + +sublocale reducedly_statically_complete_calculus \ reducedly_dynamically_complete_calculus +proof + fix B D + assume + bot_elem: \B \ Bot\ and + deriv: \chain (\Red) D\ and + fair: \reduc_fair D\ and + unsat: \lhd D \ {B}\ + have non_empty: \\ lnull D\ using chain_not_lnull[OF deriv] . + have subs: \lhd D \ Sup_llist D\ + using lhd_subset_Sup_llist[of D] non_empty by (simp add: lhd_conv_lnth) + have \Sup_llist D \ {B}\ + using unsat subset_entailed[OF subs] entails_trans[of "Sup_llist D" "lhd D"] by auto + then have Sup_no_Red: \Sup_llist D - Red_F (Sup_llist D) \ {B}\ + using bot_elem Red_F_Bot by auto + have Sup_no_Red_in_Liminf: \Sup_llist D - Red_F (Sup_llist D) \ Liminf_llist D\ + using deriv Red_in_Sup by auto + have Liminf_entails_Bot: \Liminf_llist D \ {B}\ + using Sup_no_Red subset_entailed[OF Sup_no_Red_in_Liminf] entails_trans by blast + have \reduc_saturated (Liminf_llist D)\ + using deriv fair reduc_fair_imp_Liminf_reduc_sat unfolding reduc_saturated_def + by auto + then have \\B'\Bot. B' \ Liminf_llist D\ + using bot_elem reducedly_statically_complete Liminf_entails_Bot + by auto + then show \\i\{i. enat i < llength D}. \B'\Bot. B' \ lnth D i\ + unfolding Liminf_llist_def by auto +qed + +context calculus +begin + +lemma dyn_equiv_stat: "dynamically_complete_calculus Bot Inf entails Red_Inf Red_F = + statically_complete_calculus Bot Inf entails Red_Inf Red_F" +proof + assume "dynamically_complete_calculus Bot Inf entails Red_Inf Red_F" + then interpret dynamically_complete_calculus Bot Inf entails Red_Inf Red_F + by simp + show "statically_complete_calculus Bot Inf entails Red_Inf Red_F" + by (simp add: statically_complete_calculus_axioms) +next + assume "statically_complete_calculus Bot Inf entails Red_Inf Red_F" + then interpret statically_complete_calculus Bot Inf entails Red_Inf Red_F + by simp + show "dynamically_complete_calculus Bot Inf entails Red_Inf Red_F" + by (simp add: dynamically_complete_calculus_axioms) +qed + +lemma red_dyn_equiv_red_stat: + "reducedly_dynamically_complete_calculus Bot Inf entails Red_Inf Red_F = + reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F" +proof + assume "reducedly_dynamically_complete_calculus Bot Inf entails Red_Inf Red_F" + then interpret reducedly_dynamically_complete_calculus Bot Inf entails Red_Inf Red_F + by simp + show "reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F" + by (simp add: reducedly_statically_complete_calculus_axioms) +next + assume "reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F" + then interpret reducedly_statically_complete_calculus Bot Inf entails Red_Inf Red_F + by simp + show "reducedly_dynamically_complete_calculus Bot Inf entails Red_Inf Red_F" + by (simp add: reducedly_dynamically_complete_calculus_axioms) +qed + +interpretation reduc_calc: reduced_calculus Bot Inf entails Red_Red_Inf Red_F + by (fact reduc_calc) + +(* thm:reduced-dyn-ref-compl 1/3 (v) \ (vii) *) +theorem dyn_ref_eq_dyn_ref_red: + "dynamically_complete_calculus Bot Inf entails Red_Inf Red_F \ + dynamically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + using dyn_equiv_stat stat_is_stat_red reduc_calc.dyn_equiv_stat by meson + +(* thm:reduced-dyn-ref-compl 2/3 (viii) \ (vii) *) +theorem red_dyn_ref_red_eq_dyn_ref_red: + "reducedly_dynamically_complete_calculus Bot Inf entails Red_Red_Inf Red_F \ + dynamically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + using red_dyn_equiv_red_stat dyn_equiv_stat red_stat_red_is_stat_red + by (simp add: reduc_calc.dyn_equiv_stat reduc_calc.red_dyn_equiv_red_stat) + +(* thm:reduced-dyn-ref-compl 3/3 (vi) \ (vii) *) +theorem red_dyn_ref_eq_dyn_ref_red: + "reducedly_dynamically_complete_calculus Bot Inf entails Red_Inf Red_F \ + dynamically_complete_calculus Bot Inf entails Red_Red_Inf Red_F" + 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