(* Title: HOL/ex/Records.thy
ID: $Id$
Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Extensible Records *}
theory Records = Main:
subsection {* Points *}
record point =
Xcoord :: int
Ycoord :: int
text {*
Apart many other things, above record declaration produces the
following theorems:
*}
thm "point.simps"
text {*
Incomprehensible equations: the selectors Xcoord and Ycoord, also "more";
Updates, make, make_scheme and equality introduction (extensionality)
*}
thm "point.iffs"
text {*
@{thm[display] point.iffs}
%%\rulename{point.iffs}
Simplify equations involving Xcoord, Ycoord (and presumably also both Xcoord and Ycoord)
*}
thm "point.update_defs"
text {*
@{thm[display] point.update_defs}
%%\rulename{point.update_defs}
Definitions of updates to Xcoord and Ycoord, also "more"
*}
text {*
The set of theorems @{thm [source] point.simps} is added
automatically to the standard simpset, @{thm [source] point.iffs} is
added to the Classical Reasoner and Simplifier context.
*}
text {* Exchanging Xcoord and Ycoord yields a different type: we must
unfortunately write the fields in a canonical order.*}
constdefs
pt1 :: point
"pt1 == (| Xcoord = 999, Ycoord = 23 |)"
pt2 :: "(| Xcoord :: int, Ycoord :: int |)"
"pt2 == (| Xcoord = -45, Ycoord = 97 |)"
subsubsection {* Some lemmas about records *}
text {* Basic simplifications. *}
lemma "Xcoord (| Xcoord = a, Ycoord = b |) = a"
by simp -- "selection"
lemma "(| Xcoord = a, Ycoord = b |) (| Xcoord:= 0 |) = (| Xcoord = 0, Ycoord = b |)"
by simp -- "update"
subsection {* Coloured points: record extension *}
text {*
Records are extensible.
The name@{text "more"} is reserved, since it is used for extensibility.
*}
datatype colour = Red | Green | Blue
record cpoint = point +
col :: colour
constdefs
cpt1 :: cpoint
"cpt1 == (| Xcoord = 999, Ycoord = 23, col = Green |)"
subsection {* Generic operations *}
text {* Record selection and record update; these are generic! *}
lemma "Xcoord (| Xcoord = a, Ycoord = b, ... = p |) = a"
by simp -- "selection"
lemma "point.more cpt1 = \<lparr>col = Green\<rparr>"
by (simp add: cpt1_def) -- "tail of this record"
lemma "(| Xcoord = a, Ycoord = b, ... = p |) (| Xcoord:= 0 |) = (| Xcoord = 0, Ycoord = b, ... = p |)"
by simp -- "update"
text {*
Record declarations define new type abbreviations:
@{text [display]
" point = (| Xcoord :: int, Ycoord :: int |)
'a point_scheme = (| Xcoord :: int, Ycoord :: int, ... :: 'a |)"}
*}
constdefs
getX :: "'a point_scheme \<Rightarrow> int"
"getX r == Xcoord r"
setX :: "['a point_scheme, int] \<Rightarrow> 'a point_scheme"
"setX r a == r (| Xcoord := a |)"
text {*
\medskip Concrete records are type instances of record schemes.
*}
lemma "getX (| Xcoord = 64, Ycoord = 36 |) = 64"
by (simp add: getX_def)
text {* \medskip Manipulating the `...' (more) part. beware: EACH record
has its OWN more field, so a compound name is required! *}
constdefs
incX :: "'a point_scheme \<Rightarrow> 'a point_scheme"
"incX r == \<lparr>Xcoord = (Xcoord r) + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
constdefs
setGreen :: "[colour, 'a point_scheme] \<Rightarrow> cpoint"
"setGreen cl r == (| Xcoord = Xcoord r, Ycoord = Ycoord r, col = cl |)"
text {* works (I think) for ALL extensions of type point? *}
lemma "incX r = setX r ((getX r) + 1)"
by (simp add: getX_def setX_def incX_def)
text {* An equivalent definition. *}
lemma "incX r = r \<lparr>Xcoord := (Xcoord r) + 1\<rparr>"
by (simp add: incX_def)
text {*
Functions on @{text point} schemes work for type @{text cpoint} as
well. *}
lemma "getX \<lparr>Xcoord = 23, Ycoord = 10, col = Blue\<rparr> = 23"
by (simp add: getX_def)
subsubsection {* Non-coercive structural subtyping *}
text {*
Function @{term setX} can be applied to type @{typ cpoint}, not just type
@{typ point}, and returns a result of the same type! *}
lemma "setX \<lparr>Xcoord = 12, Ycoord = 0, col = Blue\<rparr> 23 =
\<lparr>Xcoord = 23, Ycoord = 0, col = Blue\<rparr>"
by (simp add: setX_def)
subsection {* Other features *}
text {* Field names (and order) contribute to record identity. *}
text {* \medskip Polymorphic records. *}
record 'a polypoint = point +
content :: 'a
types cpolypoint = "colour polypoint"
subsection {* Equality of records. *}
lemma "(\<lparr>Xcoord = a, Ycoord = b\<rparr> = \<lparr>Xcoord = a', Ycoord = b'\<rparr>) = (a = a' & b = b')"
-- "simplification of concrete record equality"
by simp
text {* \medskip Surjective pairing *}
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r\<rparr>"
by simp
lemma "\<lparr>Xcoord = a, Ycoord = b, \<dots> = p\<rparr> = \<lparr>Xcoord = a, Ycoord = b\<rparr>"
by auto
text {*
A rigid record has ()::unit in its name@{text "more"} part
*}
text {* a polymorphic record equality (covers all possible extensions) *}
lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Ycoord := b\<rparr> = r \<lparr>Ycoord := b\<rparr> \<lparr>Xcoord := a\<rparr>"
-- "introduction of abstract record equality
(order of updates doesn't affect the value)"
by simp
lemma "r \<lparr>Xcoord := a, Ycoord := b\<rparr> = r \<lparr>Ycoord := b, Xcoord := a\<rparr>"
-- "abstract record equality (the same with iterated updates)"
by simp
text {* Showing that repeated updates don't matter *}
lemma "r \<lparr>Xcoord := a\<rparr> \<lparr>Xcoord := a'\<rparr> = r \<lparr>Xcoord := a'\<rparr>"
by simp
text {* surjective *}
lemma "r = \<lparr>Xcoord = Xcoord r, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
by simp
text {*
\medskip Splitting abstract record variables.
*}
lemma "r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
-- "elimination of abstract record equality (manual proof, by selector)"
apply (drule_tac f=Xcoord in arg_cong)
--{* @{subgoals[display,indent=0,margin=65]} *}
by simp
text {*So we replace the ugly manual proof by the "cases" method.*}
lemma "r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
apply (cases r)
--{* @{subgoals[display,indent=0,margin=65]} *}
by simp
constdefs
cpt2 :: cpoint
"cpt2 \<equiv> point.extend pt1 (cpoint.fields Green)"
text {*
@{thm[display] point.defs}
*};
text {*
@{thm[display] cpoint.defs}
*};
text{*cpt2 is the same as cpt1, but defined by extending point pt1*}
lemma "cpt1 = cpt2"
apply (simp add: cpt1_def cpt2_def point.defs cpoint.defs)
--{* @{subgoals[display,indent=0,margin=65]} *}
by (simp add: pt1_def)
lemma "point.truncate cpt2 = pt1"
by (simp add: pt1_def cpt2_def point.defs)
end