author wenzelm Thu Sep 21 15:58:13 2000 +0200 (2000-09-21) changeset 10052 5fa8d8d5c852 parent 10051 6c3c87d1d275 child 10053 ef58424d7893
renamed HOL/ex/Points to HOL/ex/Records;
 doc-src/HOL/HOL.tex file | annotate | diff | revisions src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/ex/ROOT.ML file | annotate | diff | revisions src/HOL/ex/Records.thy file | annotate | diff | revisions
     1.1 --- a/doc-src/HOL/HOL.tex	Thu Sep 21 14:55:46 2000 +0200
1.2 +++ b/doc-src/HOL/HOL.tex	Thu Sep 21 15:58:13 2000 +0200
1.3 @@ -1767,7 +1767,7 @@
1.4  characteristic properties (see {\S}\ref{sec:HOL:record-thms}).
1.5
1.6  There is an example theory demonstrating most basic aspects of extensible
1.7 -records (see theory \texttt{HOL/ex/Points} in the Isabelle sources).
1.8 +records (see theory \texttt{HOL/ex/Records} in the Isabelle sources).
1.9
1.10
1.11  \subsection{Defining records}\label{sec:HOL:record-def}
1.12 @@ -1937,7 +1937,7 @@
1.13
1.14  \medskip
1.15
1.16 -The example theory \texttt{HOL/ex/Points} demonstrates typical proofs
1.17 +The example theory \texttt{HOL/ex/Records} demonstrates typical proofs
1.18  concerning records.  The basic idea is to make \ttindex{record_split_tac}
1.19  expand quantified record variables and then simplify by the conversion rules.
1.20  By using a combination of the simplifier and classical prover together with

     2.1 --- a/src/HOL/IsaMakefile	Thu Sep 21 14:55:46 2000 +0200
2.2 +++ b/src/HOL/IsaMakefile	Thu Sep 21 15:58:13 2000 +0200
2.3 @@ -441,7 +441,7 @@
2.4    ex/StringEx.thy ex/Tarski.ML ex/Tarski.thy \
2.5    ex/BinEx.ML ex/BinEx.thy ex/svc_test.thy ex/svc_test.ML ex/MonoidGroup.thy \
2.6    ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
2.7 -  ex/Antiquote.thy ex/Multiquote.thy ex/Points.thy ex/Tuple.thy
2.8 +  ex/Antiquote.thy ex/Multiquote.thy ex/Records.thy ex/Tuple.thy
2.9  	@$(ISATOOL) usedir$(OUT)/HOL ex
2.10
2.11

     3.1 --- a/src/HOL/ex/ROOT.ML	Thu Sep 21 14:55:46 2000 +0200
