--- a/src/HOL/ex/Points.thy Fri Oct 23 19:40:00 1998 +0200
+++ b/src/HOL/ex/Points.thy Fri Oct 23 20:28:33 1998 +0200
@@ -1,28 +1,41 @@
+(* Title: HOL/ex/Points.thy
+ ID: $Id$
+ Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
-Points = Main +
+Basic use of extensible records in HOL, including the famous points
+and coloured points.
+*)
+
+Points = Main +
-(** To find out, which theorems are produced by the record delaration, **)
-(** type the following commands in Isabelle **)
-(** - thms "point.simps"; **)
-(** - thms "point.iffs"; **)
-(** - thms "point.update_defs"; **)
-(** **)
-(** The set of theorems "point.simps" is added automatically **)
-(** to the standard simpset **)
-
+(** points **)
record point =
x :: nat
y :: nat
+(*
+ To find out, which theorems are produced by the record declaration,
+ type the following commands:
+
+ thms "point.simps";
+ thms "point.iffs";
+ thms "point.update_defs";
+
+ The set of theorems "point.simps" is added automatically to the
+ standard simpset, "point.iffs" is added to the claset and simpset.
+*)
-(** Record declarations define new type constructors: **)
-(** point = (| x :: nat, y :: nat |) **)
-(** 'a point_scheme = (| x :: nat, y :: nat, ... :: 'a |) **)
-(** **)
-(** Extensions must be in type class 'more'!!! **)
+(*
+ Record declarations define new type abbreviations:
+
+ point = (| x :: nat, y :: nat |)
+ 'a point_scheme = (| x :: nat, y :: nat, ... :: 'a |)
+
+ Extensions `...' must be in type class `more'!
+*)
consts foo1 :: point
consts foo2 :: "(| x :: nat, y :: nat |)"
@@ -30,48 +43,43 @@
consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)"
+(* Introducing concrete records and record schemes *)
-(** Introducing concrete records and record schemes **)
-
-defs
+defs
foo1_def "foo1 == (| x = 1, y = 0 |)"
foo3_def "foo3 ext == (| x = 1, y = 0, ... = ext |)"
+(* Record selection and record update *)
-(** Record selection and record update **)
-
-constdefs
+constdefs
getX :: ('a::more) point_scheme => nat
"getX r == x r"
setX :: ('a::more) point_scheme => nat => 'a point_scheme
"setX r n == r (| x := n |)"
-
-(** Concrete records are type instances of record schemes **)
+(* concrete records are type instances of record schemes *)
constdefs
foo5 :: nat
- "foo5 == getX (| x = 1, y = 0 |)"
+ "foo5 == getX (| x = 1, y = 0 |)"
-
-(** Binding the "..." (more-part) **)
+(* manipulating the `...' (more-part) *)
constdefs
incX :: ('a::more) point_scheme => 'a point_scheme
- "incX r == (| x = Suc (x r), y = (y r), ... = (point.more r) |)"
+ "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)"
-(* Alternative *)
-
+(*alternative definition*)
constdefs
incX' :: ('a::more) point_scheme => 'a point_scheme
"incX' r == r (| x := Suc (x r) |)"
-(** Record extension **)
+(** coloured points: record extension **)
datatype colour = Red | Green | Blue
@@ -79,10 +87,12 @@
colour :: colour
+(*
+ The record declaration defines new type constructors:
-(** The record declaration defines new type constructors: **)
-(** cpoint = (| x :: nat, y :: nat, colour :: colour |) **)
-(** 'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |) **)
+ cpoint = (| x :: nat, y :: nat, colour :: colour |)
+ 'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |)
+*)
consts foo6 :: cpoint
consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)"
@@ -90,25 +100,25 @@
consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"
+(* functions on point schemes work for cpoints as well *)
-(** Functions on point schemes work for cpoints as well **)
-
-constdefs
+constdefs
foo10 :: nat
"foo10 == getX (| x = 2, y = 0, colour = Blue |)"
-
-(** Subtyping is _not_ destructive !! **)
-(** foo11 hast type cpoint, not type point **)
+(* non-coercive structural subtyping *)
-constdefs
+(*foo11 has type cpoint, not type point*) (*Great!*)
+constdefs
foo11 :: cpoint
- "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
+ "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
-(** Field names contribute to identity **)
+(** other features **)
+
+(* field names contribute to record identity *)
record point' =
x' :: nat
@@ -116,29 +126,18 @@
consts
foo12 :: nat
-(* invalid *)
-(* "foo12 == getX (| x' = 2, y' = 0 |)" *)
+(*"foo12 == getX (| x' = 2, y' = 0 |)"*) (*invalid*)
-
-(** Polymorphic records **)
+(* polymorphic records *)
record 'a point'' = point +
content :: 'a
-
-
-(** Instantiating type variables **)
-
types cpoint'' = colour point''
-(** Have a lot of fun !!! **)
+(*Have a lot of fun!*)
end
-
-
-
-
-