# HG changeset patch
# User wenzelm
# Date 1723999891 -7200
# Node ID 49067bf1cf9253e3cc6100f46fbc7a522334a00f
# Parent  5f13872a33ea16511cc16535b31070fd8340a800
tuned: more antiquotations;

diff -r 5f13872a33ea -r 49067bf1cf92 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Aug 18 18:08:16 2024 +0200
+++ b/src/HOL/Tools/inductive.ML	Sun Aug 18 18:51:31 2024 +0200
@@ -134,7 +134,7 @@
       (if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2);
 
 fun make_bool_args' xs =
-  make_bool_args (K \<^term>\<open>False\<close>) (K \<^term>\<open>True\<close>) xs;
+  make_bool_args (K \<^Const>\<open>False\<close>) (K \<^Const>\<open>True\<close>) xs;
 
 fun arg_types_of k c = drop k (binder_types (fastype_of c));
 
@@ -146,7 +146,7 @@
       else apsnd (cons p) (find_arg T x ps);
 
 fun make_args Ts xs =
-  map (fn (T, (NONE, ())) => Const (\<^const_name>\<open>undefined\<close>, T) | (_, (SOME t, ())) => t)
+  map (fn (T, (NONE, ())) => \<^Const>\<open>undefined T\<close> | (_, (SOME t, ())) => t)
     (fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts));
 
 fun make_args' Ts xs Us =
@@ -276,9 +276,9 @@
       handle THM _ => thm RS @{thm le_boolD}
   in
     (case Thm.concl_of thm of
-      Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ => eq_to_mono (HOLogic.mk_obj_eq thm)
-    | _ $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _) => eq_to_mono thm
-    | _ $ (Const (\<^const_name>\<open>Orderings.less_eq\<close>, _) $ _ $ _) =>
+      \<^Const_>\<open>Pure.eq _ for _ _\<close> => eq_to_mono (HOLogic.mk_obj_eq thm)
+    | _ $ \<^Const_>\<open>HOL.eq _ for _ _\<close> => eq_to_mono thm
+    | _ $ \<^Const_>\<open>less_eq _ for _ _\<close> =>
       dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
         (resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}])) thm))
     | _ => thm)
@@ -369,7 +369,7 @@
 
     val _ =
       (case concl of
-        Const (\<^const_name>\<open>Trueprop\<close>, _) $ t =>
+        \<^Const_>\<open>Trueprop for t\<close> =>
           if member (op =) cs (head_of t) then
            (check_ind (err_in_rule ctxt binding rule') t;
             List.app check_prem (prems ~~ aprems))
@@ -510,11 +510,11 @@
                   HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t));
             val conjs = map2 (curry HOLogic.mk_eq) frees us @ map HOLogic.dest_Trueprop ts;
           in
-            list_ex (params', if null conjs then \<^term>\<open>True\<close> else foldr1 HOLogic.mk_conj conjs)
+            list_ex (params', if null conjs then \<^Const>\<open>True\<close> else foldr1 HOLogic.mk_conj conjs)
           end;
         val lhs = list_comb (c, params @ frees);
         val rhs =
-          if null c_intrs then \<^term>\<open>False\<close>
+          if null c_intrs then \<^Const>\<open>False\<close>
           else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs);
         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
         fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
@@ -801,8 +801,7 @@
 
 (* prove coinduction rule *)
 
-fun If_const T = Const (\<^const_name>\<open>If\<close>, HOLogic.boolT --> T --> T --> T);
-fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
+fun mk_If p t f = let val T = fastype_of t in \<^Const>\<open>If T\<close> $ p $ t $ f end;
 
 fun prove_coindrule quiet_mode preds cs argTs bs xs params intr_ts mono
     fp_def rec_preds_defs ctxt ctxt''' =  (* FIXME ctxt''' ?? *)
@@ -813,20 +812,21 @@
       make_args' argTs xs (arg_types_of (length params) pred) |> `length) preds;
     val xTss = map (map fastype_of) xss;
     val (Rs_names, names_ctxt) = Variable.variant_fixes (mk_names "X" n) ctxt;
