src/HOL/Tools/Lifting/lifting_util.ML

--- a/src/HOL/Tools/Lifting/lifting_util.ML	Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Fri Mar 08 13:14:23 2013 +0100
@@ -8,6 +8,7 @@
 sig
   val MRSL: thm list * thm -> thm
   val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b
+  val map_snd: ('b -> 'c) -> ('a * 'b) list -> ('a * 'c) list
   val dest_Quotient: term -> term * term * term * term
 
   val quot_thm_rel: thm -> term
@@ -15,6 +16,19 @@
   val quot_thm_rep: thm -> term
   val quot_thm_crel: thm -> term
   val quot_thm_rty_qty: thm -> typ * typ
+
+  val undisch: thm -> thm
+  val undisch_all: thm -> thm
+  val is_fun_type: typ -> bool
+  val get_args: int -> term -> term list
+  val strip_args: int -> term -> term
+  val all_args_conv: conv -> conv
+  val is_Type: typ -> bool
+  val is_fun_rel: term -> bool
+  val relation_types: typ -> typ * typ
+  val bottom_rewr_conv: thm list -> conv
+  val mk_HOL_eq: thm -> thm
+  val safe_HOL_meta_eq: thm -> thm
 end;
 
 
@@ -28,6 +42,8 @@
 fun option_fold a _ NONE = a
   | option_fold _ f (SOME x) = f x
 
+fun map_snd f xs = map (fn (a, b) => (a, f b)) xs
+
 fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr)
       = (rel, abs, rep, cr)
   | dest_Quotient t = raise TERM ("dest_Quotient", [t])
@@ -61,4 +77,40 @@
     (domain_type abs_type, range_type abs_type)
   end
 
+fun undisch thm =
+  let
+    val assm = Thm.cprem_of thm 1
+  in
+    Thm.implies_elim thm (Thm.assume assm)
+  end
+
+fun undisch_all thm = funpow (nprems_of thm) undisch thm
+
+fun is_fun_type (Type (@{type_name fun}, _)) = true
+  | is_fun_type _ = false
+
+fun get_args n = rev o fst o funpow_yield n (swap o dest_comb)
+
+fun strip_args n = funpow n (fst o dest_comb)
+
+fun all_args_conv conv ctm = 
+  (Conv.combination_conv (Conv.try_conv (all_args_conv conv)) conv) ctm
+
+fun is_Type (Type _) = true
+  | is_Type _ = false
+
+fun is_fun_rel (Const (@{const_name "fun_rel"}, _) $ _ $ _) = true
+  | is_fun_rel _ = false
+
+fun relation_types typ = 
+  case strip_type typ of
+    ([typ1, typ2], @{typ bool}) => (typ1, typ2)
+    | _ => error "relation_types: not a relation"
+
+fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
+
+fun mk_HOL_eq r = r RS @{thm meta_eq_to_obj_eq}
+
+fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
+
 end;