author | wenzelm |
Wed, 04 Mar 2015 19:53:18 +0100 | |
changeset 59582 | 0fbed69ff081 |
parent 55945 | e96383acecf9 |
child 60223 | b614363356ed |
permissions | -rw-r--r-- |
47698 | 1 |
(* Title: HOL/Tools/Lifting/lifting_util.ML |
2 |
Author: Ondrej Kuncar |
|
3 |
||
4 |
General-purpose functions used by the Lifting package. |
|
5 |
*) |
|
6 |
||
7 |
signature LIFTING_UTIL = |
|
8 |
sig |
|
9 |
val MRSL: thm list * thm -> thm |
|
50225 | 10 |
val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
11 |
val map_snd: ('b -> 'c) -> ('a * 'b) list -> ('a * 'c) list |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47699
diff
changeset
|
12 |
val dest_Quotient: term -> term * term * term * term |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
13 |
|
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
14 |
val quot_thm_rel: thm -> term |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
15 |
val quot_thm_abs: thm -> term |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
16 |
val quot_thm_rep: thm -> term |
50226 | 17 |
val quot_thm_crel: thm -> term |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
18 |
val quot_thm_rty_qty: thm -> typ * typ |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
19 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
20 |
val undisch: thm -> thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
21 |
val undisch_all: thm -> thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
22 |
val is_fun_type: typ -> bool |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
23 |
val get_args: int -> term -> term list |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
24 |
val strip_args: int -> term -> term |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
25 |
val all_args_conv: conv -> conv |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
26 |
val is_Type: typ -> bool |
55454 | 27 |
val same_type_constrs: typ * typ -> bool |
28 |
val Targs: typ -> typ list |
|
29 |
val Tname: typ -> string |
|
55945 | 30 |
val is_rel_fun: term -> bool |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
31 |
val relation_types: typ -> typ * typ |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
32 |
val mk_HOL_eq: thm -> thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
33 |
val safe_HOL_meta_eq: thm -> thm |
55731
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55456
diff
changeset
|
34 |
val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option |
53651 | 35 |
end |
47698 | 36 |
|
37 |
||
38 |
structure Lifting_Util: LIFTING_UTIL = |
|
39 |
struct |
|
40 |
||
41 |
infix 0 MRSL |
|
42 |
||
43 |
fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm |
|
44 |
||
50225 | 45 |
fun option_fold a _ NONE = a |
46 |
| option_fold _ f (SOME x) = f x |
|
47 |
||
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
48 |
fun map_snd f xs = map (fn (a, b) => (a, f b)) xs |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
49 |
|
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47699
diff
changeset
|
50 |
fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr) |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47699
diff
changeset
|
51 |
= (rel, abs, rep, cr) |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47699
diff
changeset
|
52 |
| dest_Quotient t = raise TERM ("dest_Quotient", [t]) |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47699
diff
changeset
|
53 |
|
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
54 |
(* |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
55 |
quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
56 |
for destructing quotient theorems (Quotient R Abs Rep T). |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
57 |
*) |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
58 |
|
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
59 |
fun quot_thm_rel quot_thm = |
59582 | 60 |
case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
61 |
(rel, _, _, _) => rel |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
62 |
|
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
63 |
fun quot_thm_abs quot_thm = |
59582 | 64 |
case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
65 |
(_, abs, _, _) => abs |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
66 |
|
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
67 |
fun quot_thm_rep quot_thm = |
59582 | 68 |
case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
69 |
(_, _, rep, _) => rep |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
70 |
|
50226 | 71 |
fun quot_thm_crel quot_thm = |
59582 | 72 |
case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of |
50226 | 73 |
(_, _, _, crel) => crel |
74 |
||
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
75 |
fun quot_thm_rty_qty quot_thm = |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
76 |
let |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
77 |
val abs = quot_thm_abs quot_thm |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
78 |
val abs_type = fastype_of abs |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
79 |
in |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
80 |
(domain_type abs_type, range_type abs_type) |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
81 |
end |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47777
diff
changeset
|
82 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
83 |
fun undisch thm = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
84 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
85 |
val assm = Thm.cprem_of thm 1 |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
86 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
87 |
Thm.implies_elim thm (Thm.assume assm) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
88 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
89 |
|
59582 | 90 |
fun undisch_all thm = funpow (Thm.nprems_of thm) undisch thm |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
91 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
92 |
fun is_fun_type (Type (@{type_name fun}, _)) = true |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
93 |
| is_fun_type _ = false |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
94 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
95 |
fun get_args n = rev o fst o funpow_yield n (swap o dest_comb) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
96 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
97 |
fun strip_args n = funpow n (fst o dest_comb) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
98 |
|
55456 | 99 |
fun all_args_conv conv ctm = Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
100 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
101 |
fun is_Type (Type _) = true |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
102 |
| is_Type _ = false |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
103 |
|
55454 | 104 |
fun same_type_constrs (Type (r, _), Type (q, _)) = (r = q) |
105 |
| same_type_constrs _ = false |
|
106 |
||
107 |
fun Targs (Type (_, args)) = args |
|
108 |
| Targs _ = [] |
|
109 |
||
110 |
fun Tname (Type (name, _)) = name |
|
111 |
| Tname _ = "" |
|
112 |
||
55945 | 113 |
fun is_rel_fun (Const (@{const_name "rel_fun"}, _) $ _ $ _) = true |
114 |
| is_rel_fun _ = false |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
115 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
116 |
fun relation_types typ = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
117 |
case strip_type typ of |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
118 |
([typ1, typ2], @{typ bool}) => (typ1, typ2) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
119 |
| _ => error "relation_types: not a relation" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
120 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
121 |
fun mk_HOL_eq r = r RS @{thm meta_eq_to_obj_eq} |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
122 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
123 |
fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
51314
diff
changeset
|
124 |
|
55731
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55456
diff
changeset
|
125 |
fun map_interrupt f l = |
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55456
diff
changeset
|
126 |
let |
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55456
diff
changeset
|
127 |
fun map_interrupt' _ [] l = SOME (rev l) |
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55456
diff
changeset
|
128 |
| map_interrupt' f (x::xs) l = (case f x of |
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55456
diff
changeset
|
129 |
NONE => NONE |
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55456
diff
changeset
|
130 |
| SOME v => map_interrupt' f xs (v::l)) |
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55456
diff
changeset
|
131 |
in |
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55456
diff
changeset
|
132 |
map_interrupt' f l [] |
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55456
diff
changeset
|
133 |
end |
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55456
diff
changeset
|
134 |
|
53651 | 135 |
end |