author  wenzelm 
Sat, 27 May 2006 17:42:02 +0200  
changeset 19736  d8d0f8f51d69 
parent 16417  9bc16273c2d4 
child 21404  eb85850d3eb7 
permissions  rwrr 
10052  1 
(* Title: HOL/ex/Records.thy 
2 
ID: $Id$ 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

3 
Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, 
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

4 
TU Muenchen 
10052  5 
*) 
6 

7 
header {* Using extensible records in HOL  points and coloured points *} 

8 

16417  9 
theory Records imports Main begin 
10052  10 

11 
subsection {* Points *} 

12 

13 
record point = 

11939  14 
xpos :: nat 
15 
ypos :: nat 

10052  16 

17 
text {* 

11939  18 
Apart many other things, above record declaration produces the 
19 
following theorems: 

10052  20 
*} 
21 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

22 

10052  23 
thm "point.simps" 
24 
thm "point.iffs" 

12266  25 
thm "point.defs" 
10052  26 

27 
text {* 

11939  28 
The set of theorems @{thm [source] point.simps} is added 
29 
automatically to the standard simpset, @{thm [source] point.iffs} is 

30 
added to the Classical Reasoner and Simplifier context. 

10052  31 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

32 
\medskip Record declarations define new types and type abbreviations: 
10357  33 
@{text [display] 
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

34 
" point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type 
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

35 
'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr> = 'a point_ext_type"} 
10052  36 
*} 
37 

38 
consts foo1 :: point 

11939  39 
consts foo2 :: "( xpos :: nat, ypos :: nat )" 
40 
consts foo3 :: "'a => 'a point_scheme" 

41 
consts foo4 :: "'a => ( xpos :: nat, ypos :: nat, ... :: 'a )" 

10052  42 

43 

44 
subsubsection {* Introducing concrete records and record schemes *} 

45 

46 
defs 

11939  47 
foo1_def: "foo1 == ( xpos = 1, ypos = 0 )" 
48 
foo3_def: "foo3 ext == ( xpos = 1, ypos = 0, ... = ext )" 

10052  49 

50 

51 
subsubsection {* Record selection and record update *} 

52 

19736  53 
definition 
11939  54 
getX :: "'a point_scheme => nat" 
19736  55 
"getX r = xpos r" 
11939  56 
setX :: "'a point_scheme => nat => 'a point_scheme" 
19736  57 
"setX r n = r ( xpos := n )" 
10052  58 

59 

60 
subsubsection {* Some lemmas about records *} 

61 

10357  62 
text {* Basic simplifications. *} 
10052  63 

11939  64 
lemma "point.make n p = ( xpos = n, ypos = p )" 
65 
by (simp only: point.make_def) 

10052  66 

11939  67 
lemma "xpos ( xpos = m, ypos = n, ... = p ) = m" 
10052  68 
by simp 
69 

11939  70 
lemma "( xpos = m, ypos = n, ... = p ) ( xpos:= 0 ) = ( xpos = 0, ypos = n, ... = p )" 
10052  71 
by simp 
72 

73 

10357  74 
text {* \medskip Equality of records. *} 
10052  75 

11939  76 
lemma "n = n' ==> p = p' ==> ( xpos = n, ypos = p ) = ( xpos = n', ypos = p' )" 
10052  77 
 "introduction of concrete record equality" 
78 
by simp 

79 

11939  80 
lemma "( xpos = n, ypos = p ) = ( xpos = n', ypos = p' ) ==> n = n'" 
10052  81 
 "elimination of concrete record equality" 
82 
by simp 

83 

11939  84 
lemma "r ( xpos := n ) ( ypos := m ) = r ( ypos := m ) ( xpos := n )" 
10052  85 
 "introduction of abstract record equality" 
86 
by simp 

87 

11939  88 
lemma "r ( xpos := n ) = r ( xpos := n' ) ==> n = n'" 
10052  89 
 "elimination of abstract record equality (manual proof)" 
90 
proof  

11939  91 
assume "r ( xpos := n ) = r ( xpos := n' )" (is "?lhs = ?rhs") 
92 
hence "xpos ?lhs = xpos ?rhs" by simp 

10052  93 
thus ?thesis by simp 
94 
qed 

95 

96 

10357  97 
text {* \medskip Surjective pairing *} 
10052  98 

11939  99 
lemma "r = ( xpos = xpos r, ypos = ypos r )" 
10052  100 
by simp 
101 

12591  102 
lemma "r = ( xpos = xpos r, ypos = ypos r, ... = point.more r )" 
10052  103 
by simp 
104 

105 

10357  106 
text {* 
11939  107 
\medskip Representation of records by cases or (degenerate) 
108 
induction. 

10357  109 
*} 
10052  110 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

111 
lemma "r( xpos := n ) ( ypos := m ) = r ( ypos := m ) ( xpos := n )" 
11939  112 
proof (cases r) 
113 
fix xpos ypos more 

114 
assume "r = ( xpos = xpos, ypos = ypos, ... = more )" 

115 
thus ?thesis by simp 

116 
qed 

117 

118 
lemma "r ( xpos := n ) ( ypos := m ) = r ( ypos := m ) ( xpos := n )" 

119 
proof (induct r) 

120 
fix xpos ypos more 

121 
show "( xpos = xpos, ypos = ypos, ... = more ) ( xpos := n, ypos := m ) = 

122 
( xpos = xpos, ypos = ypos, ... = more ) ( ypos := m, xpos := n )" 

10052  123 
by simp 
124 
qed 

125 

11939  126 
lemma "r ( xpos := n ) ( xpos := m ) = r ( xpos := m )" 
127 
proof (cases r) 

128 
fix xpos ypos more 

129 
assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>" 

130 
thus ?thesis by simp 

10052  131 
qed 
132 

11939  133 
lemma "r ( xpos := n ) ( xpos := m ) = r ( xpos := m )" 
134 
proof (cases r) 

135 
case fields 

136 
thus ?thesis by simp 

137 
qed 

138 

139 
lemma "r ( xpos := n ) ( xpos := m ) = r ( xpos := m )" 

140 
by (cases r) simp 

141 

10052  142 

10357  143 
text {* 
144 
\medskip Concrete records are type instances of record schemes. 

145 
*} 

10052  146 

19736  147 
definition 
10052  148 
foo5 :: nat 
19736  149 
"foo5 = getX ( xpos = 1, ypos = 0 )" 
10052  150 

151 

11939  152 
text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *} 
10052  153 

