10052

1 
(* Title: HOL/ex/Records.thy


2 
ID: $Id$


3 
Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen


4 
License: GPL (GNU GENERAL PUBLIC LICENSE)


5 
*)


6 


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


8 


9 
theory Records = Main:


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 


22 
thm "point.simps"


23 
thm "point.iffs"

12266

24 
thm "point.defs"

10052

25 


26 
text {*

11939

27 
The set of theorems @{thm [source] point.simps} is added


28 
automatically to the standard simpset, @{thm [source] point.iffs} is


29 
added to the Classical Reasoner and Simplifier context.

10052

30 

11939

31 
\medskip Record declarations define new type abbreviations:

10357

32 
@{text [display]

11939

33 
" point = ( xpos :: nat, ypos :: nat )


34 
'a point_scheme = ( xpos :: nat, ypos :: nat, ... :: 'a )"}

10052

35 
*}


36 


37 
consts foo1 :: point

11939

38 
consts foo2 :: "( xpos :: nat, ypos :: nat )"


39 
consts foo3 :: "'a => 'a point_scheme"


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

10052

41 


42 


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


44 


45 
defs

11939

46 
foo1_def: "foo1 == ( xpos = 1, ypos = 0 )"


47 
foo3_def: "foo3 ext == ( xpos = 1, ypos = 0, ... = ext )"

10052

48 


49 


50 
subsubsection {* Record selection and record update *}


51 


52 
constdefs

11939

53 
getX :: "'a point_scheme => nat"


54 
"getX r == xpos r"


55 
setX :: "'a point_scheme => nat => 'a point_scheme"


56 
"setX r n == r ( xpos := n )"

10052

57 


58 


59 
subsubsection {* Some lemmas about records *}


60 

10357

61 
text {* Basic simplifications. *}

10052

62 

11939

63 
lemma "point.make n p = ( xpos = n, ypos = p )"


64 
by (simp only: point.make_def)

10052

65 

11939

66 
lemma "xpos ( xpos = m, ypos = n, ... = p ) = m"

10052

67 
by simp


68 

11939

69 
lemma "( xpos = m, ypos = n, ... = p ) ( xpos:= 0 ) = ( xpos = 0, ypos = n, ... = p )"

10052

70 
by simp


71 


72 

10357

73 
text {* \medskip Equality of records. *}

10052

74 

11939

75 
lemma "n = n' ==> p = p' ==> ( xpos = n, ypos = p ) = ( xpos = n', ypos = p' )"

10052

76 
 "introduction of concrete record equality"


77 
by simp


78 

11939

79 
lemma "( xpos = n, ypos = p ) = ( xpos = n', ypos = p' ) ==> n = n'"

10052

80 
 "elimination of concrete record equality"


81 
by simp


82 

11939

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

10052

84 
 "introduction of abstract record equality"


85 
by simp


86 

11939

87 
lemma "r ( xpos := n ) = r ( xpos := n' ) ==> n = n'"

10052

88 
 "elimination of abstract record equality (manual proof)"


89 
proof 

11939

90 
assume "r ( xpos := n ) = r ( xpos := n' )" (is "?lhs = ?rhs")


91 
hence "xpos ?lhs = xpos ?rhs" by simp

10052

92 
thus ?thesis by simp


93 
qed


94 


95 

10357

96 
text {* \medskip Surjective pairing *}

10052

97 

11939

98 
lemma "r = ( xpos = xpos r, ypos = ypos r )"

10052

99 
by simp


100 

12591

101 
lemma "r = ( xpos = xpos r, ypos = ypos r, ... = point.more r )"

10052

102 
by simp


103 


104 

10357

105 
text {*

11939

106 
\medskip Representation of records by cases or (degenerate)


107 
induction.

10357

108 
*}

10052

109 

11939

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


111 
proof (cases r)


112 
fix xpos ypos more


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


114 
thus ?thesis by simp


115 
qed


116 


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


118 
proof (induct r)


119 
fix xpos ypos more


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


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

10052

122 
by simp


123 
qed


124 

11939

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


126 
proof (cases r)


127 
fix xpos ypos more


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


129 
thus ?thesis by simp

10052

130 
qed


131 

11939

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


133 
proof (cases r)


134 
case fields


135 
thus ?thesis by simp


136 
qed


137 


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


139 
by (cases r) simp


140 

10052

141 

10357

142 
text {*


143 
\medskip Concrete records are type instances of record schemes.


144 
*}

10052

145 


146 
constdefs


147 
foo5 :: nat

11939

148 
"foo5 == getX ( xpos = 1, ypos = 0 )"

10052

149 


150 

11939

151 
text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *}

10052

152 


153 
constdefs

11939

154 
incX :: "'a point_scheme => 'a point_scheme"


155 
"incX r == ( xpos = xpos r + 1, ypos = ypos r, ... = point.more r )"

10052

156 

11939

157 
lemma "incX r = setX r (Suc (getX r))"


158 
by (simp add: getX_def setX_def incX_def)


159 

10052

160 

10357

161 
text {* An alternative definition. *}

10052

162 


163 
constdefs

11939

164 
incX' :: "'a point_scheme => 'a point_scheme"


165 
"incX' r == r ( xpos := xpos r + 1 )"

10052

166 


167 


168 
subsection {* Coloured points: record extension *}


169 


170 
datatype colour = Red  Green  Blue


171 


172 
record cpoint = point +


173 
colour :: colour


174 


175 


176 
text {*


177 
The record declaration defines new type constructors:

10357

178 
@{text [display]

11939

179 
" cpoint = ( xpos :: nat, ypos :: nat, colour :: colour )


180 
'a cpoint_scheme = ( xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a )"}

10052

181 
*}


182 


183 
consts foo6 :: cpoint

11939

184 
consts foo7 :: "( xpos :: nat, ypos :: nat, colour :: colour )"


185 
consts foo8 :: "'a cpoint_scheme"


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

10052

187 


188 

10357

189 
text {*


190 
Functions on @{text point} schemes work for @{text cpoints} as well.


191 
*}

10052

192 


193 
constdefs


194 
foo10 :: nat

11939

195 
"foo10 == getX ( xpos = 2, ypos = 0, colour = Blue )"

10052

196 


197 


198 
subsubsection {* Noncoercive structural subtyping *}


199 

10357

200 
text {*


201 
Term @{term foo11} has type @{typ cpoint}, not type @{typ point} 


202 
Great!


203 
*}

10052

204 


205 
constdefs


206 
foo11 :: cpoint

11939

207 
"foo11 == setX ( xpos = 2, ypos = 0, colour = Blue ) 0"

10052

208 


209 


210 
subsection {* Other features *}


211 

10357

212 
text {* Field names contribute to record identity. *}

10052

213 


214 
record point' =

11939

215 
xpos' :: nat


216 
ypos' :: nat

10052

217 

10357

218 
text {*

11939

219 
\noindent May not apply @{term getX} to @{term [source] "( xpos' =


220 
2, ypos' = 0 )"}  type error.

10357

221 
*}

10052

222 

10357

223 
text {* \medskip Polymorphic records. *}

10052

224 


225 
record 'a point'' = point +


226 
content :: 'a


227 


228 
types cpoint'' = "colour point''"


229 


230 
end
