# 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>\HOL.eq\, _) $ _ $ _ => 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_>\HOL.eq _ for _ _\ => 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>\rel_fun\, _) $ _ $ _ => + \<^Const_>\rel_fun _ _ _ _ for _ _\ => (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>\HOL.eq\, _) $ _ $ _) => SOME (@{thm refl} RS thm) + SOME \<^Const_>\HOL.eq _ for _ _\ => SOME (@{thm refl} RS thm) | SOME _ => (case body_type (fastype_of lhs) of Type (typ_name, _) => \<^try>\ 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>\id\, _)) = true +fun is_identity \<^Const_>\id _\ = true | is_identity _ = false -fun mk_identity ty = Const (\<^const_name>\id\, ty --> ty) - fun mk_fun_compose flag (trm1, trm2) = case flag of AbsF => Const (\<^const_name>\comp\, dummyT) $ trm1 $ trm2 @@ -191,7 +189,7 @@ end in if rty = qty - then mk_identity rty + then \<^Const>\id rty\ 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>\id rty\ 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>\HOL.eq\, _)) = true +fun is_eq \<^Const_>\HOL.eq _\ = 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>\quot_type\, - fastype_of rel --> fastype_of abs --> fastype_of rep --> \<^typ>\bool\) - val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) + val \<^Type>\fun A _\ = fastype_of rel + val \<^Type>\fun _ B\ = fastype_of abs in - Goal.prove lthy [] [] goal + Goal.prove lthy [] [] (HOLogic.mk_Trueprop (\<^Const>\quot_type A B for rel abs rep\)) (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>\equivp\, _) $ _ => abs_fun_graph - | Const (\<^const_name>\part_equivp\, _) $ 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_>\equivp _ for _\ => abs_fun_graph + | \<^Const_>\part_equivp _ for rel\ => + 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>\equivp\, _) $ _ => + \<^Const_>\equivp _ for _\ => (SOME (equiv_thm RS @{thm equivp_reflp2}), [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp}) - | Const (\<^const_name>\part_equivp\, _) $ _ => + | \<^Const_>\part_equivp _ for _\ => (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>\quot_type.abs\, - (rty --> rty --> \<^typ>\bool\) --> (Rep_ty --> Abs_ty) --> rty --> Abs_ty) - val rep_const = Const (\<^const_name>\quot_type.rep\, (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>\quot_type.abs rty Abs_ty\ $ rel $ Abs_const + val rep_trm = \<^Const>\quot_type.rep Abs_ty rty\ $ 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>\bool\) --> \<^typ>\bool\ - val const = - if partial then \<^const_name>\part_equivp\ else \<^const_name>\equivp\ - 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>\part_equivp rty\ else \<^Const>\equivp rty\ + val goal = HOLogic.mk_Trueprop (const $ rel) fun after_qed [[thm]] = (snd oo add_quotient_type overloaded) (quot, thm) in