src/HOL/ex/Records.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 25707 0a599404f5a1
child 26932 c398a3866082
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     1 (*  Title:      HOL/ex/Records.thy
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, 
     4                 TU Muenchen
     5 *)
     6 
     7 header {* Using extensible records in HOL -- points and coloured points *}
     8 
     9 theory Records imports Main begin
    10 
    11 subsection {* Points *}
    12 
    13 record point =
    14   xpos :: nat
    15   ypos :: nat
    16 
    17 text {*
    18   Apart many other things, above record declaration produces the
    19   following theorems:
    20 *}
    21 
    22 
    23 thm "point.simps"
    24 thm "point.iffs"
    25 thm "point.defs"
    26 
    27 text {*
    28   The set of theorems @{thm [source] point.simps} is added
    29   automatically to the standard simpset, @{thm [source] point.iffs} is
    30   added to the Classical Reasoner and Simplifier context.
    31 
    32   \medskip Record declarations define new types and type abbreviations:
    33   @{text [display]
    34 "  point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
    35   'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type"}
    36 *}
    37 
    38 consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
    39 consts foo4 :: "'a => (| xpos :: nat, ypos :: nat, ... :: 'a |)"
    40 
    41 
    42 subsubsection {* Introducing concrete records and record schemes *}
    43 
    44 definition
    45   foo1 :: point
    46 where
    47   foo1_def: "foo1 = (| xpos = 1, ypos = 0 |)"
    48 
    49 definition
    50   foo3 :: "'a => 'a point_scheme"
    51 where
    52   foo3_def: "foo3 ext = (| xpos = 1, ypos = 0, ... = ext |)"
    53 
    54 
    55 subsubsection {* Record selection and record update *}
    56 
    57 definition
    58   getX :: "'a point_scheme => nat" where
    59   "getX r = xpos r"
    60 
    61 definition
    62   setX :: "'a point_scheme => nat => 'a point_scheme" where
    63   "setX r n = r (| xpos := n |)"
    64 
    65 
    66 subsubsection {* Some lemmas about records *}
    67 
    68 text {* Basic simplifications. *}
    69 
    70 lemma "point.make n p = (| xpos = n, ypos = p |)"
    71   by (simp only: point.make_def)
    72 
    73 lemma "xpos (| xpos = m, ypos = n, ... = p |) = m"
    74   by simp
    75 
    76 lemma "(| xpos = m, ypos = n, ... = p |) (| xpos:= 0 |) = (| xpos = 0, ypos = n, ... = p |)"
    77   by simp
    78 
    79 
    80 text {* \medskip Equality of records. *}
    81 
    82 lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)"
    83   -- "introduction of concrete record equality"
    84   by simp
    85 
    86 lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'"
    87   -- "elimination of concrete record equality"
    88   by simp
    89 
    90 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
    91   -- "introduction of abstract record equality"
    92   by simp
    93 
    94 lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'"
    95   -- "elimination of abstract record equality (manual proof)"
    96 proof -
    97   assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs")
    98   hence "xpos ?lhs = xpos ?rhs" by simp
    99   thus ?thesis by simp
   100 qed
   101 
   102 
   103 text {* \medskip Surjective pairing *}
   104 
   105 lemma "r = (| xpos = xpos r, ypos = ypos r |)"
   106   by simp
   107 
   108 lemma "r = (| xpos = xpos r, ypos = ypos r, ... = point.more r |)"
   109   by simp
   110 
   111 
   112 text {*
   113   \medskip Representation of records by cases or (degenerate)
   114   induction.
   115 *}
   116 
   117 lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
   118 proof (cases r)
   119   fix xpos ypos more
   120   assume "r = (| xpos = xpos, ypos = ypos, ... = more |)"
   121   thus ?thesis by simp
   122 qed
   123 
   124 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
   125 proof (induct r)
   126   fix xpos ypos more
   127   show "(| xpos = xpos, ypos = ypos, ... = more |) (| xpos := n, ypos := m |) =
   128       (| xpos = xpos, ypos = ypos, ... = more |) (| ypos := m, xpos := n |)"
   129     by simp
   130 qed
   131 
   132 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
   133 proof (cases r)
   134   fix xpos ypos more
   135   assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>"
   136   thus ?thesis by simp
   137 qed
   138 
   139 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
   140 proof (cases r)
   141   case fields
   142   thus ?thesis by simp
   143 qed
   144 
   145 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)"
   146   by (cases r) simp
   147 
   148 
   149 text {*
   150  \medskip Concrete records are type instances of record schemes.
   151 *}
   152 
   153 definition
   154   foo5 :: nat where
   155   "foo5 = getX (| xpos = 1, ypos = 0 |)"
   156 
   157 
   158 text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *}
   159 
   160 definition
   161   incX :: "'a point_scheme => 'a point_scheme" where
   162   "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
   163 
   164 lemma "incX r = setX r (Suc (getX r))"
   165   by (simp add: getX_def setX_def incX_def)
   166 
   167 
   168 text {* An alternative definition. *}
   169 
   170 definition
   171   incX' :: "'a point_scheme => 'a point_scheme" where
   172   "incX' r = r (| xpos := xpos r + 1 |)"
   173 
   174 
   175 subsection {* Coloured points: record extension *}
   176 
   177 datatype colour = Red | Green | Blue
   178 
   179 record cpoint = point +
   180   colour :: colour
   181 
   182 
   183 text {*
   184   The record declaration defines a new type constructure and abbreviations:
   185   @{text [display]
   186 "  cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) = 
   187      () cpoint_ext_type point_ext_type
   188    'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) = 
   189      'a cpoint_ext_type point_ext_type"}
   190 *}
   191 
   192 consts foo6 :: cpoint
   193 consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)"
   194 consts foo8 :: "'a cpoint_scheme"
   195 consts foo9 :: "(| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"
   196 
   197 
   198 text {*
   199  Functions on @{text point} schemes work for @{text cpoints} as well.
   200 *}
   201 
   202 definition
   203   foo10 :: nat where
   204   "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
   205 
   206 
   207 subsubsection {* Non-coercive structural subtyping *}
   208 
   209 text {*
   210  Term @{term foo11} has type @{typ cpoint}, not type @{typ point} ---
   211  Great!
   212 *}
   213 
   214 definition
   215   foo11 :: cpoint where
   216   "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0"
   217 
   218 
   219 subsection {* Other features *}
   220 
   221 text {* Field names contribute to record identity. *}
   222 
   223 record point' =
   224   xpos' :: nat
   225   ypos' :: nat
   226 
   227 text {*
   228   \noindent May not apply @{term getX} to @{term [source] "(| xpos' =
   229   2, ypos' = 0 |)"} -- type error.
   230 *}
   231 
   232 text {* \medskip Polymorphic records. *}
   233 
   234 record 'a point'' = point +
   235   content :: 'a
   236 
   237 types cpoint'' = "colour point''"
   238 
   239 
   240 
   241 text {* Updating a record field with an identical value is simplified.*}
   242 lemma "r (| xpos := xpos r |) = r"
   243   by simp
   244 
   245 text {* Only the most recent update to a component survives simplification. *}
   246 lemma "r (| xpos := x, ypos := y, xpos := x' |) = r (| ypos := y, xpos := x' |)"
   247   by simp
   248 
   249 text {* In some cases its convenient to automatically split
   250 (quantified) records. For this purpose there is the simproc @{ML [source]
   251 "RecordPackage.record_split_simproc"} and the tactic @{ML [source]
   252 "RecordPackage.record_split_simp_tac"}.  The simplification procedure
   253 only splits the records, whereas the tactic also simplifies the
   254 resulting goal with the standard record simplification rules. A
   255 (generalized) predicate on the record is passed as parameter that
   256 decides whether or how `deep' to split the record. It can peek on the
   257 subterm starting at the quantified occurrence of the record (including
   258 the quantifier). The value @{ML "0"} indicates no split, a value
   259 greater @{ML "0"} splits up to the given bound of record extension and
   260 finally the value @{ML "~1"} completely splits the record.
   261 @{ML [source] "RecordPackage.record_split_simp_tac"} additionally takes a list of
   262 equations for simplification and can also split fixed record variables.
   263 
   264 *}
   265 
   266 lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
   267   apply (tactic {* simp_tac
   268           (HOL_basic_ss addsimprocs [RecordPackage.record_split_simproc (K ~1)]) 1*})
   269   apply simp
   270   done
   271 
   272 lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
   273   apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*})
   274   apply simp
   275   done
   276 
   277 lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
   278   apply (tactic {* simp_tac
   279           (HOL_basic_ss addsimprocs [RecordPackage.record_split_simproc (K ~1)]) 1*})
   280   apply simp
   281   done
   282 
   283 lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
   284   apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*})
   285   apply simp
   286   done
   287 
   288 lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
   289   apply (tactic {* simp_tac
   290           (HOL_basic_ss addsimprocs [RecordPackage.record_split_simproc (K ~1)]) 1*})
   291   apply auto
   292   done
   293 
   294 lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
   295   apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*})
   296   apply auto
   297   done
   298 
   299 lemma "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
   300   apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*})
   301   apply auto
   302   done
   303 
   304 lemma fixes r shows "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
   305   apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*})
   306   apply auto
   307   done
   308 
   309 
   310 lemma True
   311 proof -
   312   {
   313     fix r
   314     assume pre: "P (xpos r)"
   315     have "\<exists>x. P x"
   316       using pre
   317       apply -
   318       apply (tactic {* RecordPackage.record_split_simp_tac [] (K ~1) 1*})
   319       apply auto 
   320       done
   321   }
   322   show ?thesis ..
   323 qed
   324 
   325 text {* The effect of simproc @{ML [source]
   326 "RecordPackage.record_ex_sel_eq_simproc"} is illustrated by the
   327 following lemma.  
   328 *}
   329 
   330 lemma "\<exists>r. xpos r = x"
   331   apply (tactic {*simp_tac 
   332            (HOL_basic_ss addsimprocs [RecordPackage.record_ex_sel_eq_simproc]) 1*})
   333   done
   334 
   335 
   336 end