1.1 --- a/doc-src/TutorialI/Misc/document/case_exprs.tex Thu Jul 26 16:08:16 2012 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,137 +0,0 @@
1.4 -%
1.5 -\begin{isabellebody}%
1.6 -\def\isabellecontext{case{\isaliteral{5F}{\isacharunderscore}}exprs}%
1.7 -%
1.8 -\isadelimtheory
1.9 -%
1.10 -\endisadelimtheory
1.11 -%
1.12 -\isatagtheory
1.13 -%
1.14 -\endisatagtheory
1.15 -{\isafoldtheory}%
1.16 -%
1.17 -\isadelimtheory
1.18 -%
1.19 -\endisadelimtheory
1.20 -%
1.21 -\begin{isamarkuptext}%
1.22 -\subsection{Case Expressions}
1.23 -\label{sec:case-expressions}\index{*case expressions}%
1.24 -HOL also features \isa{case}-expressions for analyzing
1.25 -elements of a datatype. For example,
1.26 -\begin{isabelle}%
1.27 -\ \ \ \ \ case\ xs\ of\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ y\ {\isaliteral{23}{\isacharhash}}\ ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ y%
1.28 -\end{isabelle}
1.29 -evaluates to \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} if \isa{xs} is \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and to \isa{y} if
1.30 -\isa{xs} is \isa{y\ {\isaliteral{23}{\isacharhash}}\ ys}. (Since the result in both branches must be of
1.31 -the same type, it follows that \isa{y} is of type \isa{{\isaliteral{27}{\isacharprime}}a\ list} and hence
1.32 -that \isa{xs} is of type \isa{{\isaliteral{27}{\isacharprime}}a\ list\ list}.)
1.33 -
1.34 -In general, case expressions are of the form
1.35 -\[
1.36 -\begin{array}{c}
1.37 -\isa{case}~e~\isa{of}\ pattern@1~\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}}~e@1\ \isa{{\isaliteral{7C}{\isacharbar}}}\ \dots\
1.38 - \isa{{\isaliteral{7C}{\isacharbar}}}~pattern@m~\isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}}~e@m
1.39 -\end{array}
1.40 -\]
1.41 -Like in functional programming, patterns are expressions consisting of
1.42 -datatype constructors (e.g. \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} and \isa{{\isaliteral{23}{\isacharhash}}})
1.43 -and variables, including the wildcard ``\verb$_$''.
1.44 -Not all cases need to be covered and the order of cases matters.
1.45 -However, one is well-advised not to wallow in complex patterns because
1.46 -complex case distinctions tend to induce complex proofs.
1.47 -
1.48 -\begin{warn}
1.49 -Internally Isabelle only knows about exhaustive case expressions with
1.50 -non-nested patterns: $pattern@i$ must be of the form
1.51 -$C@i~x@ {i1}~\dots~x@ {ik@i}$ and $C@1, \dots, C@m$ must be exactly the
1.52 -constructors of the type of $e$.
1.53 -%
1.54 -More complex case expressions are automatically
1.55 -translated into the simpler form upon parsing but are not translated
1.56 -back for printing. This may lead to surprising output.
1.57 -\end{warn}
1.58 -
1.59 -\begin{warn}
1.60 -Like \isa{if}, \isa{case}-expressions may need to be enclosed in
1.61 -parentheses to indicate their scope.
1.62 -\end{warn}
1.63 -
1.64 -\subsection{Structural Induction and Case Distinction}
1.65 -\label{sec:struct-ind-case}
1.66 -\index{case distinctions}\index{induction!structural}%
1.67 -Induction is invoked by \methdx{induct_tac}, as we have seen above;
1.68 -it works for any datatype. In some cases, induction is overkill and a case
1.69 -distinction over all constructors of the datatype suffices. This is performed
1.70 -by \methdx{case_tac}. Here is a trivial example:%
1.71 -\end{isamarkuptext}%
1.72 -\isamarkuptrue%
1.73 -\isacommand{lemma}\isamarkupfalse%
1.74 -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}case\ xs\ of\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ y{\isaliteral{23}{\isacharhash}}ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.75 -%
1.76 -\isadelimproof
1.77 -%
1.78 -\endisadelimproof
1.79 -%
1.80 -\isatagproof
1.81 -\isacommand{apply}\isamarkupfalse%
1.82 -{\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{29}{\isacharparenright}}%
1.83 -\begin{isamarkuptxt}%
1.84 -\noindent
1.85 -results in the proof state
1.86 -\begin{isabelle}%
1.87 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}case\ xs\ of\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ y\ {\isaliteral{23}{\isacharhash}}\ ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs\isanewline
1.88 -\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}a\ list{\isaliteral{2E}{\isachardot}}\isanewline
1.89 -\isaindent{\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }xs\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{23}{\isacharhash}}\ list\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}case\ xs\ of\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ y\ {\isaliteral{23}{\isacharhash}}\ ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs%
1.90 -\end{isabelle}
1.91 -which is solved automatically:%
1.92 -\end{isamarkuptxt}%
1.93 -\isamarkuptrue%
1.94 -\isacommand{apply}\isamarkupfalse%
1.95 -{\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}%
1.96 -\endisatagproof
1.97 -{\isafoldproof}%
1.98 -%
1.99 -\isadelimproof
1.100 -%
1.101 -\endisadelimproof
1.102 -%
1.103 -\begin{isamarkuptext}%
1.104 -Note that we do not need to give a lemma a name if we do not intend to refer
1.105 -to it explicitly in the future.
1.106 -Other basic laws about a datatype are applied automatically during
1.107 -simplification, so no special methods are provided for them.
1.108 -
1.109 -\begin{warn}
1.110 - Induction is only allowed on free (or \isasymAnd-bound) variables that
1.111 - should not occur among the assumptions of the subgoal; see
1.112 - \S\ref{sec:ind-var-in-prems} for details. Case distinction
1.113 - (\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}) works for arbitrary terms, which need to be
1.114 - quoted if they are non-atomic. However, apart from \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}-bound
1.115 - variables, the terms must not contain variables that are bound outside.
1.116 - For example, given the goal \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}xs{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}y\ ys{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}},
1.117 - \isa{case{\isaliteral{5F}{\isacharunderscore}}tac\ xs} will not work as expected because Isabelle interprets
1.118 - the \isa{xs} as a new free variable distinct from the bound
1.119 - \isa{xs} in the goal.
1.120 -\end{warn}%
1.121 -\end{isamarkuptext}%
1.122 -\isamarkuptrue%
1.123 -%
1.124 -\isadelimtheory
1.125 -%
1.126 -\endisadelimtheory
1.127 -%
1.128 -\isatagtheory
1.129 -%
1.130 -\endisatagtheory
1.131 -{\isafoldtheory}%
1.132 -%
1.133 -\isadelimtheory
1.134 -%
1.135 -\endisadelimtheory
1.136 -\end{isabellebody}%
1.137 -%%% Local Variables:
1.138 -%%% mode: latex
1.139 -%%% TeX-master: "root"
1.140 -%%% End: