renamed HOL/ex/Points to HOL/ex/Records;
authorwenzelm
Thu Sep 21 15:58:13 2000 +0200 (2000-09-21)
changeset 100525fa8d8d5c852
parent 10051 6c3c87d1d275
child 10053 ef58424d7893
renamed HOL/ex/Points to HOL/ex/Records;
doc-src/HOL/HOL.tex
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
src/HOL/ex/Records.thy
     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.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     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