# HG changeset patch
# User wenzelm
# Date 1722880643 -7200
# Node ID cc205e40192e8c257db22598a9c460052373bbcf
# Parent  3cde955e4e47ea079d8f71b22f2cda90c77fb5c6
tuned: more antiquotations;

diff -r 3cde955e4e47 -r cc205e40192e src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Aug 04 23:50:44 2024 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Aug 05 19:57:23 2024 +0200
@@ -18,73 +18,46 @@
 (* syntactic operations *)
 
 fun mk_inf (t1, t2) =
-  let
-    val T = fastype_of t1
-  in
-    Const (\<^const_name>\<open>Lattices.inf_class.inf\<close>, T --> T --> T) $ t1 $ t2
-  end
+  let val T = fastype_of t1
+  in \<^Const>\<open>inf T for t1 t2\<close> end
 
 fun mk_sup (t1, t2) =
-  let
-    val T = fastype_of t1
-  in
-    Const (\<^const_name>\<open>Lattices.sup_class.sup\<close>, T --> T --> T) $ t1 $ t2
-  end
+  let val T = fastype_of t1
+  in \<^Const>\<open>sup T for t1 t2\<close> end
 
 fun mk_Compl t =
-  let
-    val T = fastype_of t
-  in
-    Const (\<^const_name>\<open>Groups.uminus_class.uminus\<close>, T --> T) $ t
-  end
+  let val T = fastype_of t
+  in \<^Const>\<open>uminus T for t\<close> end
 
 fun mk_image t1 t2 =
-  let
-    val T as Type (\<^type_name>\<open>fun\<close>, [_ , R]) = fastype_of t1
-  in
-    Const (\<^const_name>\<open>image\<close>,
-      T --> fastype_of t2 --> HOLogic.mk_setT R) $ t1 $ t2
-  end;
+  let val \<^Type>\<open>fun A B\<close> = fastype_of t1
+  in \<^Const>\<open>image A B for t1 t2\<close> end;
 
 fun mk_sigma (t1, t2) =
   let
-    val T1 = fastype_of t1
-    val T2 = fastype_of t2
-    val setT = HOLogic.dest_setT T1
-    val resT = HOLogic.mk_setT (HOLogic.mk_prodT (setT, HOLogic.dest_setT T2))
-  in
-    Const (\<^const_name>\<open>Sigma\<close>,
-      T1 --> (setT --> T2) --> resT) $ t1 $ absdummy setT t2
-  end;
+    val \<^Type>\<open>set A\<close> = fastype_of t1
+    val \<^Type>\<open>set B\<close> = fastype_of t2
+  in \<^Const>\<open>Sigma A B for t1 \<open>absdummy A t2\<close>\<close> end;
 
 fun mk_vimage f s =
-  let
-    val T as Type (\<^type_name>\<open>fun\<close>, [T1, T2]) = fastype_of f
-  in
-    Const (\<^const_name>\<open>vimage\<close>, T --> HOLogic.mk_setT T2 --> HOLogic.mk_setT T1) $ f $ s
-  end;
+  let val \<^Type>\<open>fun A B\<close> = fastype_of f
+  in \<^Const>\<open>vimage A B for f s\<close> end;
 
-fun dest_Collect (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (x, T, t)) = ((x, T), t)
+fun dest_Collect \<^Const_>\<open>Collect _ for \<open>Abs (x, T, t)\<close>\<close> = ((x, T), t)
   | dest_Collect t = raise TERM ("dest_Collect", [t])
 
 (* Copied from predicate_compile_aux.ML *)
