# 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"\"}-bound + variables, the terms must not contain variables that are bound outside. + For example, given the goal @{prop"\xs. xs = [] \ (\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 "(\(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"\"} 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"\"}-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) %%