--- 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}
*}
(*<*)
--- 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:
--- 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}:
--- 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}:%
--- 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}
--- 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)
%%
--- 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)
%%