11387

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 {* Extensible Records *}


8 


9 
theory Records = Main:


10 


11 
subsection {* Points *}


12 


13 
record point =


14 
Xcoord :: int


15 
Ycoord :: int


16 


17 
text {*


18 
Apart many other things, above record declaration produces the


19 
following theorems:


20 
*}


21 


22 
thm "point.simps"


23 
text {*


24 
Incomprehensible equations: the selectors Xcoord and Ycoord, also "more";


25 
Updates, make, make_scheme and equality introduction (extensionality)


26 
*}


27 


28 
thm "point.iffs"


29 
text {*


30 
@{thm[display] point.iffs}


31 
%%\rulename{point.iffs}


32 
Simplify equations involving Xcoord, Ycoord (and presumably also both Xcoord and Ycoord)


33 
*}


34 


35 
thm "point.update_defs"


36 
text {*


37 
@{thm[display] point.update_defs}


38 
%%\rulename{point.update_defs}


39 
Definitions of updates to Xcoord and Ycoord, also "more"


40 
*}


41 


42 
text {*


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


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


45 
added to the Classical Reasoner and Simplifier context.


46 
*}


47 


48 
text {* Exchanging Xcoord and Ycoord yields a different type: we must


49 
unfortunately write the fields in a canonical order.*}


50 


51 


52 
constdefs


53 
pt1 :: point


54 
"pt1 == ( Xcoord = #999, Ycoord = #23 )"


55 


56 
pt2 :: "( Xcoord :: int, Ycoord :: int )"


57 
"pt2 == ( Xcoord = #45, Ycoord = #97 )"


58 


59 


60 
subsubsection {* Some lemmas about records *}


61 


62 
text {* Basic simplifications. *}


63 


64 
lemma "point.make a b = ( Xcoord = a, Ycoord = b )"


65 
by simp  "needed?? forget it"


66 


67 
lemma "Xcoord ( Xcoord = a, Ycoord = b ) = a"


68 
by simp  "selection"


69 


70 
lemma "( Xcoord = a, Ycoord = b ) ( Xcoord:= 0 ) = ( Xcoord = 0, Ycoord = b )"


71 
by simp  "update"


72 


73 
subsection {* Coloured points: record extension *}


74 


75 


76 
text {*


77 
Records are extensible.


78 


79 
The name@{text "more"} is reserved, since it is used for extensibility.


80 
*}


81 


82 


83 
datatype colour = Red  Green  Blue


84 


85 
record cpoint = point +


86 
col :: colour


87 


88 


89 
constdefs


90 
cpt1 :: cpoint


91 
"cpt1 == ( Xcoord = #999, Ycoord = #23, col = Green )"


92 


93 


94 
subsection {* Generic operations *}


95 


96 


97 
text {* Record selection and record update; these are generic! *}


98 


99 
lemma "Xcoord ( Xcoord = a, Ycoord = b, ... = p ) = a"


100 
by simp  "selection"


101 


102 
lemma "point.more cpt1 = \<lparr>col = Green\<rparr>"


103 
by (simp add: cpt1_def)  "tail of this record"


104 


105 


106 
lemma "( Xcoord = a, Ycoord = b, ... = p ) ( Xcoord:= 0 ) = ( Xcoord = 0, Ycoord = b, ... = p )"


107 
by simp  "update"


108 


109 
text {*


110 
Record declarations define new type abbreviations:


111 
@{text [display]


112 
" point = ( Xcoord :: int, Ycoord :: int )


113 
'a point_scheme = ( Xcoord :: int, Ycoord :: int, ... :: 'a )"}


114 
Extensions `...' must be in type class @{text more}.


115 
*}


116 


117 
constdefs


118 
getX :: "('a::more) point_scheme \<Rightarrow> int"


119 
"getX r == Xcoord r"


120 
setX :: "[('a::more) point_scheme, int] \<Rightarrow> 'a point_scheme"


121 
"setX r a == r ( Xcoord := a )"


122 
extendpt :: "'a \<Rightarrow> ('a::more) point_scheme"


123 
"extendpt ext == ( Xcoord = #15, Ycoord = 0, ... = ext )"


124 
text{*not sure what this is for!*}


125 


126 


127 
text {*


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


129 
*}


130 


131 
lemma "getX ( Xcoord = #64, Ycoord = #36 ) = #64"


132 
by (simp add: getX_def)


133 


134 


135 
text {* \medskip Manipulating the `...' (more) part. beware: EACH record


136 
has its OWN more field, so a compound name is required! *}


