# HG changeset patch
# User paulson
# Date 1742126627 0
# Node ID 3cb05c9ce8c4a078191839cfcafecc4510dadf00
# Parent  4042628fffa5f17c84e02ce0a4c98f0fba782365# Parent  a7216319c0bbf3c10089565e084b330d2eb2c9ec
merged

diff -r 4042628fffa5 -r 3cb05c9ce8c4 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Sun Mar 16 09:11:17 2025 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Mar 16 12:03:47 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 4042628fffa5 -r 3cb05c9ce8c4 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Mar 16 09:11:17 2025 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Mar 16 12:03:47 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
@@ -935,14 +678,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
+             (mk_meta_eq(if neg then @{thm neg_prod_sum_lt} else @{thm 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] (mk_meta_eq @{thm "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 +701,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
+             (mk_meta_eq(if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt}))) cth
         val rth = th
       in rth end
     | _ => Thm.reflexive ct)
@@ -980,14 +723,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
+             (mk_meta_eq(if neg then @{thm neg_prod_sum_le} else @{thm 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] (mk_meta_eq @{thm "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 +748,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
+             (mk_meta_eq(if neg then @{thm neg_prod_le} else @{thm pos_prod_le}))) cth
         val rth = th
       in rth end
     | _ => Thm.reflexive ct)
@@ -1023,14 +766,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]) (mk_meta_eq @{thm 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] (mk_meta_eq @{thm "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,7 +788,7 @@
              (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]) (mk_meta_eq @{thm nz_prod_eq})) cth
       in rth end
     | _ => Thm.reflexive ct);
 
diff -r 4042628fffa5 -r 3cb05c9ce8c4 src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Mar 16 09:11:17 2025 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Sun Mar 16 12:03:47 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)})