-    val Rs = map2 (fn name => fn Ts => Free (name, Ts ---> \<^typ>\<open>bool\<close>)) Rs_names xTss;
+    val Rs = map2 (fn name => fn Ts => Free (name, Ts ---> \<^Type>\<open>bool\<close>)) Rs_names xTss;
     val Rs_applied = map2 (curry list_comb) Rs xss;
     val preds_applied = map2 (curry list_comb) (map (fn p => list_comb (p, params)) preds) xss;
     val abstract_list = fold_rev (absfree o dest_Free);
     val bss = map (make_bool_args
-      (fn b => HOLogic.mk_eq (b, \<^term>\<open>False\<close>))
-      (fn b => HOLogic.mk_eq (b, \<^term>\<open>True\<close>)) bs) (0 upto n - 1);
+      (fn b => HOLogic.mk_eq (b, \<^Const>\<open>False\<close>))
+      (fn b => HOLogic.mk_eq (b, \<^Const>\<open>True\<close>)) bs) (0 upto n - 1);
     val eq_undefinedss = map (fn ys => map (fn x =>
-        HOLogic.mk_eq (x, Const (\<^const_name>\<open>undefined\<close>, fastype_of x)))
+        let val T = fastype_of x
+        in \<^Const>\<open>HOL.eq T for x \<^Const>\<open>undefined T\<close>\<close> end)
       (subtract (op =) ys xs)) xss;
     val R =
       @{fold 3} (fn bs => fn eqs => fn R => fn t => if null bs andalso null eqs then R else
         mk_If (Library.foldr1 HOLogic.mk_conj (bs @ eqs)) R t)
-      bss eq_undefinedss Rs_applied \<^term>\<open>False\<close>
+      bss eq_undefinedss Rs_applied \<^Const>\<open>False\<close>
       |> abstract_list (bs @ xs);
 
     fun subst t =
@@ -857,7 +857,7 @@
       in
         (i, fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
           (Logic.strip_params r)
-          (if null ps then \<^term>\<open>True\<close> else foldr1 HOLogic.mk_conj ps))
+          (if null ps then \<^Const>\<open>True\<close> else foldr1 HOLogic.mk_conj ps))
       end;
 
     fun mk_prem i Ps = Logic.mk_implies
@@ -920,11 +920,11 @@
 
 fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy =
   let
-    val fp_name = if coind then \<^const_name>\<open>Inductive.gfp\<close> else \<^const_name>\<open>Inductive.lfp\<close>;
-
     val argTs = fold (combine (op =) o arg_types_of (length params)) cs [];
     val k = log 2 1 (length cs);
     val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
+    val fp_const = if coind then \<^Const>\<open>gfp predT\<close> else \<^Const>\<open>lfp predT\<close>;
+
     val p :: xs =
       map Free (Variable.variant_frees lthy intr_ts
         (("p", predT) :: (mk_names "x" (length argTs) ~~ argTs)));
@@ -966,14 +966,14 @@
       in
         fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
           (Logic.strip_params r)
-          (if null ps then \<^term>\<open>True\<close> else foldr1 HOLogic.mk_conj ps)
+          (if null ps then \<^Const>\<open>True\<close> else foldr1 HOLogic.mk_conj ps)
       end;
 
     (* make a disjunction of all introduction rules *)
 
     val fp_fun =
       fold_rev lambda (p :: bs @ xs)
-        (if null intr_ts then \<^term>\<open>False\<close>
+        (if null intr_ts then \<^Const>\<open>False\<close>
          else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
 
     (* add definition of recursive predicates to theory *)
@@ -991,8 +991,7 @@
       |> Local_Theory.define
         ((rec_binding, case cnames_syn of [(_, mx)] => mx | _ => NoSyn),
          ((Thm.make_def_binding internals rec_binding, @{attributes [nitpick_unfold]}),
-           fold_rev lambda params
-             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
+           fold_rev lambda params (fp_const $ fp_fun)))
       ||> Proof_Context.restore_naming lthy;
     val fp_def' =
       Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])