# HG changeset patch
# User wenzelm
# Date 1632932552 -7200
# Node ID dc73f9e6476b8758914517c4d02592b1e103e5e8
# Parent  5399dfe9141c2a7a0cb09d22da28219dbb5c0002
clarified antiquotations;

diff -r 5399dfe9141c -r dc73f9e6476b src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Sep 29 18:21:22 2021 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Sep 29 18:22:32 2021 +0200
@@ -91,19 +91,16 @@
       let val (prfx', s') = strip_prfx s
       in if prfx = prfx' then s' else s end;
 
-fun mk_unop s t =
+fun mk_uminus t =
   let val T = fastype_of t
-  in Const (s, T --> T) $ t end;
+  in \<^Const>\<open>uminus T for t\<close> end;
 
 fun mk_times (t, u) =
   let
     val setT = fastype_of t;
     val T = HOLogic.dest_setT setT;
     val U = HOLogic.dest_setT (fastype_of u)
-  in
-    Const (\<^const_name>\<open>Sigma\<close>, setT --> (T --> HOLogic.mk_setT U) -->
-      HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
-  end;
+  in \<^Const>\<open>Sigma T U for t \<open>Abs ("", T, u)\<close>\<close> end;
 
 fun get_type thy prfx ty =
   let val {type_map, ...} = VCs.get thy
@@ -177,16 +174,12 @@
     val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));
     val k = length cs;
     val T = Type (tyname', []);
-    val p = Const (\<^const_name>\<open>pos\<close>, T --> HOLogic.intT);
-    val v = Const (\<^const_name>\<open>val\<close>, HOLogic.intT --> T);
-    val card = Const (\<^const_name>\<open>card\<close>,
-      HOLogic.mk_setT T --> HOLogic.natT) $ HOLogic.mk_UNIV T;
+    val p = \<^Const>\<open>pos T\<close>;
+    val v = \<^Const>\<open>val T\<close>;
+    val card = \<^Const>\<open>card T for \<open>HOLogic.mk_UNIV T\<close>\<close>;
 
-    fun mk_binrel_def s f = Logic.mk_equals
-      (Const (s, T --> T --> HOLogic.boolT),
-       Abs ("x", T, Abs ("y", T,
-         Const (s, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $
-           (f $ Bound 1) $ (f $ Bound 0))));
+    fun mk_binrel_def rel f = Logic.mk_equals
+      (rel T, Abs ("x", T, Abs ("y", T, rel \<^Type>\<open>int\<close> $ (f $ Bound 1) $ (f $ Bound 0))));
 
     val (((def1, def2), def3), lthy) = thy |>
 
@@ -199,9 +192,9 @@
            map (HOLogic.mk_number HOLogic.intT) (0 upto k - 1)))) ||>>
 
       define_overloaded ("less_eq_" ^ tyname ^ "_def",
-        mk_binrel_def \<^const_name>\<open>less_eq\<close> p) ||>>
+        mk_binrel_def (fn T => \<^Const>\<open>less_eq T\<close>) p) ||>>
       define_overloaded ("less_" ^ tyname ^ "_def",
-        mk_binrel_def \<^const_name>\<open>less\<close> p);
+        mk_binrel_def (fn T => \<^Const>\<open>less T\<close>) p);
 
     val UNIV_eq = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -214,8 +207,7 @@
          ALLGOALS (asm_full_simp_tac ctxt));
 
     val finite_UNIV = Goal.prove lthy [] []
-      (HOLogic.mk_Trueprop (Const (\<^const_name>\<open>finite\<close>,
-         HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T))
+      (HOLogic.mk_Trueprop \<^Const>\<open>finite T for \<open>HOLogic.mk_UNIV T\<close>\<close>)
       (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1);
 
     val card_UNIV = Goal.prove lthy [] []
@@ -225,13 +217,9 @@
 
     val range_pos = Goal.prove lthy [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Const (\<^const_name>\<open>image\<close>, (T --> HOLogic.intT) -->
-            HOLogic.mk_setT T --> HOLogic.mk_setT HOLogic.intT) $
-              p $ HOLogic.mk_UNIV T,
-          Const (\<^const_name>\<open>atLeastLessThan\<close>, HOLogic.intT -->
-            HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $
-              HOLogic.mk_number HOLogic.intT 0 $
-              (\<^term>\<open>int\<close> $ card))))
+         (\<^Const>\<open>image T \<^Type>\<open>int\<close> for p \<open>HOLogic.mk_UNIV T\<close>\<close>,
+          \<^Const>\<open>atLeastLessThan \<^Type>\<open>int\<close>
+            for \<open>HOLogic.mk_number HOLogic.intT 0\<close> \<open>\<^term>\<open>int\<close> $ card\<close>\<close>)))
       (fn {context = ctxt, ...} =>
          simp_tac (ctxt addsimps [card_UNIV]) 1 THEN
          simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN
@@ -263,13 +251,11 @@
       in (th, th') end) cs);
 
     val first_el = Goal.prove lthy' [] []
-      (HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Const (\<^const_name>\<open>first_el\<close>, T), hd cs)))
+      (HOLogic.mk_Trueprop (HOLogic.mk_eq (\<^Const>\<open>first_el T\<close>, hd cs)))
       (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1);
 
     val last_el = Goal.prove lthy' [] []
-      (HOLogic.mk_Trueprop (HOLogic.mk_eq
-         (Const (\<^const_name>\<open>last_el\<close>, T), List.last cs)))
+      (HOLogic.mk_Trueprop (HOLogic.mk_eq (\<^Const>\<open>last_el T\<close>, List.last cs)))
       (fn {context = ctxt, ...} =>
         simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1);
   in
