renamed to Records.thy;
authorwenzelm
Thu Sep 21 18:47:18 2000 +0200 (2000-09-21)
changeset 100540afe7d951447
parent 10053 ef58424d7893
child 10055 2264bdd8becc
renamed to Records.thy;
src/HOL/ex/Points.thy
     1.1 --- a/src/HOL/ex/Points.thy	Thu Sep 21 18:33:48 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,211 +0,0 @@
     1.4 -(*  Title:      HOL/ex/Points.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     1.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 -*)
     1.9 -
    1.10 -header {* Points and coloured points --- using extensible records in HOL *}
    1.11 -
    1.12 -theory Points = Main:
    1.13 -
    1.14 -
    1.15 -subsection {* Points *}
    1.16 -
    1.17 -record point =
    1.18 -  x :: nat
    1.19 -  y :: nat
    1.20 -
    1.21 -text {*
    1.22 - Apart many other things, above record declaration produces the
    1.23 - following theorems:
    1.24 -*}
    1.25 -
    1.26 -thm "point.simps"
    1.27 -thm "point.iffs"
    1.28 -thm "point.update_defs"
    1.29 -
    1.30 -text {*
    1.31 - The set of theorems "point.simps" is added automatically to the
    1.32 - standard simpset, "point.iffs" is added to the claset and simpset.
    1.33 -*}
    1.34 -
    1.35 -text {*
    1.36 -  Record declarations define new type abbreviations:
    1.37 -
    1.38 -    point = "(| x :: nat, y :: nat |)"
    1.39 -    'a point_scheme = "(| x :: nat, y :: nat, ... :: 'a |)"
    1.40 -
    1.41 -  Extensions `...' must be in type class `more'!
    1.42 -*}
    1.43 -
    1.44 -consts foo1 :: point
    1.45 -consts foo2 :: "(| x :: nat, y :: nat |)"
    1.46 -consts foo3 :: "'a => ('a::more) point_scheme"
    1.47 -consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)"
    1.48 -
    1.49 -
    1.50 -subsubsection {* Introducing concrete records and record schemes *}
    1.51 -
    1.52 -defs
    1.53 -  foo1_def: "foo1 == (| x = 1, y = 0 |)"
    1.54 -  foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)"
    1.55 -
    1.56 -
    1.57 -subsubsection {* Record selection and record update *}
    1.58 -
    1.59 -constdefs
    1.60 -  getX :: "('a::more) point_scheme => nat"
    1.61 -  "getX r == x r"
    1.62 -  setX :: "('a::more) point_scheme => nat => 'a point_scheme"
    1.63 -  "setX r n == r (| x := n |)"
    1.64 -
    1.65 -
    1.66 -subsubsection {* Some lemmas about records *}
    1.67 -
    1.68 -text {* Basic simplifications *}
    1.69 -
    1.70 -lemma "point.make n p = (| x = n, y = p |)"
    1.71 -  by simp
    1.72 -
    1.73 -lemma "x (| x = m, y = n, ... = p |) = m"
    1.74 -  by simp
    1.75 -
    1.76 -lemma "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)"
    1.77 -  by simp
    1.78 -
    1.79 -
    1.80 -text {* Equality of records *}
    1.81 -
    1.82 -lemma "n = n' ==> p = p' ==> (| x = n, y = p |) = (| x = n', y = p' |)"
    1.83 -  -- "introduction of concrete record equality"
    1.84 -  by simp
    1.85 -
    1.86 -lemma "(| x = n, y = p |) = (| x = n', y = p' |) ==> n = n'"
    1.87 -  -- "elimination of concrete record equality"
    1.88 -  by simp
    1.89 -
    1.90 -lemma "r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)"
    1.91 -  -- "introduction of abstract record equality"
    1.92 -  by simp
    1.93 -
    1.94 -lemma "r (| x := n |) = r (| x := n' |) ==> n = n'"
    1.95 -  -- "elimination of abstract record equality (manual proof)"
    1.96 -proof -
    1.97 -  assume "r (| x := n |) = r (| x := n' |)" (is "?lhs = ?rhs")
    1.98 -  hence "x ?lhs = x ?rhs" by simp
    1.99 -  thus ?thesis by simp
   1.100 -qed
   1.101 -
   1.102 -
   1.103 -text {* Surjective pairing *}
   1.104 -
   1.105 -lemma "r = (| x = x r, y = y r |)"
   1.106 -  by simp
   1.107 -
   1.108 -lemma "r = (| x = x r, y = y r, ... = more r |)"
   1.109 -  by simp
   1.110 -
   1.111 -
   1.112 -text {* Splitting quantifiers: the !!r is NECESSARY here *}
   1.113 -
   1.114 -lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)"
   1.115 -proof record_split
   1.116 -  fix x y more
   1.117 -  show "(| x = x, y = y, ... = more |)(| x := n, y := m |) =
   1.118 -        (| x = x, y = y, ... = more |)(| y := m, x := n |)"
   1.119 -    by simp
   1.120 -qed
   1.121 -
   1.122 -lemma "!!r. r (| x := n |) (| x := m |) = r (| x := m |)"
   1.123 -proof record_split
   1.124 -  fix x y more
   1.125 -  show "(| x = x, y = y, ... = more |)(| x := n, x := m |) =
   1.126 -        (| x = x, y = y, ... = more |)(| x := m |)"
   1.127 -    by simp
   1.128 -qed
   1.129 -
   1.130 -
   1.131 -
   1.132 -text {* Concrete records are type instances of record schemes *}
   1.133 -
   1.134 -constdefs
   1.135 -  foo5 :: nat
   1.136 -  "foo5 == getX (| x = 1, y = 0 |)"
   1.137 -
   1.138 -
   1.139 -text {* Manipulating the `...' (more) part *}
   1.140 -
   1.141 -constdefs
   1.142 -  incX :: "('a::more) point_scheme => 'a point_scheme"
   1.143 -  "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)"
   1.144 -
   1.145 -lemma "!!r n. incX r = setX r (Suc (getX r))"
   1.146 -proof (unfold getX_def setX_def incX_def)
   1.147 -  show "!!r n. (| x = Suc (x r), y = y r, ... = more r |) = r(| x := Suc (x r) |)"
   1.148 -    by record_split simp
   1.149 -qed
   1.150 -
   1.151 -
   1.152 -text {* alternative definition *}
   1.153 -
   1.154 -constdefs
   1.155 -  incX' :: "('a::more) point_scheme => 'a point_scheme"
   1.156 -  "incX' r == r (| x := Suc (x r) |)"
   1.157 -
   1.158 -
   1.159 -subsection {* Coloured points: record extension *}
   1.160 -
   1.161 -datatype colour = Red | Green | Blue
   1.162 -
   1.163 -record cpoint = point +
   1.164 -  colour :: colour
   1.165 -
   1.166 -
   1.167 -text {*
   1.168 -  The record declaration defines new type constructors:
   1.169 -
   1.170 -    cpoint = (| x :: nat, y :: nat, colour :: colour |)
   1.171 -    'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |)
   1.172 -*}
   1.173 -
   1.174 -consts foo6 :: cpoint
   1.175 -consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)"
   1.176 -consts foo8 :: "('a::more) cpoint_scheme"
   1.177 -consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"
   1.178 -
   1.179 -
   1.180 -text {* Functions on point schemes work for cpoints as well *}
   1.181 -
   1.182 -constdefs
   1.183 -  foo10 :: nat
   1.184 -  "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
   1.185 -
   1.186 -
   1.187 -subsubsection {* Non-coercive structural subtyping *}
   1.188 -
   1.189 -text {* foo11 has type cpoint, not type point --- Great! *}
   1.190 -
   1.191 -constdefs
   1.192 -  foo11 :: cpoint
   1.193 -  "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
   1.194 -
   1.195 -
   1.196 -subsection {* Other features *}
   1.197 -
   1.198 -text {* field names contribute to record identity *}
   1.199 -
   1.200 -record point' =
   1.201 -  x' :: nat
   1.202 -  y' :: nat
   1.203 -
   1.204 -text {* May not apply @{term getX} to @{term "(| x' = 2, y' = 0 |)"} *}
   1.205 -
   1.206 -
   1.207 -text {* Polymorphic records *}
   1.208 -
   1.209 -record 'a point'' = point +
   1.210 -  content :: 'a
   1.211 -
   1.212 -types cpoint'' = "colour point''"
   1.213 -
   1.214 -end