# HG changeset patch
# User wenzelm
# Date 1632130527 -7200
# Node ID 5c452041fe838b91c8cd8f78bf59a9f4f830fda8
# Parent  714e87ce6e9d30094b17782569f9b90bb0337a88
clarified antiquotations;

diff -r 714e87ce6e9d -r 5c452041fe83 src/HOL/Tools/Argo/argo_real.ML
--- a/src/HOL/Tools/Argo/argo_real.ML	Sun Sep 19 21:55:11 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_real.ML	Mon Sep 20 11:35:27 2021 +0200
@@ -9,63 +9,62 @@
 
 (* translating input terms *)
 
-fun trans_type _ \<^typ>\<open>Real.real\<close> tcx = SOME (Argo_Expr.Real, tcx)
+fun trans_type _ \<^Type>\<open>real\<close> tcx = SOME (Argo_Expr.Real, tcx)
   | trans_type _ _ _ = NONE
 
-fun trans_term f (@{const Groups.uminus_class.uminus (real)} $ t) tcx =
+fun trans_term f \<^Const_>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
       tcx |> f t |>> Argo_Expr.mk_neg |> SOME
-  | trans_term f (@{const Groups.plus_class.plus (real)} $ t1 $ t2) tcx =
+  | trans_term f \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_add2 |> SOME
-  | trans_term f (@{const Groups.minus_class.minus (real)} $ t1 $ t2) tcx =
+  | trans_term f \<^Const_>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_sub |> SOME
-  | trans_term f (@{const Groups.times_class.times (real)} $ t1 $ t2) tcx =
+  | trans_term f \<^Const_>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_mul |> SOME
-  | trans_term f (@{const Rings.divide_class.divide (real)} $ t1 $ t2) tcx =
+  | trans_term f \<^Const_>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_div |> SOME
-  | trans_term f (@{const Orderings.ord_class.min (real)} $ t1 $ t2) tcx =
+  | trans_term f \<^Const_>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_min |> SOME
-  | trans_term f (@{const Orderings.ord_class.max (real)} $ t1 $ t2) tcx =
+  | trans_term f \<^Const_>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_max |> SOME
-  | trans_term f (@{const Groups.abs_class.abs (real)} $ t) tcx =
+  | trans_term f \<^Const_>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
       tcx |> f t |>> Argo_Expr.mk_abs |> SOME
-  | trans_term f (@{const Orderings.ord_class.less (real)} $ t1 $ t2) tcx =
+  | trans_term f \<^Const_>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_lt |> SOME
-  | trans_term f (@{const Orderings.ord_class.less_eq (real)} $ t1 $ t2) tcx =
+  | trans_term f \<^Const_>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
       tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_le |> SOME
   | trans_term _ t tcx =
       (case try HOLogic.dest_number t of
-        SOME (\<^typ>\<open>Real.real\<close>, n) => SOME (Argo_Expr.mk_num (Rat.of_int n), tcx)
+        SOME (\<^Type>\<open>real\<close>, n) => SOME (Argo_Expr.mk_num (Rat.of_int n), tcx)
       | _ => NONE)
 
 
 (* reverse translation *)
 
-fun mk_plus t1 t2 = @{const Groups.plus_class.plus (real)} $ t1 $ t2
+fun mk_plus t1 t2 = \<^Const>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
 fun mk_sum ts = uncurry (fold_rev mk_plus) (split_last ts)
-fun mk_times t1 t2 = @{const Groups.times_class.times (real)} $ t1 $ t2
-fun mk_divide t1 t2 = @{const Rings.divide_class.divide (real)} $ t1 $ t2
-fun mk_le t1 t2 = @{const Orderings.ord_class.less_eq (real)} $ t1 $ t2
-fun mk_lt t1 t2 = @{const Orderings.ord_class.less (real)} $ t1 $ t2
+fun mk_times t1 t2 = \<^Const>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_divide t1 t2 = \<^Const>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_le t1 t2 = \<^Const>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_lt t1 t2 = \<^Const>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
 
