# HG changeset patch
# User paulson
# Date 1007651106 -3600
# Node ID 25bf458af885da4956b17868ddc12a60dec96994
# Parent  2884148a9fe94612d8e33af79397ac8c7536d9e1
replaced record_split by the cases method

diff -r 2884148a9fe9 -r 25bf458af885 doc-src/TutorialI/Types/Records.thy
--- a/doc-src/TutorialI/Types/Records.thy	Thu Dec 06 13:01:07 2001 +0100
+++ b/doc-src/TutorialI/Types/Records.thy	Thu Dec 06 16:05:06 2001 +0100
@@ -234,13 +234,10 @@
     --{* @{subgoals[display,indent=0,margin=65]} *}
 by simp
 
-text {*
-So we replace the ugly manual proof by splitting.  These must be quantified: 
-  the @{text "!!r"} is \emph{necessary}!  Note the occurrence of more, since
-  r is polymorphic.
-*}  (* FIXME better us cases/induct *)
-lemma "!!r. r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
-apply record_split --{* @{subgoals[display,indent=0,margin=65]} *}
+text {*So we replace the ugly manual proof by the "cases" method.*}
+lemma "r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
+apply (cases r)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
 by simp
 
 constdefs
diff -r 2884148a9fe9 -r 25bf458af885 doc-src/TutorialI/Types/records.tex
--- a/doc-src/TutorialI/Types/records.tex	Thu Dec 06 13:01:07 2001 +0100
+++ b/doc-src/TutorialI/Types/records.tex	Thu Dec 06 16:05:06 2001 +0100
@@ -210,8 +210,8 @@
 \end{isabelle}
 The generic version of this equality includes the field \isa{more}:
 \begin{isabelle}
-\isacommand{lemma}\ "r\ =\ \isasymlparr Xcoord\ =\ Xcoord\ r,\ Ycoord\ =\ Ycoord\ r,\ \isasymdots \ =\ point.more\
-r\isasymrparr"
+\ \ \ \ r\ =\ \isasymlparr Xcoord\ =\ Xcoord\ r,\ Ycoord\ =\ Ycoord\ r,\ \isasymdots \ =\ point.more\
+r\isasymrparr
 \end{isabelle}
 
 \medskip
@@ -234,28 +234,23 @@
 Now, \isa{simp} will reduce the assumption to the desired
 conclusion.
 
-An alternative to such forward steps is record splitting.  A record
-variable can be split only if it is bound in the subgoal by the 
-meta-quantifier \isa{\isasymAnd}, or \isa{!!} in ASCII\@.  So,
-we enter the lemma again:
+The \isa{cases} method is preferable to such a forward proof.  
+State the desired lemma again:
 \begin{isabelle}
-\isacommand{lemma}\ "!!r.\ r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\ \isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \ a\ =\
-a'"\isanewline
+\isacommand{lemma}\ "r\ \isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\ \isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \ a\ =\ a'"
 \end{isabelle}
-The \methdx{record_split} method replaces the record variable by an
-explicit record, listing all fields.  Even the field \isa{more} is
-included, since the record equality is generic.
+The \methdx{cases} method adds an equality to replace
+the named record variable by an explicit record, listing all fields.  
+It even includes the field \isa{more}, since the record equality is generic.
 \begin{isabelle}
-\isacommand{apply}\ record_split\isanewline
+\isacommand{apply}\ (cases\ r)\isanewline
 \ 1.\ \isasymAnd Xcoord\ Ycoord\ more.\isanewline
-\isaindent{\ 1.\ \ \ \ }\isasymlparr Xcoord\ =\ Xcoord,\ Ycoord\ =\ Ycoord,\ \isasymdots \ =\ more\isasymrparr \isanewline
-\isaindent{\ 1.\ \ \ \ }\isasymlparr Xcoord\ :=\ a\isasymrparr \ =\isanewline
-\isaindent{\ 1.\ \ \ \ }\isasymlparr Xcoord\ =\ Xcoord,\ Ycoord\ =\ Ycoord,\ \isasymdots \ =\ more\isasymrparr \isanewline
-\isaindent{\ 1.\ \ \ \ }\isasymlparr Xcoord\ :=\ a'\isasymrparr \ \isasymLongrightarrow \isanewline
-\isaindent{\ 1.\ \ \ \ }a\ =\ a'
+\isaindent{\ 1.\ \ \ \ }\isasymlbrakk r\isasymlparr Xcoord\ :=\ a\isasymrparr \ =\ r\isasymlparr Xcoord\ :=\ a'\isasymrparr ;\isanewline
+\isaindent{\ 1.\ \ \ \ \ \ \ }r\ =\ \isasymlparr Xcoord\ =\ Xcoord,\ Ycoord\ =\ Ycoord,\ \isasymdots \ =\ more\isasymrparr \isasymrbrakk \isanewline
+\isaindent{\ 1.\ \ \ \ }\isasymLongrightarrow \ a\ =\ a'
 \end{isabelle}
-Again, \isa{simp} finishes the proof.  Because the records have
-been split, the updates can be applied and the record equality can be
+Again, \isa{simp} finishes the proof.  Because \isa{r} has become an explicit
+record expression, the updates can be applied and the record equality can be
 replaced by equality of the corresponding fields.