# HG changeset patch
# User paulson
# Date 993826750 -7200
# Node ID 8db249f786eecc3c7b5dcf7b01f7a8a430b8fdff
# Parent  cf8d81cf80341d1c915d7541b8ecf808517caf07
for the records section

diff -r cf8d81cf8034 -r 8db249f786ee doc-src/TutorialI/Types/Records.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Types/Records.thy	Fri Jun 29 16:59:10 2001 +0200
@@ -0,0 +1,252 @@
+(*  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 "point.make a b = (| Xcoord = a, Ycoord = b |)"
+by simp -- "needed?? forget it"
+
+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 |)"}
+  Extensions `...' must be in type class @{text more}.
+*}
+
+constdefs
+  getX :: "('a::more) point_scheme \<Rightarrow> int"
+   "getX r == Xcoord r"
+  setX :: "[('a::more) point_scheme, int] \<Rightarrow> 'a point_scheme"
+   "setX r a == r (| Xcoord := a |)"
+  extendpt :: "'a \<Rightarrow> ('a::more) point_scheme"
+   "extendpt ext == (| Xcoord = #15, Ycoord = 0, ... = ext |)"
+     text{*not sure what this is for!*}
+
+
+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::more) 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::more) 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, 
+          though order of fields does the type)"
+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>"
+apply 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 splitting.  These must be quantified: 
+  the @{text "!!r"} is \emph{necessary}!  Note the occurrence of more, since
+  r is polymorphic.
+*}
+lemma "!!r. r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
+apply record_split --{* @{subgoals[display,indent=0,margin=65]} *}
+by simp 
+
+
+end