--- a/src/HOL/ex/Points.ML Fri Oct 23 19:40:00 1998 +0200
+++ b/src/HOL/ex/Points.ML Fri Oct 23 20:28:33 1998 +0200
@@ -1,32 +1,40 @@
-(** some basic simplifiactions **)
+(*Note: any of these goals may be solved by a single stroke of
+ auto(); or force 1;*)
+
+
+(* some basic simplifications *)
Goal "!!m n p. x (| x = m, y = n, ... = p |) = m";
by (Simp_tac 1);
+result();
Goal "!!m n p. (| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)";
by (Simp_tac 1);
+result();
-
-(** splitting **)
+(* splitting quantifiers *)
Goal "!!r m n. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)";
by (record_split_tac 1);
by (Simp_tac 1);
+result();
Goal "!!r m n. r (| x := n |) (| x := m |) = r (| x := m |)";
by (record_split_tac 1);
by (Simp_tac 1);
+result();
-
-(** Equality **)
+(* record equality *)
Goal "!!r. (| x = n, y = p |) = (| x = n', y = p' |) & n = 0 ==> n' = 0";
by (Asm_full_simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
+result();
Goalw [getX_def, setX_def, incX_def] "!!r n. incX r = setX r (Suc (getX r))";
by (record_split_tac 1);
-by (Simp_tac 1);
\ No newline at end of file
+by (Simp_tac 1);
+result();
--- 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
-
-
-
-
-
--- a/src/HOL/ex/ROOT.ML Fri Oct 23 19:40:00 1998 +0200
+++ b/src/HOL/ex/ROOT.ML Fri Oct 23 20:28:33 1998 +0200
@@ -11,7 +11,7 @@
writeln "Root file for HOL examples";
set proof_timing;
-(**Some examples of recursive function definitions: the TFL package**)
+(*some examples of recursive function definitions: the TFL package*)
time_use_thy "Recdefs";
time_use_thy "Primes";
time_use_thy "Fib";
@@ -35,14 +35,15 @@
time_use_thy "StringEx";
time_use_thy "BinEx";
-(*Monoids and Groups as predicates over record schemes*)
+(*basic use of extensible records*)
time_use_thy "MonoidGroup";
+time_use_thy "Points";
-(*Groups via locales*)
+(*groups via locales*)
time_use_thy "PiSets";
time_use_thy "LocaleGroup";
-(*Expressions with quote / antiquote*)
+(*expressions with quote / antiquote syntax*)
time_use_thy "Antiquote";