--- 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: "\<ominus>\<^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 \<and> 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 \<ominus>\<^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) \<oslash>\<^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="\<lambda>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 "(\<zero>\<^bsub>cring_class_ops\<^esub>::'a) = 0"
--- 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 \<open>0 < real_of_int m\<close> \<open>0 \<le> bl\<close>
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] \<open>m > 0\<close>
by (simp_all add: bitlen powr_realpow [symmetric] powr_minus powr_add field_simps)
{
- have "float_round_down prec (lb_ln2 prec * ?s) \<le> ln 2 * (e + (bitlen m - 1))"
- (is "real_of_float ?lb2 \<le> _")
- 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)
+ \<le> ln 2 * real_of_int (e + (bitlen m - 1))"
proof (rule mult_mono)
from float_gt1_scale[OF \<open>1 \<le> Float m e\<close>]
show "0 \<le> 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) \<le> ln 2 * (e + (bitlen m - 1))"
+ (is "real_of_float ?lb2 \<le> _")
+ 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)) \<le> ln ?x" (is "real_of_float ?lb_horner \<le> _")
by (auto intro!: float_round_down_le)
ultimately have "float_plus_down prec ?lb2 ?lb_horner \<le> ln x"
- unfolding Float ln_shifted_float[OF \<open>0 < m\<close>, of e] by (auto intro!: float_plus_down_le)
+ unfolding Float ln_shifted_float[OF \<open>0 < m\<close>, of e]
+ by (auto intro!: float_plus_down_le)
}
moreover
{
--- 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>\<open>Not\<close> (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>\<open>Not\<close> (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"}
--- 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 \<Longrightarrow> 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 \<Rightarrow> 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 @@
\<in> (\<lambda>((t, n), s, m). (Inum (x # bs) t / real_of_int n + Inum (x # bs) s / real_of_int m) / 2) `
(set U \<times> 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) \<in> set U" and smU: "(s, m) \<in> set U"
@@ -2271,10 +2252,7 @@
from tnU smU UU' have "?g ((t, n), (s, m)) \<in> ?f ` U'"
by blast
then have "\<exists>(t',n') \<in> 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') \<in> 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') \<in> ?g ` (U \<times> U)"
by blast
then have "\<exists>((t,n),(s,m)) \<in> U \<times> 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) \<in> U" and smU: "(s, m) \<in> U" and
th: "?f (t', n') = ?g ((t, n), (s, m))"
by blast
@@ -2361,10 +2336,7 @@
from that have "(t,n) \<in> set ?SS"
by simp
then have "\<exists>(t',n') \<in> 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') \<in> 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"
--- 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) \<Longrightarrow> isconstant p"
by (simp add: isconstant_polybound0 isnpolyh_polybound0)
-lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)"
+lemma wf_bs_polyadd: "\<lbrakk>wf_bs bs p; wf_bs bs q\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> wf_bs bs q \<Longrightarrow> 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 \<Longrightarrow> 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