author | wenzelm |
Tue, 05 Nov 2019 14:16:16 +0100 | |
changeset 71046 | b8aeeedf7e68 |
parent 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
1 |
theory Datatype_Record_Examples |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
2 |
imports "HOL-Library.Datatype_Records" |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
3 |
begin |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
4 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
5 |
text \<open>Standard usage\<close> |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
6 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
7 |
datatype_record ('a, 'b) foo = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
8 |
field_1 :: 'a |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
9 |
field_2 :: 'b |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
10 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
11 |
lemma "\<lparr> field_1 = 3, field_2 = () \<rparr> = (make_foo 3 () :: (nat, unit) foo)" .. |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
12 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
13 |
lemma "(make_foo a b) \<lparr> field_1 := y \<rparr> = make_foo y b" |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
14 |
by (simp add: datatype_record_update) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
15 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
16 |
lemma "(make_foo a b) \<lparr> foo.field_1 := y \<rparr> = make_foo y b" |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
17 |
by (simp add: datatype_record_update) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
18 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
19 |
text \<open>Existing datatypes\<close> |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
20 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
21 |
datatype x = X (a: int) (b: int) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
22 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
23 |
lemma "\<lparr> a = 1, b = 2 \<rparr> = X 1 2" .. |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
24 |
|
69597 | 25 |
local_setup \<open>Datatype_Records.mk_update_defs \<^type_name>\<open>x\<close>\<close> |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
26 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
27 |
lemma "(X 1 2) \<lparr> b := 3 \<rparr> = X 1 3" |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
28 |
by (simp add: datatype_record_update) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
29 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
30 |
text \<open>Nested recursion\<close> |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
31 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
32 |
datatype_record 'a container = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
33 |
content :: "'a option" |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
34 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
35 |
datatype 'a contrived = Contrived "'a contrived container" |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
36 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
37 |
term "Contrived \<lparr> content = None \<rparr>" |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
38 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
39 |
text \<open>Supports features of @{command datatype}\<close> |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
40 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
41 |
datatype_record (plugins del: code) (dead 'a :: finite, b_set: 'b) rec = |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
42 |
field_1 :: 'a |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
43 |
field_2 :: 'b |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
44 |
|
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
45 |
lemma "b_set \<lparr> field_1 = True, field_2 = False \<rparr> = {False}" |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
46 |
by simp |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
47 |
|
68686
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
48 |
text \<open>More tests\<close> |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
49 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
50 |
datatype_record ('a, 'b) test1 = |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
51 |
field_t11 :: 'a |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
52 |
field_t12 :: 'b |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
53 |
field_t13 :: nat |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
54 |
field_t14 :: int |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
55 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
56 |
thm test1.record_simps |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
57 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
58 |
definition ID where "ID x = x" |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
59 |
lemma ID_cong[cong]: "ID x = ID x" by (rule refl) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
60 |
|
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
61 |
lemma "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))" |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
62 |
apply (simp only: test1.record_simps) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
63 |
apply (subst ID_def) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
64 |
apply (rule refl) |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
65 |
done |
7f8db1c4ebec
datatype_record produces simp theorems; contributed in part by Yu Zhang
Lars Hupel <lars.hupel@mytum.de>
parents:
67611
diff
changeset
|
66 |
|
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
67 |
end |