# 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: "\<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"
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 \<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
     {
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" | "\<not> (\<exists>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" | "\<not> (\<exists>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 \<Longrightarrow> 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 \<open>Generic quantifier elimination\<close>
@@ -1076,11 +1066,7 @@
     by auto
   let ?N = "\<lambda>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 = "\<lambda>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 = "\<lambda>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 = "\<lambda>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 = "\<lambda>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 = "\<lambda>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 \<in> set (\<beta> (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 \<noteq> - 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 \<beta>[OF lp u d dp nb2 px])
 qed
 
+(*a duplicate in MIR.thy*)
 lemma cpmi_eq:
   fixes P P1 :: "int \<Rightarrow> bool"
   assumes "0 < D"
@@ -2092,24 +2047,22 @@
     and "\<forall>x. \<not> (\<exists>j \<in> {1..D}. \<exists>b \<in> B. P (b + j)) \<longrightarrow> P x \<longrightarrow> P (x - D)"
     and "\<forall>x k. P1 x = P1 (x - k * D)"
   shows "(\<exists>x. P x) \<longleftrightarrow> (\<exists>j \<in> {1..D}. P1 j) \<or> (\<exists>j \<in> {1..D}. \<exists>b \<in> B. P (b + j))"
-  apply (insert assms)
-  apply (rule iffI)
-  prefer 2
-  apply (drule minusinfinity)
-  apply assumption+
-  apply fastforce
-  apply clarsimp
-  apply (subgoal_tac "\<And>k. 0 \<le> k \<Longrightarrow> \<forall>x. P x \<longrightarrow> P (x - k * D)")
-  apply (frule_tac x = x and z=z in decr_lemma)
-  apply (subgoal_tac "P1 (x - (\<bar>x - z\<bar> + 1) * D)")
-  prefer 2
-  apply (subgoal_tac "0 \<le> \<bar>x - z\<bar> + 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: "\<exists>x. P x"
+  show "(\<exists>j\<in>{1..D}. P1 j) \<or> (\<exists>j\<in>{1..D}. \<exists>b\<in>B. P (b + j))"
+  proof clarsimp
+    assume \<section>: "\<forall>j\<in>{1..D}. \<forall>b\<in>B. \<not> P (b + j)"
+    then have "\<And>k. 0\<le>k \<Longrightarrow> \<forall>x. P x \<longrightarrow> P (x - k*D)"
+      by (simp add: assms decr_mult_lemma)
+    with L \<section> assms show "\<exists>j\<in>{1..D}. P1 j"
+      using periodic_finite_ex [OF \<open>D>0\<close>, of P1]
+      by (metis abs_1 abs_add_abs abs_ge_zero decr_lemma)
+  qed
+next
+  assume ?R then show "\<exists>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 "(\<exists>x. Ifm bbs (x#bs) (mirror p)) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) p)"
-  (is "(\<exists>x. ?I x ?mp) = (\<exists>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 "\<exists>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 "\<exists>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 @@
     (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y))"
   by auto
 
-lemma gather_start [no_atp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)"
+lemma gather_start [no_atp]: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)"
   by simp
 
 text\<open>Theorems for \<open>\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)\<close>\<close>
-lemma minf_lt[no_atp]:  "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
-lemma minf_gt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow>  (t < x \<longleftrightarrow>  False)"
+lemma minf_lt[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" 
+  by auto
+lemma minf_gt[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t < x \<longleftrightarrow> False)"
   by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
 
-lemma minf_le[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma minf_le[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" 
+  by (auto simp add: less_le)
 lemma minf_ge[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
   by (auto simp add: less_le not_less not_le)
-lemma minf_eq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
-lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
-lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
+lemma minf_eq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" 
+  by auto
+lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" 
+  by auto
+lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" 
+  by blast
 
 text\<open>Theorems for \<open>\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)\<close>\<close>
-lemma pinf_gt[no_atp]:  "\<exists>z. \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
+lemma pinf_gt[no_atp]:  "\<exists>z. \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" 
+  by auto
 lemma pinf_lt[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow>  (x < t \<longleftrightarrow>  False)"
   by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
 
-lemma pinf_ge[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma pinf_ge[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" 
+  by (auto simp add: less_le)
 lemma pinf_le[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
   by (auto simp add: less_le not_less not_le)
 lemma pinf_eq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
@@ -86,104 +93,22 @@
 lemma lin_dense_lt[no_atp]:
   "t \<in> U \<Longrightarrow>
     \<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> x < t \<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> y < t)"
-proof clarsimp
-  fix x l u y
-  assume tU: "t \<in> U"
-    and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> 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 \<noteq> y" by auto
-  have False if H: "t < y"
-  proof -
-    from less_trans[OF lx px] less_trans[OF H yu] have "l < t \<and> t < u"
-      by simp
-    with tU noU show ?thesis
-      by auto
-  qed
-  then have "\<not> t < y"
-    by auto
-  then have "y \<le> 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 \<in> U \<Longrightarrow>
     \<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t < x \<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> t < y)"
-proof clarsimp
-  fix x l u y
-  assume tU: "t \<in> U"
-    and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> 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 \<noteq> y" by auto
-  have False if H: "y < t"
-  proof -
-    from less_trans[OF ly H] less_trans[OF px xu] have "l < t \<and> t < u"
-      by simp
-    with tU noU show ?thesis
-      by auto
-  qed
-  then have "\<not> y < t"
-    by auto
-  then have "t \<le> 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 \<in> U \<Longrightarrow>
     \<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> x \<le> t \<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> y \<le> t)"
-proof clarsimp
-  fix x l u y
-  assume tU: "t \<in> U"
-    and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U"
-    and lx: "l < x"
-    and xu: "x < u"
-    and px: "x \<le> t"
-    and ly: "l < y"
-    and yu: "y < u"
-  from tU noU ly yu have tny: "t \<noteq> 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 \<and> t < u" by simp
-    with tU noU show ?thesis by auto
-  qed
-  then have "\<not> t < y" by auto
-  then show "y \<le> 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 \<in> U \<Longrightarrow>
     \<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t \<le> x \<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> t \<le> y)"
-proof clarsimp
-  fix x l u y
-  assume tU: "t \<in> U"
-    and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U"
-    and lx: "l < x"
-    and xu: "x < u"
-    and px: "t \<le> x"
-    and ly: "l < y"
-    and yu: "y < u"
-  from tU noU ly yu have tny: "t \<noteq> 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 \<and> t < u" by simp
-    with tU noU show ?thesis by auto
-  qed
-  then have "\<not> y < t" by auto
-  then show "t \<le> 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 \<in> U \<Longrightarrow>
@@ -207,6 +132,7 @@
   \<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> (P1 x \<and> P2 x)
   \<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
   by blast
+
 lemma lin_dense_disj[no_atp]:
   "\<lbrakk>\<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> P1 x
   \<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> P1 y) ;
@@ -264,26 +190,7 @@
   then have binS: "?b \<in> S"
     using xMS by blast
   have noy: "\<forall>y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
-  proof clarsimp
-    fix y
-    assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
-    from yS have "y \<in> ?Mx \<or> y \<in> ?xM"
-      by (auto simp add: linear)
-    then show False
-    proof
-      assume "y \<in> ?Mx"
-      then have "y \<le> ?a"
-        using Mxne fMx by auto
-      with ay show ?thesis
-        by (simp add: not_le[symmetric])
-    next
-      assume "y \<in> ?xM"
-      then have "?b \<le> 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: "\<forall>x\<in> S. l \<le> x"
     and Su: "\<forall>x\<in> S. x \<le> u"
   shows "(\<exists>s\<in> S. P s) \<or> (\<exists>a \<in> S. \<exists>b \<in> S. (\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> 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 \<in> S" and bs: "b \<in> S"
-    and noS: "\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S"
-    and axb: "a \<le> x \<and> x \<le> b \<and> P x"
-    by auto
-  from axb have "x = a \<or> x = b \<or> (a < x \<and> 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 \<noteq> {}"
     and fL: "finite L"
     and fU: "finite U"
-  shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> (\<forall>l \<in> L. \<forall>u \<in> U. l < u)"
-proof (simp only: atomize_eq, rule iffI)
+  shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) = (\<forall>l \<in> L. \<forall>u \<in> U. l < u)"
+proof 
   assume H: "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)"
   then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < y"
     by blast
   have "l < u" if l: "l \<in> L" and u: "u \<in> 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 "\<forall>l\<in>L. \<forall>u\<in>U. l < u" by blast
 next
   assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l < u"
@@ -361,30 +255,21 @@
 lemma dlo_qe_noub[no_atp]:
   assumes ne: "L \<noteq> {}"
     and fL: "finite L"
-  shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> 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 "\<forall>x \<in> L. x \<le> Max L"
-    by simp
-  with M have "\<forall>x\<in>L. x < M"
-    by (auto intro: le_less_trans)
-  then show "\<exists>x. \<forall>y\<in>L. y < x"
-    by blast
-qed
+  shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) = True"
+  using fL local.Max_less_iff local.gt_ex by fastforce
 
 lemma dlo_qe_nolb[no_atp]:
   assumes ne: "U \<noteq> {}"
     and fU: "finite U"
-  shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True"
-proof (simp add: atomize_eq)
+  shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) = True"
+proof -
   from lt_ex[of "Min U"] obtain M where M: "M < Min U"
     by blast
   from ne fU have "\<forall>x \<in> U. Min U \<le> x"
     by simp
   with M have "\<forall>x\<in>U. M < x"
     by (auto intro: less_le_trans)
-  then show "\<exists>x. \<forall>y\<in>U. x < y"
+  then show ?thesis
     by blast
 qed
 
@@ -396,6 +281,7 @@
 
 lemma axiom[no_atp]: "class.unbounded_dense_linorder (\<le>) (<)"
   by (rule unbounded_dense_linorder_axioms)
+
 lemma atoms[no_atp]:
   shows "TERM (less :: 'a \<Rightarrow> _)"
     and "TERM (less_eq :: 'a \<Rightarrow> _)"
@@ -457,52 +343,19 @@
   assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
     and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
-proof -
-  from ex1 ex2 obtain z1 and z2
-    where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
-    and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
-    by blast
-  from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z"
-    by blast
-  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z"
-    by simp_all
-  have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" if H: "z \<sqsubset> 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: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
     and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   shows "\<exists>z. \<forall>x. z \<sqsubset>  x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
-proof-
-  from ex1 ex2 obtain z1 and z2
-    where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
-    and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
-    by blast
-  from gt_ex obtain z where z: "ord.max less_eq z1 z2 \<sqsubset> z"
-    by blast
-  from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z"
-    by simp_all
-  have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" if H: "z \<sqsubset> 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: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)"
     and p1: P1
   shows "\<exists>x. P x"
-proof -
-  from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)"
-    by blast
-  from gt_ex obtain x where x: "z \<sqsubset> 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: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
     and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
-proof -
-  from ex1 ex2 obtain z1 and z2
-    where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
-    and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
-    by blast
-  from lt_ex obtain z where z: "z \<sqsubset> ord.min less_eq z1 z2"
-    by blast
-  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2"
-    by simp_all
-  have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" if H: "x \<sqsubset> 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: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
     and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
   shows "\<exists>z. \<forall>x. x \<sqsubset>  z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
-proof -
-  from ex1 ex2 obtain z1 and z2
-    where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
-    and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
-    by blast
-  from lt_ex obtain z where z: "z \<sqsubset> ord.min less_eq z1 z2"
-    by blast
-  from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2"
-    by simp_all
-  have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" if H: "x \<sqsubset> 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: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)"
     and p1: P1
   shows "\<exists>x. P x"
-proof -
-  from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)"
-    by blast
-  from lt_ex obtain x where x: "x \<sqsubset> 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 "\<exists>u\<in> U. \<exists>u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'"
-    by auto
-  then obtain u and u' where uU: "u\<in> U" and uU': "u' \<in> U" and ux: "u \<sqsubseteq> x" and xu': "x \<sqsubseteq> u'"
+  from px nmi npi nmpiU 
+  obtain u u' where uU: "u\<in> U" and uU': "u' \<in> U" and ux: "u \<sqsubseteq> x" and xu': "x \<sqsubseteq> u'"
     by auto
   from uU have Une: "U \<noteq> {}"
     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 = \<open>t1 \<in> U\<close> and t2M = \<open>t2\<in> U\<close>
