# HG changeset patch
# User wenzelm
# Date 1635505491 -7200
# Node ID 9b1d33c7bbccaceb4abe7bcfc26c7b0dbe86b254
# Parent  9568db8f48828517fb211e2a1dd879ef42e97fdb
clarified antiquotations;

diff -r 9568db8f4882 -r 9b1d33c7bbcc src/HOL/Library/Sum_of_Squares/positivstellensatz.ML
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Fri Oct 29 12:42:06 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Fri Oct 29 13:04:51 2021 +0200
@@ -315,9 +315,6 @@
 
 fun is_comb t = (case Thm.term_of t of _ $ _ => true | _ => false);
 
-fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
-  handle CTERM _ => false;
-
 
 (* Map back polynomials to HOL.                         *)
 
@@ -550,21 +547,21 @@
           | _ => (acc,t)
       in fn t => h ([],t)
       end
-
-    fun f ct =
+  in
+    fn A =>
       let
         val nnf_norm_conv' =
           nnf_conv ctxt then_conv
-          literals_conv [\<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>] []
+          literals_conv [\<^Const>\<open>conj\<close>, \<^Const>\<open>disj\<close>] []
           (Conv.cache_conv
             (first_conv [real_lt_conv, real_le_conv,
                          real_eq_conv, real_not_lt_conv,
                          real_not_le_conv, real_not_eq_conv, all_conv]))
-        fun absremover ct = (literals_conv [\<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>] []
+        fun absremover ct = (literals_conv [\<^Const>\<open>conj\<close>, \<^Const>\<open>disj\<close>] []
                   (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv
                   try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
-        val nct = \<^instantiate>\<open>A = ct in cprop \<open>\<not> A\<close>\<close>
-        val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
+        val not_A = \<^instantiate>\<open>A in cprop \<open>\<not> A\<close>\<close>
+        val th0 = (init_conv then_conv arg_conv nnf_norm_conv') not_A
         val tm0 = Thm.dest_arg (Thm.rhs_of th0)
         val (th, certificates) =
           if tm0 aconvc \<^cterm>\<open>False\<close> then (equal_implies_1_rule th0, Trivial) else
@@ -576,13 +573,12 @@
             val th3 =
               fold simple_choose evs
                 (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> bod))) th2)
-          in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
+          in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume not_A)) th3), certs)
           end
       in
-        (Thm.implies_elim \<^instantiate>\<open>A = ct in lemma \<open>(\<not> A \<Longrightarrow> False) \<Longrightarrow> A\<close> by blast\<close> th,
+        (Thm.implies_elim \<^instantiate>\<open>A in lemma \<open>(\<not> A \<Longrightarrow> False) \<Longrightarrow> A\<close> by blast\<close> th,
           certificates)
       end
-  in f
   end;
 
 (* A linear arithmetic prover *)
diff -r 9568db8f4882 -r 9b1d33c7bbcc src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Fri Oct 29 12:42:06 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Fri Oct 29 13:04:51 2021 +0200
@@ -105,7 +105,7 @@
 val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
 
 fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
-  (fn (x, k) => (Thm.cterm_of ctxt (Free (x, \<^typ>\<open>real\<close>)), k))
+  (fn (x, k) => (Thm.cterm_of ctxt (Free (x, \<^Type>\<open>real\<close>)), k))
 
 fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
   (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)
diff -r 9568db8f4882 -r 9b1d33c7bbcc src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Oct 29 12:42:06 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Oct 29 13:04:51 2021 +0200
@@ -270,7 +270,7 @@
         end handle CTERM ("dest_comb",_) => poly_var tm)
 in
   val poly_of_term = fn tm =>
-    if type_of (Thm.term_of tm) = \<^typ>\<open>real\<close>
+    if type_of (Thm.term_of tm) = \<^Type>\<open>real\<close>
     then poly_of_term tm
     else error "poly_of_term: term does not have real type"
 end;
@@ -852,22 +852,22 @@
   open Conv
   val concl = Thm.dest_arg o Thm.cprop_of
   val shuffle1 =
