# HG changeset patch # User paulson # Date 1742144561 0 # Node ID 3fb2525699e64263acbbd12962092617567f15d2 # Parent 26fbbf43863b64ad2f47344b3b96499cd95d37a8# Parent 5d91cca0aaf36806c612e9e36442d9bf7c4b306a merged diff -r 26fbbf43863b -r 3fb2525699e6 src/HOL/Decision_Procs/Algebra_Aux.thy --- a/src/HOL/Decision_Procs/Algebra_Aux.thy Sun Mar 16 14:21:00 2025 +0100 +++ b/src/HOL/Decision_Procs/Algebra_Aux.thy Sun Mar 16 17:02:41 2025 +0000 @@ -259,10 +259,12 @@ by (simp add: cring_class_ops_def) lemma uminus_class: "\\<^bsub>cring_class_ops\<^esub> x = - x" - apply (simp add: a_inv_def m_inv_def cring_class_ops_def) - apply (rule the_equality) - apply (simp_all add: eq_neg_iff_add_eq_0) - done +proof - + have "(THE y::'a. x + y = 0 \ y + x = 0) = - x" + by (rule the_equality) (simp_all add: eq_neg_iff_add_eq_0) + then show ?thesis + by (simp add: a_inv_def m_inv_def cring_class_ops_def) +qed lemma minus_class: "x \\<^bsub>cring_class_ops\<^esub> y = x - y" by (simp add: a_minus_def carrier_class plus_class uminus_class) @@ -482,20 +484,11 @@ lemma field_class: "field (cring_class_ops::'a::field ring)" apply unfold_locales apply (simp_all add: cring_class_ops_def) - apply (auto simp add: Units_def) - apply (rule_tac x="1 / x" in exI) - apply simp - done + using field_class.field_inverse by (force simp add: Units_def) lemma div_class: "(x::'a::field) \\<^bsub>cring_class_ops\<^esub> y = x / y" - apply (simp add: m_div_def m_inv_def class_simps) - apply (rule impI) - apply (rule ssubst [OF the_equality, of _ "1 / y"]) - apply simp_all - apply (drule conjunct2) - apply (drule_tac f="\x. x / y" in arg_cong) - apply simp - done + by (simp add: carrier_class class_simps cring_class.comm_inv_char + field_class.field_divide_inverse m_div_def) interpretation field_class: field "cring_class_ops::'a::field ring" rewrites "(\\<^bsub>cring_class_ops\<^esub>::'a) = 0" diff -r 26fbbf43863b -r 3fb2525699e6 src/HOL/Decision_Procs/Approximation_Bounds.thy --- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Sun Mar 16 14:21:00 2025 +0100 +++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Sun Mar 16 17:02:41 2025 +0000 @@ -2648,10 +2648,7 @@ thus ?thesis unfolding bl_def[symmetric] using \0 < real_of_int m\ \0 \ bl\ apply (simp add: ln_mult) - apply (cases "e=0") - apply (cases "bl = 0", simp_all add: powr_minus ln_inverse ln_powr) - apply (cases "bl = 0", simp_all add: powr_minus ln_inverse ln_powr field_simps) - done + by argo next case False hence "0 < -e" by auto @@ -2788,21 +2785,23 @@ using abs_real_le_2_powr_bitlen [of m] \m > 0\ by (simp_all add: bitlen powr_realpow [symmetric] powr_minus powr_add field_simps) { - have "float_round_down prec (lb_ln2 prec * ?s) \ ln 2 * (e + (bitlen m - 1))" - (is "real_of_float ?lb2 \ _") - apply (rule float_round_down_le) - unfolding nat_0 power_0 mult_1_right times_float.rep_eq - using lb_ln2[of prec] + have "real_of_float (lb_ln2 prec) * + real_of_float (Float (e + (bitlen m - 1)) 0) + \ ln 2 * real_of_int (e + (bitlen m - 1))" proof (rule mult_mono) from float_gt1_scale[OF \1 \ Float m e\] show "0 \ real_of_float (Float (e + (bitlen m - 1)) 0)" by simp - qed auto - moreover + qed (use lb_ln2[of prec] in auto) + then have "float_round_down prec (lb_ln2 prec * ?s) \ ln 2 * (e + (bitlen m - 1))" + (is "real_of_float ?lb2 \ _") + by (simp add: Interval_Float.float_round_down_le) + moreover from ln_float_bounds(1)[OF x_bnds] have "float_round_down prec ((?x - 1) * lb_ln_horner prec (get_even prec) 1 (?x - 1)) \ ln ?x" (is "real_of_float ?lb_horner \ _") by (auto intro!: float_round_down_le) ultimately have "float_plus_down prec ?lb2 ?lb_horner \ ln x" - unfolding Float ln_shifted_float[OF \0 < m\, of e] by (auto intro!: float_plus_down_le) + unfolding Float ln_shifted_float[OF \0 < m\, of e] + by (auto intro!: float_plus_down_le) } moreover { diff -r 26fbbf43863b -r 3fb2525699e6 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Sun Mar 16 14:21:00 2025 +0100 +++ b/src/HOL/Decision_Procs/Cooper.thy Sun Mar 16 17:02:41 2025 +0000 @@ -713,11 +713,7 @@ case 2 with one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"] show ?thesis - apply (cases "i = 0") - apply (simp_all add: Let_def) - apply (cases "i > 0") - apply simp_all - done + by (cases i rule: linorder_cases) (auto simp: Let_def) next case i: 3 consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast @@ -748,11 +744,7 @@ case 2 with one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"] show ?thesis - apply (cases "i = 0") - apply (simp_all add: Let_def) - apply (cases "i > 0") - apply simp_all - done + by (cases i rule: linorder_cases) (auto simp: Let_def) next case i: 3 consider v where "?sa = C v" | "\ (\v. ?sa = C v)" by blast @@ -814,10 +806,8 @@ qed (auto simp add: disj_def imp_def iff_def conj_def not_bn) lemma simpfm_qf: "qfree p \ qfree (simpfm p)" - apply (induct p rule: simpfm.induct) - apply (auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def) - apply (case_tac "simpnum a", auto)+ - done +proof (induct p rule: simpfm.induct) +qed (auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def split: Cooper.num.splits) subsection \Generic quantifier elimination\ @@ -1076,11 +1066,7 @@ by auto let ?N = "\t. Inum (i # bs) t" from 5 Ia nb show ?case - apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r") - apply auto - subgoal for nat a b by (cases nat) auto - done + by (cases "?r") (auto split: prod.splits dest: less_imp_Suc_add) next case (6 a) let ?c = "fst (zsplit0 a)" @@ -1092,11 +1078,7 @@ by auto let ?N = "\t. Inum (i # bs) t" from 6 Ia nb show ?case - apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r") - apply auto - subgoal for nat a b by (cases nat) auto - done + by (cases "?r") (auto simp: Let_def split_def algebra_simps dest: less_imp_Suc_add) next case (7 a) let ?c = "fst (zsplit0 a)" @@ -1108,11 +1090,7 @@ by auto let ?N = "\t. Inum (i # bs) t" from 7 Ia nb show ?case - apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r") - apply auto - subgoal for nat a b by (cases nat) auto - done + by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add) next case (8 a) let ?c = "fst (zsplit0 a)" @@ -1124,11 +1102,7 @@ by auto let ?N = "\t. Inum (i # bs) t" from 8 Ia nb show ?case - apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r") - apply auto - subgoal for nat a b by (cases nat) auto - done + by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add) next case (9 a) let ?c = "fst (zsplit0 a)" @@ -1140,11 +1114,7 @@ by auto let ?N = "\t. Inum (i # bs) t" from 9 Ia nb show ?case - apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r") - apply auto - subgoal for nat a b by (cases nat) auto - done + by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add) next case (10 a) let ?c = "fst (zsplit0 a)" @@ -1156,11 +1126,7 @@ by auto let ?N = "\t. Inum (i # bs) t" from 10 Ia nb show ?case - apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r") - apply auto - subgoal for nat a b by (cases nat) auto - done + by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add) next case (11 j a) let ?c = "fst (zsplit0 a)" @@ -1183,11 +1149,7 @@ next case 2 with zsplit0_I[OF spl, where x="i" and bs="bs"] show ?thesis - apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r") - apply auto - subgoal for nat a b by (cases nat) auto - done + by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add) next case 3 then have l: "?L (?l (Dvd j a))" @@ -1223,11 +1185,7 @@ next case 2 with zsplit0_I[OF spl, where x="i" and bs="bs"] show ?thesis - apply (auto simp add: Let_def split_def algebra_simps) - apply (cases "?r") - apply auto - subgoal for nat a b by (cases nat) auto - done + by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add) next case 3 then have l: "?L (?l (Dvd j a))" @@ -1403,15 +1361,11 @@ proof (induct p rule: minusinf.induct) case (1 p q) then show ?case - apply auto - subgoal for z z' by (rule exI [where x = "min z z'"]) simp - done + by (fastforce simp: intro: exI [where x = "min _ _"]) next case (2 p q) then show ?case - apply auto - subgoal for z z' by (rule exI [where x = "min z z'"]) simp - done + by (fastforce simp: intro: exI [where x = "min _ _"]) next case (3 c e) then have c1: "c = 1" and nb: "numbound0 e" @@ -2002,12 +1956,12 @@ have vb: "?v \ set (\ (Eq (CN 0 c e)))" by simp from p have "x= - ?e" - by (simp add: c1) with 3(5) - show ?case - using dp apply simp - apply (erule ballE[where x="1"]) - apply (simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"]) - done + by (simp add: c1) + moreover have "x \ - 1 - Inum (a # bs) e + 1" + using dp 3 by force + ultimately have False + using bn decrnum by fastforce + then show ?case .. next case (4 c e) then @@ -2085,6 +2039,7 @@ show "?P (x - d)" by (rule \[OF lp u d dp nb2 px]) qed +(*a duplicate in MIR.thy*) lemma cpmi_eq: fixes P P1 :: "int \ bool" assumes "0 < D" @@ -2092,24 +2047,22 @@ and "\x. \ (\j \ {1..D}. \b \ B. P (b + j)) \ P x \ P (x - D)" and "\x k. P1 x = P1 (x - k * D)" shows "(\x. P x) \ (\j \ {1..D}. P1 j) \ (\j \ {1..D}. \b \ B. P (b + j))" - apply (insert assms) - apply (rule iffI) - prefer 2 - apply (drule minusinfinity) - apply assumption+ - apply fastforce - apply clarsimp - apply (subgoal_tac "\k. 0 \ k \ \x. P x \ P (x - k * D)") - apply (frule_tac x = x and z=z in decr_lemma) - apply (subgoal_tac "P1 (x - (\x - z\ + 1) * D)") - prefer 2 - apply (subgoal_tac "0 \ \x - z\ + 1") - prefer 2 apply arith - apply fastforce - apply (drule (1) periodic_finite_ex) - apply blast - apply (blast dest: decr_mult_lemma) - done + (is "_ = ?R") +proof + assume L: "\x. P x" + show "(\j\{1..D}. P1 j) \ (\j\{1..D}. \b\B. P (b + j))" + proof clarsimp + assume \
: "\j\{1..D}. \b\B. \ P (b + j)" + then have "\k. 0\k \ \x. P x \ P (x - k*D)" + by (simp add: assms decr_mult_lemma) + with L \
assms show "\j\{1..D}. P1 j" + using periodic_finite_ex [OF \D>0\, of P1] + by (metis abs_1 abs_add_abs abs_ge_zero decr_lemma) + qed +next + assume ?R then show "\x. P x" + using decr_lemma assms by blast +qed theorem cp_thm: assumes lp: "iszlfm p" @@ -2141,22 +2094,7 @@ lemma mirror_ex: assumes "iszlfm p" shows "(\x. Ifm bbs (x#bs) (mirror p)) \ (\x. Ifm bbs (x#bs) p)" - (is "(\x. ?I x ?mp) = (\x. ?I x p)") -proof auto - fix x - assume "?I x ?mp" - then have "?I (- x) p" - using mirror[OF assms] by blast - then show "\x. ?I x p" - by blast -next - fix x - assume "?I x p" - then have "?I (- x) ?mp" - using mirror[OF assms, where x="- x", symmetric] by auto - then show "\x. ?I x ?mp" - by blast -qed + by (metis assms minus_equation_iff mirror) lemma cp_thm': assumes "iszlfm p" diff -r 26fbbf43863b -r 3fb2525699e6 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 16 14:21:00 2025 +0100 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 16 17:02:41 2025 +0000 @@ -29,27 +29,34 @@ (\x. (\y \ (insert l L). y < x) \ (\y \ U. x < y))" by auto -lemma gather_start [no_atp]: "(\x. P x) \ (\x. (\y \ {}. y < x) \ (\y\ {}. x < y) \ P x)" +lemma gather_start [no_atp]: "(\x. P x) \ (\x. (\y \ {}. y < x) \ (\y\ {}. x < y) \ P x)" by simp text\Theorems for \\z. \x. x < z \ (P x \ P\<^sub>-\<^sub>\)\\ -lemma minf_lt[no_atp]: "\z . \x. x < z \ (x < t \ True)" by auto -lemma minf_gt[no_atp]: "\z . \x. x < z \ (t < x \ False)" +lemma minf_lt[no_atp]: "\z. \x. x < z \ (x < t \ True)" + by auto +lemma minf_gt[no_atp]: "\z. \x. x < z \ (t < x \ False)" by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) -lemma minf_le[no_atp]: "\z. \x. x < z \ (x \ t \ True)" by (auto simp add: less_le) +lemma minf_le[no_atp]: "\z. \x. x < z \ (x \ t \ True)" + by (auto simp add: less_le) lemma minf_ge[no_atp]: "\z. \x. x < z \ (t \ x \ False)" by (auto simp add: less_le not_less not_le) -lemma minf_eq[no_atp]: "\z. \x. x < z \ (x = t \ False)" by auto -lemma minf_neq[no_atp]: "\z. \x. x < z \ (x \ t \ True)" by auto -lemma minf_P[no_atp]: "\z. \x. x < z \ (P \ P)" by blast +lemma minf_eq[no_atp]: "\z. \x. x < z \ (x = t \ False)" + by auto +lemma minf_neq[no_atp]: "\z. \x. x < z \ (x \ t \ True)" + by auto +lemma minf_P[no_atp]: "\z. \x. x < z \ (P \ P)" + by blast text\Theorems for \\z. \x. x < z \ (P x \ P\<^sub>+\<^sub>\)\\ -lemma pinf_gt[no_atp]: "\z. \x. z < x \ (t < x \ True)" by auto +lemma pinf_gt[no_atp]: "\z. \x. z < x \ (t < x \ True)" + by auto lemma pinf_lt[no_atp]: "\z. \x. z < x \ (x < t \ False)" by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le) -lemma pinf_ge[no_atp]: "\z. \x. z < x \ (t \ x \ True)" by (auto simp add: less_le) +lemma pinf_ge[no_atp]: "\z. \x. z < x \ (t \ x \ True)" + by (auto simp add: less_le) lemma pinf_le[no_atp]: "\z. \x. z < x \ (x \ t \ False)" by (auto simp add: less_le not_less not_le) lemma pinf_eq[no_atp]: "\z. \x. z < x \ (x = t \ False)" by auto @@ -86,104 +93,22 @@ lemma lin_dense_lt[no_atp]: "t \ U \ \x l u. (\t. l < t \ t < u \ t \ U) \ l < x \ x < u \ x < t \ (\y. l < y \ y < u \ y < t)" -proof clarsimp - fix x l u y - assume tU: "t \ U" - and noU: "\t. l < t \ t < u \ t \ U" - and lx: "l < x" - and xu: "x < u" - and px: "x < t" - and ly: "l < y" - and yu: "y < u" - from tU noU ly yu have tny: "t \ y" by auto - have False if H: "t < y" - proof - - from less_trans[OF lx px] less_trans[OF H yu] have "l < t \ t < u" - by simp - with tU noU show ?thesis - by auto - qed - then have "\ t < y" - by auto - then have "y \ t" - by (simp add: not_less) - then show "y < t" - using tny by (simp add: less_le) -qed + by (metis antisym_conv3 order.strict_trans) lemma lin_dense_gt[no_atp]: "t \ U \ \x l u. (\t. l < t \ t < u \ t \ U) \ l < x \ x < u \ t < x \ (\y. l < y \ y < u \ t < y)" -proof clarsimp - fix x l u y - assume tU: "t \ U" - and noU: "\t. l < t \ t < u \ t \ U" - and lx: "l < x" - and xu: "x < u" - and px: "t < x" - and ly: "l < y" - and yu: "y < u" - from tU noU ly yu have tny: "t \ y" by auto - have False if H: "y < t" - proof - - from less_trans[OF ly H] less_trans[OF px xu] have "l < t \ t < u" - by simp - with tU noU show ?thesis - by auto - qed - then have "\ y < t" - by auto - then have "t \ y" - by (auto simp add: not_less) - then show "t < y" - using tny by (simp add: less_le) -qed + by (metis antisym_conv3 order.strict_trans) lemma lin_dense_le[no_atp]: "t \ U \ \x l u. (\t. l < t \ t < u \ t \ U) \ l < x \ x < u \ x \ t \ (\y. l < y \ y < u \ y \ t)" -proof clarsimp - fix x l u y - assume tU: "t \ U" - and noU: "\t. l < t \ t < u \ t \ U" - and lx: "l < x" - and xu: "x < u" - and px: "x \ t" - and ly: "l < y" - and yu: "y < u" - from tU noU ly yu have tny: "t \ y" by auto - have False if H: "t < y" - proof - - from less_le_trans[OF lx px] less_trans[OF H yu] - have "l < t \ t < u" by simp - with tU noU show ?thesis by auto - qed - then have "\ t < y" by auto - then show "y \ t" by (simp add: not_less) -qed + by (metis local.less_le_trans local.less_trans local.not_less) lemma lin_dense_ge[no_atp]: "t \ U \ \x l u. (\t. l < t \ t < u \ t \ U) \ l < x \ x < u \ t \ x \ (\y. l < y \ y < u \ t \ y)" -proof clarsimp - fix x l u y - assume tU: "t \ U" - and noU: "\t. l < t \ t < u \ t \ U" - and lx: "l < x" - and xu: "x < u" - and px: "t \ x" - and ly: "l < y" - and yu: "y < u" - from tU noU ly yu have tny: "t \ y" by auto - have False if H: "y < t" - proof - - from less_trans[OF ly H] le_less_trans[OF px xu] - have "l < t \ t < u" by simp - with tU noU show ?thesis by auto - qed - then have "\ y < t" by auto - then show "t \ y" by (simp add: not_less) -qed + by (metis local.le_less_trans local.nle_le not_le) lemma lin_dense_eq[no_atp]: "t \ U \ @@ -207,6 +132,7 @@ \x l u. (\t. l < t \ t < u \ t \ U) \ l < x \ x < u \ (P1 x \ P2 x) \ (\y. l < y \ y < u \ (P1 y \ P2 y))" by blast + lemma lin_dense_disj[no_atp]: "\\x l u. (\t. l < t \ t < u \ t \ U) \ l < x \ x < u \ P1 x \ (\y. l < y \ y < u \ P1 y) ; @@ -264,26 +190,7 @@ then have binS: "?b \ S" using xMS by blast have noy: "\y. ?a < y \ y < ?b \ y \ S" - proof clarsimp - fix y - assume ay: "?a < y" and yb: "y < ?b" and yS: "y \ S" - from yS have "y \ ?Mx \ y \ ?xM" - by (auto simp add: linear) - then show False - proof - assume "y \ ?Mx" - then have "y \ ?a" - using Mxne fMx by auto - with ay show ?thesis - by (simp add: not_le[symmetric]) - next - assume "y \ ?xM" - then have "?b \ y" - using xMne fxM by auto - with yb show ?thesis - by (simp add: not_le[symmetric]) - qed - qed + using Mxne fMx fxM local.linear xMne by auto from ainS binS noy ax xb px show ?thesis by blast qed @@ -298,17 +205,8 @@ and lS: "\x\ S. l \ x" and Su: "\x\ S. x \ u" shows "(\s\ S. P s) \ (\a \ S. \b \ S. (\y. a < y \ y < b \ y \ S) \ a < x \ x < b \ P x)" -proof - - from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] - obtain a and b where as: "a \ S" and bs: "b \ S" - and noS: "\y. a < y \ y < b \ y \ S" - and axb: "a \ x \ x \ b \ P x" - by auto - from axb have "x = a \ x = b \ (a < x \ x < b)" - by (auto simp add: le_less) - then show ?thesis - using px as bs noS by blast -qed + using finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su] + by (metis local.neq_le_trans) end @@ -326,17 +224,13 @@ and neU: "U \ {}" and fL: "finite L" and fU: "finite U" - shows "(\x. (\y \ L. y < x) \ (\y \ U. x < y)) \ (\l \ L. \u \ U. l < u)" -proof (simp only: atomize_eq, rule iffI) + shows "(\x. (\y \ L. y < x) \ (\y \ U. x < y)) = (\l \ L. \u \ U. l < u)" +proof assume H: "\x. (\y\L. y < x) \ (\y\U. x < y)" then obtain x where xL: "\y\L. y < x" and xU: "\y\U. x < y" by blast have "l < u" if l: "l \ L" and u: "u \ U" for l u - proof - - have "l < x" using xL l by blast - also have "x < u" using xU u by blast - finally show ?thesis . - qed + using local.dual_order.strict_trans that(1) u xL xU by blast then show "\l\L. \u\U. l < u" by blast next assume H: "\l\L. \u\U. l < u" @@ -361,30 +255,21 @@ lemma dlo_qe_noub[no_atp]: assumes ne: "L \ {}" and fL: "finite L" - shows "(\x. (\y \ L. y < x) \ (\y \ {}. x < y)) \ True" -proof (simp add: atomize_eq) - from gt_ex[of "Max L"] obtain M where M: "Max L < M" - by blast - from ne fL have "\x \ L. x \ Max L" - by simp - with M have "\x\L. x < M" - by (auto intro: le_less_trans) - then show "\x. \y\L. y < x" - by blast -qed + shows "(\x. (\y \ L. y < x) \ (\y \ {}. x < y)) = True" + using fL local.Max_less_iff local.gt_ex by fastforce lemma dlo_qe_nolb[no_atp]: assumes ne: "U \ {}" and fU: "finite U" - shows "(\x. (\y \ {}. y < x) \ (\y \ U. x < y)) \ True" -proof (simp add: atomize_eq) + shows "(\x. (\y \ {}. y < x) \ (\y \ U. x < y)) = True" +proof - from lt_ex[of "Min U"] obtain M where M: "M < Min U" by blast from ne fU have "\x \ U. Min U \ x" by simp with M have "\x\U. M < x" by (auto intro: less_le_trans) - then show "\x. \y\U. x < y" + then show ?thesis by blast qed @@ -396,6 +281,7 @@ lemma axiom[no_atp]: "class.unbounded_dense_linorder (\) (<)" by (rule unbounded_dense_linorder_axioms) + lemma atoms[no_atp]: shows "TERM (less :: 'a \ _)" and "TERM (less_eq :: 'a \ _)" @@ -457,52 +343,19 @@ assumes ex1: "\z1. \x. z1 \ x \ (P1 x \ P1')" and ex2: "\z2. \x. z2 \ x \ (P2 x \ P2')" shows "\z. \x. z \ x \ ((P1 x \ P2 x) \ (P1' \ P2'))" -proof - - from ex1 ex2 obtain z1 and z2 - where z1: "\x. z1 \ x \ (P1 x \ P1')" - and z2: "\x. z2 \ x \ (P2 x \ P2')" - by blast - from gt_ex obtain z where z:"ord.max less_eq z1 z2 \ z" - by blast - from z have zz1: "z1 \ z" and zz2: "z2 \ z" - by simp_all - have "(P1 x \ P2 x) \ (P1' \ P2')" if H: "z \ x" for x - using less_trans[OF zz1 H] less_trans[OF zz2 H] z1 zz1 z2 zz2 by auto - then show ?thesis - by blast -qed + by (metis ex1 ex2 local.max_less_iff_conj) lemma pinf_disj[no_atp]: assumes ex1: "\z1. \x. z1 \ x \ (P1 x \ P1')" and ex2: "\z2. \x. z2 \ x \ (P2 x \ P2')" shows "\z. \x. z \ x \ ((P1 x \ P2 x) \ (P1' \ P2'))" -proof- - from ex1 ex2 obtain z1 and z2 - where z1: "\x. z1 \ x \ (P1 x \ P1')" - and z2: "\x. z2 \ x \ (P2 x \ P2')" - by blast - from gt_ex obtain z where z: "ord.max less_eq z1 z2 \ z" - by blast - from z have zz1: "z1 \ z" and zz2: "z2 \ z" - by simp_all - have "(P1 x \ P2 x) \ (P1' \ P2')" if H: "z \ x" for x - using less_trans[OF zz1 H] less_trans[OF zz2 H] z1 zz1 z2 zz2 by auto - then show ?thesis - by blast -qed + by (metis ex1 ex2 local.max.strict_boundedE) lemma pinf_ex[no_atp]: assumes ex: "\z. \x. z \ x \ (P x \ P1)" and p1: P1 shows "\x. P x" -proof - - from ex obtain z where z: "\x. z \ x \ (P x \ P1)" - by blast - from gt_ex obtain x where x: "z \ x" - by blast - from z x p1 show ?thesis - by blast -qed + using ex local.gt_ex p1 by auto end @@ -521,52 +374,19 @@ assumes ex1: "\z1. \x. x \ z1 \ (P1 x \ P1')" and ex2: "\z2. \x. x \ z2 \ (P2 x \ P2')" shows "\z. \x. x \ z \ ((P1 x \ P2 x) \ (P1' \ P2'))" -proof - - from ex1 ex2 obtain z1 and z2 - where z1: "\x. x \ z1 \ (P1 x \ P1')" - and z2: "\x. x \ z2 \ (P2 x \ P2')" - by blast - from lt_ex obtain z where z: "z \ ord.min less_eq z1 z2" - by blast - from z have zz1: "z \ z1" and zz2: "z \ z2" - by simp_all - have "(P1 x \ P2 x) \ (P1' \ P2')" if H: "x \ z" for x - using less_trans[OF H zz1] less_trans[OF H zz2] z1 zz1 z2 zz2 by auto - then show ?thesis - by blast -qed + by (metis ex1 ex2 local.min_less_iff_conj) lemma minf_disj[no_atp]: assumes ex1: "\z1. \x. x \ z1 \ (P1 x \ P1')" and ex2: "\z2. \x. x \ z2 \ (P2 x \ P2')" shows "\z. \x. x \ z \ ((P1 x \ P2 x) \ (P1' \ P2'))" -proof - - from ex1 ex2 obtain z1 and z2 - where z1: "\x. x \ z1 \ (P1 x \ P1')" - and z2: "\x. x \ z2 \ (P2 x \ P2')" - by blast - from lt_ex obtain z where z: "z \ ord.min less_eq z1 z2" - by blast - from z have zz1: "z \ z1" and zz2: "z \ z2" - by simp_all - have "(P1 x \ P2 x) \ (P1' \ P2')" if H: "x \ z" for x - using less_trans[OF H zz1] less_trans[OF H zz2] z1 zz1 z2 zz2 by auto - then show ?thesis - by blast -qed + by (metis ex1 ex2 local.min_less_iff_conj) lemma minf_ex[no_atp]: assumes ex: "\z. \x. x \ z \ (P x \ P1)" and p1: P1 shows "\x. P x" -proof - - from ex obtain z where z: "\x. x \ z \ (P x \ P1)" - by blast - from lt_ex obtain x where x: "x \ z" - by blast - from z x p1 show ?thesis - by blast -qed + using ex local.lt_ex p1 by auto end @@ -600,9 +420,8 @@ proof - from ex obtain x where px: "P x" by blast - from px nmi npi nmpiU have "\u\ U. \u' \ U. u \ x \ x \ u'" - by auto - then obtain u and u' where uU: "u\ U" and uU': "u' \ U" and ux: "u \ x" and xu': "x \ u'" + from px nmi npi nmpiU + obtain u u' where uU: "u\ U" and uU': "u' \ U" and ux: "u \ x" and xu': "x \ u'" by auto from uU have Une: "U \ {}" by auto @@ -628,21 +447,16 @@ by blast then show ?thesis proof cases - case u: 1 - have "between u u = u" by (simp add: between_same) - with u have "P (between u u)" by simp - with u show ?thesis by blast + case 1 then show ?thesis + by (metis between_same) next case 2 - note t1M = \t1 \ U\ and t2M = \t2\ U\ - and noM = \\y. t1 \ y \ y \ t2 \ y \ U\ - and t1x = \t1 \ x\ and xt2 = \x \ t2\ - and px = \P x\ - from less_trans[OF t1x xt2] have t1t2: "t1 \ t2" . + then have t1t2: "t1 \ t2" + by order let ?u = "between t1 t2" from between_less t1t2 have t1lu: "t1 \ ?u" and ut2: "?u \ t2" by auto - from lin_dense noM t1x xt2 px t1lu ut2 have "P ?u" by blast - with t1M t2M show ?thesis by blast + then show ?thesis + using "2" lin_dense px by blast qed qed @@ -653,43 +467,26 @@ and nmibnd: "\x. \ MP \ P x \ (\u\ U. u \ x)" and npibnd: "\x. \PP \ P x \ (\u\ U. x \ u)" and mi: "\z. \x. x \ z \ (P x = MP)" and pi: "\z. \x. z \ x \ (P x = PP)" - shows "(\x. P x) \ (MP \ PP \ (\u \ U. \u'\ U. P (between u u')))" - (is "_ \ (_ \ _ \ ?F)" is "?E \ ?D") -proof - - have "?E \ ?D" - proof - show ?D if px: ?E - proof - - consider "MP \ PP" | "\ MP" "\ PP" by blast - then show ?thesis - proof cases - case 1 - then show ?thesis by blast - next - case 2 - from npmibnd[OF nmibnd npibnd] - have nmpiU: "\x. \ MP \ \PP \ P x \ (\u\ U. \u' \ U. u \ x \ x \ u')" . - from rinf_U[OF fU lin_dense nmpiU \\ MP\ \\ PP\ px] show ?thesis - by blast - qed - qed - show ?E if ?D - proof - - from that consider MP | PP | ?F by blast - then show ?thesis - proof cases - case 1 - from minf_ex[OF mi this] show ?thesis . - next - case 2 - from pinf_ex[OF pi this] show ?thesis . - next - case 3 - then show ?thesis by blast - qed + shows "(\x. P x) = (MP \ PP \ (\u \ U. \u'\ U. P (between u u')))" + (is"?E = ?D") +proof + show ?D if px: ?E + proof - + consider "MP \ PP" | "\ MP" "\ PP" by blast + then show ?thesis + proof cases + case 1 + then show ?thesis by blast + next + case 2 + from npmibnd[OF nmibnd npibnd] + have nmpiU: "\x. \ MP \ \PP \ P x \ (\u\ U. \u' \ U. u \ x \ x \ u')" . + from rinf_U[OF fU lin_dense nmpiU \\ MP\ \\ PP\ px] show ?thesis + by blast qed qed - then show "?E \ ?D" by simp + show ?E if ?D + using local.gt_ex local.lt_ex mi pi that by blast qed lemmas minf_thms[no_atp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P @@ -758,135 +555,81 @@ lemma neg_prod_lt: fixes c :: "'a::linordered_field" assumes "c < 0" - shows "c * x < 0 \ x > 0" -proof - - have "c * x < 0 \ 0 / c < x" - by (simp only: neg_divide_less_eq[OF \c < 0\] algebra_simps) - also have "\ \ 0 < x" by simp - finally show "PROP ?thesis" by simp -qed + shows "c * x < 0 \ x > 0" + by (metis assms mult_less_0_iff mult_neg_neg zero_less_mult_pos) lemma pos_prod_lt: fixes c :: "'a::linordered_field" assumes "c > 0" - shows "c * x < 0 \ x < 0" -proof - - have "c * x < 0 \ 0 /c > x" - by (simp only: pos_less_divide_eq[OF \c > 0\] algebra_simps) - also have "\ \ 0 > x" by simp - finally show "PROP ?thesis" by simp -qed + shows "c * x < 0 \ x < 0" + by (meson assms mult_less_0_iff order_less_imp_not_less) lemma neg_prod_sum_lt: fixes c :: "'a::linordered_field" assumes "c < 0" - shows "c * x + t < 0 \ x > (- 1 / c) * t" -proof - - have "c * x + t < 0 \ c * x < - t" - by (subst less_iff_diff_less_0 [of "c * x" "- t"]) simp - also have "\ \ - t / c < x" - by (simp only: neg_divide_less_eq[OF \c < 0\] algebra_simps) - also have "\ \ (- 1 / c) * t < x" by simp - finally show "PROP ?thesis" by simp -qed + shows "c * x + t < 0 \ x > (- 1 / c) * t" + using assms by (auto simp add: mult.commute divide_simps) lemma pos_prod_sum_lt: fixes c :: "'a::linordered_field" assumes "c > 0" - shows "c * x + t < 0 \ x < (- 1 / c) * t" -proof - - have "c * x + t < 0 \ c * x < - t" - by (subst less_iff_diff_less_0 [of "c * x" "- t"]) simp - also have "\ \ - t / c > x" - by (simp only: pos_less_divide_eq[OF \c > 0\] algebra_simps) - also have "\ \ (- 1 / c) * t > x" by simp - finally show "PROP ?thesis" by simp -qed + shows "c * x + t < 0 \ x < (- 1 / c) * t" + using assms by (auto simp add: mult.commute divide_simps) lemma sum_lt: fixes x :: "'a::ordered_ab_group_add" - shows "x + t < 0 \ x < - t" + shows "x + t < 0 \ x < - t" using less_diff_eq[where a= x and b=t and c=0] by simp lemma neg_prod_le: fixes c :: "'a::linordered_field" assumes "c < 0" - shows "c * x \ 0 \ x \ 0" -proof - - have "c * x \ 0 \ 0 / c \ x" - by (simp only: neg_divide_le_eq[OF \c < 0\] algebra_simps) - also have "\ \ 0 \ x" by simp - finally show "PROP ?thesis" by simp -qed + shows "c * x \ 0 \ x \ 0" + using assms linorder_not_less mult_le_0_iff by auto lemma pos_prod_le: fixes c :: "'a::linordered_field" assumes "c > 0" - shows "c * x \ 0 \ x \ 0" -proof - - have "c * x \ 0 \ 0 / c \ x" - by (simp only: pos_le_divide_eq[OF \c > 0\] algebra_simps) - also have "\ \ 0 \ x" by simp - finally show "PROP ?thesis" by simp -qed + shows "c * x \ 0 \ x \ 0" + using assms linorder_not_less mult_le_0_iff by auto lemma neg_prod_sum_le: fixes c :: "'a::linordered_field" assumes "c < 0" - shows "c * x + t \ 0 \ x \ (- 1 / c) * t" -proof - - have "c * x + t \ 0 \ c * x \ -t" - by (subst le_iff_diff_le_0 [of "c*x" "-t"]) simp - also have "\ \ - t / c \ x" - by (simp only: neg_divide_le_eq[OF \c < 0\] algebra_simps) - also have "\ \ (- 1 / c) * t \ x" by simp - finally show "PROP ?thesis" by simp -qed + shows "c * x + t \ 0 \ x \ (- 1 / c) * t" + using assms by (auto simp add: mult.commute divide_simps) lemma pos_prod_sum_le: fixes c :: "'a::linordered_field" assumes "c > 0" - shows "c * x + t \ 0 \ x \ (- 1 / c) * t" -proof - - have "c * x + t \ 0 \ c * x \ - t" - by (subst le_iff_diff_le_0 [of "c*x" "-t"]) simp - also have "\ \ - t / c \ x" - by (simp only: pos_le_divide_eq[OF \c > 0\] algebra_simps) - also have "\ \ (- 1 / c) * t \ x" by simp - finally show "PROP ?thesis" by simp -qed + shows "c * x + t \ 0 \ x \ (- 1 / c) * t" + using assms by (auto simp add: mult.commute divide_simps) lemma sum_le: fixes x :: "'a::ordered_ab_group_add" - shows "x + t \ 0 \ x \ - t" + shows "x + t \ 0 \ x \ - t" using le_diff_eq[where a= x and b=t and c=0] by simp lemma nz_prod_eq: fixes c :: "'a::linordered_field" assumes "c \ 0" - shows "c * x = 0 \ x = 0" + shows "c * x = 0 \ x = 0" using assms by simp lemma nz_prod_sum_eq: fixes c :: "'a::linordered_field" assumes "c \ 0" - shows "c * x + t = 0 \ x = (- 1/c) * t" -proof - - have "c * x + t = 0 \ c * x = - t" - by (subst eq_iff_diff_eq_0 [of "c*x" "-t"]) simp - also have "\ \ x = - t / c" - by (simp only: nonzero_eq_divide_eq[OF \c \ 0\] algebra_simps) - finally show "PROP ?thesis" by simp -qed + shows "c * x + t = 0 \ x = (- 1/c) * t" + using assms by (auto simp add: mult.commute divide_simps) lemma sum_eq: fixes x :: "'a::ordered_ab_group_add" - shows "x + t = 0 \ x = - t" + shows "x + t = 0 \ x = - t" using eq_diff_eq[where a= x and b=t and c=0] by simp interpretation class_dense_linordered_field: constr_dense_linorder "(\)" "(<)" "\x y. 1/2 * ((x::'a::linordered_field) + y)" - by unfold_locales (dlo, dlo, auto) + by unfold_locales (auto simp add: gt_ex lt_ex) declaration \ let @@ -918,6 +661,21 @@ else ("Nox",[]) | t => if t aconv Thm.term_of x then ("x",[]) else ("Nox",[]); +local +val sum_lt = mk_meta_eq @{thm sum_lt} +val sum_le = mk_meta_eq @{thm sum_le} +val sum_eq = mk_meta_eq @{thm sum_eq} +val neg_prod_sum_lt = mk_meta_eq @{thm neg_prod_sum_lt} +val pos_prod_sum_lt = mk_meta_eq @{thm pos_prod_sum_lt} +val neg_prod_sum_le = mk_meta_eq @{thm neg_prod_sum_le} +val pos_prod_sum_le = mk_meta_eq @{thm pos_prod_sum_le} +val neg_prod_lt = mk_meta_eq @{thm neg_prod_lt} +val pos_prod_lt = mk_meta_eq @{thm pos_prod_lt} +val neg_prod_le = mk_meta_eq @{thm neg_prod_le} +val pos_prod_le = mk_meta_eq @{thm pos_prod_le} +val nz_prod_sum_eq = mk_meta_eq @{thm nz_prod_sum_eq} +val nz_prod_eq = mk_meta_eq @{thm nz_prod_eq} +in fun xnormalize_conv ctxt [] ct = Thm.reflexive ct | xnormalize_conv ctxt (vs as (x::_)) ct = case Thm.term_of ct of @@ -935,14 +693,14 @@ else Thm.apply (Thm.apply clt cz) c)) val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t]) - (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth + (if neg then neg_prod_sum_lt else pos_prod_sum_lt)) cth val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th in rth end | ("x+t",[t]) => let val T = Thm.ctyp_of_cterm x - val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"} + val th = Thm.instantiate' [SOME T] [SOME x, SOME t] sum_lt val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th in rth end @@ -958,7 +716,7 @@ else Thm.apply (Thm.apply clt cz) c)) val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x]) - (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth + (if neg then neg_prod_lt else pos_prod_lt)) cth val rth = th in rth end | _ => Thm.reflexive ct) @@ -980,14 +738,14 @@ else Thm.apply (Thm.apply clt cz) c)) val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI val th = Thm.implies_elim (Thm.instantiate' [SOME cT] (map SOME [c,x,t]) - (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth + (if neg then neg_prod_sum_le else pos_prod_sum_le)) cth val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th in rth end | ("x+t",[t]) => let val T = Thm.ctyp_of_cterm x - val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"} + val th = Thm.instantiate' [SOME T] [SOME x, SOME t] sum_le val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th in rth end @@ -1005,7 +763,7 @@ else Thm.apply (Thm.apply clt cz) c)) val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x]) - (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth + (if neg then neg_prod_le else pos_prod_le)) cth val rth = th in rth end | _ => Thm.reflexive ct) @@ -1023,14 +781,14 @@ (Thm.apply \<^cterm>\Not\ (Thm.apply (Thm.apply ceq c) cz))) val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI val th = Thm.implies_elim - (Thm.instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth + (Thm.instantiate' [SOME T] (map SOME [c,x,t]) nz_prod_sum_eq) cth val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th in rth end | ("x+t",[t]) => let val T = Thm.ctyp_of_cterm x - val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"} + val th = Thm.instantiate' [SOME T] [SOME x, SOME t] sum_eq val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th in rth end @@ -1045,9 +803,10 @@ (Thm.apply \<^cterm>\Not\ (Thm.apply (Thm.apply ceq c) cz))) val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI val rth = Thm.implies_elim - (Thm.instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth + (Thm.instantiate' [SOME T] (map SOME [c,x]) nz_prod_eq) cth in rth end | _ => Thm.reflexive ct); +end local val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"} diff -r 26fbbf43863b -r 3fb2525699e6 src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Sun Mar 16 14:21:00 2025 +0100 +++ b/src/HOL/Decision_Procs/Ferrack.thy Sun Mar 16 17:02:41 2025 +0000 @@ -1021,10 +1021,8 @@ qed (auto simp add: disj_def imp_def iff_def conj_def) lemma simpfm_qf: "qfree p \ qfree (simpfm p)" - apply (induct p rule: simpfm.induct) - apply (auto simp add: Let_def) - apply (case_tac "simpnum a", auto)+ - done + by (induct p rule: simpfm.induct) (auto simp: Let_def split: num.splits) + fun prep :: "fm \ fm" where @@ -1256,17 +1254,11 @@ proof (induct p rule: minusinf.induct) case (1 p q) then show ?case - apply auto - apply (rule_tac x= "min z za" in exI) - apply auto - done + by (fastforce simp: intro: exI [where x= "min _ _"]) next case (2 p q) then show ?case - apply auto - apply (rule_tac x= "min z za" in exI) - apply auto - done + by (fastforce simp: intro: exI [where x= "min _ _"]) next case (3 c e) from 3 have nb: "numbound0 e" by simp @@ -1386,17 +1378,11 @@ proof (induct p rule: isrlfm.induct) case (1 p q) then show ?case - apply auto - apply (rule_tac x= "max z za" in exI) - apply auto - done + by (fastforce simp: intro: exI [where x= "max _ _"]) next case (2 p q) then show ?case - apply auto - apply (rule_tac x= "max z za" in exI) - apply auto - done + by (fastforce simp: intro: exI [where x= "max _ _"]) next case (3 c e) from 3 have nb: "numbound0 e" by simp @@ -2195,12 +2181,7 @@ \ (\((t, n), s, m). (Inum (x # bs) t / real_of_int n + Inum (x # bs) s / real_of_int m) / 2) ` (set U \ set U)" using mnz nnz th - apply (auto simp add: th add_divide_distrib algebra_simps split_def image_def) - apply (rule_tac x="(s,m)" in bexI) - apply simp_all - apply (rule_tac x="(t,n)" in bexI) - apply (simp_all add: mult.commute) - done + by (force simp add: th add_divide_distrib algebra_simps split_def image_def) next fix t n s m assume tnU: "(t, n) \ set U" and smU: "(s, m) \ set U" @@ -2271,10 +2252,7 @@ from tnU smU UU' have "?g ((t, n), (s, m)) \ ?f ` U'" by blast then have "\(t',n') \ U'. ?g ((t, n), (s, m)) = ?f (t', n')" - apply auto - apply (rule_tac x="(a, b)" in bexI) - apply auto - done + by fastforce then obtain t' n' where tnU': "(t',n') \ U'" and th: "?g ((t, n), (s, m)) = ?f (t', n')" by blast from U' tnU' have tnb': "numbound0 t'" and np': "real_of_int n' > 0" @@ -2296,10 +2274,7 @@ from tnU' UU' have "?f (t', n') \ ?g ` (U \ U)" by blast then have "\((t,n),(s,m)) \ U \ U. ?f (t', n') = ?g ((t, n), (s, m))" - apply auto - apply (rule_tac x="(a,b)" in bexI) - apply auto - done + by force then obtain t n s m where tnU: "(t, n) \ U" and smU: "(s, m) \ U" and th: "?f (t', n') = ?g ((t, n), (s, m))" by blast @@ -2361,10 +2336,7 @@ from that have "(t,n) \ set ?SS" by simp then have "\(t',n') \ set ?S. simp_num_pair (t', n') = (t, n)" - apply (auto simp add: split_def simp del: map_map) - apply (rule_tac x="((aa,ba),(ab,bb))" in bexI) - apply simp_all - done + by (force simp add: split_def simp del: map_map) then obtain t' n' where tn'S: "(t', n') \ set ?S" and tns: "simp_num_pair (t', n') = (t, n)" by blast from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" diff -r 26fbbf43863b -r 3fb2525699e6 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sun Mar 16 14:21:00 2025 +0100 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sun Mar 16 17:02:41 2025 +0000 @@ -860,11 +860,17 @@ case (1 c p n) then have pn: "isnpolyh p n" by simp from 1(1)[OF pn] - have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . - then show ?case using "1.hyps" - apply (simp add: Let_def,cases "behead p = 0\<^sub>p") - apply (simp_all add: th[symmetric] field_simps) - done + have *: "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . + show ?case + proof (cases "behead p = 0\<^sub>p") + case True + then show ?thesis + using * by auto + next + case False + then show ?thesis + by (simp add: field_simps flip: *) + qed qed (auto simp add: Let_def) lemma behead_isnpolyh: @@ -1011,7 +1017,7 @@ lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \ isconstant p" by (simp add: isconstant_polybound0 isnpolyh_polybound0) -lemma wf_bs_polyadd: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p +\<^sub>p q)" +lemma wf_bs_polyadd: "\wf_bs bs p; wf_bs bs q\ \ wf_bs bs (p +\<^sub>p q)" by (induct p q rule: polyadd.induct) (auto simp add: Let_def wf_bs_def) lemma wf_bs_polyul: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p *\<^sub>p q)" @@ -1019,7 +1025,7 @@ case (4 c n p c' n' p') then show ?case apply (simp add: wf_bs_def) - by (metis Suc_eq_plus1 max.bounded_iff max_0L maxindex.simps(2) maxindex.simps(8) wf_bs_def wf_bs_polyadd) + by (metis "4.prems"(1) max.bounded_iff max_0L maxindex.simps(2,8) wf_bs_def wf_bs_polyadd) qed (simp_all add: wf_bs_def) lemma wf_bs_polyneg: "wf_bs bs p \ wf_bs bs (~\<^sub>p p)" @@ -1600,9 +1606,8 @@ show ?ths proof (cases "s = 0\<^sub>p") case True - with np show ?thesis - apply (clarsimp simp: polydivide_aux.simps) - by (metis polyadd_0(1) polymul_0(1) zero_normh) + with np polyadd_0 polymul_0 zero_normh show ?thesis + by (metis degree.simps(2) nakk' polydivide_aux.simps prod.sel order.refl) next case sz: False show ?thesis @@ -1711,10 +1716,7 @@ by (simp add: h1) with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]] polyadd_0(2)[OF polymul_normh[OF np nxdn]] show ?thesis - apply auto - apply (rule exI[where x="?xdn"]) - apply (auto simp add: polymul_commute[of p]) - done + using polymul_commute by auto qed then show ?thesis by blast qed diff -r 26fbbf43863b -r 3fb2525699e6 src/HOL/Decision_Procs/ferrante_rackoff.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Mar 16 14:21:00 2025 +0100 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Mar 16 17:02:41 2025 +0000 @@ -161,7 +161,7 @@ val qe_th = Drule.implies_elim_list ((fconv_rule (Thm.beta_conversion true)) (Thm.instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th]) - qe)) + (mk_meta_eq qe))) [fU, ld_th, nmi_th, npi_th, minf_th, pinf_th] val bex_conv = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms bex_simps(1-5)})