--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Aug 08 14:24:18 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Aug 08 16:03:34 2024 +0200
@@ -145,17 +145,9 @@
fun try_prove_refl_rel ctxt rel =
let
- fun mk_ge_eq x =
- let
- val T = fastype_of x
- in
- Const (\<^const_name>\<open>less_eq\<close>, T --> T --> HOLogic.boolT) $
- (Const (\<^const_name>\<open>HOL.eq\<close>, T)) $ x
- end;
- val goal = HOLogic.mk_Trueprop (mk_ge_eq rel);
- in
- mono_eq_prover ctxt goal
- end;
+ val T as \<^Type>\<open>fun A _\<close> = fastype_of rel
+ val ge_eq = \<^Const>\<open>less_eq T for \<^Const>\<open>HOL.eq A\<close> rel\<close>
+ in mono_eq_prover ctxt (HOLogic.mk_Trueprop ge_eq) end;
fun try_prove_reflexivity ctxt prop =
let
@@ -223,7 +215,9 @@
fun zip_transfer_rules ctxt thm =
let
- fun mk_POS ty = Const (\<^const_name>\<open>POS\<close>, ty --> ty --> HOLogic.boolT)
+ fun mk_POS ty =
+ let val \<^Type>\<open>fun A \<^Type>\<open>fun B bool\<close>\<close> = ty
+ in \<^Const>\<open>POS A B\<close> end
val rel = (Thm.dest_fun2 o Thm.dest_arg o Thm.cprop_of) thm
val typ = Thm.typ_of_cterm rel
val POS_const = Thm.cterm_of ctxt (mk_POS typ)
@@ -279,21 +273,21 @@
(* Generation of the code certificate from the rsp theorem *)
-fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
+fun get_body_types (\<^Type>\<open>fun _ U\<close>, \<^Type>\<open>fun _ V\<close>) = get_body_types (U, V)
| get_body_types (U, V) = (U, V)
-fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
+fun get_binder_types (\<^Type>\<open>fun T U\<close>, \<^Type>\<open>fun V W\<close>) = (T, V) :: get_binder_types (U, W)
| get_binder_types _ = []
-fun get_binder_types_by_rel (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) =
+fun get_binder_types_by_rel \<^Const_>\<open>rel_fun _ _ _ _ for _ S\<close> (\<^Type>\<open>fun T U\<close>, \<^Type>\<open>fun V W\<close>) =
(T, V) :: get_binder_types_by_rel S (U, W)
| get_binder_types_by_rel _ _ = []
-fun get_body_type_by_rel (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) =
+fun get_body_type_by_rel \<^Const_>\<open>rel_fun _ _ _ _ for _ S\<close> (\<^Type>\<open>fun _ U\<close>, \<^Type>\<open>fun _ V\<close>) =
get_body_type_by_rel S (U, V)
| get_body_type_by_rel _ (U, V) = (U, V)
-fun get_binder_rels (Const (\<^const_name>\<open>rel_fun\<close>, _) $ R $ S) = R :: get_binder_rels S
+fun get_binder_rels \<^Const_>\<open>rel_fun _ _ _ _ for R S\<close> = R :: get_binder_rels S
| get_binder_rels _ = []
fun force_rty_type ctxt rty rhs =
@@ -337,7 +331,7 @@
let
fun unfold_conv ctm =
case (Thm.term_of ctm) of
- Const (\<^const_name>\<open>map_fun\<close>, _) $ _ $ _ =>
+ \<^Const_>\<open>map_fun _ _ _ _ for _ _\<close> =>
(Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
| _ => Conv.all_conv ctm
in
@@ -376,9 +370,9 @@
fun can_generate_code_cert quot_thm =
case quot_thm_rel quot_thm of
- Const (\<^const_name>\<open>HOL.eq\<close>, _) => true
- | Const (\<^const_name>\<open>eq_onp\<close>, _) $ _ => true
- | _ => false
+ \<^Const_>\<open>HOL.eq _\<close> => true
+ | \<^Const_>\<open>eq_onp _ for _\<close> => true
+ | _ => false
fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
let
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Thu Aug 08 14:24:18 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Thu Aug 08 16:03:34 2024 +0200
@@ -179,12 +179,10 @@
(** witnesses **)
-fun mk_undefined T = Const (\<^const_name>\<open>undefined\<close>, T);
-
fun mk_witness quot_thm =
let
val wit_thm = quot_thm RS @{thm type_definition_Quotient_not_empty_witness}
- val wit = quot_thm_rep quot_thm $ mk_undefined (quot_thm_rty_qty quot_thm |> snd)
+ val wit = quot_thm_rep quot_thm $ \<^Const>\<open>undefined \<open>quot_thm_rty_qty quot_thm |> snd\<close>\<close>
in
(wit, wit_thm)
end
@@ -238,9 +236,8 @@
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
fun ret_rel_conv conv ctm =
case (Thm.term_of ctm) of
- Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ =>
- binop_conv2 Conv.all_conv conv ctm
- | _ => conv ctm
+ \<^Const_>\<open>rel_fun _ _ _ _ for _ _\<close> => binop_conv2 Conv.all_conv conv ctm
+ | _ => conv ctm
fun R_conv rel_eq_onps ctxt =
Conv.top_sweep_rewrs_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} ctxt
then_conv Conv.bottom_rewrs_conv rel_eq_onps ctxt
@@ -392,7 +389,7 @@
SOME code_dt =>
(fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_witness_of_code_dt qty_ret code_dt),
wit_thm_of_code_dt code_dt :: wits)
- | NONE => (fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T), wits)
+ | NONE => (fold_rev (Term.lambda o curry Free Name.uu) Ts \<^Const>\<open>undefined T\<close>, wits)
in
@{fold_map 2} (fn Ts => fn k' => fn wits =>
(if k = k' then (fold_rev Term.lambda xs x, wits) else gen_undef_wit Ts wits)) ctr_Tss ks []
@@ -434,13 +431,8 @@
|>> mk_lift_const_of_lift_def (qty_isom --> qty_ret))) sel_names sel_rhs lthy5
(* now we can execute the qty qty_isom isomorphism *)
- fun mk_type_definition newT oldT RepC AbsC A =
- let
- val typedefC =
- Const (\<^const_name>\<open>type_definition\<close>,
- (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
- in typedefC $ RepC $ AbsC $ A end;
- val typedef_goal = mk_type_definition qty_isom qty rep_isom abs_isom (HOLogic.mk_UNIV qty) |>
+ val typedef_goal =
+ \<^Const>\<open>type_definition qty_isom qty for rep_isom abs_isom \<open>HOLogic.mk_UNIV qty\<close>\<close> |>
HOLogic.mk_Trueprop;
fun typ_isom_tac ctxt i =
EVERY' [ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms type_definition_def}),
@@ -700,7 +692,7 @@
(K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq ctxt)))) ctxt
in
case (Thm.term_of ctm) of
- Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ =>
+ \<^Const_>\<open>rel_fun _ _ _ _ for _ _\<close> =>
(binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
| _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm
end
@@ -723,11 +715,11 @@
fun rename_to_tnames ctxt term =
let
- fun all_typs (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T, t)) = T :: all_typs t
+ fun all_typs \<^Const_>\<open>Pure.all _ for \<open>Abs (_, T, t)\<close>\<close> = T :: all_typs t
| all_typs _ = []
- fun rename (Const (\<^const_name>\<open>Pure.all\<close>, T1) $ Abs (_, T2, t)) (new_name :: names) =
- (Const (\<^const_name>\<open>Pure.all\<close>, T1) $ Abs (new_name, T2, rename t names))
+ fun rename \<^Const_>\<open>Pure.all T1 for \<open>Abs (_, T2, t)\<close>\<close> (new_name :: names) =
+ \<^Const>\<open>Pure.all T1 for \<open>Abs (new_name, T2, rename t names)\<close>\<close>
| rename t _ = t
val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
--- a/src/HOL/Tools/Lifting/lifting_info.ML Thu Aug 08 14:24:18 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Thu Aug 08 16:03:34 2024 +0200
@@ -478,12 +478,9 @@
val concl = perhaps (try HOLogic.dest_Trueprop) (Thm.concl_of rule);
val (lhs, rhs) =
(case concl of
- Const (\<^const_name>\<open>less_eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs =>
- (lhs, rhs)
- | Const (\<^const_name>\<open>less_eq\<close>, _) $ rhs $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) =>
- (lhs, rhs)
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs =>
- (lhs, rhs)
+ \<^Const_>\<open>less_eq _ for \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> rhs\<close> => (lhs, rhs)
+ | \<^Const_>\<open>less_eq _ for rhs \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close>\<close> => (lhs, rhs)
+ | \<^Const_>\<open>HOL.eq _ for \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> rhs\<close> => (lhs, rhs)
| _ => error "The rule has a wrong format.")
val lhs_vars = Term.add_vars lhs []
@@ -501,10 +498,9 @@
val rhs_args = (snd o strip_comb) rhs;
fun check_comp t =
(case t of
- Const (\<^const_name>\<open>relcompp\<close>, _) $ Var _ $ Var _ => ()
+ \<^Const_>\<open>relcompp _ _ _ for \<open>Var _\<close> \<open>Var _\<close>\<close> => ()
| _ => error "There is an argument on the rhs that is not a composition.")
- val _ = map check_comp rhs_args
- in () end
+ in List.app check_comp rhs_args end
in
fun add_distr_rule distr_rule context =
@@ -513,11 +509,11 @@
val concl = perhaps (try HOLogic.dest_Trueprop) (Thm.concl_of distr_rule)
in
(case concl of
- Const (\<^const_name>\<open>less_eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ =>
+ \<^Const_>\<open>less_eq _ for \<^Const_>\<open>relcompp _ _ _ for _ _\<close> _\<close> =>
add_pos_distr_rule distr_rule context
- | Const (\<^const_name>\<open>less_eq\<close>, _) $ _ $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) =>
+ | \<^Const_>\<open>less_eq _ for _ \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> =>
add_neg_distr_rule distr_rule context
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ =>
+ | \<^Const_>\<open>HOL.eq _ for \<^Const_>\<open>relcompp _ _ _ for _ _\<close> _\<close> =>
add_eq_distr_rule distr_rule context)
end
end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Thu Aug 08 14:24:18 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu Aug 08 16:03:34 2024 +0200
@@ -81,15 +81,11 @@
val args_fixed = (map (Term_Subst.instantiate (instT, Vars.empty))) args_subst
val param_rel_fixed = Term_Subst.instantiate (instT, Vars.empty) param_rel_subst
val rty = (domain_type o fastype_of) param_rel_fixed
- val relcomp_op = Const (\<^const_name>\<open>relcompp\<close>,
- (rty --> rty' --> HOLogic.boolT) -->
- (rty' --> qty --> HOLogic.boolT) -->
- rty --> qty --> HOLogic.boolT)
val qty_name = dest_Type_name qty
val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name)
val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT])
val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
- val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
+ val rhs = \<^Const>\<open>relcompp rty rty' qty for param_rel_fixed fixed_crel\<close>
val definition_term = Logic.mk_equals (lhs, rhs)
fun note_def lthy =
Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] []
@@ -151,7 +147,7 @@
(Conv.bottom_rewrs_conv (Transfer.get_relator_eq args_ctxt) args_ctxt)))
in
case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of
- Const (\<^const_name>\<open>relcompp\<close>, _) $ Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ =>
+ \<^Const_>\<open>relcompp _ _ _ for \<^Const_>\<open>HOL.eq _\<close> _\<close> =>
let
val thm =
pcr_cr_eq
@@ -164,8 +160,8 @@
in
(thm, lthy')
end
- | Const (\<^const_name>\<open>relcompp\<close>, _) $ t $ _ => print_generate_pcr_cr_eq_error args_ctxt t
- | _ => error "generate_pcr_cr_eq: implementation error"
+ | \<^Const_>\<open>relcompp _ _ _ for t _\<close> => print_generate_pcr_cr_eq_error args_ctxt t
+ | _ => error "generate_pcr_cr_eq: implementation error"
end
end
@@ -217,13 +213,12 @@
Pretty.brk 1] @
((Pretty.commas o map (Pretty.str o quote)) extras) @
[Pretty.str "."])]
- val not_type_constr =
- case qty of
- Type _ => []
- | _ => [Pretty.block [Pretty.str "The quotient type ",
- Pretty.quote (Syntax.pretty_typ ctxt' qty),
- Pretty.brk 1,
- Pretty.str "is not a type constructor."]]
+ val not_type_constr =
+ if is_Type qty then []
+ else [Pretty.block [Pretty.str "The quotient type ",
+ Pretty.quote (Syntax.pretty_typ ctxt' qty),
+ Pretty.brk 1,
+ Pretty.str "is not a type constructor."]]
val errs = extra_rty_tfrees @ not_type_constr
in
if null errs then () else raise QUOT_ERROR errs
@@ -641,22 +636,20 @@
(**)
val T_def = Morphism.thm (Local_Theory.target_morphism lthy1) T_def
(**)
- val quot_thm = case typedef_set of
- Const (\<^const_name>\<open>top\<close>, _) =>
- [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
- | Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, _) =>
- [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
- | _ =>
- [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
+ val quot_thm =
+ case typedef_set of
+ \<^Const_>\<open>top _\<close> => [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
+ | \<^Const_>\<open>Collect _ for \<open>Abs _\<close>\<close> => [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
+ | _ => [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
val (rty, qty) = quot_thm_rty_qty quot_thm
val qty_full_name = dest_Type_name qty
val qty_name = Binding.name (Long_Name.base_name qty_full_name)
val qualify = Binding.qualify_name true qty_name
val opt_reflp_thm =
case typedef_set of
- Const (\<^const_name>\<open>top\<close>, _) =>
+ \<^Const_>\<open>top _\<close> =>
SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
- | _ => NONE
+ | _ => NONE
val dom_thm = get_Domainp_thm quot_thm
fun setup_transfer_rules_nonpar notes =
@@ -789,9 +782,9 @@
end
in
case input_term of
- (Const (\<^const_name>\<open>Quotient\<close>, _) $ _ $ _ $ _ $ _) => setup_quotient ()
- | (Const (\<^const_name>\<open>type_definition\<close>, _) $ _ $ _ $ _) => setup_typedef ()
- | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
+ \<^Const_>\<open>Quotient _ _ for _ _ _ _\<close> => setup_quotient ()
+ | \<^Const_>\<open>type_definition _ _ for _ _ _\<close> => setup_typedef ()
+ | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
end
val _ =
@@ -830,7 +823,7 @@
Pretty.brk 1,
Thm.pretty_thm ctxt pcr_cr_eq]]
val (pcr_const_eq, eqs) = strip_comb eq_lhs
- fun is_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _)) = true
+ fun is_eq \<^Const_>\<open>HOL.eq _\<close> = true
| is_eq _ = false
fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
| eq_Const _ _ = false
@@ -929,14 +922,14 @@
(* lifting_forget *)
-val monotonicity_names = [\<^const_name>\<open>right_unique\<close>, \<^const_name>\<open>left_unique\<close>, \<^const_name>\<open>right_total\<close>,
- \<^const_name>\<open>left_total\<close>, \<^const_name>\<open>bi_unique\<close>, \<^const_name>\<open>bi_total\<close>]
-
-fun fold_transfer_rel f (Const (\<^const_name>\<open>Transfer.Rel\<close>, _) $ rel $ _ $ _) = f rel
- | fold_transfer_rel f (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
- (Const (\<^const_name>\<open>Domainp\<close>, _) $ rel) $ _) = f rel
- | fold_transfer_rel f (Const (name, _) $ rel) =
- if member op= monotonicity_names name then f rel else f \<^term>\<open>undefined\<close>
+fun fold_transfer_rel f \<^Const_>\<open>Transfer.Rel _ _ for rel _ _\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>HOL.eq _ for \<^Const_>\<open>Domainp _ _ for rel\<close> _\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>right_unique _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>left_unique _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>right_total _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>left_total _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>bi_unique _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>bi_total _ _ for rel\<close> = f rel
| fold_transfer_rel f _ = f \<^term>\<open>undefined\<close>
fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
--- a/src/HOL/Tools/Lifting/lifting_term.ML Thu Aug 08 14:24:18 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Thu Aug 08 16:03:34 2024 +0200
@@ -108,8 +108,8 @@
(case Lifting_Info.lookup_relator_distr_data ctxt s of
SOME rel_distr_thm =>
(case tm of
- Const (\<^const_name>\<open>POS\<close>, _) => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm)
- | Const (\<^const_name>\<open>NEG\<close>, _) => map (Thm.transfer' ctxt) (#neg_distr_rules rel_distr_thm))
+ \<^Const_>\<open>POS _ _\<close> => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm)
+ | \<^Const_>\<open>NEG _ _\<close> => map (Thm.transfer' ctxt) (#neg_distr_rules rel_distr_thm))
| NONE => raise QUOT_THM_INTERNAL (Pretty.block
[Pretty.str ("No relator distr. data for the type " ^ quote s),
Pretty.brk 1,
@@ -461,8 +461,8 @@
fun is_POS_or_NEG ctm =
case (head_of o Thm.term_of o Thm.dest_arg) ctm of
- Const (\<^const_name>\<open>POS\<close>, _) => true
- | Const (\<^const_name>\<open>NEG\<close>, _) => true
+ \<^Const_>\<open>POS _ _\<close> => true
+ | \<^Const_>\<open>NEG _ _\<close> => true
| _ => false
val inst_distr_rule = rewr_imp distr_rule ctm
@@ -480,8 +480,8 @@
in
case get_args 2 rel of
- [Const (\<^const_name>\<open>HOL.eq\<close>, _), _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
- | [_, Const (\<^const_name>\<open>HOL.eq\<close>, _)] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
+ [\<^Const_>\<open>HOL.eq _\<close>, _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
+ | [_, \<^Const_>\<open>HOL.eq _\<close>] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
| [_, trans_rel] =>
let
val (rty', qty) = (relation_types o fastype_of) trans_rel