1(* Title: HOL/Tools/Lifting/lifting_util.ML 2 Author: Ondrej Kuncar 3 4General-purpose functions used by the Lifting package. 5*) 6 7signature LIFTING_UTIL = 8sig 9 val MRSL: thm list * thm -> thm 10 val dest_Quotient: term -> term * term * term * term 11 12 val quot_thm_rel: thm -> term 13 val quot_thm_abs: thm -> term 14 val quot_thm_rep: thm -> term 15 val quot_thm_crel: thm -> term 16 val quot_thm_rty_qty: thm -> typ * typ 17 val Quotient_conv: conv -> conv -> conv -> conv -> conv 18 val Quotient_R_conv: conv -> conv 19 20 val undisch: thm -> thm 21 val undisch_all: thm -> thm 22 val is_fun_type: typ -> bool 23 val get_args: int -> term -> term list 24 val strip_args: int -> term -> term 25 val all_args_conv: conv -> conv 26 val same_type_constrs: typ * typ -> bool 27 val Targs: typ -> typ list 28 val Tname: typ -> string 29 val is_rel_fun: term -> bool 30 val relation_types: typ -> typ * typ 31 val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option 32 val conceal_naming_result: (local_theory -> 'a * local_theory) -> local_theory -> 'a * local_theory 33end 34 35 36structure Lifting_Util: LIFTING_UTIL = 37struct 38 39infix 0 MRSL 40 41fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm 42 43fun dest_Quotient (Const (\<^const_name>\<open>Quotient\<close>, _) $ rel $ abs $ rep $ cr) 44 = (rel, abs, rep, cr) 45 | dest_Quotient t = raise TERM ("dest_Quotient", [t]) 46 47(* 48 quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions 49 for destructing quotient theorems (Quotient R Abs Rep T). 50*) 51 52fun quot_thm_rel quot_thm = 53 case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of 54 (rel, _, _, _) => rel 55 56fun quot_thm_abs quot_thm = 57 case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of 58 (_, abs, _, _) => abs 59 60fun quot_thm_rep quot_thm = 61 case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of 62 (_, _, rep, _) => rep 63 64fun quot_thm_crel quot_thm = 65 case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of 66 (_, _, _, crel) => crel 67 68fun quot_thm_rty_qty quot_thm = 69 let 70 val abs = quot_thm_abs quot_thm 71 val abs_type = fastype_of abs 72 in 73 (domain_type abs_type, range_type abs_type) 74 end 75 76fun Quotient_conv R_conv Abs_conv Rep_conv T_conv = Conv.combination_conv (Conv.combination_conv 77 (Conv.combination_conv (Conv.arg_conv R_conv) Abs_conv) Rep_conv) T_conv; 78 79fun Quotient_R_conv R_conv = Quotient_conv R_conv Conv.all_conv Conv.all_conv Conv.all_conv; 80 81fun undisch thm = 82 let 83 val assm = Thm.cprem_of thm 1 84 in 85 Thm.implies_elim thm (Thm.assume assm) 86 end 87 88fun undisch_all thm = funpow (Thm.nprems_of thm) undisch thm 89 90fun is_fun_type (Type (\<^type_name>\<open>fun\<close>, _)) = true 91 | is_fun_type _ = false 92 93fun get_args n = rev o fst o funpow_yield n (swap o dest_comb) 94 95fun strip_args n = funpow n (fst o dest_comb) 96 97fun all_args_conv conv ctm = Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm 98 99fun same_type_constrs (Type (r, _), Type (q, _)) = (r = q) 100 | same_type_constrs _ = false 101 102fun Targs (Type (_, args)) = args 103 | Targs _ = [] 104 105fun Tname (Type (name, _)) = name 106 | Tname _ = "" 107 108fun is_rel_fun (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) = true 109 | is_rel_fun _ = false 110 111fun relation_types typ = 112 case strip_type typ of 113 ([typ1, typ2], \<^typ>\<open>bool\<close>) => (typ1, typ2) 114 | _ => error "relation_types: not a relation" 115 116fun map_interrupt f l = 117 let 118 fun map_interrupt' _ [] l = SOME (rev l) 119 | map_interrupt' f (x::xs) l = (case f x of 120 NONE => NONE 121 | SOME v => map_interrupt' f xs (v::l)) 122 in 123 map_interrupt' f l [] 124 end 125 126fun conceal_naming_result f lthy = 127 lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming lthy; 128 129end 130