# HG changeset patch
# User wenzelm
# Date 1635503447 -7200
# Node ID 82ff15b980e9fcf319846c28c0159de978d9c5b4
# Parent  d622d1dce05cbc35d1c6e4dc265c22609d45990d
clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;

diff -r d622d1dce05c -r 82ff15b980e9 src/HOL/Library/Sum_of_Squares/positivstellensatz.ML
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Fri Oct 29 11:59:02 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Fri Oct 29 12:30:47 2021 +0200
@@ -724,37 +724,33 @@
 
   val absmaxmin_elim_conv2 =
     let
-      val p_v = (("P", 0), \<^typ>\<open>real \<Rightarrow> bool\<close>)
-      val x_v = (("x", 0), \<^typ>\<open>real\<close>)
-      val y_v = (("y", 0), \<^typ>\<open>real\<close>)
-      fun is_abs \<^Const_>\<open>abs \<^Type>\<open>real\<close> for _\<close> = true
-        | is_abs _ = false
-      fun is_max \<^Const_>\<open>max \<^Type>\<open>real\<close> for _ _\<close> = true
-        | is_max _ = false
-      fun is_min \<^Const_>\<open>min \<^Type>\<open>real\<close> for _ _\<close> = true
-        | is_min _ = false
-      fun eliminate_construct p c tm =
+      fun elim_construct pred conv tm =
         let
-          val t = find_cterm (p o Thm.term_of) tm
-          val th0 = Thm.symmetric (Thm.beta_conversion false (Thm.apply (Thm.lambda t tm) t))
-          val (P, a) = Thm.dest_comb (Thm.rhs_of th0)
-        in
-          fconv_rule
-            (arg_conv (binop_conv (arg_conv (Thm.beta_conversion false))))
-            (Thm.transitive th0 (c P a))
-        end
+          val a = find_cterm (pred o Thm.term_of) tm
+          val P = Thm.lambda a tm
+        in conv P a end
 
-      val elim_abs = eliminate_construct is_abs
+      val elim_abs = elim_construct (fn \<^Const_>\<open>abs \<^Type>\<open>real\<close> for _\<close> => true | _ => false)
         (fn P => fn a =>
-          Thm.instantiate (TVars.empty, Vars.make [(p_v,P), (x_v, Thm.dest_arg a)]) pth_abs)
-      val elim_max = eliminate_construct is_max
+          let val x = Thm.dest_arg a in
+            \<^instantiate>\<open>P and x in
+              lemma \<open>P \<bar>x\<bar> \<equiv> (x \<ge> 0 \<and> P x \<or> x < 0 \<and> P (- x))\<close> for x :: real
+                by (atomize (full)) (auto split: abs_split)\<close>
+          end)
+      val elim_max = elim_construct (fn \<^Const_>\<open>max \<^Type>\<open>real\<close> for _ _\<close> => true | _ => false)
         (fn P => fn a =>
-          let val (x, y) = Thm.dest_binop a
-          in Thm.instantiate (TVars.empty, Vars.make [(p_v,P), (x_v,x), (y_v,y)]) pth_max end)
-      val elim_min = eliminate_construct is_min
+          let val (x, y) = Thm.dest_binop a in
+            \<^instantiate>\<open>P and x and y in
+              lemma \<open>P (max x y) \<equiv> (x \<le> y \<and> P y \<or> x > y \<and> P x)\<close> for x y :: real
+                by (atomize (full)) (auto simp add: max_def)\<close>
+          end)
+      val elim_min = elim_construct (fn \<^Const_>\<open>min \<^Type>\<open>real\<close> for _ _\<close> => true | _ => false)
         (fn P => fn a =>
-          let val (x, y) = Thm.dest_binop a
-          in Thm.instantiate (TVars.empty, Vars.make [(p_v,P), (x_v,x), (y_v,y)]) pth_min end)
+          let val (x, y) = Thm.dest_binop a in
+            \<^instantiate>\<open>P and x and y in
+              lemma \<open>P (min x y) \<equiv> (x \<le> y \<and> P x \<or> x > y \<and> P y)\<close> for x y :: real
+                by (atomize (full)) (auto simp add: min_def)\<close>
+          end)
     in first_conv [elim_abs, elim_max, elim_min, all_conv] end;
 in
 fun gen_real_arith ctxt (mkconst,eq,ge,gt,norm,neg,add,mul,prover) =