137 


138 
constdefs


139 
incX :: "('a::more) point_scheme \<Rightarrow> 'a point_scheme"


140 
"incX r == \<lparr>Xcoord = (Xcoord r) + #1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"


141 


142 
constdefs


143 
setGreen :: "[colour, ('a::more) point_scheme] \<Rightarrow> cpoint"


144 
"setGreen cl r == ( Xcoord = Xcoord r, Ycoord = Ycoord r, col = cl )"


145 


146 


147 
text {* works (I think) for ALL extensions of type point? *}


148 


149 
lemma "incX r = setX r ((getX r) + #1)"


150 
by (simp add: getX_def setX_def incX_def)


151 


152 
text {* An equivalent definition. *}


153 
lemma "incX r = r \<lparr>Xcoord := (Xcoord r) + #1\<rparr>"


154 
by (simp add: incX_def)


155 


156 


157 


158 
text {*


159 
Functions on @{text point} schemes work for type @{text cpoint} as


160 
well. *}


161 


162 
lemma "getX \<lparr>Xcoord = #23, Ycoord = #10, col = Blue\<rparr> = #23"


163 
by (simp add: getX_def)


164 


165 


166 
subsubsection {* Noncoercive structural subtyping *}


167 


168 
text {*


169 
Function @{term setX} can be applied to type @{typ cpoint}, not just type


170 
@{typ point}, and returns a result of the same type! *}


171 


172 
lemma "setX \<lparr>Xcoord = #12, Ycoord = 0, col = Blue\<rparr> #23 =


173 
\<lparr>Xcoord = #23, Ycoord = 0, col = Blue\<rparr>"


174 
by (simp add: setX_def)


175 


176 


177 
subsection {* Other features *}


178 


179 
text {* Field names (and order) contribute to record identity. *}


180 


181 


182 
text {* \medskip Polymorphic records. *}


183 


184 
record 'a polypoint = point +


185 
content :: 'a


186 


187 
types cpolypoint = "colour polypoint"


188 


189 


190 
subsection {* Equality of records. *}


191 


192 
lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) = (a = a' & b = b')"


193 
 "simplification of concrete record equality"


194 
by simp


195 


196 
text {* \medskip Surjective pairing *}


197 


198 
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r\<rparr>"


199 
by simp


200 


201 


202 


203 
lemma "\<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = \<lparr>Xcoord = a, Ycoord = b\<rparr>"


204 
by auto


205 


206 
text {*


207 
A rigid record has ()::unit in its name@{text "more"} part


208 
*}


209 


210 
text {* a polymorphic record equality (covers all possible extensions) *}


211 
lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Ycoord := b\<rparr> = r \<lparr>Ycoord := b\<rparr> \<lparr>Xcoord := a\<rparr>"


212 
 "introduction of abstract record equality


213 
(order of updates doesn't affect the value,


214 
though order of fields does the type)"


215 
by simp


216 


217 
lemma "r \<lparr>Xcoord := a, Ycoord := b\<rparr> = r \<lparr>Ycoord := b, Xcoord := a\<rparr>"


218 
 "abstract record equality (the same with iterated updates)"


219 
by simp


220 


221 
text {* Showing that repeated updates don't matter *}


222 
lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Xcoord := a'\<rparr> = r \<lparr>Xcoord := a'\<rparr>"


223 
apply simp


224 


225 


226 
text {* surjective *}


227 


228 
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"


229 
by simp


230 


231 


232 
text {*


233 
\medskip Splitting abstract record variables.


234 
*}


235 


236 
lemma "r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"


237 
 "elimination of abstract record equality (manual proof, by selector)"


238 
apply (drule_tac f=Xcoord in arg_cong)


239 
{* @{subgoals[display,indent=0,margin=65]} *}


240 
by simp


241 


242 
text {*


243 
So we replace the ugly manual proof by splitting. These must be quantified:


244 
the @{text "!!r"} is \emph{necessary}! Note the occurrence of more, since


245 
r is polymorphic.


246 
*}


247 
lemma "!!r. r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"


248 
apply record_split {* @{subgoals[display,indent=0,margin=65]} *}


249 
by simp


250 


251 


252 
end
