--- a/src/HOL/ex/Points.ML Wed May 26 22:45:08 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* Title: HOL/ex/Points.thy
- ID: $Id$
- Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
-
-Basic use of extensible records in HOL, including the famous points
-and coloured points.
-
-Note: any of these goals may be solved at a stroke by Auto_tac or Force_tac
-*)
-
-
-(* some basic simplifications *)
-
-Goal "x (| x = m, y = n, ... = p |) = m";
-by (Simp_tac 1);
-result();
-
-Goal "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)";
-by (Simp_tac 1);
-result();
-
-
-(* splitting quantifiers: the !!r is NECESSARY *)
-
-Goal "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)";
-by (record_split_tac 1);
-by (Simp_tac 1);
-result();
-
-Goal "!!r. r (| x := n |) (| x := m |) = r (| x := m |)";
-by (record_split_tac 1);
-by (Simp_tac 1);
-result();
-
-
-(* record equality *)
-
-Goal "(| x = n, y = p |) = (| x = n', y = p' |) & n = 0 ==> n' = 0";
-by (Asm_full_simp_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);
-result();
--- a/src/HOL/ex/Points.thy Wed May 26 22:45:08 1999 +0200
+++ b/src/HOL/ex/Points.thy Wed May 26 22:45:59 1999 +0200
@@ -1,143 +1,194 @@
(* Title: HOL/ex/Points.thy
ID: $Id$
Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
-
-Basic use of extensible records in HOL, including the famous points
-and coloured points.
*)
-Points = Main +
+theory Points = Main:;
+
+title "Basic use of extensible records in HOL, including the famous points
+ and coloured points.";
-(** points **)
+section "Points";
record point =
x :: nat
- y :: nat
+ y :: nat;
-(*
- To find out, which theorems are produced by the record declaration,
- type the following commands:
+text {|
+ Apart many other things, above record declaration produces the
+ following theorems:
- thms "point.simps";
- thms "point.iffs";
- thms "point.update_defs";
+ 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.
-*)
+|};
-
-(*
+text {|
Record declarations define new type abbreviations:
- point = (| x :: nat, y :: nat |)
- 'a point_scheme = (| x :: nat, y :: nat, ... :: 'a |)
+ 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 |)";
+consts foo3 :: "'a => ('a::more) point_scheme";
+consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)";
+
+
+subsection "Introducing concrete records and record schemes";
+
+defs
+ foo1_def: "foo1 == (| x = 1, y = 0 |)"
+ foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)";
-consts foo1 :: point
-consts foo2 :: "(| x :: nat, y :: nat |)"
-consts foo3 :: 'a => ('a::more) point_scheme
-consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)"
+
+subsection "Record selection and record update";
+
+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 |)";
+
+
+subsection "Some lemmas about records";
+
+text "Note: any of these goals may be solved with a single
+ stroke of auto or force.";
-(* Introducing concrete records and record schemes *)
+text "basic simplifications";
-defs
- foo1_def "foo1 == (| x = 1, y = 0 |)"
- foo3_def "foo3 ext == (| x = 1, y = 0, ... = ext |)"
+lemma "x (| x = m, y = n, ... = p |) = m";
+ by simp;
+
+lemma "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)";
+ by simp;
-(* Record selection and record update *)
+text "splitting quantifiers: the !!r is NECESSARY";
-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 |)"
+lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)";
+proof record_split;
+ fix a b rest;
+ show "(| x = a, y = b, ... = rest |)(| x := n, y := m |) =
+ (| x = a, y = b, ... = rest |)(| y := m, x := n |)";
+ by simp;
+qed;
+
+lemma "!!r. r (| x := n |) (| x := m |) = r (| x := m |)";
+proof record_split;
+ fix a b rest;
+ show "(| x = a, y = b, ... = rest |)(| x := n, x := m |) =
+ (| x = a, y = b, ... = rest |)(| x := m |)";
+ by simp;
+qed;
-(* concrete records are type instances of record schemes *)
+text "equality of records";
+
+lemma "(| x = n, y = p |) = (| x = n', y = p' |) --> n = n'" (is "??EQ --> _");
+proof;
+ assume ??EQ;
+ thus "n = n'"; by simp;
+qed;
+
+
+text "concrete records are type instances of record schemes";
constdefs
foo5 :: nat
- "foo5 == getX (| x = 1, y = 0 |)"
+ "foo5 == getX (| x = 1, y = 0 |)";
-(* manipulating the `...' (more-part) *)
+text "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 :: "('a::more) point_scheme => 'a point_scheme"
+ "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)";
-(*alternative definition*)
+lemma "!!r n. incX r = setX r (Suc (getX r))";
+proof (unfold getX_def setX_def incX_def);
+ show "!! r n. (| x = Suc (x r), y = y r, ... = more r |) = r(| x := Suc (x r) |)";
+ by (record_split, simp);
+qed;
+
+
+text "alternative definition";
+
constdefs
- incX' :: ('a::more) point_scheme => 'a point_scheme
- "incX' r == r (| x := Suc (x r) |)"
+ incX' :: "('a::more) point_scheme => 'a point_scheme"
+ "incX' r == r (| x := Suc (x r) |)";
-(** coloured points: record extension **)
+section "coloured points: record extension";
-datatype colour = Red | Green | Blue
+datatype colour = Red | Green | Blue;
record cpoint = point +
- colour :: colour
+ colour :: colour;
-(*
+text {|
The record declaration defines new type constructors:
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 |)"
-consts foo8 :: ('a::more) cpoint_scheme
-consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"
+consts foo6 :: cpoint;
+consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)";
+consts foo8 :: "('a::more) cpoint_scheme";
+consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)";
-(* functions on point schemes work for cpoints as well *)
+text "functions on point schemes work for cpoints as well";
constdefs
foo10 :: nat
- "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
+ "foo10 == getX (| x = 2, y = 0, colour = Blue |)";
-(* non-coercive structural subtyping *)
+subsection "Non-coercive structural subtyping";
-(*foo11 has type cpoint, not type point*) (*Great!*)
+text "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";
-(** other features **)
+section "Other features";
-(* field names contribute to record identity *)
+text "field names contribute to record identity";
record point' =
x' :: nat
- y' :: nat
+ y' :: nat;
consts
- foo12 :: nat
-(*"foo12 == getX (| x' = 2, y' = 0 |)"*) (*invalid*)
+ foo12 :: nat;
+
+text {| Definition @{term "foo12 == getX (| x' = 2, y' = 0 |)"} is invalid |};
-(* polymorphic records *)
+text "polymorphic records";
record 'a point'' = point +
- content :: 'a
+ content :: 'a;
-types cpoint'' = colour point''
+types cpoint'' = "colour point''";
+text "Have a lot of fun!";
-(*Have a lot of fun!*)
-
-end
+end;