updated;
authorwenzelm
Tue Jun 13 18:33:55 2000 +0200 (2000-06-13)
changeset 90592b537d9e6f49
parent 9058 7856a01119fb
child 9060 b0dd884b1848
updated;
src/HOL/ex/Points.thy
     1.1 --- a/src/HOL/ex/Points.thy	Tue Jun 13 18:33:34 2000 +0200
     1.2 +++ b/src/HOL/ex/Points.thy	Tue Jun 13 18:33:55 2000 +0200
     1.3 @@ -3,29 +3,31 @@
     1.4      Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     1.5  *)
     1.6  
     1.7 -theory Points = Main:;
     1.8 +theory Points = Main:
     1.9  
    1.10  text {* Basic use of extensible records in HOL, including the famous points
    1.11 - and coloured points. *};
    1.12 + and coloured points. *}
    1.13  
    1.14  
    1.15 -section {* Points *};
    1.16 +section {* Points *}
    1.17  
    1.18  record point =
    1.19    x :: nat
    1.20 -  y :: nat;
    1.21 +  y :: nat
    1.22  
    1.23  text {*
    1.24 -  Apart many other things, above record declaration produces the
    1.25 -  following theorems:
    1.26 + Apart many other things, above record declaration produces the
    1.27 + following theorems:
    1.28 +*}
    1.29  
    1.30 -    thms "point.simps"
    1.31 -    thms "point.iffs"
    1.32 -    thms "point.update_defs"
    1.33 +thm "point.simps"
    1.34 +thm "point.iffs"
    1.35 +thm "point.update_defs"
    1.36  
    1.37 -  The set of theorems "point.simps" is added automatically to the
    1.38 -  standard simpset, "point.iffs" is added to the claset and simpset.
    1.39 -*};
    1.40 +text {*
    1.41 + The set of theorems "point.simps" is added automatically to the
    1.42 + standard simpset, "point.iffs" is added to the claset and simpset.
    1.43 +*}
    1.44  
    1.45  text {*
    1.46    Record declarations define new type abbreviations:
    1.47 @@ -34,107 +36,100 @@
    1.48      'a point_scheme = "(| x :: nat, y :: nat, ... :: 'a |)"
    1.49  
    1.50    Extensions `...' must be in type class `more'!
    1.51 -*};
    1.52 +*}
    1.53  
    1.54 -consts foo1 :: point;
    1.55 -consts foo2 :: "(| x :: nat, y :: nat |)";
    1.56 -consts foo3 :: "'a => ('a::more) point_scheme";
    1.57 -consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)";
    1.58 +consts foo1 :: point
    1.59 +consts foo2 :: "(| x :: nat, y :: nat |)"
    1.60 +consts foo3 :: "'a => ('a::more) point_scheme"
    1.61 +consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)"
    1.62  
    1.63  
    1.64 -subsection {* Introducing concrete records and record schemes *};
    1.65 +subsection {* Introducing concrete records and record schemes *}
    1.66  
    1.67  defs
    1.68    foo1_def: "foo1 == (| x = 1, y = 0 |)"
    1.69 -  foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)";
    1.70 +  foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)"
    1.71  
    1.72  
    1.73 -subsection {* Record selection and record update *};
    1.74 +subsection {* Record selection and record update *}
    1.75  
    1.76  constdefs
    1.77    getX :: "('a::more) point_scheme => nat"
    1.78    "getX r == x r"
    1.79    setX :: "('a::more) point_scheme => nat => 'a point_scheme"
    1.80 -  "setX r n == r (| x := n |)";
    1.81 +  "setX r n == r (| x := n |)"
    1.82  
    1.83  
    1.84 -subsection {* Some lemmas about records *};
    1.85 +subsection {* Some lemmas about records *}
    1.86  
    1.87 -text {* Note: any of these goals may be solved with a single
    1.88 - stroke of the auto or force proof method. *};
    1.89 -
    1.90 +text {* basic simplifications *}
    1.91  
    1.92 -text {* basic simplifications *};
    1.93 +lemma "x (| x = m, y = n, ... = p |) = m"
    1.94 +  by simp
    1.95  
    1.96 -lemma "x (| x = m, y = n, ... = p |) = m";
    1.97 -  by simp;
    1.98 -
    1.99 -lemma "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)";
   1.100 -  by simp;
   1.101 +lemma "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)"
   1.102 +  by simp
   1.103  
   1.104  
   1.105 -text {* splitting quantifiers: the !!r is NECESSARY *};
   1.106 +text {* splitting quantifiers: the !!r is NECESSARY here *}
   1.107  
   1.108 -lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)";
   1.109 -proof record_split;
   1.110 -  fix a b rest;
   1.111 -  show "(| x = a, y = b, ... = rest |)(| x := n, y := m |) =
   1.112 -        (| x = a, y = b, ... = rest |)(| y := m, x := n |)";
   1.113 -    by simp;
   1.114 -qed;
   1.115 +lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)"
   1.116 +proof record_split
   1.117 +  fix x y more
   1.118 +  show "(| x = x, y = y, ... = more |)(| x := n, y := m |) =
   1.119 +        (| x = x, y = y, ... = more |)(| y := m, x := n |)"
   1.120 +    by simp
   1.121 +qed
   1.122  
   1.123 -lemma "!!r. r (| x := n |) (| x := m |) = r (| x := m |)";
   1.124 -proof record_split;
   1.125 -  fix a b rest;
   1.126 -  show "(| x = a, y = b, ... = rest |)(| x := n, x := m |) =
   1.127 -        (| x = a, y = b, ... = rest |)(| x := m |)";
   1.128 -    by simp;
   1.129 -qed;
   1.130 +lemma "!!r. r (| x := n |) (| x := m |) = r (| x := m |)"
   1.131 +proof record_split
   1.132 +  fix x y more
   1.133 +  show "(| x = x, y = y, ... = more |)(| x := n, x := m |) =
   1.134 +        (| x = x, y = y, ... = more |)(| x := m |)"
   1.135 +    by simp
   1.136 +qed
   1.137  
   1.138  
   1.139 -text {* equality of records *};
   1.140 +text {* equality of records *}
   1.141  
   1.142 -lemma "(| x = n, y = p |) = (| x = n', y = p' |) --> n = n'" (is "?EQ --> _");
   1.143 -proof;
   1.144 -  assume ?EQ;
   1.145 -  thus "n = n'"; by simp;
   1.146 -qed;
   1.147 +lemma "(| x = n, y = p |) = (| x = n', y = p' |) ==> n = n'"
   1.148 +  by simp
   1.149  
   1.150  
   1.151 -text {* concrete records are type instances of record schemes *};
   1.152 +text {* concrete records are type instances of record schemes *}
   1.153  
   1.154  constdefs
   1.155    foo5 :: nat
   1.156 -  "foo5 == getX (| x = 1, y = 0 |)";
   1.157 +  "foo5 == getX (| x = 1, y = 0 |)"
   1.158  
   1.159  
   1.160 -text {* manipulating the `...' (more) part *};
   1.161 +text {* manipulating the `...' (more) part *}
   1.162  
   1.163  constdefs
   1.164    incX :: "('a::more) point_scheme => 'a point_scheme"
   1.165 -  "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)";
   1.166 +  "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)"
   1.167  
   1.168 -lemma "!!r n. incX r = setX r (Suc (getX r))";
   1.169 -proof (unfold getX_def setX_def incX_def);
   1.170 -  show "!! r n. (| x = Suc (x r), y = y r, ... = more r |) = r(| x := Suc (x r) |)";
   1.171 -    by (record_split, simp);
   1.172 -qed;
   1.173 +lemma "!!r n. incX r = setX r (Suc (getX r))"
   1.174 +proof (unfold getX_def setX_def incX_def)
   1.175 +  show "!! r n. (| x = Suc (x r), y = y r, ... = more r |) = r(| x := Suc (x r) |)"
   1.176 +    by record_split simp
   1.177 +qed
   1.178  
   1.179  
   1.180 -text {* alternative definition *};
   1.181 +text {* alternative definition *}
   1.182  
   1.183  constdefs
   1.184    incX' :: "('a::more) point_scheme => 'a point_scheme"
   1.185 -  "incX' r == r (| x := Suc (x r) |)";
   1.186 +  "incX' r == r (| x := Suc (x r) |)"
   1.187  
   1.188  
   1.189  
   1.190 -section {* coloured points: record extension *};
   1.191 +section {* coloured points: record extension *}
   1.192  
   1.193 -datatype colour = Red | Green | Blue;
   1.194 +datatype colour = Red | Green | Blue
   1.195  
   1.196  record cpoint = point +
   1.197 -  colour :: colour;
   1.198 +  colour :: colour
   1.199  
   1.200  
   1.201  text {*
   1.202 @@ -142,53 +137,50 @@
   1.203  
   1.204      cpoint = (| x :: nat, y :: nat, colour :: colour |)
   1.205      'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |)
   1.206 -*};
   1.207 +*}
   1.208  
   1.209 -consts foo6 :: cpoint;
   1.210 -consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)";
   1.211 -consts foo8 :: "('a::more) cpoint_scheme";
   1.212 -consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)";
   1.213 +consts foo6 :: cpoint
   1.214 +consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)"
   1.215 +consts foo8 :: "('a::more) cpoint_scheme"
   1.216 +consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"
   1.217  
   1.218  
   1.219 -text {* functions on point schemes work for cpoints as well *};
   1.220 +text {* functions on point schemes work for cpoints as well *}
   1.221  
   1.222  constdefs
   1.223    foo10 :: nat
   1.224 -  "foo10 == getX (| x = 2, y = 0, colour = Blue |)";
   1.225 +  "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
   1.226  
   1.227  
   1.228 -subsection {* Non-coercive structural subtyping *};
   1.229 +subsection {* Non-coercive structural subtyping *}
   1.230  
   1.231 -text {* foo11 has type cpoint, not type point --- Great! *};
   1.232 +text {* foo11 has type cpoint, not type point --- Great! *}
   1.233  
   1.234  constdefs
   1.235    foo11 :: cpoint
   1.236 -  "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0";
   1.237 +  "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
   1.238  
   1.239  
   1.240  
   1.241 -section {* Other features *};
   1.242 +section {* Other features *}
   1.243  
   1.244 -text {* field names contribute to record identity *};
   1.245 +text {* field names contribute to record identity *}
   1.246  
   1.247  record point' =
   1.248    x' :: nat
   1.249 -  y' :: nat;
   1.250 +  y' :: nat
   1.251  
   1.252  consts
   1.253 -  foo12 :: nat;
   1.254 +  foo12 :: nat
   1.255  
   1.256 -text {* Definition @{term "foo12 == getX (| x' = 2, y' = 0 |)"} is invalid *};
   1.257 +text {* Definition @{term "foo12 == getX (| x' = 2, y' = 0 |)"} is invalid *}
   1.258  
   1.259  
   1.260 -text {* polymorphic records *};
   1.261 +text {* polymorphic records *}
   1.262  
   1.263  record 'a point'' = point +
   1.264 -  content :: 'a;
   1.265 -
   1.266 -types cpoint'' = "colour point''";
   1.267 +  content :: 'a
   1.268  
   1.269 +types cpoint'' = "colour point''"
   1.270  
   1.271 -text {* Have a lot of fun! *};
   1.272 -
   1.273 -end;
   1.274 +end