# HG changeset patch # User paulson # Date 1742144547 0 # Node ID 5d91cca0aaf36806c612e9e36442d9bf7c4b306a # Parent 3cb05c9ce8c4a078191839cfcafecc4510dadf00 Tidied up a few messy proofs diff -r 3cb05c9ce8c4 -r 5d91cca0aaf3 src/HOL/Decision_Procs/Algebra_Aux.thy --- a/src/HOL/Decision_Procs/Algebra_Aux.thy Sun Mar 16 12:03:47 2025 +0000 +++ b/src/HOL/Decision_Procs/Algebra_Aux.thy Sun Mar 16 17:02:27 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 3cb05c9ce8c4 -r 5d91cca0aaf3 src/HOL/Decision_Procs/Approximation_Bounds.thy --- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Sun Mar 16 12:03:47 2025 +0000 +++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Sun Mar 16 17:02:27 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 3cb05c9ce8c4 -r 5d91cca0aaf3 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 16 12:03:47 2025 +0000 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 16 17:02:27 2025 +0000 @@ -661,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 @@ -678,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]) - (mk_meta_eq(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] (mk_meta_eq @{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 @@ -701,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]) - (mk_meta_eq(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) @@ -723,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]) - (mk_meta_eq(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] (mk_meta_eq @{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 @@ -748,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]) - (mk_meta_eq(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) @@ -766,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]) (mk_meta_eq @{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] (mk_meta_eq @{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 @@ -788,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]) (mk_meta_eq @{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 3cb05c9ce8c4 -r 5d91cca0aaf3 src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Sun Mar 16 12:03:47 2025 +0000 +++ b/src/HOL/Decision_Procs/Ferrack.thy Sun Mar 16 17:02:27 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 3cb05c9ce8c4 -r 5d91cca0aaf3 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sun Mar 16 12:03:47 2025 +0000 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sun Mar 16 17:02:27 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