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


27 
The set of theorems "point.simps" is added automatically to the


28 
standard simpset, "point.iffs" is added to the claset and simpset.


29 
*}


30 


31 
text {*


32 
Record declarations define new type abbreviations:


33 


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


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


36 


37 
Extensions `...' must be in type class `more'!


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 


64 
text {* Basic simplifications *}


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 


76 
text {* Equality of records *}


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 


99 
text {* Surjective pairing *}


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 


108 
text {* Splitting quantifiers: the !!r is NECESSARY here *}


109 


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


111 
proof record_split


112 
fix x y more


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


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


115 
by simp


116 
qed


117 


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


119 
proof record_split


120 
fix x y more


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


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


123 
by simp


124 
qed


125 


126 


127 


128 
text {* Concrete records are type instances of record schemes *}


129 


130 
constdefs


131 
foo5 :: nat


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


133 


134 


135 
text {* Manipulating the `...' (more) part *}


136 


137 
constdefs


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


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


140 


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


142 
proof (unfold getX_def setX_def incX_def)


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


144 
by record_split simp


145 
qed


146 


147 


148 
text {* alternative definition *}


149 


150 
constdefs


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


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


153 


154 


155 
subsection {* Coloured points: record extension *}


156 


157 
datatype colour = Red  Green  Blue


158 


159 
record cpoint = point +


160 
colour :: colour


161 


162 


163 
text {*


164 
The record declaration defines new type constructors:


165 


166 
cpoint = ( x :: nat, y :: nat, colour :: colour )


167 
'a cpoint_scheme = ( x :: nat, y :: nat, colour :: colour, ... :: 'a )


168 
*}


169 


170 
consts foo6 :: cpoint


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


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


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


174 


175 


176 
text {* Functions on point schemes work for cpoints as well *}


177 


178 
constdefs


179 
foo10 :: nat


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


181 


182 


183 
subsubsection {* Noncoercive structural subtyping *}


184 


185 
text {* foo11 has type cpoint, not type point  Great! *}


186 


187 
constdefs


188 
foo11 :: cpoint


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


190 


191 


192 
subsection {* Other features *}


193 


194 
text {* field names contribute to record identity *}


195 


196 
record point' =


197 
x' :: nat


198 
y' :: nat


199 


200 
text {* May not apply @{term getX} to @{term "( x' = 2, y' = 0 )"} *}


201 


202 


203 
text {* Polymorphic records *}


204 


205 
record 'a point'' = point +


206 
content :: 'a


207 


208 
types cpoint'' = "colour point''"


209 


210 
end
