equal
deleted
inserted
replaced
1 (* Title: HOL/ex/Records.thy |
1 (* Title: HOL/ex/Records.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen |
3 Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, |
|
4 TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 *) |
6 *) |
6 |
7 |
7 header {* Using extensible records in HOL -- points and coloured points *} |
8 header {* Using extensible records in HOL -- points and coloured points *} |
8 |
9 |
17 text {* |
18 text {* |
18 Apart many other things, above record declaration produces the |
19 Apart many other things, above record declaration produces the |
19 following theorems: |
20 following theorems: |
20 *} |
21 *} |
21 |
22 |
|
23 |
22 thm "point.simps" |
24 thm "point.simps" |
23 thm "point.iffs" |
25 thm "point.iffs" |
24 thm "point.defs" |
26 thm "point.defs" |
25 |
27 |
26 text {* |
28 text {* |
27 The set of theorems @{thm [source] point.simps} is added |
29 The set of theorems @{thm [source] point.simps} is added |
28 automatically to the standard simpset, @{thm [source] point.iffs} is |
30 automatically to the standard simpset, @{thm [source] point.iffs} is |
29 added to the Classical Reasoner and Simplifier context. |
31 added to the Classical Reasoner and Simplifier context. |
30 |
32 |
31 \medskip Record declarations define new type abbreviations: |
33 \medskip Record declarations define new types and type abbreviations: |
32 @{text [display] |
34 @{text [display] |
33 " point = (| xpos :: nat, ypos :: nat |) |
35 " point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type |
34 'a point_scheme = (| xpos :: nat, ypos :: nat, ... :: 'a |)"} |
36 'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr> = 'a point_ext_type"} |
35 *} |
37 *} |
36 |
38 |
37 consts foo1 :: point |
39 consts foo1 :: point |
38 consts foo2 :: "(| xpos :: nat, ypos :: nat |)" |
40 consts foo2 :: "(| xpos :: nat, ypos :: nat |)" |
39 consts foo3 :: "'a => 'a point_scheme" |
41 consts foo3 :: "'a => 'a point_scheme" |
105 text {* |
107 text {* |
106 \medskip Representation of records by cases or (degenerate) |
108 \medskip Representation of records by cases or (degenerate) |
107 induction. |
109 induction. |
108 *} |
110 *} |
109 |
111 |
110 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)" |
112 lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)" |
111 proof (cases r) |
113 proof (cases r) |
112 fix xpos ypos more |
114 fix xpos ypos more |
113 assume "r = (| xpos = xpos, ypos = ypos, ... = more |)" |
115 assume "r = (| xpos = xpos, ypos = ypos, ... = more |)" |
114 thus ?thesis by simp |
116 thus ?thesis by simp |
115 qed |
117 qed |
172 record cpoint = point + |
174 record cpoint = point + |
173 colour :: colour |
175 colour :: colour |
174 |
176 |
175 |
177 |
176 text {* |
178 text {* |
177 The record declaration defines new type constructors: |
179 The record declaration defines a new type constructure and abbreviations: |
178 @{text [display] |
180 @{text [display] |
179 " cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) |
181 " cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) = |
180 'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"} |
182 () cpoint_ext_type point_ext_type |
|
183 'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) = |
|
184 'a cpoint_ext_type point_ext_type"} |
181 *} |
185 *} |
182 |
186 |
183 consts foo6 :: cpoint |
187 consts foo6 :: cpoint |
184 consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)" |
188 consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)" |
185 consts foo8 :: "'a cpoint_scheme" |
189 consts foo8 :: "'a cpoint_scheme" |