-    fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))"
+    fconv_rule (rewr_conv @{lemma "(a + x \<equiv> y) \<equiv> (x \<equiv> y - a)" for a x y :: real
       by (atomize (full)) (simp add: field_simps)})
   val shuffle2 =
-    fconv_rule (rewr_conv @{lemma "(x + a == y) ==  (x == y - (a::real))"
+    fconv_rule (rewr_conv @{lemma "(x + a \<equiv> y) \<equiv> (x \<equiv> y - a)" for a x y :: real
       by (atomize (full)) (simp add: field_simps)})
   fun substitutable_monomial fvs tm =
     (case Thm.term_of tm of
-      Free (_, \<^typ>\<open>real\<close>) =>
+      Free (_, \<^Type>\<open>real\<close>) =>
         if not (Cterms.defined fvs tm) then (@1, tm)
         else raise Failure "substitutable_monomial"
-    | \<^term>\<open>(*) :: real \<Rightarrow> _\<close> $ _ $ (Free _) =>
+    | \<^Const_>\<open>times \<^typ>\<open>real\<close> for _ \<open>Free _\<close>\<close> =>
         if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso
           not (Cterms.defined fvs (Thm.dest_arg tm))
         then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
         else raise Failure "substitutable_monomial"
-    | \<^term>\<open>(+) :: real \<Rightarrow> _\<close>$_$_ =>
+    | \<^Const_>\<open>plus \<^Type>\<open>real\<close> for _ _\<close> =>
          (substitutable_monomial (Drule.add_frees_cterm (Thm.dest_arg tm) fvs)
            (Thm.dest_arg1 tm)
            handle Failure _ =>
@@ -882,7 +882,7 @@
       if v aconvc w then th
       else
         (case Thm.term_of w of
-          \<^term>\<open>(+) :: real \<Rightarrow> _\<close> $ _ $ _ =>
+          \<^Const_>\<open>plus \<^Type>\<open>real\<close> for _ _\<close> =>
             if Thm.dest_arg1 w aconvc v then shuffle2 th
             else isolate_variable v (shuffle1 th)
         | _ => error "isolate variable : This should not happen?")
@@ -938,21 +938,21 @@
 end;
 
 val known_sos_constants =
-  [\<^term>\<open>(\<Longrightarrow>)\<close>, \<^term>\<open>Trueprop\<close>,
-   \<^term>\<open>HOL.False\<close>, \<^term>\<open>HOL.implies\<close>, \<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>,
-   \<^term>\<open>Not\<close>, \<^term>\<open>(=) :: bool \<Rightarrow> _\<close>,
-   \<^term>\<open>All :: (real \<Rightarrow> _) \<Rightarrow> _\<close>, \<^term>\<open>Ex :: (real \<Rightarrow> _) \<Rightarrow> _\<close>,
-   \<^term>\<open>(=) :: real \<Rightarrow> _\<close>, \<^term>\<open>(<) :: real \<Rightarrow> _\<close>,
-   \<^term>\<open>(\<le>) :: real \<Rightarrow> _\<close>,
-   \<^term>\<open>(+) :: real \<Rightarrow> _\<close>, \<^term>\<open>(-) :: real \<Rightarrow> _\<close>,
-   \<^term>\<open>(*) :: real \<Rightarrow> _\<close>, \<^term>\<open>uminus :: real \<Rightarrow> _\<close>,
-   \<^term>\<open>(/) :: real \<Rightarrow> _\<close>, \<^term>\<open>inverse :: real \<Rightarrow> _\<close>,
-   \<^term>\<open>(^) :: real \<Rightarrow> _\<close>, \<^term>\<open>abs :: real \<Rightarrow> _\<close>,
-   \<^term>\<open>min :: real \<Rightarrow> _\<close>, \<^term>\<open>max :: real \<Rightarrow> _\<close>,
-   \<^term>\<open>0::real\<close>, \<^term>\<open>1::real\<close>,
-   \<^term>\<open>numeral :: num \<Rightarrow> nat\<close>,
-   \<^term>\<open>numeral :: num \<Rightarrow> real\<close>,
-   \<^term>\<open>Num.Bit0\<close>, \<^term>\<open>Num.Bit1\<close>, \<^term>\<open>Num.One\<close>];
+  [\<^Const>\<open>Pure.imp\<close>, \<^Const>\<open>Trueprop\<close>,
+   \<^Const>\<open>False\<close>, \<^Const>\<open>implies\<close>, \<^Const>\<open>conj\<close>, \<^Const>\<open>disj\<close>,
+   \<^Const>\<open>Not\<close>, \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close>\<close>,
+   \<^Const>\<open>All \<^Type>\<open>real\<close>\<close>, \<^Const>\<open>Ex \<^Type>\<open>real\<close>\<close>,
+   \<^Const>\<open>HOL.eq \<^Type>\<open>real\<close>\<close>, \<^Const>\<open>less \<^Type>\<open>real\<close>\<close>,
+   \<^Const>\<open>less_eq \<^Type>\<open>real\<close>\<close>,
+   \<^Const>\<open>plus \<^Type>\<open>real\<close>\<close>, \<^Const>\<open>minus \<^Type>\<open>real\<close>\<close>,
+   \<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, \<^Const>\<open>uminus \<^Type>\<open>real\<close>\<close>,
+   \<^Const>\<open>divide \<^Type>\<open>real\<close>\<close>, \<^Const>\<open>inverse \<^Type>\<open>real\<close>\<close>,
+   \<^Const>\<open>power \<^Type>\<open>real\<close>\<close>, \<^Const>\<open>abs \<^Type>\<open>real\<close>\<close>,
+   \<^Const>\<open>min \<^Type>\<open>real\<close>\<close>, \<^Const>\<open>max \<^Type>\<open>real\<close>\<close>,
+   \<^Const>\<open>zero_class.zero \<^Type>\<open>real\<close>\<close>, \<^Const>\<open>one_class.one \<^Type>\<open>real\<close>\<close>,
+   \<^Const>\<open>numeral \<^Type>\<open>nat\<close>\<close>,
+   \<^Const>\<open>numeral \<^Type>\<open>real\<close>\<close>,
+   \<^Const>\<open>Num.Bit0\<close>, \<^Const>\<open>Num.Bit1\<close>, \<^Const>\<open>Num.One\<close>];
 
 fun check_sos kcts ct =
   let
@@ -963,12 +963,12 @@
       else ()
     val fs = Term.add_frees t []
     val _ =
-      if exists (fn ((_,T)) => not (T = \<^typ>\<open>real\<close>)) fs
+      if exists (fn ((_,T)) => T <> \<^Type>\<open>real\<close>) fs
       then error "SOS: not sos. Variables with type not real"
       else ()
     val vs = Term.add_vars t []
     val _ =
-      if exists (fn ((_,T)) => not (T = \<^typ>\<open>real\<close>)) vs
+      if exists (fn ((_,T)) => T <> \<^Type>\<open>real\<close>) vs
       then error "SOS: not sos. Variables with type not real"
       else ()
     val ukcs = subtract (fn (t,p) => Const p aconv t) kcts (Term.add_consts t [])
@@ -996,13 +996,13 @@
 in
   fun get_denom b ct =
     (case Thm.term_of ct of
-      \<^term>\<open>(/) :: real \<Rightarrow> _\<close> $ _ $ _ =>
+      \<^Const_>\<open>divide \<^Type>\<open>real\<close> for _ _\<close> =>
         if is_numeral (Thm.dest_arg ct)
         then get_denom b (Thm.dest_arg1 ct)
         else default_SOME (get_denom b) (get_denom b (Thm.dest_arg ct)) (Thm.dest_arg ct, b)
-    | \<^term>\<open>(<) :: real \<Rightarrow> _\<close> $ _ $ _ =>
+    | \<^Const_>\<open>less \<^Type>\<open>real\<close> for _ _\<close> =>
         lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
-    | \<^term>\<open>(\<le>) :: real \<Rightarrow> _\<close> $ _ $ _ =>
+    | \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for _ _\<close> =>
         lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
     | _ $ _ => lift_SOME (get_denom b) (get_denom b (Thm.dest_fun ct)) (Thm.dest_arg ct)
     | _ => NONE)