# HG changeset patch
# User wenzelm
# Date 1724002652 -7200
# Node ID bb292fc53f82b1b1cced9b9602b54c4a0158bfa3
# Parent  49067bf1cf9253e3cc6100f46fbc7a522334a00f
tuned: more antiquotations;

diff -r 49067bf1cf92 -r bb292fc53f82 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sun Aug 18 18:51:31 2024 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Sun Aug 18 19:37:32 2024 +0200
@@ -49,22 +49,16 @@
           in Thm.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
             (p (fold (Logic.all o Var) vs t) f)
           end;
-        fun mkop \<^const_name>\<open>HOL.conj\<close> T x =
-              SOME (Const (\<^const_name>\<open>Lattices.inf\<close>, T --> T --> T), x)
-          | mkop \<^const_name>\<open>HOL.disj\<close> T x =
-              SOME (Const (\<^const_name>\<open>Lattices.sup\<close>, T --> T --> T), x)
-          | mkop _ _ _ = NONE;
-        fun mk_collect p T t =
-          let val U = HOLogic.dest_setT T
-          in HOLogic.Collect_const U $
-            HOLogic.mk_ptupleabs (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
-          end;
-        fun decomp (Const (s, _) $ ((m as Const (\<^const_name>\<open>Set.member\<close>,
-              Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
-                mkop s T (m, p, S, mk_collect p T (head_of u))
-          | decomp (Const (s, _) $ u $ ((m as Const (\<^const_name>\<open>Set.member\<close>,
-              Type (_, [_, Type (_, [T, _])]))) $ p $ S)) =
-                mkop s T (m, p, mk_collect p T (head_of u), S)
+        fun mk_collect p A t =
+          \<^Const>\<open>Collect A for \<open>HOLogic.mk_ptupleabs (HOLogic.flat_tuple_paths p) A \<^Type>\<open>bool\<close> t\<close>\<close>;
+        fun decomp \<^Const_>\<open>conj for \<open>(m as \<^Const_>\<open>Set.member A\<close>) $ p $ S\<close> u\<close> =
+              SOME (\<^Const>\<open>inf \<^Type>\<open>set A\<close>\<close>, (m, p, S, mk_collect p A (head_of u)))
+          | decomp \<^Const_>\<open>conj for u \<open>(m as \<^Const_>\<open>Set.member A\<close>) $ p $ S\<close>\<close> =
+              SOME (\<^Const>\<open>inf \<^Type>\<open>set A\<close>\<close>, (m, p, mk_collect p A (head_of u), S))
+          | decomp \<^Const_>\<open>disj for \<open>(m as \<^Const_>\<open>Set.member A\<close>) $ p $ S\<close> u\<close> =
+              SOME (\<^Const>\<open>sup \<^Type>\<open>set A\<close>\<close>, (m, p, S, mk_collect p A (head_of u)))
+          | decomp \<^Const_>\<open>disj for u \<open>(m as \<^Const_>\<open>Set.member A\<close>) $ p $ S\<close>\<close> =
+              SOME (\<^Const>\<open>sup \<^Type>\<open>set A\<close>\<close>, (m, p, mk_collect p A (head_of u), S))
           | decomp _ = NONE;
         val simp =
           full_simp_tac
@@ -210,13 +204,12 @@
     let
       val (Ts, T) = strip_type (fastype_of x);
       val U = HOLogic.dest_setT T;
-      val x' = map_type
-        (K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
+      val x' = map_type (K (Ts @ HOLogic.strip_ptupleT ps U ---> \<^Type>\<open>bool\<close>)) x;
     in
       (dest_Var x,
        Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
-         (HOLogic.Collect_const U $
-            HOLogic.mk_ptupleabs ps U HOLogic.boolT
+         (\<^Const>\<open>Collect U\<close> $
+            HOLogic.mk_ptupleabs ps U \<^Type>\<open>bool\<close>
               (list_comb (x', map Bound (length Ts - 1 downto 0))))))
     end) fs;
 
@@ -236,9 +229,9 @@
               dest_comb |> snd |> strip_comb |> snd |> hd |> dest_comb;
           in
             thm' RS (infer_instantiate ctxt [(arg_cong_f,
-              Thm.cterm_of ctxt (Abs ("P", Ts ---> HOLogic.boolT,
-                HOLogic.Collect_const U $ HOLogic.mk_ptupleabs fs' U
-                  HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
+              Thm.cterm_of ctxt (Abs ("P", Ts ---> \<^Type>\<open>bool\<close>,
+                \<^Const>\<open>Collect U\<close> $ HOLogic.mk_ptupleabs fs' U
+                  \<^Type>\<open>bool\<close> (Bound 0))))] arg_cong' RS sym)
           end)
   in
     Simplifier.simplify
@@ -254,14 +247,14 @@
 
 fun add context thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
   (case Thm.prop_of thm of
-    Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) $ lhs $ rhs) =>
+    \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq T for lhs rhs\<close>\<close> =>
       (case body_type T of
-         \<^typ>\<open>bool\<close> =>
+         \<^Type>\<open>bool\<close> =>
            let
              val thy = Context.theory_of context;
              val ctxt = Context.proof_of context;
              fun factors_of t fs = case strip_abs_body t of
-                 Const (\<^const_name>\<open>Set.member\<close>, _) $ u $ S =>
+                 \<^Const_>\<open>Set.member _ for u S\<close> =>
                    if is_Free S orelse is_Var S then
                      let val ps = HOLogic.flat_tuple_paths u
                      in (SOME ps, (S, ps) :: fs) end
@@ -271,7 +264,7 @@
              val (pfs, fs) = fold_map factors_of ts [];
              val ((h', ts'), fs') = (case rhs of
                  Abs _ => (case strip_abs_body rhs of
-                     Const (\<^const_name>\<open>Set.member\<close>, _) $ u $ S =>
+                     \<^Const_>\<open>Set.member _ for u S\<close> =>
                        (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
                    | _ => raise Malformed "member symbol on right-hand side expected")
                | _ => (strip_comb rhs, NONE))
@@ -410,7 +403,7 @@
     val {set_arities, pred_arities, to_pred_simps, ...} =
       Data.get (Context.Proof lthy);
     fun infer (Abs (_, _, t)) = infer t
-      | infer (Const (\<^const_name>\<open>Set.member\<close>, _) $ t $ u) =
+      | infer \<^Const_>\<open>Set.member _ for t u\<close> =
           infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
       | infer (t $ u) = infer t #> infer u
       | infer _ = I;
@@ -423,11 +416,10 @@
           let
             val T = HOLogic.dest_setT (fastype_of x);
             val Ts = HOLogic.strip_ptupleT fs T;
-            val x' = map_type (K (Ts ---> HOLogic.boolT)) x
+            val x' = map_type (K (Ts ---> \<^Type>\<open>bool\<close>)) x
           in
             (x, (x',
-              (HOLogic.Collect_const T $
-                 HOLogic.mk_ptupleabs fs T HOLogic.boolT x',
+              (\<^Const>\<open>Collect T\<close> $ HOLogic.mk_ptupleabs fs T \<^Type>\<open>bool\<close> x',
                fold_rev (Term.abs o pair "x") Ts
                  (HOLogic.mk_mem
                    (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)), x)))))
@@ -449,13 +441,11 @@
            Pretty.block (Pretty.commas (map (Syntax.pretty_typ lthy) paramTs)),
            Pretty.str "of declared parameters"]));
         val Ts = HOLogic.strip_ptupleT fs U;
-        val c' = Free (s ^ "p",
-          map fastype_of params1 @ Ts ---> HOLogic.boolT)
+        val c' = Free (s ^ "p", map fastype_of params1 @ Ts ---> \<^Type>\<open>bool\<close>)
       in
         ((c', (fs, U, Ts)),
          (list_comb (c, params2),
-          HOLogic.Collect_const U $ HOLogic.mk_ptupleabs fs U HOLogic.boolT
-            (list_comb (c', params1))))
+          \<^Const>\<open>Collect U\<close> $ HOLogic.mk_ptupleabs fs U \<^Type>\<open>bool\<close> (list_comb (c', params1))))
       end) |> split_list |>> split_list;
     val eqns' = eqns @
       map (Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)
@@ -484,8 +474,8 @@
       |> fold_map Local_Theory.define
         (map (fn (((b, mx), (fs, U, _)), p) =>
           ((b, mx), ((Thm.def_binding b, []),
-            fold_rev lambda params (HOLogic.Collect_const U $
-              HOLogic.mk_ptupleabs fs U HOLogic.boolT (list_comb (p, params3))))))
+            fold_rev lambda params (\<^Const>\<open>Collect U\<close> $
+              HOLogic.mk_ptupleabs fs U \<^Type>\<open>bool\<close> (list_comb (p, params3))))))
             (cnames_syn ~~ cs_info ~~ preds));
 
     (* prove theorems for converting predicate to set notation *)