-fun strip_ex (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (x, T, t)) =
-  let
-    val (xTs, t') = strip_ex t
-  in
-    ((x, T) :: xTs, t')
-  end
+fun strip_ex \<^Const_>\<open>Ex _ for \<open>Abs (x, T, t)\<close>\<close> =
+      let val (xTs, t') = strip_ex t
+      in ((x, T) :: xTs, t') end
   | strip_ex t = ([], t)
 
 fun mk_prod1 Ts (t1, t2) =
-  let
-    val (T1, T2) = apply2 (curry fastype_of1 Ts) (t1, t2)
-  in
-    HOLogic.pair_const T1 T2 $ t1 $ t2
-  end;
+  let val (A, B) = apply2 (curry fastype_of1 Ts) (t1, t2)
+  in \<^Const>\<open>Pair A B for t1 t2\<close> end;
 
 fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end
-  | mk_split_abs vs (Const (\<^const_name>\<open>Product_Type.Pair\<close>, _) $ u $ v) t =
+  | mk_split_abs vs \<^Const_>\<open>Pair _ _ for u v\<close> t =
       HOLogic.mk_case_prod (mk_split_abs vs u (mk_split_abs vs v t))
   | mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]);
 
@@ -92,7 +65,7 @@
 val strip_ptupleabs =
   let
     fun strip [] qs vs t = (t, rev vs, qs)
-      | strip (p :: ps) qs vs (Const (\<^const_name>\<open>case_prod\<close>, _) $ t) =
+      | strip (p :: ps) qs vs \<^Const_>\<open>case_prod _ _ _ for t\<close> =
           strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) vs t
       | strip (_ :: ps) qs vs (Abs (s, T, t)) = strip ps qs ((s, T) :: vs) t
       | strip (_ :: ps) qs vs t = strip ps qs
@@ -114,8 +87,8 @@
 fun term_of_pattern Ts (Pattern bs) =
     let
       fun mk [b] = Bound b
-        | mk (b :: bs) = HOLogic.pair_const (nth Ts b) (type_of_pattern Ts (Pattern bs))
-           $ Bound b $ mk bs
+        | mk (b :: bs) =
+            \<^Const>\<open>Pair \<open>nth Ts b\<close> \<open>type_of_pattern Ts (Pattern bs)\<close> for \<open>Bound b\<close> \<open>mk bs\<close>\<close>
     in mk bs end;
 
 (* formulas *)
@@ -125,8 +98,8 @@
 fun map_atom f (Atom a) = Atom (f a)
   | map_atom _ x = x
 
-fun is_collect_atom (Atom (_, Const(\<^const_name>\<open>Collect\<close>, _) $ _)) = true
-  | is_collect_atom (Atom (_, Const (\<^const_name>\<open>Groups.uminus_class.uminus\<close>, _) $ (Const(\<^const_name>\<open>Collect\<close>, _) $ _))) = true
+fun is_collect_atom (Atom (_, \<^Const_>\<open>Collect _ for _\<close>)) = true
+  | is_collect_atom (Atom (_, \<^Const_>\<open>uminus _ for \<^Const_>\<open>Collect _ for _\<close>\<close>)) = true
   | is_collect_atom _ = false
 
 fun mk_case_prod _ [(x, T)] t = (T, Abs (x, T, t))
@@ -151,12 +124,12 @@
   let
     val (tuple, (vs', t')) = mk_term vs t
     val T = HOLogic.mk_tupleT (map snd vs')
-    val s = HOLogic.Collect_const T $ (snd (mk_case_prod \<^typ>\<open>bool\<close> vs' t'))
+    val s = \<^Const>\<open>Collect T for \<open>snd (mk_case_prod \<^Type>\<open>bool\<close> vs' t')\<close>\<close>
   in
     (tuple, Atom (tuple, s))
   end
 
-fun mk_atom vs (t as Const (\<^const_name>\<open>Set.member\<close>, _) $ x $ s) =
+fun mk_atom vs (t as \<^Const_>\<open>Set.member _ for x s\<close>) =
     if not (null (loose_bnos s)) then
       default_atom vs t
     else
@@ -165,10 +138,10 @@
     | NONE =>
         let
           val (tuple, (vs', x')) = mk_term vs x
-          val rT = HOLogic.dest_setT (fastype_of s)
+          val \<^Type>\<open>set rT\<close> = fastype_of s
           val s = mk_vimage (snd (mk_case_prod rT vs' x')) s
         in (tuple, Atom (tuple, s)) end)
-  | mk_atom vs (Const (\<^const_name>\<open>HOL.Not\<close>, _) $ t) = apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t)
+  | mk_atom vs \<^Const_>\<open>Not for t\<close> = apsnd (map_atom (apsnd mk_Compl)) (mk_atom vs t)
   | mk_atom vs t = default_atom vs t
 
 fun merge' [] (pats1, pats2) = ([], (pats1, pats2))
@@ -305,14 +278,14 @@
 
 (* proof tactic *)
 
-val case_prod_beta =
-  @{lemma "case_prod g x z = case_prod (\<lambda>x y. (g x y) z) x" by (simp add: case_prod_beta)}
+val case_prod_beta = @{lemma "case_prod g x z = case_prod (\<lambda>x y. (g x y) z) x" by (simp add: case_prod_beta)}
 
-val vimageI2' = @{lemma "f a \<notin> A \<Longrightarrow> a \<notin> f -` A" by simp}
-val vimageE' = @{lemma "a \<notin> f -` B \<Longrightarrow> (\<And> x. f a = x ==> x \<notin> B \<Longrightarrow> P) \<Longrightarrow> P" by simp}
+val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
+val vimageE' =
+  @{lemma "a \<notin> f -` B ==> (\<And> x. f a = x ==> x \<notin> B ==> P) ==> P" by simp}
 
-val collectI' = @{lemma "\<not> P a \<Longrightarrow> a \<notin> {x. P x}" by auto}
-val collectE' = @{lemma "a \<notin> {x. P x} \<Longrightarrow> (\<not> P a \<Longrightarrow> Q) \<Longrightarrow> Q" by auto}
+val collectI' = @{lemma "\<not> P a ==> a \<notin> {x. P x}" by auto}
+val collectE' = @{lemma "a \<notin> {x. P x} ==> (\<not> P a ==> Q) ==> Q" by auto}
 
 fun elim_Collect_tac ctxt =
   dresolve_tac ctxt @{thms iffD1 [OF mem_Collect_eq]}
@@ -415,7 +388,7 @@
 
 fun comprehension_conv ctxt ct =
   let
-    fun dest_Collect (Const (\<^const_name>\<open>Collect\<close>, T) $ t) = (HOLogic.dest_setT (body_type T), t)
+    fun dest_Collect \<^Const_>\<open>Collect A for t\<close> = (A, t)
       | dest_Collect t = raise TERM ("dest_Collect", [t])
     fun list_ex vs t = fold_rev (fn (x, T) => fn t => HOLogic.exists_const T $ Abs (x, T, t)) vs t
     fun mk_term t =
@@ -428,7 +401,7 @@
         val eq = HOLogic.eq_const T $ Bound (length Ts) $
           (HOLogic.mk_ptuple fp (HOLogic.mk_ptupleT fp Ts) (rev (map_index (fn (i, _) => Bound i) Ts)))
       in
-        HOLogic.Collect_const T $ absdummy T (list_ex vs (HOLogic.mk_conj (eq, t'')))
+        \<^Const>\<open>Collect T for \<open>absdummy T (list_ex vs (HOLogic.mk_conj (eq, t'')))\<close>\<close>
       end;
     fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (Thm.prop_of th))
     val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.case}