# HG changeset patch
# User nipkow
# Date 978946431 -3600
# Node ID 4a212e635318f138c8c686086afcd7e25287deeb
# Parent  88cb1547d952bc1a75c1d5d285ed247ffc6d4faf
*** empty log message ***

diff -r 88cb1547d952 -r 4a212e635318 doc-src/TutorialI/Misc/case_exprs.thy
--- a/doc-src/TutorialI/Misc/case_exprs.thy	Sun Jan 07 22:39:28 2001 +0100
+++ b/doc-src/TutorialI/Misc/case_exprs.thy	Mon Jan 08 10:33:51 2001 +0100
@@ -42,7 +42,7 @@
 
 subsection{*Structural induction and case distinction*}
 
-text{*
+text{*\label{sec:struct-ind-case}
 \indexbold{structural induction}
 \indexbold{induction!structural}
 \indexbold{case distinction}
@@ -67,6 +67,19 @@
 text{*
 Note that we do not need to give a lemma a name if we do not intend to refer
 to it explicitly in the future.
+
+\begin{warn}
+  Induction is only allowed on free (or \isasymAnd-bound) variables that
+  should not occur among the assumptions of the subgoal; see
+  \S\ref{sec:ind-var-in-prems} for details. Case distinction
+  (@{text"case_tac"}) works for arbitrary terms, which need to be
+  quoted if they are non-atomic. However, apart from @{text"\<And>"}-bound
+  variables, the terms must not contain variables that are bound outside.
+  For example, given the goal @{prop"\<forall>xs. xs = [] \<or> (\<exists>y ys. xs = y#ys)"},
+  @{text"case_tac xs"} will not work as expected because Isabelle interprets
+  the @{term xs} as a new free variable distinct from the bound
+  @{term xs} in the goal.
+\end{warn}
 *}
 
 (*<*)
diff -r 88cb1547d952 -r 4a212e635318 doc-src/TutorialI/Misc/document/case_exprs.tex
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Sun Jan 07 22:39:28 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Jan 08 10:33:51 2001 +0100
@@ -53,6 +53,7 @@
 }
 %
 \begin{isamarkuptext}%
+\label{sec:struct-ind-case}
 \indexbold{structural induction}
 \indexbold{induction!structural}
 \indexbold{case distinction}
@@ -77,7 +78,20 @@
 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
 \begin{isamarkuptext}%
 Note that we do not need to give a lemma a name if we do not intend to refer
-to it explicitly in the future.%
+to it explicitly in the future.
+
+\begin{warn}
+  Induction is only allowed on free (or \isasymAnd-bound) variables that
+  should not occur among the assumptions of the subgoal; see
+  \S\ref{sec:ind-var-in-prems} for details. Case distinction
+  (\isa{case{\isacharunderscore}tac}) works for arbitrary terms, which need to be
+  quoted if they are non-atomic. However, apart from \isa{{\isasymAnd}}-bound
+  variables, the terms must not contain variables that are bound outside.
+  For example, given the goal \isa{{\isasymforall}xs{\isachardot}\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymor}\ {\isacharparenleft}{\isasymexists}y\ ys{\isachardot}\ xs\ {\isacharequal}\ y\ {\isacharhash}\ ys{\isacharparenright}},
+  \isa{case{\isacharunderscore}tac\ xs} will not work as expected because Isabelle interprets
+  the \isa{xs} as a new free variable distinct from the bound
+  \isa{xs} in the goal.
+\end{warn}%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
diff -r 88cb1547d952 -r 4a212e635318 doc-src/TutorialI/Types/Pairs.thy
--- a/doc-src/TutorialI/Types/Pairs.thy	Sun Jan 07 22:39:28 2001 +0100
+++ b/doc-src/TutorialI/Types/Pairs.thy	Mon Jan 08 10:33:51 2001 +0100
@@ -83,16 +83,20 @@
 
 txt{*
 @{subgoals[display,indent=0]}
-This subgoal is easily proved by simplification. The @{text"only:"} above
-merely serves to show the effect of splitting and to avoid solving the goal
-outright.
+This subgoal is easily proved by simplification. Thus we could have combined
+simplification and splitting in one command that proves the goal outright:
+*}
+(*<*)
+by simp
+lemma "(\<lambda>(x,y).y) p = snd p"(*>*)
+by(simp split: split_split)
 
+text{*
 Let us look at a second example:
 *}
 
