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 =


14 
x :: nat


15 
y :: nat


16 


17 
text {*


18 
Apart many other things, above record declaration produces the


19 
following theorems:


20 
*}


21 


22 
thm "point.simps"


23 
thm "point.iffs"


24 
thm "point.update_defs"


25 


26 
text {*

10357

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 
*}


31 


32 
text {*


33 
Record declarations define new type abbreviations:

10357

34 
@{text [display]


35 
" point = ( x :: nat, y :: nat )


36 
'a point_scheme = ( x :: nat, y :: nat, ... :: 'a )"}


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

10052

38 
*}


39 


40 
consts foo1 :: point


41 
consts foo2 :: "( x :: nat, y :: nat )"


42 
consts foo3 :: "'a => ('a::more) point_scheme"


43 
consts foo4 :: "'a => ( x :: nat, y :: nat, ... :: 'a )"


44 


45 


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


47 


48 
defs


49 
foo1_def: "foo1 == ( x = 1, y = 0 )"


50 
foo3_def: "foo3 ext == ( x = 1, y = 0, ... = ext )"


51 


52 


53 
subsubsection {* Record selection and record update *}


54 


55 
constdefs


56 
getX :: "('a::more) point_scheme => nat"


57 
"getX r == x r"


58 
setX :: "('a::more) point_scheme => nat => 'a point_scheme"


59 
"setX r n == r ( x := n )"


60 


61 


62 
subsubsection {* Some lemmas about records *}


63 

10357

64 
text {* Basic simplifications. *}

10052

65 


66 
lemma "point.make n p = ( x = n, y = p )"


67 
by simp


68 


69 
lemma "x ( x = m, y = n, ... = p ) = m"


70 
by simp


71 


72 
lemma "( x = m, y = n, ... = p ) ( x:= 0 ) = ( x = 0, y = n, ... = p )"


73 
by simp


74 


75 

10357

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

10052

77 


78 
lemma "n = n' ==> p = p' ==> ( x = n, y = p ) = ( x = n', y = p' )"


79 
 "introduction of concrete record equality"


80 
by simp


81 


82 
lemma "( x = n, y = p ) = ( x = n', y = p' ) ==> n = n'"


83 
 "elimination of concrete record equality"


84 
by simp


85 


86 
lemma "r ( x := n ) ( y := m ) = r ( y := m ) ( x := n )"


87 
 "introduction of abstract record equality"


88 
by simp


89 


90 
lemma "r ( x := n ) = r ( x := n' ) ==> n = n'"


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


92 
proof 


93 
assume "r ( x := n ) = r ( x := n' )" (is "?lhs = ?rhs")


94 
hence "x ?lhs = x ?rhs" by simp


95 
thus ?thesis by simp


96 
qed


97 


98 

10357

99 
text {* \medskip Surjective pairing *}

10052

100 


101 
lemma "r = ( x = x r, y = y r )"


102 
by simp


103 


104 
lemma "r = ( x = x r, y = y r, ... = more r )"


105 
by simp


106 


107 

10357

108 
text {*


109 
\medskip Splitting quantifiers: the @{text "!!r"} is \emph{necessary}


110 
here!


111 
*}

10052

112 


113 
lemma "!!r. r ( x := n ) ( y := m ) = r ( y := m ) ( x := n )"


114 
proof record_split


115 
fix x y more


116 
show "( x = x, y = y, ... = more )( x := n, y := m ) =


117 
( x = x, y = y, ... = more )( y := m, x := n )"


118 
by simp


119 
qed


120 


121 
lemma "!!r. r ( x := n ) ( x := m ) = r ( x := m )"


122 
proof record_split


123 
fix x y more


124 
show "( x = x, y = y, ... = more )( x := n, x := m ) =


125 
( x = x, y = y, ... = more )( x := m )"


126 
by simp


127 
qed


128 


129 

10357

130 
text {*


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


132 
*}

10052

133 


134 
constdefs


135 
foo5 :: nat


136 
"foo5 == getX ( x = 1, y = 0 )"


137 


138 

10357

139 
text {* \medskip Manipulating the `...' (more) part. *}

10052

140 


141 
constdefs


142 
incX :: "('a::more) point_scheme => 'a point_scheme"


143 
"incX r == ( x = Suc (x r), y = y r, ... = point.more r )"


144 


145 
lemma "!!r n. incX r = setX r (Suc (getX r))"


146 
proof (unfold getX_def setX_def incX_def)


147 
show "!!r n. ( x = Suc (x r), y = y r, ... = more r ) = r( x := Suc (x r) )"


148 
by record_split simp


149 
qed


150 

10357

151 
text {* An alternative definition. *}

10052

152 


153 
constdefs


154 
incX' :: "('a::more) point_scheme => 'a point_scheme"


155 
"incX' r == r ( x := Suc (x r) )"


156 


157 


158 
subsection {* Coloured points: record extension *}


159 


160 
datatype colour = Red  Green  Blue


161 


162 
record cpoint = point +


163 
colour :: colour


164 


165 


166 
text {*


167 
The record declaration defines new type constructors:

10357

168 
@{text [display]


169 
" cpoint = ( x :: nat, y :: nat, colour :: colour )


170 
'a cpoint_scheme = ( x :: nat, y :: nat, colour :: colour, ... :: 'a )"}

10052

171 
*}


172 


173 
consts foo6 :: cpoint


174 
consts foo7 :: "( x :: nat, y :: nat, colour :: colour )"


175 
consts foo8 :: "('a::more) cpoint_scheme"


176 
consts foo9 :: "( x :: nat, y :: nat, colour :: colour, ... :: 'a )"


177 


178 

10357

179 
text {*


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


181 
*}

10052

182 


183 
constdefs


184 
foo10 :: nat


185 
"foo10 == getX ( x = 2, y = 0, colour = Blue )"


186 


187 


188 
subsubsection {* Noncoercive structural subtyping *}


189 

10357

190 
text {*


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


192 
Great!


193 
*}

10052

194 


195 
constdefs


196 
foo11 :: cpoint


197 
"foo11 == setX ( x = 2, y = 0, colour = Blue ) 0"


198 


199 


200 
subsection {* Other features *}


201 

10357

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

10052

203 


204 
record point' =


205 
x' :: nat


206 
y' :: nat


207 

10357

208 
text {*


209 
\noindent May not apply @{term getX} to


210 
@{term [source] "( x' = 2, y' = 0 )"}.


211 
*}

10052

212 

10357

213 
text {* \medskip Polymorphic records. *}

10052

214 


215 
record 'a point'' = point +


216 
content :: 'a


217 


218 
types cpoint'' = "colour point''"


219 


220 
end
