adding creation of exhaustive generators for records; simplifying dependencies in Main theory
1 (* Title: HOL/Record.thy
2 Author: Wolfgang Naraschewski, TU Muenchen
3 Author: Markus Wenzel, TU Muenchen
4 Author: Norbert Schirmer, TU Muenchen
5 Author: Thomas Sewell, NICTA
6 Author: Florian Haftmann, TU Muenchen
9 header {* Extensible records with structural subtyping *}
12 imports Plain Quickcheck_Exhaustive
13 uses ("Tools/record.ML")
16 subsection {* Introduction *}
19 Records are isomorphic to compound tuple types. To implement
20 efficient records, we make this isomorphism explicit. Consider the
21 record access/update simplification @{text "alpha (beta_update f
22 rec) = alpha rec"} for distinct fields alpha and beta of some record
23 rec with n fields. There are @{text "n ^ 2"} such theorems, which
24 prohibits storage of all of them for large n. The rules can be
25 proved on the fly by case decomposition and simplification in O(n)
26 time. By creating O(n) isomorphic-tuple types while defining the
27 record, however, we can prove the access/update simplification in
28 @{text "O(log(n)^2)"} time.
30 The O(n) cost of case decomposition is not because O(n) steps are
31 taken, but rather because the resulting rule must contain O(n) new
32 variables and an O(n) size concrete record construction. To sidestep
33 this cost, we would like to avoid case decomposition in proving
34 access/update theorems.
36 Record types are defined as isomorphic to tuple types. For instance,
37 a record type with fields @{text "'a"}, @{text "'b"}, @{text "'c"}
38 and @{text "'d"} might be introduced as isomorphic to @{text "'a \<times>
39 ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to @{text "('a \<times>
40 'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to the
41 underlying type then using O(log(n)) fst or snd operations.
42 Updators can be defined similarly, if we introduce a @{text
43 "fst_update"} and @{text "snd_update"} function. Furthermore, we can
44 prove the access/update theorem in O(log(n)) steps by using simple
45 rewrites on fst, snd, @{text "fst_update"} and @{text "snd_update"}.
47 The catch is that, although O(log(n)) steps were taken, the
48 underlying type we converted to is a tuple tree of size
49 O(n). Processing this term type wastes performance. We avoid this
50 for large n by taking each subtree of size K and defining a new type
51 isomorphic to that tuple subtree. A record can now be defined as
52 isomorphic to a tuple tree of these O(n/K) new types, or, if @{text
53 "n > K*K"}, we can repeat the process, until the record can be
54 defined in terms of a tuple tree of complexity less than the
57 If we prove the access/update theorem on this type with the
58 analagous steps to the tuple tree, we consume @{text "O(log(n)^2)"}
59 time as the intermediate terms are @{text "O(log(n))"} in size and
60 the types needed have size bounded by K. To enable this analagous
61 traversal, we define the functions seen below: @{text
62 "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"}
63 and @{text "iso_tuple_snd_update"}. These functions generalise tuple
64 operations by taking a parameter that encapsulates a tuple
65 isomorphism. The rewrites needed on these functions now need an
66 additional assumption which is that the isomorphism works.
68 These rewrites are typically used in a structured way. They are here
69 presented as the introduction rule @{text "isomorphic_tuple.intros"}
70 rather than as a rewrite rule set. The introduction form is an
71 optimisation, as net matching can be performed at one term location
72 for each step rather than the simplifier searching the term for
73 possible pattern matches. The rule set is used as it is viewed
74 outside the locale, with the locale assumption (that the isomorphism
75 is valid) left as a rule assumption. All rules are structured to aid
76 net matching, using either a point-free form or an encapsulating
80 subsection {* Operators and lemmas for types isomorphic to tuples *}
82 datatype ('a, 'b, 'c) tuple_isomorphism =
83 Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
86 repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where
87 "repr (Tuple_Isomorphism r a) = r"
90 abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
91 "abst (Tuple_Isomorphism r a) = a"
94 iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
95 "iso_tuple_fst isom = fst \<circ> repr isom"
98 iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
99 "iso_tuple_snd isom = snd \<circ> repr isom"
102 iso_tuple_fst_update ::
103 "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
104 "iso_tuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
107 iso_tuple_snd_update ::
108 "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
109 "iso_tuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
113 "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
114 "iso_tuple_cons isom = curry (abst isom)"
117 subsection {* Logical infrastructure for records *}
120 iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
121 "iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
124 iso_tuple_update_accessor_cong_assist ::
125 "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
126 "iso_tuple_update_accessor_cong_assist upd ac \<longleftrightarrow>
127 (\<forall>f v. upd (\<lambda>x. f (ac v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
130 iso_tuple_update_accessor_eq_assist ::
131 "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
132 "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<longleftrightarrow>
133 upd f v = v' \<and> ac v = x \<and> iso_tuple_update_accessor_cong_assist upd ac"
135 lemma update_accessor_congruence_foldE:
136 assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
137 and r: "r = r'" and v: "ac r' = v'"
138 and f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
139 shows "upd f r = upd f' r'"
140 using uac r v [symmetric]
141 apply (subgoal_tac "upd (\<lambda>x. f (ac r')) r' = upd (\<lambda>x. f' (ac r')) r'")
142 apply (simp add: iso_tuple_update_accessor_cong_assist_def)
146 lemma update_accessor_congruence_unfoldE:
147 "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
148 r = r' \<Longrightarrow> ac r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v) \<Longrightarrow>
150 apply (erule(2) update_accessor_congruence_foldE)
154 lemma iso_tuple_update_accessor_cong_assist_id:
155 "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow> upd id = id"
156 by rule (simp add: iso_tuple_update_accessor_cong_assist_def)
158 lemma update_accessor_noopE:
159 assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
160 and ac: "f (ac x) = ac x"
163 by (simp add: ac iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
164 cong: update_accessor_congruence_unfoldE [OF uac])
166 lemma update_accessor_noop_compE:
167 assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
168 and ac: "f (ac x) = ac x"
169 shows "upd (g \<circ> f) x = upd g x"
170 by (simp add: ac cong: update_accessor_congruence_unfoldE[OF uac])
172 lemma update_accessor_cong_assist_idI:
173 "iso_tuple_update_accessor_cong_assist id id"
174 by (simp add: iso_tuple_update_accessor_cong_assist_def)
176 lemma update_accessor_cong_assist_triv:
177 "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
178 iso_tuple_update_accessor_cong_assist upd ac"
181 lemma update_accessor_accessor_eqE:
182 "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> ac v = x"
183 by (simp add: iso_tuple_update_accessor_eq_assist_def)
185 lemma update_accessor_updator_eqE:
186 "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> upd f v = v'"
187 by (simp add: iso_tuple_update_accessor_eq_assist_def)
189 lemma iso_tuple_update_accessor_eq_assist_idI:
190 "v' = f v \<Longrightarrow> iso_tuple_update_accessor_eq_assist id id v f v' v"
191 by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
193 lemma iso_tuple_update_accessor_eq_assist_triv:
194 "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
195 iso_tuple_update_accessor_eq_assist upd ac v f v' x"
198 lemma iso_tuple_update_accessor_cong_from_eq:
199 "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
200 iso_tuple_update_accessor_cong_assist upd ac"
201 by (simp add: iso_tuple_update_accessor_eq_assist_def)
203 lemma iso_tuple_surjective_proof_assistI:
204 "f x = y \<Longrightarrow> iso_tuple_surjective_proof_assist x y f"
205 by (simp add: iso_tuple_surjective_proof_assist_def)
207 lemma iso_tuple_surjective_proof_assist_idE:
208 "iso_tuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
209 by (simp add: iso_tuple_surjective_proof_assist_def)
211 locale isomorphic_tuple =
212 fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
213 assumes repr_inv: "\<And>x. abst isom (repr isom x) = x"
214 and abst_inv: "\<And>y. repr isom (abst isom y) = y"
217 lemma repr_inj: "repr isom x = repr isom y \<longleftrightarrow> x = y"
218 by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"]
221 lemma abst_inj: "abst isom x = abst isom y \<longleftrightarrow> x = y"
222 by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"]
225 lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj
227 lemma iso_tuple_access_update_fst_fst:
228 "f o h g = j o f \<Longrightarrow>
229 (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g =
230 j o (f o iso_tuple_fst isom)"
231 by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps
232 intro!: ext elim!: o_eq_elim)
234 lemma iso_tuple_access_update_snd_snd:
235 "f o h g = j o f \<Longrightarrow>
236 (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g =
237 j o (f o iso_tuple_snd isom)"
238 by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps
239 intro!: ext elim!: o_eq_elim)
241 lemma iso_tuple_access_update_fst_snd:
242 "(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g =
243 id o (f o iso_tuple_fst isom)"
244 by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps
245 intro!: ext elim!: o_eq_elim)
247 lemma iso_tuple_access_update_snd_fst:
248 "(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g =
249 id o (f o iso_tuple_snd isom)"
250 by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps
251 intro!: ext elim!: o_eq_elim)
253 lemma iso_tuple_update_swap_fst_fst:
254 "h f o j g = j g o h f \<Longrightarrow>
255 (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g =
256 (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f"
257 by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
259 lemma iso_tuple_update_swap_snd_snd:
260 "h f o j g = j g o h f \<Longrightarrow>
261 (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g =
262 (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f"
263 by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
265 lemma iso_tuple_update_swap_fst_snd:
266 "(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g =
267 (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f"
268 by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def
271 lemma iso_tuple_update_swap_snd_fst:
272 "(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g =
273 (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f"
274 by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext)
276 lemma iso_tuple_update_compose_fst_fst:
277 "h f o j g = k (f o g) \<Longrightarrow>
278 (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g =
279 (iso_tuple_fst_update isom o k) (f o g)"
280 by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
282 lemma iso_tuple_update_compose_snd_snd:
283 "h f o j g = k (f o g) \<Longrightarrow>
284 (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g =
285 (iso_tuple_snd_update isom o k) (f o g)"
286 by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
288 lemma iso_tuple_surjective_proof_assist_step:
289 "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \<Longrightarrow>
290 iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom o f) \<Longrightarrow>
291 iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f"
292 by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps
293 iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def)
295 lemma iso_tuple_fst_update_accessor_cong_assist:
296 assumes "iso_tuple_update_accessor_cong_assist f g"
297 shows "iso_tuple_update_accessor_cong_assist
298 (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)"
300 from assms have "f id = id"
301 by (rule iso_tuple_update_accessor_cong_assist_id)
302 with assms show ?thesis
303 by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
304 iso_tuple_fst_update_def iso_tuple_fst_def)
307 lemma iso_tuple_snd_update_accessor_cong_assist:
308 assumes "iso_tuple_update_accessor_cong_assist f g"
309 shows "iso_tuple_update_accessor_cong_assist
310 (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)"
312 from assms have "f id = id"
313 by (rule iso_tuple_update_accessor_cong_assist_id)
314 with assms show ?thesis
315 by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
316 iso_tuple_snd_update_def iso_tuple_snd_def)
319 lemma iso_tuple_fst_update_accessor_eq_assist:
320 assumes "iso_tuple_update_accessor_eq_assist f g a u a' v"
321 shows "iso_tuple_update_accessor_eq_assist
322 (iso_tuple_fst_update isom o f) (g o iso_tuple_fst isom)
323 (iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v"
325 from assms have "f id = id"
326 by (auto simp add: iso_tuple_update_accessor_eq_assist_def
327 intro: iso_tuple_update_accessor_cong_assist_id)
328 with assms show ?thesis
329 by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
330 iso_tuple_fst_update_def iso_tuple_fst_def
331 iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
334 lemma iso_tuple_snd_update_accessor_eq_assist:
335 assumes "iso_tuple_update_accessor_eq_assist f g b u b' v"
336 shows "iso_tuple_update_accessor_eq_assist
337 (iso_tuple_snd_update isom o f) (g o iso_tuple_snd isom)
338 (iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v"
340 from assms have "f id = id"
341 by (auto simp add: iso_tuple_update_accessor_eq_assist_def
342 intro: iso_tuple_update_accessor_cong_assist_id)
343 with assms show ?thesis
344 by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
345 iso_tuple_snd_update_def iso_tuple_snd_def
346 iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
349 lemma iso_tuple_cons_conj_eqI:
350 "a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
351 iso_tuple_cons isom a b = iso_tuple_cons isom c d \<and> P \<longleftrightarrow> Q"
352 by (clarsimp simp: iso_tuple_cons_def simps)
355 iso_tuple_access_update_fst_fst
356 iso_tuple_access_update_snd_snd
357 iso_tuple_access_update_fst_snd
358 iso_tuple_access_update_snd_fst
359 iso_tuple_update_swap_fst_fst
360 iso_tuple_update_swap_snd_snd
361 iso_tuple_update_swap_fst_snd
362 iso_tuple_update_swap_snd_fst
363 iso_tuple_update_compose_fst_fst
364 iso_tuple_update_compose_snd_snd
365 iso_tuple_surjective_proof_assist_step
366 iso_tuple_fst_update_accessor_eq_assist
367 iso_tuple_snd_update_accessor_eq_assist
368 iso_tuple_fst_update_accessor_cong_assist
369 iso_tuple_snd_update_accessor_cong_assist
370 iso_tuple_cons_conj_eqI
374 lemma isomorphic_tuple_intro:
376 assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
377 and abst_inv: "\<And>z. repr (abst z) = z"
378 and v: "v \<equiv> Tuple_Isomorphism repr abst"
379 shows "isomorphic_tuple v"
381 fix x have "repr (abst (repr x)) = repr x"
382 by (simp add: abst_inv)
383 then show "Record.abst v (Record.repr v x) = x"
384 by (simp add: v repr_inj)
387 show "Record.repr v (Record.abst v y) = y"
388 by (simp add: v) (fact abst_inv)
392 "tuple_iso_tuple \<equiv> Tuple_Isomorphism id id"
394 lemma tuple_iso_tuple:
395 "isomorphic_tuple tuple_iso_tuple"
396 by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def)
398 lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
401 lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
404 lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
407 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
410 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
411 by (simp add: comp_def)
413 lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
416 lemma o_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"
420 subsection {* Concrete record syntax *}
432 "_constify" :: "id => ident" ("_")
433 "_constify" :: "longid => ident" ("_")
435 "_field_type" :: "ident => type => field_type" ("(2_ ::/ _)")
436 "" :: "field_type => field_types" ("_")
437 "_field_types" :: "field_type => field_types => field_types" ("_,/ _")
438 "_record_type" :: "field_types => type" ("(3'(| _ |'))")
439 "_record_type_scheme" :: "field_types => type => type" ("(3'(| _,/ (2... ::/ _) |'))")
441 "_field" :: "ident => 'a => field" ("(2_ =/ _)")
442 "" :: "field => fields" ("_")
443 "_fields" :: "field => fields => fields" ("_,/ _")
444 "_record" :: "fields => 'a" ("(3'(| _ |'))")
445 "_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))")
447 "_field_update" :: "ident => 'a => field_update" ("(2_ :=/ _)")
448 "" :: "field_update => field_updates" ("_")
449 "_field_updates" :: "field_update => field_updates => field_updates" ("_,/ _")
450 "_record_update" :: "'a => field_updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900)
453 "_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)")
454 "_record_type_scheme" :: "field_types => type => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
455 "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)")
456 "_record_scheme" :: "fields => 'a => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
457 "_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
460 subsection {* Record package *}
462 use "Tools/record.ML" setup Record.setup
464 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
465 iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
466 iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
467 iso_tuple_update_accessor_eq_assist tuple_iso_tuple