-(*<*)by simp(*>*)
 lemma "let (x,y) = p in fst p = x";
-apply(simp only:Let_def)
+apply(simp only: Let_def)
 
 txt{*
 @{subgoals[display,indent=0]}
@@ -148,6 +152,10 @@
 Again, @{text case_tac} is applicable because @{text"\<times>"} is a datatype.
 The subgoal is easily proved by @{text simp}.
 
+Splitting by @{text case_tac} also solves the previous examples and may thus
+appear preferable to the more arcane methods introduced first. However, see
+the warning about @{text case_tac} in \S\ref{sec:struct-ind-case}.
+
 In case the term to be split is a quantified variable, there are more options.
 You can split \emph{all} @{text"\<And>"}-quantified variables in a goal
 with the rewrite rule @{thm[source]split_paired_all}:
diff -r 88cb1547d952 -r 4a212e635318 doc-src/TutorialI/Types/document/Pairs.tex
--- a/doc-src/TutorialI/Types/document/Pairs.tex	Sun Jan 07 22:39:28 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex	Mon Jan 08 10:33:51 2001 +0100
@@ -86,14 +86,15 @@
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymlongrightarrow}\ y\ {\isacharequal}\ snd\ p%
 \end{isabelle}
-This subgoal is easily proved by simplification. The \isa{only{\isacharcolon}} above
-merely serves to show the effect of splitting and to avoid solving the goal
-outright.
-
+This subgoal is easily proved by simplification. Thus we could have combined
+simplification and splitting in one command that proves the goal outright:%
+\end{isamarkuptxt}%
+\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ split{\isacharunderscore}split{\isacharparenright}%
+\begin{isamarkuptext}%
 Let us look at a second example:%
-\end{isamarkuptxt}%
+\end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}let\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ p\ in\ fst\ p\ {\isacharequal}\ x{\isachardoublequote}\isanewline
-\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}Let{\isacharunderscore}def{\isacharparenright}%
+\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptxt}%
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ fst\ p\ {\isacharequal}\ x{\isacharparenright}\ p%
@@ -146,6 +147,10 @@
 Again, \isa{case{\isacharunderscore}tac} is applicable because \isa{{\isasymtimes}} is a datatype.
 The subgoal is easily proved by \isa{simp}.
 
+Splitting by \isa{case{\isacharunderscore}tac} also solves the previous examples and may thus
+appear preferable to the more arcane methods introduced first. However, see
+the warning about \isa{case{\isacharunderscore}tac} in \S\ref{sec:struct-ind-case}.
+
 In case the term to be split is a quantified variable, there are more options.
 You can split \emph{all} \isa{{\isasymAnd}}-quantified variables in a goal
 with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:%
diff -r 88cb1547d952 -r 4a212e635318 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Sun Jan 07 22:39:28 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Mon Jan 08 10:33:51 2001 +0100
@@ -219,15 +219,6 @@
 
 \input{Misc/document/case_exprs.tex}
 
-\begin{warn}
-  Induction is only allowed on free (or \isasymAnd-bound) variables that
-  should not occur among the assumptions of the subgoal; see
-  {\S}\ref{sec:ind-var-in-prems} for details. Case distinction
-  (\isa{case_tac}) works for arbitrary terms, which need to be
-  quoted if they are non-atomic.
-\end{warn}
-
-
 \input{Ifexpr/document/Ifexpr.tex}
 
 \section{Some basic types}
diff -r 88cb1547d952 -r 4a212e635318 doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Sun Jan 07 22:39:28 2001 +0100
+++ b/doc-src/TutorialI/isabelle.sty	Mon Jan 08 10:33:51 2001 +0100
@@ -1,4 +1,5 @@
 %%
+%% $Id$
 %% Author: Markus Wenzel, TU Muenchen
 %% License: GPL (GNU GENERAL PUBLIC LICENSE)
 %%
diff -r 88cb1547d952 -r 4a212e635318 doc-src/TutorialI/isabellesym.sty
--- a/doc-src/TutorialI/isabellesym.sty	Sun Jan 07 22:39:28 2001 +0100
+++ b/doc-src/TutorialI/isabellesym.sty	Mon Jan 08 10:33:51 2001 +0100
@@ -1,4 +1,5 @@
 %%
+%% $Id$
 %% Author: Markus Wenzel, TU Muenchen
 %% License: GPL (GNU GENERAL PUBLIC LICENSE)
 %%