# HG changeset patch # User wenzelm # Date 1723318330 -7200 # Node ID b21af525f543ea9d8bb3220aae1f49e74ef95d78 # Parent f91aa8f591f121c9363de3be6277261f530db31b misc tuning; diff -r f91aa8f591f1 -r b21af525f543 src/HOL/Tools/Lifting/lifting_util.ML --- a/src/HOL/Tools/Lifting/lifting_util.ML Sat Aug 10 21:14:07 2024 +0200 +++ b/src/HOL/Tools/Lifting/lifting_util.ML Sat Aug 10 21:32:10 2024 +0200 @@ -30,7 +30,6 @@ val conceal_naming_result: (local_theory -> 'a * local_theory) -> local_theory -> 'a * local_theory end - structure Lifting_Util: LIFTING_UTIL = struct @@ -45,46 +44,27 @@ fun dest_Quotient \<^Const_>\Quotient _ _ for rel abs rep cr\ = (rel, abs, rep, cr) | dest_Quotient t = raise TERM ("dest_Quotient", [t]) -(* - quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions - for destructing quotient theorems (Quotient R Abs Rep T). -*) - -fun quot_thm_rel quot_thm = - case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of - (rel, _, _, _) => rel +val dest_Quotient_thm = dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of -fun quot_thm_abs quot_thm = - case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of - (_, abs, _, _) => abs - -fun quot_thm_rep quot_thm = - case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of - (_, _, rep, _) => rep - -fun quot_thm_crel quot_thm = - case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of - (_, _, _, crel) => crel +val quot_thm_rel = #1 o dest_Quotient_thm +val quot_thm_abs = #2 o dest_Quotient_thm +val quot_thm_rep = #3 o dest_Quotient_thm +val quot_thm_crel = #4 o dest_Quotient_thm fun quot_thm_rty_qty quot_thm = - let - val abs = quot_thm_abs quot_thm - val abs_type = fastype_of abs - in - (domain_type abs_type, range_type abs_type) - end + let val \<^Type>\fun A B\ = fastype_of (quot_thm_abs quot_thm) + in (A, B) end -fun Quotient_conv R_conv Abs_conv Rep_conv T_conv = Conv.combination_conv (Conv.combination_conv - (Conv.combination_conv (Conv.arg_conv R_conv) Abs_conv) Rep_conv) T_conv; - -fun Quotient_R_conv R_conv = Quotient_conv R_conv Conv.all_conv Conv.all_conv Conv.all_conv; +fun Quotient_conv R_conv Abs_conv Rep_conv T_conv = + Conv.combination_conv (Conv.combination_conv + (Conv.combination_conv (Conv.arg_conv R_conv) Abs_conv) Rep_conv) T_conv + +fun Quotient_R_conv R_conv = + Quotient_conv R_conv Conv.all_conv Conv.all_conv Conv.all_conv fun undisch thm = - let - val assm = Thm.cprem_of thm 1 - in - Thm.implies_elim thm (Thm.assume assm) - end + let val assm = Thm.cprem_of thm 1 + in Thm.implies_elim thm (Thm.assume assm) end fun undisch_all thm = funpow (Thm.nprems_of thm) undisch thm @@ -92,30 +72,27 @@ fun strip_args n = funpow n (fst o dest_comb) -fun all_args_conv conv ctm = Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm - -fun Targs (Type (_, args)) = args - | Targs _ = [] +fun all_args_conv conv ctm = + Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm -fun Tname (Type (name, _)) = name - | Tname _ = "" +fun Targs T = if is_Type T then dest_Type_args T else [] +fun Tname T = if is_Type T then dest_Type_name T else "" -fun relation_types typ = - case strip_type typ of - ([typ1, typ2], \<^typ>\bool\) => (typ1, typ2) - | _ => error "relation_types: not a relation" +fun relation_types typ = + (case strip_type typ of + ([typ1, typ2], \<^Type>\bool\) => (typ1, typ2) + | _ => error "relation_types: not a relation") fun map_interrupt f l = let fun map_interrupt' _ [] l = SOME (rev l) - | map_interrupt' f (x::xs) l = (case f x of - NONE => NONE - | SOME v => map_interrupt' f xs (v::l)) - in - map_interrupt' f l [] - end + | map_interrupt' f (x::xs) l = + (case f x of + NONE => NONE + | SOME v => map_interrupt' f xs (v::l)) + in map_interrupt' f l [] end -fun conceal_naming_result f lthy = - lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming lthy; +fun conceal_naming_result f lthy = + lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming lthy end