-fun mk_real_num i = HOLogic.mk_number \<^typ>\<open>Real.real\<close> i
+fun mk_real_num i = HOLogic.mk_number \<^Type>\<open>real\<close> i
 
 fun mk_number n =
   let val (p, q) = Rat.dest n
   in if q = 1 then mk_real_num p else mk_divide (mk_real_num p) (mk_real_num q) end
 
 fun term_of _ (Argo_Expr.E (Argo_Expr.Num n, _)) = SOME (mk_number n)
-  | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) =
-      SOME (@{const Groups.uminus_class.uminus (real)} $ f e)
+  | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = SOME \<^Const>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Add, es)) = SOME (mk_sum (map f es))
   | term_of f (Argo_Expr.E (Argo_Expr.Sub, [e1, e2])) =
-      SOME (@{const Groups.minus_class.minus (real)} $ f e1 $ f e2)
+      SOME \<^Const>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) = SOME (mk_times (f e1) (f e2))
   | term_of f (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) = SOME (mk_divide (f e1) (f e2))
   | term_of f (Argo_Expr.E (Argo_Expr.Min, [e1, e2])) =
-      SOME (@{const Orderings.ord_class.min (real)} $ f e1 $ f e2)
+      SOME \<^Const>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Max, [e1, e2])) =
-      SOME (@{const Orderings.ord_class.max (real)} $ f e1 $ f e2)
-  | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME (@{const Groups.abs_class.abs (real)} $ f e)
+      SOME \<^Const>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+  | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME \<^Const>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
   | term_of f (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (mk_le (f e1) (f e2))
   | term_of f (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (mk_lt (f e1) (f e2))
   | term_of _ _ = NONE
@@ -93,15 +92,15 @@
 fun inv_num_conv ctxt = nums_conv mk_divide (fn (_, n) => Rat.inv n) ctxt @1
 
 fun cmp_nums_conv ctxt b ct =
-  let val t = if b then \<^const>\<open>HOL.True\<close> else \<^const>\<open>HOL.False\<close>
+  let val t = if b then \<^Const>\<open>True\<close> else \<^Const>\<open>False\<close>
   in simp_conv ctxt (HOLogic.mk_eq (Thm.term_of ct, t)) ct end
 
 local
 
-fun is_add2 (@{const Groups.plus_class.plus (real)} $ _ $ _) = true
+fun is_add2 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ _\<close> = true
   | is_add2 _ = false
 
-fun is_add3 (@{const Groups.plus_class.plus (real)} $ _ $ t) = is_add2 t
+fun is_add3 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ t\<close> = is_add2 t
   | is_add3 _ = false
 
 val flatten_thm = mk_rewr @{lemma "(a::real) + b + c = a + (b + c)" by simp}
diff -r 714e87ce6e9d -r 5c452041fe83 src/HOL/Tools/Argo/argo_tactic.ML
--- a/src/HOL/Tools/Argo/argo_tactic.ML	Sun Sep 19 21:55:11 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML	Mon Sep 20 11:35:27 2021 +0200
@@ -144,8 +144,8 @@
     SOME ty => (ty, tcx)
   | NONE => add_new_type T tcx)
 
-fun trans_type _ \<^typ>\<open>HOL.bool\<close> = pair Argo_Expr.Bool
-  | trans_type ctxt (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
+fun trans_type _ \<^Type>\<open>bool\<close> = pair Argo_Expr.Bool
+  | trans_type ctxt \<^Type>\<open>fun T1 T2\<close> =
       trans_type ctxt T1 ##>> trans_type ctxt T2 #>> Argo_Expr.Func
   | trans_type ctxt T = (fn tcx =>
       (case ext_trans_type ctxt (trans_type ctxt) T tcx of
@@ -164,23 +164,23 @@
     SOME c => (Argo_Expr.mk_con c, tcx)
   | NONE => add_new_term ctxt t (Term.fastype_of t) tcx)
 
-fun mk_eq \<^typ>\<open>HOL.bool\<close> = Argo_Expr.mk_iff
+fun mk_eq \<^Type>\<open>bool\<close> = Argo_Expr.mk_iff
   | mk_eq _ = Argo_Expr.mk_eq
 
-fun trans_term _ \<^const>\<open>HOL.True\<close> = pair Argo_Expr.true_expr
-  | trans_term _ \<^const>\<open>HOL.False\<close> = pair Argo_Expr.false_expr
-  | trans_term ctxt (\<^const>\<open>HOL.Not\<close> $ t) = trans_term ctxt t #>> Argo_Expr.mk_not
-  | trans_term ctxt (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
+fun trans_term _ \<^Const_>\<open>True\<close> = pair Argo_Expr.true_expr
+  | trans_term _ \<^Const_>\<open>False\<close> = pair Argo_Expr.false_expr
+  | trans_term ctxt \<^Const_>\<open>Not for t\<close> = trans_term ctxt t #>> Argo_Expr.mk_not
+  | trans_term ctxt \<^Const_>\<open>conj for t1 t2\<close> =
       trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_and2
-  | trans_term ctxt (\<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+  | trans_term ctxt \<^Const_>\<open>disj for t1 t2\<close> =
       trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_or2
-  | trans_term ctxt (\<^const>\<open>HOL.implies\<close> $ t1 $ t2) =
+  | trans_term ctxt \<^Const_>\<open>implies for t1 t2\<close> =
       trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_imp
-  | trans_term ctxt (Const (\<^const_name>\<open>HOL.If\<close>, _) $ t1 $ t2 $ t3) =
+  | trans_term ctxt \<^Const_>\<open>If _ for t1 t2 t3\<close> =
       trans_term ctxt t1 ##>> trans_term ctxt t2 ##>> trans_term ctxt t3 #>>
       (fn ((u1, u2), u3) => Argo_Expr.mk_ite u1 u2 u3)
-  | trans_term ctxt (Const (\<^const_name>\<open>HOL.eq\<close>, T) $ t1 $ t2) =
-      trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry (mk_eq (Term.domain_type T))
+  | trans_term ctxt \<^Const_>\<open>HOL.eq T for t1 t2\<close> =
+      trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry (mk_eq T)
   | trans_term ctxt (t as (t1 $ t2)) = (fn tcx =>
       (case ext_trans_term ctxt (trans_term ctxt) t tcx of
         SOME result => result
@@ -258,18 +258,16 @@
   | mk_nary' _ f ts = mk_nary f ts
 
 fun mk_ite t1 t2 t3 =
-  let
-    val T = Term.fastype_of t2
-    val ite = Const (\<^const_name>\<open>HOL.If\<close>, [\<^typ>\<open>HOL.bool\<close>, T, T] ---> T)
-  in ite $ t1 $ t2 $ t3 end
+  let val T = Term.fastype_of t2
+  in \<^Const>\<open>If T for t1 t2 t3\<close> end
 
-fun term_of _ (Argo_Expr.E (Argo_Expr.True, _)) = \<^const>\<open>HOL.True\<close>
-  | term_of _ (Argo_Expr.E (Argo_Expr.False, _)) = \<^const>\<open>HOL.False\<close>
+fun term_of _ (Argo_Expr.E (Argo_Expr.True, _)) = \<^Const>\<open>True\<close>
+  | term_of _ (Argo_Expr.E (Argo_Expr.False, _)) = \<^Const>\<open>False\<close>
   | term_of cx (Argo_Expr.E (Argo_Expr.Not, [e])) = HOLogic.mk_not (term_of cx e)
   | term_of cx (Argo_Expr.E (Argo_Expr.And, es)) =
-      mk_nary' \<^const>\<open>HOL.True\<close> HOLogic.mk_conj (map (term_of cx) es)
+      mk_nary' \<^Const>\<open>True\<close> HOLogic.mk_conj (map (term_of cx) es)
   | term_of cx (Argo_Expr.E (Argo_Expr.Or, es)) =
-      mk_nary' \<^const>\<open>HOL.False\<close> HOLogic.mk_disj (map (term_of cx) es)
+      mk_nary' \<^Const>\<open>False\<close> HOLogic.mk_disj (map (term_of cx) es)
   | term_of cx (Argo_Expr.E (Argo_Expr.Imp, [e1, e2])) =
       HOLogic.mk_imp (term_of cx e1, term_of cx e2)
   | term_of cx (Argo_Expr.E (Argo_Expr.Iff, [e1, e2])) =
@@ -289,7 +287,7 @@
         SOME t => t
       | NONE => raise Fail "bad expression")
 
-fun as_prop ct = Thm.apply \<^cterm>\<open>HOL.Trueprop\<close> ct
+fun as_prop ct = Thm.apply \<^cterm>\<open>Trueprop\<close> ct
 
 fun cterm_of ctxt cons e = Thm.cterm_of ctxt (term_of (ctxt, cons) e)
 fun cprop_of ctxt cons e = as_prop (cterm_of ctxt cons e)
@@ -317,7 +315,7 @@
 fun with_frees ctxt n mk =
   let
     val ns = map (fn i => "P" ^ string_of_int i) (0 upto (n - 1))
-    val ts = map (Free o rpair \<^typ>\<open>bool\<close>) ns
+    val ts = map (Free o rpair \<^Type>\<open>bool\<close>) ns
     val t = mk_nary HOLogic.mk_disj (mk ts)
   in prove_taut ctxt ns t end
 
@@ -374,12 +372,12 @@
 
 fun flat_conj_conv ct =
   (case Thm.term_of ct of
-    \<^const>\<open>HOL.conj\<close> $ _ $ _ => flatten_conv flat_conj_conv flatten_and_thm ct
+    \<^Const_>\<open>conj for _ _\<close> => flatten_conv flat_conj_conv flatten_and_thm ct
   | _ => Conv.all_conv ct)
 
 fun flat_disj_conv ct =
   (case Thm.term_of ct of
-    \<^const>\<open>HOL.disj\<close> $ _ $ _ => flatten_conv flat_disj_conv flatten_or_thm ct
+    \<^Const_>\<open>disj for _ _\<close> => flatten_conv flat_disj_conv flatten_or_thm ct
   | _ => Conv.all_conv ct)
 
 fun explode rule1 rule2 thm =
@@ -415,7 +413,7 @@
   in mk_rewr (discharge2 lhs rhs rule) end
 
 fun with_conj f g ct = iff_intro iff_conj_thm (f o explode_conj) g ct
-fun with_ndis f g ct = iff_intro iff_ndis_thm (f o explode_ndis) g (Thm.apply \<^cterm>\<open>HOL.Not\<close> ct)
+fun with_ndis f g ct = iff_intro iff_ndis_thm (f o explode_ndis) g (Thm.apply \<^cterm>\<open>Not\<close> ct)
 
 fun swap_indices n iss = map (fn i => find_index (fn is => member (op =) is i) iss) (0 upto (n - 1))
 fun sort_nary w f g (n, iss) = w (f (map hd iss)) (under_assumption (f (swap_indices n iss) o g))
@@ -485,7 +483,7 @@
   | replay_args_conv ctxt [c1, c2] ct = binop_conv (replay_conv ctxt c1) (replay_conv ctxt c2) ct
   | replay_args_conv ctxt (c :: cs) ct =
       (case Term.head_of (Thm.term_of ct) of
-        Const (\<^const_name>\<open>HOL.If\<close>, _) =>
+        \<^Const_>\<open>If _\<close> =>
           let val (cs', c') = split_last cs
           in Conv.combination_conv (replay_args_conv ctxt (c :: cs')) (replay_conv ctxt c') ct end
       | _ => binop_conv (replay_conv ctxt c) (replay_args_conv ctxt cs) ct)
@@ -521,7 +519,7 @@
 
 val unit_rule = @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not>P \<Longrightarrow> False) \<Longrightarrow> False" by fast}
 val unit_rule_var = Thm.dest_arg (Thm.dest_arg1 (Thm.cprem_of unit_rule 1))
-val bogus_ct = \<^cterm>\<open>HOL.True\<close>
+val bogus_ct = \<^cterm>\<open>True\<close>
 
 fun replay_unit_res lit (pthm, plits) (nthm, nlits) =
   let
@@ -544,7 +542,7 @@
 fun replay_hyp i ct =
   if i < 0 then (Thm.assume ct, [(~i, ct)])
   else
-    let val cu = as_prop (Thm.apply \<^cterm>\<open>HOL.Not\<close> (Thm.apply \<^cterm>\<open>HOL.Not\<close> (Thm.dest_arg ct)))
+    let val cu = as_prop (Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply \<^cterm>\<open>Not\<close> (Thm.dest_arg ct)))
     in (discharge (Thm.assume cu) dneg_rule, [(~i, cu)]) end
 
 
@@ -602,7 +600,7 @@
 
 fun unclausify (thm, lits) ls =
   (case (Thm.prop_of thm, lits) of
-    (\<^const>\<open>HOL.Trueprop\<close> $ \<^const>\<open>HOL.False\<close>, [(_, ct)]) =>
+    (\<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>False\<close>\<close>\<close>, [(_, ct)]) =>
       let val thm = Thm.implies_intr ct thm
       in (discharge thm unclausify_rule1 handle THM _ => discharge thm unclausify_rule2, ls) end
   | _ => (thm, Ord_List.union lit_ord lits ls))
@@ -669,22 +667,22 @@
   let val ct = Drule.strip_imp_concl (Thm.cprop_of thm)
   in
     (case Thm.term_of ct of
-      \<^const>\<open>HOL.Trueprop\<close> $ Var (_, \<^typ>\<open>HOL.bool\<close>) =>
-        instantiate (Thm.dest_arg ct) \<^cterm>\<open>HOL.False\<close> thm
-    | Var _ => instantiate ct \<^cprop>\<open>HOL.False\<close> thm
+      \<^Const_>\<open>Trueprop for \<open>Var (_, \<^Type>\<open>bool\<close>)\<close>\<close> =>
+        instantiate (Thm.dest_arg ct) \<^cterm>\<open>False\<close> thm
+    | Var _ => instantiate ct \<^cprop>\<open>False\<close> thm
     | _ => thm)
   end
 
 fun atomize_conv ctxt ct =
   (case Thm.term_of ct of
-    \<^const>\<open>HOL.Trueprop\<close> $ _ => Conv.all_conv
-  | \<^const>\<open>Pure.imp\<close> $ _ $ _ =>
+    \<^Const_>\<open>Trueprop for _\<close> => Conv.all_conv
+  | \<^Const_>\<open>Pure.imp for _ _\<close> =>
       Conv.binop_conv (atomize_conv ctxt) then_conv
       Conv.rewr_conv @{thm atomize_imp}
-  | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ =>
+  | \<^Const>\<open>Pure.eq _ for _ _\<close> =>
       Conv.binop_conv (atomize_conv ctxt) then_conv
       Conv.rewr_conv @{thm atomize_eq}
-  | Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs _ =>
+  | \<^Const>\<open>Pure.all _ for \<open>Abs _\<close>\<close> =>
       Conv.binder_conv (atomize_conv o snd) ctxt then_conv
       Conv.rewr_conv @{thm atomize_all}
   | _ => Conv.all_conv) ct