# HG changeset patch
# User wenzelm
# Date 1723150180 -7200
# Node ID 6fedd6d3fa41f38a7c999c8825deae0fb547ebd3
# Parent  32073335a8e99db070f599b9ef645b54dc5b5175
tuned: more antiquotations;

diff -r 32073335a8e9 -r 6fedd6d3fa41 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Thu Aug 08 17:06:08 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Thu Aug 08 22:49:40 2024 +0200
@@ -93,9 +93,9 @@
     fun abs_conv2 cv = Conv.abs_conv (Conv.abs_conv (cv o #2) o #2) ctxt
     fun erase_quants ctxt' ctm' =
       case (Thm.term_of ctm') of
-        Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.all_conv ctm'
-        | _ => (Conv.binder_conv (erase_quants o #2) ctxt' then_conv
-          Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
+        \<^Const_>\<open>HOL.eq _ for _ _\<close> => Conv.all_conv ctm'
+      | _ => (Conv.binder_conv (erase_quants o #2) ctxt' then_conv
+        Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
     val norm_fun_eq = abs_conv2 erase_quants then_conv Thm.eta_conversion
 
     fun simp_arrows_conv ctm =
@@ -107,9 +107,9 @@
         fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
       in
         case (Thm.term_of ctm) of
-          Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ =>
+          \<^Const_>\<open>rel_fun _ _ _ _ for _ _\<close> =>
             (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
-          | _ => Conv.all_conv ctm
+        | _ => Conv.all_conv ctm
       end
 
     val unfold_ret_val_invs = Conv.bottom_conv
@@ -159,7 +159,7 @@
           |> try HOLogic.dest_Trueprop
       in
         case lhs_eq of
-          SOME (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _) => SOME (@{thm refl} RS thm)
+          SOME \<^Const_>\<open>HOL.eq _ for _ _\<close> => SOME (@{thm refl} RS thm)
           | SOME _ => (case body_type (fastype_of lhs) of
             Type (typ_name, _) =>
               \<^try>\<open>
diff -r 32073335a8e9 -r 6fedd6d3fa41 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Aug 08 17:06:08 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Aug 08 22:49:40 2024 +0200
@@ -55,11 +55,9 @@
 fun negF AbsF = RepF
   | negF RepF = AbsF
 
-fun is_identity (Const (\<^const_name>\<open>id\<close>, _)) = true
+fun is_identity \<^Const_>\<open>id _\<close> = true
   | is_identity _ = false
 
-fun mk_identity ty = Const (\<^const_name>\<open>id\<close>, ty --> ty)
-
 fun mk_fun_compose flag (trm1, trm2) =
   case flag of
     AbsF => Const (\<^const_name>\<open>comp\<close>, dummyT) $ trm1 $ trm2
@@ -191,7 +189,7 @@
       end
   in
     if rty = qty
-    then mk_identity rty
+    then \<^Const>\<open>id rty\<close>
     else
       case (rty, qty) of
         (Type (s, tys), Type (s', tys')) =>
@@ -235,7 +233,7 @@
             end
       | (TFree x, TFree x') =>
           if x = x'
-          then mk_identity rty
+          then \<^Const>\<open>id rty\<close>
           else raise (LIFT_MATCH "absrep_fun (frees)")
       | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
       | _ => raise (LIFT_MATCH "absrep_fun (default)")
@@ -264,7 +262,7 @@
     map_types (Envir.subst_type ty_inst) trm
   end
 
-fun is_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _)) = true
+fun is_eq \<^Const_>\<open>HOL.eq _\<close> = true
   | is_eq _ = false
 
 fun mk_rel_compose (trm1, trm2) =
diff -r 32073335a8e9 -r 6fedd6d3fa41 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Thu Aug 08 17:06:08 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Thu Aug 08 22:49:40 2024 +0200
@@ -72,11 +72,10 @@
 (* proves the quot_type theorem for the new type *)
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
   let
-    val quot_type_const = Const (\<^const_name>\<open>quot_type\<close>,
-      fastype_of rel --> fastype_of abs --> fastype_of rep --> \<^typ>\<open>bool\<close>)
-    val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
+    val \<^Type>\<open>fun A _\<close> = fastype_of rel
+    val \<^Type>\<open>fun _ B\<close> = fastype_of abs
   in
-    Goal.prove lthy [] [] goal
+    Goal.prove lthy [] [] (HOLogic.mk_Trueprop (\<^Const>\<open>quot_type A B for rel abs rep\<close>))
       (fn {context = ctxt, ...} => typedef_quot_type_tac ctxt equiv_thm typedef_info)
   end
 
@@ -97,12 +96,12 @@
 
     val (rty, qty) = (dest_funT o fastype_of) abs_fun
     val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
-    val Abs_body = (case (HOLogic.dest_Trueprop o Thm.prop_of) equiv_thm of
-      Const (\<^const_name>\<open>equivp\<close>, _) $ _ => abs_fun_graph
-      | Const (\<^const_name>\<open>part_equivp\<close>, _) $ rel =>
-        HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
-      | _ => error "unsupported equivalence theorem"
-      )
+    val Abs_body =
+      (case (HOLogic.dest_Trueprop o Thm.prop_of) equiv_thm of
+        \<^Const_>\<open>equivp _ for _\<close> => abs_fun_graph
+      | \<^Const_>\<open>part_equivp _ for rel\<close> =>
+          HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
+      | _ => error "unsupported equivalence theorem")
     val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
     val qty_name = Binding.name (Long_Name.base_name (dest_Type_name qty))
     val cr_rel_name = Binding.prefix_name "cr_" qty_name
@@ -122,10 +121,10 @@
     val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
     val (reflp_thm, quot_thm) =
       (case (HOLogic.dest_Trueprop o Thm.prop_of) equiv_thm of
-        Const (\<^const_name>\<open>equivp\<close>, _) $ _ =>
+        \<^Const_>\<open>equivp _ for _\<close> =>
           (SOME (equiv_thm RS @{thm equivp_reflp2}),
             [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp})
-      | Const (\<^const_name>\<open>part_equivp\<close>, _) $ _ =>
+      | \<^Const_>\<open>part_equivp _ for _\<close> =>
           (NONE, [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient})
       | _ => error "unsupported equivalence theorem")
     val config = { notes = true }
@@ -177,11 +176,8 @@
     val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
 
     (* more useful abs and rep definitions *)
-    val abs_const = Const (\<^const_name>\<open>quot_type.abs\<close>,
-      (rty --> rty --> \<^typ>\<open>bool\<close>) --> (Rep_ty --> Abs_ty) --> rty --> Abs_ty)
-    val rep_const = Const (\<^const_name>\<open>quot_type.rep\<close>, (Abs_ty --> Rep_ty) --> Abs_ty --> rty)
-    val abs_trm = abs_const $ rel $ Abs_const
-    val rep_trm = rep_const $ Rep_const
+    val abs_trm = \<^Const>\<open>quot_type.abs rty Abs_ty\<close> $ rel $ Abs_const
+    val rep_trm = \<^Const>\<open>quot_type.rep Abs_ty rty\<close> $ Rep_const
     val (rep_name, abs_name) =
       (case opt_morphs of
         NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name)
@@ -301,16 +297,9 @@
     val _ = sanity_check quot
     val _ = map_check lthy quot
 
-    fun mk_goal (rty, rel, partial) =
-      let
-        val equivp_ty = ([rty, rty] ---> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>
-        val const =
-          if partial then \<^const_name>\<open>part_equivp\<close> else \<^const_name>\<open>equivp\<close>
-      in
-        HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
-      end
-
-    val goal = (mk_goal o #2) quot
+    val (rty, rel, partial) = #2 quot
+    val const = if partial then \<^Const>\<open>part_equivp rty\<close> else \<^Const>\<open>equivp rty\<close>
+    val goal = HOLogic.mk_Trueprop (const $ rel)
 
     fun after_qed [[thm]] = (snd oo add_quotient_type overloaded) (quot, thm)
   in