ex/Points Isar'ized;
authorwenzelm
Wed May 26 22:45:59 1999 +0200 (1999-05-26)
changeset 673703f0ff7ee029
parent 6736 a0b2cfa12d0d
child 6738 06189132c67b
ex/Points Isar'ized;
src/HOL/IsaMakefile
src/HOL/ex/Points.ML
src/HOL/ex/Points.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed May 26 22:45:08 1999 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed May 26 22:45:59 1999 +0200
     1.3 @@ -318,7 +318,7 @@
     1.4    ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \
     1.5    ex/StringEx.thy ex/BinEx.ML ex/BinEx.thy ex/MonoidGroup.thy \
     1.6    ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
     1.7 -  ex/Antiquote.thy ex/Antiquote.ML ex/Points.thy ex/Points.ML
     1.8 +  ex/Antiquote.thy ex/Antiquote.ML ex/Points.thy
     1.9  	@$(ISATOOL) usedir $(OUT)/HOL ex
    1.10  
    1.11  
     2.1 --- a/src/HOL/ex/Points.ML	Wed May 26 22:45:08 1999 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,46 +0,0 @@
     2.4 -(*  Title:      HOL/ex/Points.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     2.7 -
     2.8 -Basic use of extensible records in HOL, including the famous points
     2.9 -and coloured points.
    2.10 -
    2.11 -Note: any of these goals may be solved at a stroke by Auto_tac or Force_tac
    2.12 -*)
    2.13 -
    2.14 -
    2.15 -(* some basic simplifications *)
    2.16 -
    2.17 -Goal "x (| x = m, y = n, ... = p |) = m";
    2.18 -by (Simp_tac 1);
    2.19 -result();
    2.20 -
    2.21 -Goal "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)";
    2.22 -by (Simp_tac 1);
    2.23 -result();
    2.24 -
    2.25 -
    2.26 -(* splitting quantifiers: the !!r is NECESSARY *)
    2.27 -
    2.28 -Goal "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)";
    2.29 -by (record_split_tac 1);
    2.30 -by (Simp_tac 1);
    2.31 -result();
    2.32 -
    2.33 -Goal "!!r. r (| x := n |) (| x := m |) = r (| x := m |)";
    2.34 -by (record_split_tac 1);
    2.35 -by (Simp_tac 1);
    2.36 -result();
    2.37 -
    2.38 -
    2.39 -(* record equality *)
    2.40 -
    2.41 -Goal "(| x = n, y = p |) = (| x = n', y = p' |) & n = 0 ==> n' = 0";
    2.42 -by (Asm_full_simp_tac 1);
    2.43 -by (Blast_tac 1);
    2.44 -result();
    2.45 -
    2.46 -Goalw [getX_def, setX_def, incX_def] "!!r n. incX r = setX r (Suc (getX r))";
    2.47 -by (record_split_tac 1);
    2.48 -by (Simp_tac 1);
    2.49 -result();
     3.1 --- a/src/HOL/ex/Points.thy	Wed May 26 22:45:08 1999 +0200
     3.2 +++ b/src/HOL/ex/Points.thy	Wed May 26 22:45:59 1999 +0200
     3.3 @@ -1,143 +1,194 @@
     3.4  (*  Title:      HOL/ex/Points.thy
     3.5      ID:         $Id$
     3.6      Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     3.7 -
     3.8 -Basic use of extensible records in HOL, including the famous points
     3.9 -and coloured points.
    3.10  *)
    3.11  
    3.12 -Points = Main +
    3.13 +theory Points = Main:;
    3.14 +
    3.15 +title "Basic use of extensible records in HOL, including the famous points
    3.16 + and coloured points.";
    3.17  
    3.18  
    3.19 -(** points **)
    3.20 +section "Points";
    3.21  
    3.22  record point =
    3.23    x :: nat
    3.24 -  y :: nat
    3.25 +  y :: nat;
    3.26  
    3.27 -(*
    3.28 -  To find out, which theorems are produced by the record declaration,
    3.29 -  type the following commands:
    3.30 +text {|
    3.31 +  Apart many other things, above record declaration produces the
    3.32 +  following theorems:
    3.33  
    3.34 -    thms "point.simps";
    3.35 -    thms "point.iffs";
    3.36 -    thms "point.update_defs";
    3.37 +    thms "point.simps"
    3.38 +    thms "point.iffs"
    3.39 +    thms "point.update_defs"
    3.40  
    3.41    The set of theorems "point.simps" is added automatically to the
    3.42    standard simpset, "point.iffs" is added to the claset and simpset.
    3.43 -*)
    3.44 +|};
    3.45  
    3.46 -
    3.47 -(*
    3.48 +text {|
    3.49    Record declarations define new type abbreviations:
    3.50  
    3.51 -    point = (| x :: nat, y :: nat |)
    3.52 -    'a point_scheme = (| x :: nat, y :: nat, ... :: 'a |)
    3.53 +    point = "(| x :: nat, y :: nat |)"
    3.54 +    'a point_scheme = "(| x :: nat, y :: nat, ... :: 'a |)"
    3.55  
    3.56    Extensions `...' must be in type class `more'!
    3.57 -*)
    3.58 +|};
    3.59 +
    3.60 +consts foo1 :: point;
    3.61 +consts foo2 :: "(| x :: nat, y :: nat |)";
    3.62 +consts foo3 :: "'a => ('a::more) point_scheme";
    3.63 +consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)";
    3.64 +
    3.65 +
    3.66 +subsection "Introducing concrete records and record schemes";
    3.67 +
    3.68 +defs
    3.69 +  foo1_def: "foo1 == (| x = 1, y = 0 |)"
    3.70 +  foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)";
    3.71  
    3.72 -consts foo1 :: point
    3.73 -consts foo2 :: "(| x :: nat, y :: nat |)"
    3.74 -consts foo3 :: 'a => ('a::more) point_scheme
    3.75 -consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)"
    3.76 +
    3.77 +subsection "Record selection and record update";
    3.78 +
    3.79 +constdefs
    3.80 +  getX :: "('a::more) point_scheme => nat"
    3.81 +  "getX r == x r"
    3.82 +  setX :: "('a::more) point_scheme => nat => 'a point_scheme"
    3.83 +  "setX r n == r (| x := n |)";
    3.84 +
    3.85 +
    3.86 +subsection "Some lemmas about records";
    3.87 +
    3.88 +text "Note: any of these goals may be solved with a single
    3.89 + stroke of auto or force.";
    3.90  
    3.91  
    3.92 -(* Introducing concrete records and record schemes *)
    3.93 +text "basic simplifications";
    3.94  
    3.95 -defs
    3.96 -  foo1_def "foo1 == (| x = 1, y = 0 |)"
    3.97 -  foo3_def "foo3 ext == (| x = 1, y = 0, ... = ext |)"
    3.98 +lemma "x (| x = m, y = n, ... = p |) = m";
    3.99 +  by simp;
   3.100 +
   3.101 +lemma "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)";
   3.102 +  by simp;
   3.103  
   3.104  
   3.105 -(* Record selection and record update *)
   3.106 +text "splitting quantifiers: the !!r is NECESSARY";
   3.107  
   3.108 -constdefs
   3.109 -  getX :: ('a::more) point_scheme => nat
   3.110 -  "getX r == x r"
   3.111 -  setX :: ('a::more) point_scheme => nat => 'a point_scheme
   3.112 -  "setX r n == r (| x := n |)"
   3.113 +lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)";
   3.114 +proof record_split;
   3.115 +  fix a b rest;
   3.116 +  show "(| x = a, y = b, ... = rest |)(| x := n, y := m |) =
   3.117 +        (| x = a, y = b, ... = rest |)(| y := m, x := n |)";
   3.118 +    by simp;
   3.119 +qed;
   3.120 +
   3.121 +lemma "!!r. r (| x := n |) (| x := m |) = r (| x := m |)";
   3.122 +proof record_split;
   3.123 +  fix a b rest;
   3.124 +  show "(| x = a, y = b, ... = rest |)(| x := n, x := m |) =
   3.125 +        (| x = a, y = b, ... = rest |)(| x := m |)";
   3.126 +    by simp;
   3.127 +qed;
   3.128  
   3.129  
   3.130 -(* concrete records are type instances of record schemes *)
   3.131 +text "equality of records";
   3.132 +
   3.133 +lemma "(| x = n, y = p |) = (| x = n', y = p' |) --> n = n'" (is "??EQ --> _");
   3.134 +proof;
   3.135 +  assume ??EQ;
   3.136 +  thus "n = n'"; by simp;
   3.137 +qed;
   3.138 +
   3.139 +
   3.140 +text "concrete records are type instances of record schemes";
   3.141  
   3.142  constdefs
   3.143    foo5 :: nat
   3.144 -  "foo5 == getX (| x = 1, y = 0 |)"
   3.145 +  "foo5 == getX (| x = 1, y = 0 |)";
   3.146  
   3.147  
   3.148 -(* manipulating the `...' (more-part) *)
   3.149 +text "manipulating the `...' (more) part";
   3.150  
   3.151  constdefs
   3.152 -  incX :: ('a::more) point_scheme => 'a point_scheme
   3.153 -  "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)"
   3.154 +  incX :: "('a::more) point_scheme => 'a point_scheme"
   3.155 +  "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)";
   3.156  
   3.157 -(*alternative definition*)
   3.158 +lemma "!!r n. incX r = setX r (Suc (getX r))";
   3.159 +proof (unfold getX_def setX_def incX_def);
   3.160 +  show "!! r n. (| x = Suc (x r), y = y r, ... = more r |) = r(| x := Suc (x r) |)";
   3.161 +    by (record_split, simp);
   3.162 +qed;
   3.163 +
   3.164 +
   3.165 +text "alternative definition";
   3.166 +
   3.167  constdefs
   3.168 -  incX' :: ('a::more) point_scheme => 'a point_scheme
   3.169 -  "incX' r == r (| x := Suc (x r) |)"
   3.170 +  incX' :: "('a::more) point_scheme => 'a point_scheme"
   3.171 +  "incX' r == r (| x := Suc (x r) |)";
   3.172  
   3.173  
   3.174  
   3.175 -(** coloured points: record extension **)
   3.176 +section "coloured points: record extension";
   3.177  
   3.178 -datatype colour = Red | Green | Blue
   3.179 +datatype colour = Red | Green | Blue;
   3.180  
   3.181  record cpoint = point +
   3.182 -  colour :: colour
   3.183 +  colour :: colour;
   3.184  
   3.185  
   3.186 -(*
   3.187 +text {|
   3.188    The record declaration defines new type constructors:
   3.189  
   3.190      cpoint = (| x :: nat, y :: nat, colour :: colour |)
   3.191      'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |)
   3.192 -*)
   3.193 +|};
   3.194  
   3.195 -consts foo6 :: cpoint
   3.196 -consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)"
   3.197 -consts foo8 :: ('a::more) cpoint_scheme
   3.198 -consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"
   3.199 +consts foo6 :: cpoint;
   3.200 +consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)";
   3.201 +consts foo8 :: "('a::more) cpoint_scheme";
   3.202 +consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)";
   3.203  
   3.204  
   3.205 -(* functions on point schemes work for cpoints as well *)
   3.206 +text "functions on point schemes work for cpoints as well";
   3.207  
   3.208  constdefs
   3.209    foo10 :: nat
   3.210 -  "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
   3.211 +  "foo10 == getX (| x = 2, y = 0, colour = Blue |)";
   3.212  
   3.213  
   3.214 -(* non-coercive structural subtyping *)
   3.215 +subsection "Non-coercive structural subtyping";
   3.216  
   3.217 -(*foo11 has type cpoint, not type point*)                       (*Great!*)
   3.218 +text "foo11 has type cpoint, not type point --- Great!";
   3.219 +
   3.220  constdefs
   3.221    foo11 :: cpoint
   3.222 -  "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
   3.223 +  "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0";
   3.224  
   3.225  
   3.226  
   3.227 -(** other features **)
   3.228 +section "Other features";
   3.229  
   3.230 -(* field names contribute to record identity *)
   3.231 +text "field names contribute to record identity";
   3.232  
   3.233  record point' =
   3.234    x' :: nat
   3.235 -  y' :: nat
   3.236 +  y' :: nat;
   3.237  
   3.238  consts
   3.239 -  foo12 :: nat
   3.240 -(*"foo12 == getX (| x' = 2, y' = 0 |)"*)        (*invalid*)
   3.241 +  foo12 :: nat;
   3.242 +
   3.243 +text {| Definition @{term "foo12 == getX (| x' = 2, y' = 0 |)"} is invalid |};
   3.244  
   3.245  
   3.246 -(* polymorphic records *)
   3.247 +text "polymorphic records";
   3.248  
   3.249  record 'a point'' = point +
   3.250 -  content :: 'a
   3.251 +  content :: 'a;
   3.252  
   3.253 -types cpoint'' = colour point''
   3.254 +types cpoint'' = "colour point''";
   3.255  
   3.256  
   3.257 +text "Have a lot of fun!";
   3.258  
   3.259 -(*Have a lot of fun!*)
   3.260 -
   3.261 -end
   3.262 +end;