@@ -444,13 +430,10 @@
       | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop \<^const_name>\<open>modulo\<close>
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("-", [e])) =
-          (mk_unop \<^const_name>\<open>uminus\<close> (fst (tm_of vs e)), integerN)
+      | tm_of vs (Funct ("-", [e])) = (mk_uminus (fst (tm_of vs e)), integerN)
 
       | tm_of vs (Funct ("**", [e, e'])) =
-          (Const (\<^const_name>\<open>power\<close>, HOLogic.intT --> HOLogic.natT -->
-             HOLogic.intT) $ fst (tm_of vs e) $
-               (\<^const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
+          (\<^Const>\<open>power \<^Type>\<open>int\<close>\<close> $ fst (tm_of vs e) $ (\<^Const>\<open>nat\<close> $ fst (tm_of vs e')), integerN)
 
       | tm_of (tab, _) (Ident s) =
           (case Symtab.lookup tab s of
@@ -528,18 +511,14 @@
           (* enumeration type to integer *)
           (case try (unsuffix "__pos") s of
              SOME tyname => (case es of
-               [e] => (Const (\<^const_name>\<open>pos\<close>,
-                   mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
-                 integerN)
+               [e] => (\<^Const>\<open>pos \<open>mk_type thy prfx tyname\<close> for \<open>fst (tm_of vs e)\<close>\<close>, integerN)
              | _ => error ("Function " ^ s ^ " expects one argument"))
            | NONE =>
 
           (* integer to enumeration type *)
           (case try (unsuffix "__val") s of
              SOME tyname => (case es of
-               [e] => (Const (\<^const_name>\<open>val\<close>,
-                   HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
-                 tyname)
+               [e] => (\<^Const>\<open>val \<open>mk_type thy prfx tyname\<close> for \<open>fst (tm_of vs e)\<close>\<close>, tyname)
              | _ => error ("Function " ^ s ^ " expects one argument"))
            | NONE =>
 
@@ -548,11 +527,9 @@
               [e] =>
                 let
                   val (t, tyname) = tm_of vs e;
-                  val T = mk_type thy prfx tyname
-                in (Const
-                  (if s = "succ" then \<^const_name>\<open>succ\<close>
-                   else \<^const_name>\<open>pred\<close>, T --> T) $ t, tyname)
-                end
+                  val T = mk_type thy prfx tyname;
+                  val const = if s = "succ" then \<^Const>\<open>succ T\<close> else \<^Const>\<open>pred T\<close>;
+                in (const $ t, tyname) end
             | _ => error ("Function " ^ s ^ " expects one argument"))
 
           (* user-defined proof function *)
@@ -578,11 +555,9 @@
                   val T = foldr1 HOLogic.mk_prodT
                     (map (mk_type thy prfx) idxtys);
                   val U = mk_type thy prfx elty;
-                  val fT = T --> U
                 in
-                  (Const (\<^const_name>\<open>fun_upd\<close>, fT --> T --> U --> fT) $
-                     t $ foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $
-                       fst (tm_of vs e'),
+                  (\<^Const>\<open>fun_upd T U\<close> $ t $
+                    foldr1 HOLogic.mk_prod (map (fst o tm_of vs) es) $ fst (tm_of vs e'),
                    ty)
                 end
             | _ => error (ty ^ " is not an array type")
@@ -628,9 +603,8 @@
                  val T = foldr1 HOLogic.mk_prodT Ts;
                  val U = mk_type thy prfx elty;
                  fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
-                   | mk_idx' T (e, SOME e') = Const (\<^const_name>\<open>atLeastAtMost\<close>,
-                       T --> T --> HOLogic.mk_setT T) $
-                         fst (tm_of vs e) $ fst (tm_of vs e');
+                   | mk_idx' T (e, SOME e') =
+                      \<^Const>\<open>atLeastAtMost T for \<open>fst (tm_of vs e)\<close> \<open>fst (tm_of vs e')\<close>\<close>;
                  fun mk_idx idx =
                    if length Ts <> length idx then
                      error ("Arity mismatch in construction of array " ^ s)
@@ -638,14 +612,12 @@
                  fun mk_upd (idxs, e) t =
                    if length idxs = 1 andalso forall (is_none o snd) (hd idxs)
                    then
-                     Const (\<^const_name>\<open>fun_upd\<close>, (T --> U) -->
-                         T --> U --> T --> U) $ t $
+                     \<^Const>\<open>fun_upd T U\<close> $ t $
                        foldl1 HOLogic.mk_prod
                          (map (fst o tm_of vs o fst) (hd idxs)) $
                        fst (tm_of vs e)
                    else
-                     Const (\<^const_name>\<open>fun_upds\<close>, (T --> U) -->
-                         HOLogic.mk_setT T --> U --> T --> U) $ t $
+                     \<^Const>\<open>fun_upds T U\<close> $ t $
                        foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>)
                          (map mk_idx idxs) $
                        fst (tm_of vs e)
@@ -653,7 +625,7 @@
                  (fold mk_upd assocs
                     (case default of
                        SOME e => Abs ("x", T, fst (tm_of vs e))
-                     | NONE => Const (\<^const_name>\<open>undefined\<close>, T --> U)),
+                     | NONE => \<^Const>\<open>undefined \<open>T --> U\<close>\<close>),
                   s)
                end
            | _ => error (s ^ " is not an array type"))