src/HOL/ex/Points.thy

 (*  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 |)"
+
+  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 |)";
 
 
-(*
-  Record declarations define new type abbreviations:
+subsection "Introducing concrete records and record schemes";
 
-    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 |)"
+defs
+  foo1_def: "foo1 == (| x = 1, y = 0 |)"
+  foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)";
 
 
-(* Introducing concrete records and record schemes *)
+subsection "Record selection and record update";
 
-defs
-  foo1_def "foo1 == (| x = 1, y = 0 |)"
-  foo3_def "foo3 ext == (| x = 1, y = 0, ... = ext |)"
+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 |)";
 
 
-(* Record selection and record update *)
+subsection "Some lemmas about records";
 
-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 |)"
+text "Note: any of these goals may be solved with a single
+ stroke of auto or force.";
 
 
-(* concrete records are type instances of record schemes *)
+text "basic simplifications";
+
+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;
+
+
+text "splitting quantifiers: the !!r is NECESSARY";
+
+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;
+
+
+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;