-      and noM = \<open>\<forall>y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U\<close>
-      and t1x = \<open>t1 \<sqsubset> x\<close> and xt2 = \<open>x \<sqsubset> t2\<close>
-      and px = \<open>P x\<close>
-    from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" .
+    then have t1t2: "t1 \<sqsubset> t2"
+      by order 
     let ?u = "between t1 t2"
     from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> 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: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists>u\<in> U. u \<sqsubseteq> x)"
     and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists>u\<in> U. x \<sqsubseteq> u)"
     and mi: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x = MP)"  and pi: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x = PP)"
-  shows "(\<exists>x. P x) \<equiv> (MP \<or> PP \<or> (\<exists>u \<in> U. \<exists>u'\<in> U. P (between u u')))"
-  (is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D")
-proof -
-  have "?E \<longleftrightarrow> ?D"
-  proof
-    show ?D if px: ?E
-    proof -
-      consider "MP \<or> PP" | "\<not> MP" "\<not> 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: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists>u\<in> U. \<exists>u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')" .
-        from rinf_U[OF fU lin_dense nmpiU \<open>\<not> MP\<close> \<open>\<not> PP\<close> 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 "(\<exists>x. P x) = (MP \<or> PP \<or> (\<exists>u \<in> U. \<exists>u'\<in> U. P (between u u')))"
+         (is"?E = ?D")
+proof 
+  show ?D if px: ?E
+  proof -
+    consider "MP \<or> PP" | "\<not> MP" "\<not> 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: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists>u\<in> U. \<exists>u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')" .
+      from rinf_U[OF fU lin_dense nmpiU \<open>\<not> MP\<close> \<open>\<not> PP\<close> px] show ?thesis
+        by blast
     qed
   qed
-  then show "?E \<equiv> ?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 \<equiv> x > 0"
-proof -
-  have "c * x < 0 \<longleftrightarrow> 0 / c < x"
-    by (simp only: neg_divide_less_eq[OF \<open>c < 0\<close>] algebra_simps)
-  also have "\<dots> \<longleftrightarrow> 0 < x" by simp
-  finally show "PROP ?thesis" by simp
-qed
+  shows "c * x < 0 \<longleftrightarrow> 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 \<equiv> x < 0"
-proof -
-  have "c * x < 0 \<longleftrightarrow> 0 /c > x"
-    by (simp only: pos_less_divide_eq[OF \<open>c > 0\<close>] algebra_simps)
-  also have "\<dots> \<longleftrightarrow> 0 > x" by simp
-  finally show "PROP ?thesis" by simp
-qed
+  shows "c * x < 0 \<longleftrightarrow> 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 \<equiv> x > (- 1 / c) * t"
-proof -
-  have "c * x + t < 0 \<longleftrightarrow> c * x < - t"
-    by (subst less_iff_diff_less_0 [of "c * x" "- t"]) simp
-  also have "\<dots> \<longleftrightarrow> - t / c < x"
-    by (simp only: neg_divide_less_eq[OF \<open>c < 0\<close>] algebra_simps)
-  also have "\<dots> \<longleftrightarrow> (- 1 / c) * t < x" by simp
-  finally show "PROP ?thesis" by simp
-qed
+  shows "c * x + t < 0 \<longleftrightarrow> 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 \<equiv> x < (- 1 / c) * t"
-proof -
-  have "c * x + t < 0 \<longleftrightarrow> c * x < - t"
-    by (subst less_iff_diff_less_0 [of "c * x" "- t"]) simp
-  also have "\<dots> \<longleftrightarrow> - t / c > x"
-    by (simp only: pos_less_divide_eq[OF \<open>c > 0\<close>] algebra_simps)
-  also have "\<dots> \<longleftrightarrow> (- 1 / c) * t > x" by simp
-  finally show "PROP ?thesis" by simp
-qed
+  shows "c * x + t < 0 \<longleftrightarrow> 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 \<equiv> x < - t"
+  shows "x + t < 0 \<longleftrightarrow> 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 \<le> 0 \<equiv> x \<ge> 0"
-proof -
-  have "c * x \<le> 0 \<longleftrightarrow> 0 / c \<le> x"
-    by (simp only: neg_divide_le_eq[OF \<open>c < 0\<close>] algebra_simps)
-  also have "\<dots> \<longleftrightarrow> 0 \<le> x" by simp
-  finally show "PROP ?thesis" by simp
-qed
+  shows "c * x \<le> 0 \<longleftrightarrow> x \<ge> 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 \<le> 0 \<equiv> x \<le> 0"
-proof -
-  have "c * x \<le> 0 \<longleftrightarrow> 0 / c \<ge> x"
-    by (simp only: pos_le_divide_eq[OF \<open>c > 0\<close>] algebra_simps)
-  also have "\<dots> \<longleftrightarrow> 0 \<ge> x" by simp
-  finally show "PROP ?thesis" by simp
-qed
+  shows "c * x \<le> 0 \<longleftrightarrow> x \<le> 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 \<le> 0 \<equiv> x \<ge> (- 1 / c) * t"
-proof -
-  have "c * x + t \<le> 0 \<longleftrightarrow> c * x \<le> -t"
-    by (subst le_iff_diff_le_0 [of "c*x" "-t"]) simp
-  also have "\<dots> \<longleftrightarrow> - t / c \<le> x"
-    by (simp only: neg_divide_le_eq[OF \<open>c < 0\<close>] algebra_simps)
-  also have "\<dots> \<longleftrightarrow> (- 1 / c) * t \<le> x" by simp
-  finally show "PROP ?thesis" by simp
-qed
+  shows "c * x + t \<le> 0 \<longleftrightarrow> x \<ge> (- 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 \<le> 0 \<equiv> x \<le> (- 1 / c) * t"
-proof -
-  have "c * x + t \<le> 0 \<longleftrightarrow> c * x \<le> - t"
-    by (subst le_iff_diff_le_0 [of "c*x" "-t"]) simp
-  also have "\<dots> \<longleftrightarrow> - t / c \<ge> x"
-    by (simp only: pos_le_divide_eq[OF \<open>c > 0\<close>] algebra_simps)
-  also have "\<dots> \<longleftrightarrow> (- 1 / c) * t \<ge> x" by simp
-  finally show "PROP ?thesis" by simp
-qed
+  shows "c * x + t \<le> 0 \<longleftrightarrow> x \<le> (- 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 \<le> 0 \<equiv> x \<le> - t"
+  shows "x + t \<le> 0 \<longleftrightarrow> x \<le> - 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 \<noteq> 0"
-  shows "c * x = 0 \<equiv> x = 0"
+  shows "c * x = 0 \<longleftrightarrow> x = 0"
   using assms by simp
 
 lemma nz_prod_sum_eq:
   fixes c :: "'a::linordered_field"
   assumes "c \<noteq> 0"
-  shows "c * x + t = 0 \<equiv> x = (- 1/c) * t"
-proof -
-  have "c * x + t = 0 \<longleftrightarrow> c * x = - t"
-    by (subst eq_iff_diff_eq_0 [of "c*x" "-t"]) simp
-  also have "\<dots> \<longleftrightarrow> x = - t / c"
-    by (simp only: nonzero_eq_divide_eq[OF \<open>c \<noteq> 0\<close>] algebra_simps)
-  finally show "PROP ?thesis" by simp
-qed
+  shows "c * x + t = 0 \<longleftrightarrow> 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 \<equiv> x = - t"
+  shows "x + t = 0 \<longleftrightarrow> 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
   "(\<le>)" "(<)" "\<lambda>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 \<open>
 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>\<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]) @{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>\<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]) @{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 \<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"
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) \<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
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)})