# HG changeset patch
# User wenzelm
# Date 1723284773 -7200
# Node ID c5c9b4470d06b64dfb1131dee49d133d42f5656e
# Parent  6fedd6d3fa41f38a7c999c8825deae0fb547ebd3
tuned: more antiquotations;

diff -r 6fedd6d3fa41 -r c5c9b4470d06 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Aug 08 22:49:40 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 10 12:12:53 2024 +0200
@@ -109,14 +109,10 @@
 
 fun ball_bex_range_simproc ctxt redex =
   (case Thm.term_of redex of
-    (Const (\<^const_name>\<open>Ball\<close>, _) $ (Const (\<^const_name>\<open>Respects\<close>, _) $
-      (Const (\<^const_name>\<open>rel_fun\<close>, _) $ R1 $ R2)) $ _) =>
-        calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
-
-  | (Const (\<^const_name>\<open>Bex\<close>, _) $ (Const (\<^const_name>\<open>Respects\<close>, _) $
-      (Const (\<^const_name>\<open>rel_fun\<close>, _) $ R1 $ R2)) $ _) =>
-        calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
-
+    \<^Const_>\<open>Ball _ for \<open>\<^Const_>\<open>Respects _ for \<^Const_>\<open>rel_fun _ _ _ _ for R1 R2\<close>\<close>\<close> _\<close> =>
+      calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
+  | \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for \<^Const_>\<open>rel_fun _ _ _ _ for R1 R2\<close>\<close> _\<close> =>
+      calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   | _ => NONE)
 
 (* Regularize works as follows:
@@ -179,19 +175,17 @@
 *)
 fun find_qt_asm asms =
   let
-    fun find_fun trm =
-      (case trm of
-        (Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>Quot_True\<close>, _) $ _)) => true
-      | _ => false)
+    fun find_fun \<^Const_>\<open>Trueprop for \<^Const_>\<open>Quot_True _ for _\<close>\<close> = true
+      | find_fun _ = false
   in
