--- a/src/HOL/ex/Points.thy Tue Jun 13 18:33:34 2000 +0200
+++ b/src/HOL/ex/Points.thy Tue Jun 13 18:33:55 2000 +0200
@@ -3,29 +3,31 @@
Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
*)
-theory Points = Main:;
+theory Points = Main:
text {* Basic use of extensible records in HOL, including the famous points
- and coloured points. *};
+ and coloured points. *}
-section {* Points *};
+section {* Points *}
record point =
x :: nat
- y :: nat;
+ y :: nat
text {*
- Apart many other things, above record declaration produces the
- following theorems:
+ Apart many other things, above record declaration produces the
+ following theorems:
+*}
- thms "point.simps"
- thms "point.iffs"
- thms "point.update_defs"
+thm "point.simps"
+thm "point.iffs"
+thm "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 {*
+ 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:
@@ -34,107 +36,100 @@
'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 |)";
+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 *};
+subsection {* Introducing concrete records and record schemes *}
defs
foo1_def: "foo1 == (| x = 1, y = 0 |)"
- foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)";
+ foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)"
-subsection {* Record selection and record update *};
+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 |)";
+ "setX r n == r (| x := n |)"
-subsection {* Some lemmas about records *};
+subsection {* Some lemmas about records *}
-text {* Note: any of these goals may be solved with a single
- stroke of the auto or force proof method. *};
-
+text {* basic simplifications *}
-text {* basic simplifications *};
+lemma "x (| x = m, y = n, ... = p |) = m"
+ by simp
-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;
+lemma "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)"
+ by simp
-text {* splitting quantifiers: the !!r is NECESSARY *};
+text {* splitting quantifiers: the !!r is NECESSARY here *}
-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 |) (| y := m |) = r (| y := m |) (| x := n |)"
+proof record_split
+ fix x y more
+ show "(| x = x, y = y, ... = more |)(| x := n, y := m |) =
+ (| x = x, y = y, ... = more |)(| 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;
+lemma "!!r. r (| x := n |) (| x := m |) = r (| x := m |)"
+proof record_split
+ fix x y more
+ show "(| x = x, y = y, ... = more |)(| x := n, x := m |) =
+ (| x = x, y = y, ... = more |)(| x := m |)"
+ by simp
+qed
-text {* equality of records *};
+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;
+lemma "(| x = n, y = p |) = (| x = n', y = p' |) ==> n = n'"
+ by simp
-text {* concrete records are type instances of record schemes *};
+text {* concrete records are type instances of record schemes *}
constdefs
foo5 :: nat
- "foo5 == getX (| x = 1, y = 0 |)";
+ "foo5 == getX (| x = 1, y = 0 |)"
-text {* 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 r == (| x = Suc (x r), y = y r, ... = point.more r |)"
-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;
+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 *};
+text {* alternative definition *}
constdefs
incX' :: "('a::more) point_scheme => 'a point_scheme"
- "incX' r == r (| x := Suc (x r) |)";
+ "incX' r == r (| x := Suc (x r) |)"
-section {* 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 {*
@@ -142,53 +137,50 @@
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 |)"
-text {* 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 |)"
-subsection {* Non-coercive structural subtyping *};
+subsection {* Non-coercive structural subtyping *}
-text {* 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"
-section {* Other features *};
+section {* Other features *}
-text {* 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 :: nat
-text {* Definition @{term "foo12 == getX (| x' = 2, y' = 0 |)"} is invalid *};
+text {* Definition @{term "foo12 == getX (| x' = 2, y' = 0 |)"} is invalid *}
-text {* polymorphic records *};
+text {* polymorphic records *}
record 'a point'' = point +
- content :: 'a;
-
-types cpoint'' = "colour point''";
+ content :: 'a
+types cpoint'' = "colour point''"
-text {* Have a lot of fun! *};
-
-end;
+end