misc tuning;

--- 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_>\<open>Quotient _ _ for rel abs rep cr\<close> = (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>\<open>fun A B\<close> = 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>\<open>bool\<close>) => (typ1, typ2)
-    | _ => error "relation_types: not a relation"
+fun relation_types typ =
+  (case strip_type typ of
+    ([typ1, typ2], \<^Type>\<open>bool\<close>) => (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