1theory Datatype_Record_Examples
2imports "HOL-Library.Datatype_Records"
3begin
4
5text \<open>Standard usage\<close>
6
7datatype_record ('a, 'b) foo =
8  field_1 :: 'a
9  field_2 :: 'b
10
11lemma "\<lparr> field_1 = 3, field_2 = () \<rparr> = (make_foo 3 () :: (nat, unit) foo)" ..
12
13lemma "(make_foo a b) \<lparr> field_1 := y \<rparr> = make_foo y b"
14  by (simp add: datatype_record_update)
15
16lemma "(make_foo a b) \<lparr> foo.field_1 := y \<rparr> = make_foo y b"
17  by (simp add: datatype_record_update)
18
19text \<open>Existing datatypes\<close>
20
21datatype x = X (a: int) (b: int)
22
23lemma "\<lparr> a = 1, b = 2 \<rparr> = X 1 2" ..
24
25local_setup \<open>Datatype_Records.mk_update_defs \<^type_name>\<open>x\<close>\<close>
26
27lemma "(X 1 2) \<lparr> b := 3 \<rparr> = X 1 3"
28  by (simp add: datatype_record_update)
29
30text \<open>Nested recursion\<close>
31
32datatype_record 'a container =
33  content :: "'a option"
34
35datatype 'a contrived = Contrived "'a contrived container"
36
37term "Contrived \<lparr> content = None \<rparr>"
38
39text \<open>Supports features of @{command datatype}\<close>
40
41datatype_record (plugins del: code) (dead 'a :: finite, b_set: 'b) rec =
42  field_1 :: 'a
43  field_2 :: 'b
44
45lemma "b_set \<lparr> field_1 = True, field_2 = False \<rparr> = {False}"
46  by simp
47
48text \<open>More tests\<close>
49
50datatype_record ('a, 'b) test1 =
51  field_t11 :: 'a
52  field_t12 :: 'b
53  field_t13 :: nat
54  field_t14 :: int
55
56thm test1.record_simps
57
58definition ID where "ID x = x"
59lemma ID_cong[cong]: "ID x = ID x" by (rule refl)
60
61lemma "update_field_t11 f (update_field_t12 g (update_field_t11 h x)) = ID (update_field_t12 g (update_field_t11 (\<lambda>x. f (h x)) x))"
62  apply (simp only: test1.record_simps)
63  apply (subst ID_def)
64  apply (rule refl)
65  done
66
67end