equal
deleted
inserted
replaced
5 *) |
5 *) |
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 |
|
11 val dest_Quotient: term -> term * term * term * term |
10 val dest_Quotient: term -> term * term * term * term |
12 |
11 |
13 val quot_thm_rel: thm -> term |
12 val quot_thm_rel: thm -> term |
14 val quot_thm_abs: thm -> term |
13 val quot_thm_abs: thm -> term |
15 val quot_thm_rep: thm -> term |
14 val quot_thm_rep: thm -> term |
38 struct |
37 struct |
39 |
38 |
40 infix 0 MRSL |
39 infix 0 MRSL |
41 |
40 |
42 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm |
41 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm |
43 |
|
44 fun option_fold a _ NONE = a |
|
45 | option_fold _ f (SOME x) = f x |
|
46 |
42 |
47 fun dest_Quotient (Const (\<^const_name>\<open>Quotient\<close>, _) $ rel $ abs $ rep $ cr) |
43 fun dest_Quotient (Const (\<^const_name>\<open>Quotient\<close>, _) $ rel $ abs $ rep $ cr) |
48 = (rel, abs, rep, cr) |
44 = (rel, abs, rep, cr) |
49 | dest_Quotient t = raise TERM ("dest_Quotient", [t]) |
45 | dest_Quotient t = raise TERM ("dest_Quotient", [t]) |
50 |
46 |