|
1 (* Title: HOL/IsTuple.thy |
|
2 Author: Thomas Sewell, NICTA |
|
3 *) |
|
4 |
|
5 header {* Operators on types isomorphic to tuples *} |
|
6 |
1 theory IsTuple imports Product_Type |
7 theory IsTuple imports Product_Type |
2 |
8 |
3 uses ("Tools/istuple_support.ML") |
9 uses ("Tools/istuple_support.ML") |
4 |
10 |
5 begin |
11 begin |
6 |
12 |
|
13 text {* |
|
14 This module provides operators and lemmas for types isomorphic to tuples. |
|
15 These types are used in defining efficient records. Consider the record |
|
16 access/update simplification, alpha (beta_update f rec) = alpha rec for |
|
17 distinct fields alpha and beta of some record type with n fields. There |
|
18 are n^2 such theorems, which is prohibits storage of all of them for |
|
19 large n. The rules can be proved on the fly by case decomposition and |
|
20 simplification in O(n) time. By creating O(n) isomorphic-tuple types |
|
21 while defining the record, however, we can prove the access/update |
|
22 simplification in O(log(n)^2) time. |
|
23 |
|
24 The O(n) cost of case decomposition is not because O(n) steps are taken, |
|
25 but rather because the resulting rule must contain O(n) new variables and |
|
26 an O(n) size concrete record construction. To sidestep this cost, we would |
|
27 like to avoid case decomposition in proving access/update theorems. |
|
28 |
|
29 Record types are defined as isomorphic to tuple types. For instance, a |
|
30 record type with fields 'a, 'b, 'c and 'd might be introduced as |
|
31 isomorphic to 'a \<times> ('b \<times> ('c \<times> 'd)). If we balance the tuple tree to |
|
32 ('a \<times> 'b) \<times> ('c \<times> 'd) then accessors can be defined by converting to |
|
33 the underlying type then using O(log(n)) fst or snd operations. |
|
34 Updators can be defined similarly, if we introduce a fst_update and |
|
35 snd_update function. Furthermore, we can prove the access/update |
|
36 theorem in O(log(n)) steps by using simple rewrites on fst, snd, |
|
37 fst_update and snd_update. |
|
38 |
|
39 The catch is that, although O(log(n)) steps were taken, the underlying |
|
40 type we converted to is a tuple tree of size O(n). Processing this term |
|
41 type wastes performance. We avoid this for large n by taking each |
|
42 subtree of size K and defining a new type isomorphic to that tuple |
|
43 subtree. The record can now be defined as isomorphic to a tuple tree |
|
44 of these O(n/K) new types, or, if n > K*K, we can repeat the process, |
|
45 until the record can be defined in terms of a tuple tree of complexity |
|
46 less than the constant K. |
|
47 |
|
48 If we prove the access/update theorem on this type with the analagous |
|
49 steps to the tuple tree, we consume O(log(n)^2) time as the intermediate |
|
50 terms are O(log(n)) in size and the types needed have size bounded by K. |
|
51 To enable this analagous traversal, we define the functions seen below: |
|
52 istuple_fst, istuple_snd, istuple_fst_update and istuple_snd. These |
|
53 functions generalise tuple operations by taking a parameter that |
|
54 encapsulates a tuple isomorphism. The rewrites needed on these functions |
|
55 now need an additional assumption which is that the isomorphism works. |
|
56 |
|
57 These rewrites are typically used in a structured way. With a little |
|
58 thinking they can be presented as an introduction rule set rather than |
|
59 a rewrite rule set. This is an optimisation, as net matching can be |
|
60 performed at one term location for each step rather than the simplifier |
|
61 searching the term for possible applications. |
|
62 *} |
|
63 |
|
64 typedef ('a, 'b, 'c) tuple_isomorphism |
|
65 = "UNIV :: (('a \<Rightarrow> ('b \<times> 'c)) \<times> (('b \<times> 'c) \<Rightarrow> 'a)) set" |
|
66 by simp |
|
67 |
7 constdefs |
68 constdefs |
8 istuple_fst :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> 'a \<Rightarrow> 'b" |
69 "TupleIsomorphism repr abst \<equiv> Abs_tuple_isomorphism (repr, abst)" |
9 "istuple_fst isom \<equiv> (fst \<circ> isom)" |
70 |
10 istuple_snd :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> 'a \<Rightarrow> 'c" |
71 constdefs |
11 "istuple_snd isom \<equiv> (snd \<circ> isom)" |
72 istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" |
12 istuple_fst_update :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> (('b \<times> 'c) \<Rightarrow> 'a) |
73 "istuple_fst isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in fst \<circ> repr" |
13 \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" |
74 istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" |
14 "istuple_fst_update isom inv \<equiv> \<lambda>f v. inv (f (fst (isom v)), snd (isom v))" |
75 "istuple_snd isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in snd \<circ> repr" |
15 istuple_snd_update :: "('a \<Rightarrow> ('b \<times> 'c)) \<Rightarrow> (('b \<times> 'c) \<Rightarrow> 'a) |
76 istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" |
16 \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" |
77 "istuple_fst_update isom \<equiv> |
17 "istuple_snd_update isom inv \<equiv> \<lambda>f v. inv (fst (isom v), f (snd (isom v)))" |
78 let (repr, abst) = Rep_tuple_isomorphism isom in |
|
79 (\<lambda>f v. abst (f (fst (repr v)), snd (repr v)))" |
|
80 istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" |
|
81 "istuple_snd_update isom \<equiv> |
|
82 let (repr, abst) = Rep_tuple_isomorphism isom in |
|
83 (\<lambda>f v. abst (fst (repr v), f (snd (repr v))))" |
|
84 istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" |
|
85 "istuple_cons isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in curry abst" |
|
86 |
|
87 text {* |
|
88 These predicates are used in the introduction rule set to constrain |
|
89 matching appropriately. The elimination rules for them produce the |
|
90 desired theorems once they are proven. The final introduction rules are |
|
91 used when no further rules from the introduction rule set can apply. |
|
92 *} |
18 |
93 |
19 constdefs |
94 constdefs |
20 istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" |
95 istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" |
21 "istuple_surjective_proof_assist x y f \<equiv> f x = y" |
96 "istuple_surjective_proof_assist x y f \<equiv> f x = y" |
22 istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) |
97 istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) |
119 lemma istuple_surjective_proof_assist_idE: |
194 lemma istuple_surjective_proof_assist_idE: |
120 "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y" |
195 "istuple_surjective_proof_assist x y id \<Longrightarrow> x = y" |
121 by (simp add: istuple_surjective_proof_assist_def) |
196 by (simp add: istuple_surjective_proof_assist_def) |
122 |
197 |
123 locale isomorphic_tuple = |
198 locale isomorphic_tuple = |
124 fixes isom :: "'a \<Rightarrow> ('b \<times> 'c)" and inv :: "('b \<times> 'c) \<Rightarrow> 'a" |
199 fixes isom :: "('a, 'b, 'c) tuple_isomorphism" |
125 and cons :: "'b \<Rightarrow> 'c \<Rightarrow> 'a" |
200 and repr and abst |
126 assumes isom_eq: "(isom x = isom y) = (x = y)" |
201 defines "repr \<equiv> fst (Rep_tuple_isomorphism isom)" |
127 and inverse_inv: "isom (inv v) = v" |
202 defines "abst \<equiv> snd (Rep_tuple_isomorphism isom)" |
128 and cons_def: "cons \<equiv> curry inv" |
203 assumes repr_inv: "\<And>x. abst (repr x) = x" |
|
204 assumes abst_inv: "\<And>y. repr (abst y) = y" |
129 |
205 |
130 begin |
206 begin |
131 |
207 |
132 lemma inverse_isom: |
208 lemma repr_inj: |
133 "(inv (isom v)) = v" |
209 "(repr x = repr y) = (x = y)" |
134 by (rule iffD1 [OF isom_eq], simp add: inverse_inv) |
210 apply (rule iffI, simp_all) |
135 |
211 apply (drule_tac f=abst in arg_cong, simp add: repr_inv) |
136 lemma inv_eq: |
212 done |
137 "(inv x = inv y) = (x = y)" |
213 |
138 apply (rule iffI) |
214 lemma abst_inj: |
139 apply (drule arg_cong[where f=isom]) |
215 "(abst x = abst y) = (x = y)" |
140 apply (simp add: inverse_inv) |
216 apply (rule iffI, simp_all) |
141 apply simp |
217 apply (drule_tac f=repr in arg_cong, simp add: abst_inv) |
142 done |
218 done |
143 |
219 |
144 lemmas simps = isom_eq inv_eq inverse_inv inverse_isom cons_def |
220 lemma split_Rep: |
|
221 "split f (Rep_tuple_isomorphism isom) |
|
222 = f repr abst" |
|
223 by (simp add: split_def repr_def abst_def) |
|
224 |
|
225 lemmas simps = Let_def split_Rep repr_inv abst_inv repr_inj abst_inj |
145 |
226 |
146 lemma istuple_access_update_fst_fst: |
227 lemma istuple_access_update_fst_fst: |
147 "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow> |
228 "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow> |
148 (f o istuple_fst isom) o (istuple_fst_update isom inv o h) g |
229 (f o istuple_fst isom) o (istuple_fst_update isom o h) g |
149 = j o (f o istuple_fst isom)" |
230 = j o (f o istuple_fst isom)" |
150 by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps |
231 by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps |
151 intro!: ext elim!: o_eq_elim) |
232 intro!: ext elim!: o_eq_elim) |
152 |
233 |
153 lemma istuple_access_update_snd_snd: |
234 lemma istuple_access_update_snd_snd: |
154 "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow> |
235 "\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow> |
155 (f o istuple_snd isom) o (istuple_snd_update isom inv o h) g |
236 (f o istuple_snd isom) o (istuple_snd_update isom o h) g |
156 = j o (f o istuple_snd isom)" |
237 = j o (f o istuple_snd isom)" |
157 by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps |
238 by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps |
158 intro!: ext elim!: o_eq_elim) |
239 intro!: ext elim!: o_eq_elim) |
159 |
240 |
160 lemma istuple_access_update_fst_snd: |
241 lemma istuple_access_update_fst_snd: |
161 "(f o istuple_fst isom) o (istuple_snd_update isom inv o h) g |
242 "(f o istuple_fst isom) o (istuple_snd_update isom o h) g |
162 = id o (f o istuple_fst isom)" |
243 = id o (f o istuple_fst isom)" |
163 by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps |
244 by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps |
164 intro!: ext elim!: o_eq_elim) |
245 intro!: ext elim!: o_eq_elim) |
165 |
246 |
166 lemma istuple_access_update_snd_fst: |
247 lemma istuple_access_update_snd_fst: |
167 "(f o istuple_snd isom) o (istuple_fst_update isom inv o h) g |
248 "(f o istuple_snd isom) o (istuple_fst_update isom o h) g |
168 = id o (f o istuple_snd isom)" |
249 = id o (f o istuple_snd isom)" |
169 by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps |
250 by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps |
170 intro!: ext elim!: o_eq_elim) |
251 intro!: ext elim!: o_eq_elim) |
171 |
252 |
172 lemma istuple_update_swap_fst_fst: |
253 lemma istuple_update_swap_fst_fst: |
173 "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow> |
254 "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow> |
174 (istuple_fst_update isom inv o h) f o (istuple_fst_update isom inv o j) g |
255 (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g |
175 = (istuple_fst_update isom inv o j) g o (istuple_fst_update isom inv o h) f" |
256 = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f" |
176 by (clarsimp simp: istuple_fst_update_def simps |
257 by (clarsimp simp: istuple_fst_update_def simps |
177 intro!: ext elim!: o_eq_elim) |
258 intro!: ext elim!: o_eq_elim) |
178 |
259 |
179 lemma istuple_update_swap_snd_snd: |
260 lemma istuple_update_swap_snd_snd: |
180 "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow> |
261 "\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow> |
181 (istuple_snd_update isom inv o h) f o (istuple_snd_update isom inv o j) g |
262 (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g |
182 = (istuple_snd_update isom inv o j) g o (istuple_snd_update isom inv o h) f" |
263 = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f" |
183 by (clarsimp simp: istuple_snd_update_def simps |
264 by (clarsimp simp: istuple_snd_update_def simps |
184 intro!: ext elim!: o_eq_elim) |
265 intro!: ext elim!: o_eq_elim) |
185 |
266 |
186 lemma istuple_update_swap_fst_snd: |
267 lemma istuple_update_swap_fst_snd: |
187 "(istuple_snd_update isom inv o h) f o (istuple_fst_update isom inv o j) g |
268 "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g |
188 = (istuple_fst_update isom inv o j) g o (istuple_snd_update isom inv o h) f" |
269 = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f" |
189 by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps |
270 by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps |
190 intro!: ext elim!: o_eq_elim) |
271 intro!: ext elim!: o_eq_elim) |
191 |
272 |
192 lemma istuple_update_swap_snd_fst: |
273 lemma istuple_update_swap_snd_fst: |
193 "(istuple_fst_update isom inv o h) f o (istuple_snd_update isom inv o j) g |
274 "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g |
194 = (istuple_snd_update isom inv o j) g o (istuple_fst_update isom inv o h) f" |
275 = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f" |
195 by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps |
276 by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps |
196 intro!: ext elim!: o_eq_elim) |
277 intro!: ext elim!: o_eq_elim) |
197 |
278 |
198 lemma istuple_update_compose_fst_fst: |
279 lemma istuple_update_compose_fst_fst: |
199 "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow> |
280 "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow> |
200 (istuple_fst_update isom inv o h) f o (istuple_fst_update isom inv o j) g |
281 (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g |
201 = (istuple_fst_update isom inv o k) (f o g)" |
282 = (istuple_fst_update isom o k) (f o g)" |
202 by (fastsimp simp: istuple_fst_update_def simps |
283 by (fastsimp simp: istuple_fst_update_def simps |
203 intro!: ext elim!: o_eq_elim dest: fun_cong) |
284 intro!: ext elim!: o_eq_elim dest: fun_cong) |
204 |
285 |
205 lemma istuple_update_compose_snd_snd: |
286 lemma istuple_update_compose_snd_snd: |
206 "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow> |
287 "\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow> |
207 (istuple_snd_update isom inv o h) f o (istuple_snd_update isom inv o j) g |
288 (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g |
208 = (istuple_snd_update isom inv o k) (f o g)" |
289 = (istuple_snd_update isom o k) (f o g)" |
209 by (fastsimp simp: istuple_snd_update_def simps |
290 by (fastsimp simp: istuple_snd_update_def simps |
210 intro!: ext elim!: o_eq_elim dest: fun_cong) |
291 intro!: ext elim!: o_eq_elim dest: fun_cong) |
211 |
292 |
212 lemma istuple_surjective_proof_assist_step: |
293 lemma istuple_surjective_proof_assist_step: |
213 "\<lbrakk> istuple_surjective_proof_assist v a (istuple_fst isom o f); |
294 "\<lbrakk> istuple_surjective_proof_assist v a (istuple_fst isom o f); |
214 istuple_surjective_proof_assist v b (istuple_snd isom o f) \<rbrakk> |
295 istuple_surjective_proof_assist v b (istuple_snd isom o f) \<rbrakk> |
215 \<Longrightarrow> istuple_surjective_proof_assist v (cons a b) f" |
296 \<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f" |
216 by (clarsimp simp: istuple_surjective_proof_assist_def simps |
297 by (clarsimp simp: istuple_surjective_proof_assist_def simps |
217 istuple_fst_def istuple_snd_def) |
298 istuple_fst_def istuple_snd_def istuple_cons_def) |
218 |
299 |
219 lemma istuple_fst_update_accessor_cong_assist: |
300 lemma istuple_fst_update_accessor_cong_assist: |
220 "istuple_update_accessor_cong_assist f g \<Longrightarrow> |
301 "istuple_update_accessor_cong_assist f g \<Longrightarrow> |
221 istuple_update_accessor_cong_assist (istuple_fst_update isom inv o f) (g o istuple_fst isom)" |
302 istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)" |
222 by (simp add: istuple_update_accessor_cong_assist_def istuple_fst_update_def istuple_fst_def simps) |
303 by (clarsimp simp: istuple_update_accessor_cong_assist_def simps |
|
304 istuple_fst_update_def istuple_fst_def) |
223 |
305 |
224 lemma istuple_snd_update_accessor_cong_assist: |
306 lemma istuple_snd_update_accessor_cong_assist: |
225 "istuple_update_accessor_cong_assist f g \<Longrightarrow> |
307 "istuple_update_accessor_cong_assist f g \<Longrightarrow> |
226 istuple_update_accessor_cong_assist (istuple_snd_update isom inv o f) (g o istuple_snd isom)" |
308 istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)" |
227 by (simp add: istuple_update_accessor_cong_assist_def istuple_snd_update_def istuple_snd_def simps) |
309 by (clarsimp simp: istuple_update_accessor_cong_assist_def simps |
|
310 istuple_snd_update_def istuple_snd_def) |
228 |
311 |
229 lemma istuple_fst_update_accessor_eq_assist: |
312 lemma istuple_fst_update_accessor_eq_assist: |
230 "istuple_update_accessor_eq_assist f g a u a' v \<Longrightarrow> |
313 "istuple_update_accessor_eq_assist f g a u a' v \<Longrightarrow> |
231 istuple_update_accessor_eq_assist (istuple_fst_update isom inv o f) (g o istuple_fst isom) |
314 istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom) |
232 (cons a b) u (cons a' b) v" |
315 (istuple_cons isom a b) u (istuple_cons isom a' b) v" |
233 by (simp add: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def simps |
316 by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def |
234 istuple_update_accessor_cong_assist_def) |
317 istuple_update_accessor_cong_assist_def istuple_cons_def simps) |
235 |
318 |
236 lemma istuple_snd_update_accessor_eq_assist: |
319 lemma istuple_snd_update_accessor_eq_assist: |
237 "istuple_update_accessor_eq_assist f g b u b' v \<Longrightarrow> |
320 "istuple_update_accessor_eq_assist f g b u b' v \<Longrightarrow> |
238 istuple_update_accessor_eq_assist (istuple_snd_update isom inv o f) (g o istuple_snd isom) |
321 istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom) |
239 (cons a b) u (cons a b') v" |
322 (istuple_cons isom a b) u (istuple_cons isom a b') v" |
240 by (simp add: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def simps |
323 by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def |
241 istuple_update_accessor_cong_assist_def) |
324 istuple_update_accessor_cong_assist_def istuple_cons_def simps) |
242 |
325 |
243 lemma cons_conj_eqI: |
326 lemma istuple_cons_conj_eqI: |
244 "\<lbrakk> (a = c \<and> b = d \<and> P) = Q \<rbrakk> \<Longrightarrow> |
327 "\<lbrakk> (a = c \<and> b = d \<and> P) = Q \<rbrakk> \<Longrightarrow> |
245 (cons a b = cons c d \<and> P) = Q" |
328 (istuple_cons isom a b = istuple_cons isom c d \<and> P) = Q" |
246 by (simp add: simps) |
329 by (clarsimp simp: istuple_cons_def simps) |
247 |
330 |
248 lemmas intros = |
331 lemmas intros = |
249 istuple_access_update_fst_fst |
332 istuple_access_update_fst_fst |
250 istuple_access_update_snd_snd |
333 istuple_access_update_snd_snd |
251 istuple_access_update_fst_snd |
334 istuple_access_update_fst_snd |