3.2 +++ b/src/HOL/ex/ROOT.ML	Thu Sep 21 15:58:13 2000 +0200
3.3 @@ -31,7 +31,7 @@
3.4
3.5  (*basic use of extensible records*)
3.6  time_use_thy "MonoidGroup";
3.7 -time_use_thy "Points";
3.8 +time_use_thy "Records";
3.9
3.10  (*groups via locales*)
3.11  time_use_thy "PiSets";

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/ex/Records.thy	Thu Sep 21 15:58:13 2000 +0200
4.3 @@ -0,0 +1,210 @@
4.4 +(*  Title:      HOL/ex/Records.thy
4.5 +    ID:         $Id$
4.6 +    Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
4.8 +*)
4.9 +
4.10 +header {* Using extensible records in HOL -- points and coloured points *}
4.11 +
4.12 +theory Records = Main:
4.13 +
4.14 +subsection {* Points *}
4.15 +
4.16 +record point =
4.17 +  x :: nat
4.18 +  y :: nat
4.19 +
4.20 +text {*
4.21 + Apart many other things, above record declaration produces the
4.22 + following theorems:
4.23 +*}
4.24 +
4.25 +thm "point.simps"
4.26 +thm "point.iffs"
4.27 +thm "point.update_defs"
4.28 +
4.29 +text {*
4.30 + The set of theorems "point.simps" is added automatically to the
4.31 + standard simpset, "point.iffs" is added to the claset and simpset.
4.32 +*}
4.33 +
4.34 +text {*
4.35 +  Record declarations define new type abbreviations:
4.36 +
4.37 +    point = "(| x :: nat, y :: nat |)"
4.38 +    'a point_scheme = "(| x :: nat, y :: nat, ... :: 'a |)"
4.39 +
4.40 +  Extensions ...' must be in type class more'!
4.41 +*}
4.42 +
4.43 +consts foo1 :: point
4.44 +consts foo2 :: "(| x :: nat, y :: nat |)"
4.45 +consts foo3 :: "'a => ('a::more) point_scheme"
4.46 +consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)"
4.47 +
4.48 +
4.49 +subsubsection {* Introducing concrete records and record schemes *}
4.50 +
4.51 +defs
4.52 +  foo1_def: "foo1 == (| x = 1, y = 0 |)"
4.53 +  foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)"
4.54 +
4.55 +
4.56 +subsubsection {* Record selection and record update *}
4.57 +
4.58 +constdefs
4.59 +  getX :: "('a::more) point_scheme => nat"
4.60 +  "getX r == x r"
4.61 +  setX :: "('a::more) point_scheme => nat => 'a point_scheme"
4.62 +  "setX r n == r (| x := n |)"
4.63 +
4.64 +
4.65 +subsubsection {* Some lemmas about records *}
4.66 +
4.67 +text {* Basic simplifications *}
4.68 +
4.69 +lemma "point.make n p = (| x = n, y = p |)"
4.70 +  by simp
4.71 +
4.72 +lemma "x (| x = m, y = n, ... = p |) = m"
4.73 +  by simp
4.74 +
4.75 +lemma "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)"
4.76 +  by simp
4.77 +
4.78 +
4.79 +text {* Equality of records *}
4.80 +
4.81 +lemma "n = n' ==> p = p' ==> (| x = n, y = p |) = (| x = n', y = p' |)"
4.82 +  -- "introduction of concrete record equality"
4.83 +  by simp
4.84 +
4.85 +lemma "(| x = n, y = p |) = (| x = n', y = p' |) ==> n = n'"
4.86 +  -- "elimination of concrete record equality"
4.87 +  by simp
4.88 +
4.89 +lemma "r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)"
4.90 +  -- "introduction of abstract record equality"
4.91 +  by simp
4.92 +
4.93 +lemma "r (| x := n |) = r (| x := n' |) ==> n = n'"
4.94 +  -- "elimination of abstract record equality (manual proof)"
4.95 +proof -
4.96 +  assume "r (| x := n |) = r (| x := n' |)" (is "?lhs = ?rhs")
4.97 +  hence "x ?lhs = x ?rhs" by simp
4.98 +  thus ?thesis by simp
4.99 +qed
4.100 +
4.101 +
4.102 +text {* Surjective pairing *}
4.103 +
4.104 +lemma "r = (| x = x r, y = y r |)"
4.105 +  by simp
4.106 +
4.107 +lemma "r = (| x = x r, y = y r, ... = more r |)"
4.108 +  by simp
4.109 +
4.110 +
4.111 +text {* Splitting quantifiers: the !!r is NECESSARY here *}
4.112 +
4.113 +lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)"
4.114 +proof record_split
4.115 +  fix x y more
4.116 +  show "(| x = x, y = y, ... = more |)(| x := n, y := m |) =
4.117 +        (| x = x, y = y, ... = more |)(| y := m, x := n |)"
4.118 +    by simp
4.119 +qed
4.120 +
4.121 +lemma "!!r. r (| x := n |) (| x := m |) = r (| x := m |)"
4.122 +proof record_split
4.123 +  fix x y more
4.124 +  show "(| x = x, y = y, ... = more |)(| x := n, x := m |) =
4.125 +        (| x = x, y = y, ... = more |)(| x := m |)"
4.126 +    by simp
4.127 +qed
4.128 +
4.129 +
4.130 +
4.131 +text {* Concrete records are type instances of record schemes *}
4.132 +
4.133 +constdefs
4.134 +  foo5 :: nat
4.135 +  "foo5 == getX (| x = 1, y = 0 |)"
4.136 +
4.137 +
4.138 +text {* Manipulating the ...' (more) part *}
4.139 +
4.140 +constdefs
4.141 +  incX :: "('a::more) point_scheme => 'a point_scheme"
4.142 +  "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)"
4.143 +
4.144 +lemma "!!r n. incX r = setX r (Suc (getX r))"
4.145 +proof (unfold getX_def setX_def incX_def)
4.146 +  show "!!r n. (| x = Suc (x r), y = y r, ... = more r |) = r(| x := Suc (x r) |)"
4.147 +    by record_split simp
4.148 +qed
4.149 +
4.150 +
4.151 +text {* alternative definition *}
4.152 +
4.153 +constdefs
4.154 +  incX' :: "('a::more) point_scheme => 'a point_scheme"
4.155 +  "incX' r == r (| x := Suc (x r) |)"
4.156 +
4.157 +
4.158 +subsection {* Coloured points: record extension *}
4.159 +
4.160 +datatype colour = Red | Green | Blue
4.161 +
4.162 +record cpoint = point +
4.163 +  colour :: colour
4.164 +
4.165 +
4.166 +text {*
4.167 +  The record declaration defines new type constructors:
4.168 +
4.169 +    cpoint = (| x :: nat, y :: nat, colour :: colour |)
4.170 +    'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |)
4.171 +*}
4.172 +
4.173 +consts foo6 :: cpoint
4.174 +consts foo7 :: "(| x :: nat, y :: nat, colour :: colour |)"
4.175 +consts foo8 :: "('a::more) cpoint_scheme"
4.176 +consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"
4.177 +
4.178 +
4.179 +text {* Functions on point schemes work for cpoints as well *}
4.180 +
4.181 +constdefs
4.182 +  foo10 :: nat
4.183 +  "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
4.184 +
4.185 +
4.186 +subsubsection {* Non-coercive structural subtyping *}
4.187 +
4.188 +text {* foo11 has type cpoint, not type point --- Great! *}
4.189 +
4.190 +constdefs
4.191 +  foo11 :: cpoint
4.192 +  "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
4.193 +
4.194 +
4.195 +subsection {* Other features *}
4.196 +
4.197 +text {* field names contribute to record identity *}
4.198 +
4.199 +record point' =
4.200 +  x' :: nat
4.201 +  y' :: nat
4.202 +
4.203 +text {* May not apply @{term getX} to @{term "(| x' = 2, y' = 0 |)"} *}
4.204 +
4.205 +
4.206 +text {* Polymorphic records *}
4.207 +
4.208 +record 'a point'' = point +
4.209 +  content :: 'a
4.210 +
4.211 +types cpoint'' = "colour point''"
4.212 +
4.213 +end
`