equal
deleted
inserted
replaced
6 |
6 |
7 signature LIFTING_UTIL = |
7 signature LIFTING_UTIL = |
8 sig |
8 sig |
9 val MRSL: thm list * thm -> thm |
9 val MRSL: thm list * thm -> thm |
10 val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b |
10 val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b |
11 val map_snd: ('b -> 'c) -> ('a * 'b) list -> ('a * 'c) list |
|
12 val dest_Quotient: term -> term * term * term * term |
11 val dest_Quotient: term -> term * term * term * term |
13 |
12 |
14 val quot_thm_rel: thm -> term |
13 val quot_thm_rel: thm -> term |
15 val quot_thm_abs: thm -> term |
14 val quot_thm_abs: thm -> term |
16 val quot_thm_rep: thm -> term |
15 val quot_thm_rep: thm -> term |
28 val same_type_constrs: typ * typ -> bool |
27 val same_type_constrs: typ * typ -> bool |
29 val Targs: typ -> typ list |
28 val Targs: typ -> typ list |
30 val Tname: typ -> string |
29 val Tname: typ -> string |
31 val is_rel_fun: term -> bool |
30 val is_rel_fun: term -> bool |
32 val relation_types: typ -> typ * typ |
31 val relation_types: typ -> typ * typ |
33 val safe_HOL_meta_eq: thm -> thm |
|
34 val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option |
32 val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option |
35 val conceal_naming_result: (local_theory -> 'a * local_theory) -> local_theory -> 'a * local_theory |
33 val conceal_naming_result: (local_theory -> 'a * local_theory) -> local_theory -> 'a * local_theory |
36 end |
34 end |
37 |
35 |
38 |
36 |
43 |
41 |
44 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm |
42 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm |
45 |
43 |
46 fun option_fold a _ NONE = a |
44 fun option_fold a _ NONE = a |
47 | option_fold _ f (SOME x) = f x |
45 | option_fold _ f (SOME x) = f x |
48 |
|
49 fun map_snd f xs = map (fn (a, b) => (a, f b)) xs |
|
50 |
46 |
51 fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr) |
47 fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr) |
52 = (rel, abs, rep, cr) |
48 = (rel, abs, rep, cr) |
53 | dest_Quotient t = raise TERM ("dest_Quotient", [t]) |
49 | dest_Quotient t = raise TERM ("dest_Quotient", [t]) |
54 |
50 |
119 fun relation_types typ = |
115 fun relation_types typ = |
120 case strip_type typ of |
116 case strip_type typ of |
121 ([typ1, typ2], @{typ bool}) => (typ1, typ2) |
117 ([typ1, typ2], @{typ bool}) => (typ1, typ2) |
122 | _ => error "relation_types: not a relation" |
118 | _ => error "relation_types: not a relation" |
123 |
119 |
124 fun safe_HOL_meta_eq r = HOLogic.mk_obj_eq r handle Thm.THM _ => r |
|
125 |
|
126 fun map_interrupt f l = |
120 fun map_interrupt f l = |
127 let |
121 let |
128 fun map_interrupt' _ [] l = SOME (rev l) |
122 fun map_interrupt' _ [] l = SOME (rev l) |
129 | map_interrupt' f (x::xs) l = (case f x of |
123 | map_interrupt' f (x::xs) l = (case f x of |
130 NONE => NONE |
124 NONE => NONE |