19736  154 
definition 
11939  155 
incX :: "'a point_scheme => 'a point_scheme" 
19736  156 
"incX r = ( xpos = xpos r + 1, ypos = ypos r, ... = point.more r )" 
10052  157 

11939  158 
lemma "incX r = setX r (Suc (getX r))" 
159 
by (simp add: getX_def setX_def incX_def) 

160 

10052  161 

10357  162 
text {* An alternative definition. *} 
10052  163 

19736  164 
definition 
11939  165 
incX' :: "'a point_scheme => 'a point_scheme" 
19736  166 
"incX' r = r ( xpos := xpos r + 1 )" 
10052  167 

168 

169 
subsection {* Coloured points: record extension *} 

170 

171 
datatype colour = Red  Green  Blue 

172 

173 
record cpoint = point + 

174 
colour :: colour 

175 

176 

177 
text {* 

14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

178 
The record declaration defines a new type constructure and abbreviations: 
10357  179 
@{text [display] 
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

180 
" cpoint = ( xpos :: nat, ypos :: nat, colour :: colour ) = 
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

181 
() cpoint_ext_type point_ext_type 
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

182 
'a cpoint_scheme = ( xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a ) = 
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
12591
diff
changeset

183 
'a cpoint_ext_type point_ext_type"} 
10052  184 
*} 
185 

186 
consts foo6 :: cpoint 

11939  187 
consts foo7 :: "( xpos :: nat, ypos :: nat, colour :: colour )" 
188 
consts foo8 :: "'a cpoint_scheme" 

189 
consts foo9 :: "( xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a )" 

10052  190 

191 

10357  192 
text {* 
193 
Functions on @{text point} schemes work for @{text cpoints} as well. 

194 
*} 

10052  195 

19736  196 
definition 
10052  197 
foo10 :: nat 
19736  198 
"foo10 = getX ( xpos = 2, ypos = 0, colour = Blue )" 
10052  199 

200 

201 
subsubsection {* Noncoercive structural subtyping *} 

202 

10357  203 
text {* 
204 
Term @{term foo11} has type @{typ cpoint}, not type @{typ point}  

205 
Great! 

206 
*} 

10052  207 

19736  208 
definition 
10052  209 
foo11 :: cpoint 
19736  210 
"foo11 = setX ( xpos = 2, ypos = 0, colour = Blue ) 0" 
10052  211 

212 

213 
subsection {* Other features *} 

214 

10357  215 
text {* Field names contribute to record identity. *} 
10052  216 

217 
record point' = 

11939  218 
xpos' :: nat 
219 
ypos' :: nat 

10052  220 

10357  221 
text {* 
11939  222 
\noindent May not apply @{term getX} to @{term [source] "( xpos' = 
223 
2, ypos' = 0 )"}  type error. 

10357  224 
*} 
10052  225 

10357  226 
text {* \medskip Polymorphic records. *} 
10052  227 

228 
record 'a point'' = point + 

229 
content :: 'a 

230 

231 
types cpoint'' = "colour point''" 

232 

233 
end 