32 \end{isabelle} |
32 \end{isabelle} |
33 which, after simplification, becomes |
33 which, after simplification, becomes |
34 \begin{isabelle} |
34 \begin{isabelle} |
35 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ [] |
35 \ 1.\ xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd\ []\ =\ last\ [] |
36 \end{isabelle} |
36 \end{isabelle} |
37 We cannot prove this equality because we do not know what @{term"hd"} and |
37 We cannot prove this equality because we do not know what @{term hd} and |
38 @{term"last"} return when applied to @{term"[]"}. |
38 @{term last} return when applied to @{term"[]"}. |
39 |
39 |
40 The point is that we have violated the above warning. Because the induction |
40 The point is that we have violated the above warning. Because the induction |
41 formula is only the conclusion, the occurrence of @{term"xs"} in the premises is |
41 formula is only the conclusion, the occurrence of @{term xs} in the premises is |
42 not modified by induction. Thus the case that should have been trivial |
42 not modified by induction. Thus the case that should have been trivial |
43 becomes unprovable. Fortunately, the solution is easy: |
43 becomes unprovable. Fortunately, the solution is easy:\footnote{A very similar |
|
44 heuristic applies to rule inductions; see \S\ref{sec:rtc}.} |
44 \begin{quote} |
45 \begin{quote} |
45 \emph{Pull all occurrences of the induction variable into the conclusion |
46 \emph{Pull all occurrences of the induction variable into the conclusion |
46 using @{text"\<longrightarrow>"}.} |
47 using @{text"\<longrightarrow>"}.} |
47 \end{quote} |
48 \end{quote} |
48 This means we should prove |
49 This means we should prove |