-     (case find_first find_fun asms of
-       SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
-     | _ => NONE)
+    (case find_first find_fun asms of
+      SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
+    | _ => NONE)
   end
 
 fun quot_true_simple_conv ctxt fnctn ctrm =
   (case Thm.term_of ctrm of
-    (Const (\<^const_name>\<open>Quot_True\<close>, _) $ x) =>
+    \<^Const_>\<open>Quot_True _ for x\<close> =>
       let
         val fx = fnctn x;
         val cx = Thm.cterm_of ctxt x;
@@ -205,7 +199,7 @@
 
 fun quot_true_conv ctxt fnctn ctrm =
   (case Thm.term_of ctrm of
-    (Const (\<^const_name>\<open>Quot_True\<close>, _) $ _) =>
+    \<^Const_>\<open>Quot_True _ for _\<close> =>
       quot_true_simple_conv ctxt fnctn ctrm
   | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
   | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
@@ -314,54 +308,53 @@
 fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
   (case bare_concl goal of
       (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
-    (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $ (Abs _) $ (Abs _)
-        => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
+    \<^Const_>\<open>rel_fun _ _ _ _ for _ _ \<open>Abs _\<close> \<open>Abs _\<close>\<close> =>
+      resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
 
       (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
-  | (Const (\<^const_name>\<open>HOL.eq\<close>,_) $
-      (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
-      (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _))
-        => resolve_tac ctxt @{thms ball_rsp} THEN' dresolve_tac ctxt @{thms QT_all}
+  | \<^Const_>\<open>HOL.eq _ for
+      \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+      \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+      resolve_tac ctxt @{thms ball_rsp} THEN' dresolve_tac ctxt @{thms QT_all}
 
       (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
-  | (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $
-      (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
-      (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _)
-        => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
+  | \<^Const_>\<open>rel_fun _ _ _ _ for _ _
+      \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+      \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+      resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
 
       (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
-  | Const (\<^const_name>\<open>HOL.eq\<close>,_) $
-      (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
-      (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _)
-        => resolve_tac ctxt @{thms bex_rsp} THEN' dresolve_tac ctxt @{thms QT_ex}
+  | \<^Const_>\<open>HOL.eq _ for
+      \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+      \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+      resolve_tac ctxt @{thms bex_rsp} THEN' dresolve_tac ctxt @{thms QT_ex}
 
       (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
-  | (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $
-      (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
-      (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _)
-        => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
+  | \<^Const_>\<open>rel_fun _ _ _ _ for _ _
+      \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+      \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+      resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
 
-  | (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $
-      (Const(\<^const_name>\<open>Bex1_rel\<close>,_) $ _) $ (Const(\<^const_name>\<open>Bex1_rel\<close>,_) $ _)
-        => resolve_tac ctxt @{thms bex1_rel_rsp} THEN' quotient_tac ctxt
+  | \<^Const_>\<open>rel_fun _ _ _ _ for _ _ \<^Const_>\<open>Bex1_rel _ for _\<close> \<^Const_>\<open>Bex1_rel _ for _\<close>\<close> =>
+      resolve_tac ctxt @{thms bex1_rel_rsp} THEN' quotient_tac ctxt
 
   | (_ $
-      (Const(\<^const_name>\<open>Babs\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
-      (Const(\<^const_name>\<open>Babs\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _))
-        => resolve_tac ctxt @{thms babs_rsp} THEN' quotient_tac ctxt
+      \<^Const_>\<open>Babs _ _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> $
+      \<^Const_>\<open>Babs _ _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>) =>
+      resolve_tac ctxt @{thms babs_rsp} THEN' quotient_tac ctxt
 
-  | Const (\<^const_name>\<open>HOL.eq\<close>,_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
-     (resolve_tac ctxt @{thms refl} ORELSE'
+  | \<^Const_>\<open>HOL.eq _ for \<open>R $ _ $ _\<close> \<open>_ $ _ $ _\<close>\<close> =>
+      (resolve_tac ctxt @{thms refl} ORELSE'
       (equals_rsp_tac R ctxt THEN' RANGE [
          quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
 
       (* reflexivity of operators arising from Cong_tac *)
-  | Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _ => resolve_tac ctxt @{thms refl}
+  | \<^Const_>\<open>HOL.eq _ for _ _\<close> => resolve_tac ctxt @{thms refl}
 
      (* respectfulness of constants; in particular of a simple relation *)
-  | _ $ (Const _) $ (Const _)  (* rel_fun, list_rel, etc but not equality *)
-      => resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_respect\<close>))
-          THEN_ALL_NEW quotient_tac ctxt
+  | _ $ Const _ $ Const _ => (* rel_fun, list_rel, etc but not equality *)
+      resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_respect\<close>))
+      THEN_ALL_NEW quotient_tac ctxt
 
       (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
       (* observe map_fun *)
@@ -411,10 +404,10 @@
 (* expands all map_funs, except in front of the (bound) variables listed in xs *)
 fun map_fun_simple_conv xs ctrm =
   (case Thm.term_of ctrm of
-    ((Const (\<^const_name>\<open>map_fun\<close>, _) $ _ $ _) $ h $ _) =>
-        if member (op=) xs h
-        then Conv.all_conv ctrm
-        else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
+    \<^Const_>\<open>map_fun _ _ _ _ for _ _ h _\<close> =>
+      if member (op=) xs h
+      then Conv.all_conv ctrm
+      else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
   | _ => Conv.all_conv ctrm)
 
 fun map_fun_conv xs ctxt ctrm =
@@ -439,7 +432,7 @@
 
 fun make_inst lhs t =
   let
-    val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+    val _ $ (Abs (_, _, (_ $ ((f as Var (_, \<^Type>\<open>fun T _\<close>)) $ u)))) = lhs;
     val _ $ (Abs (_, _, (_ $ g))) = t;
   in
     (f, Abs ("x", T, mk_abs u 0 g))
@@ -447,7 +440,7 @@
 
 fun make_inst_id lhs t =
   let
-    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+    val _ $ (Abs (_, _, (f as Var (_, \<^Type>\<open>fun T _\<close>)) $ u)) = lhs;
     val _ $ (Abs (_, _, g)) = t;
   in
     (f, Abs ("x", T, mk_abs u 0 g))