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