141 by (induct xs arbitrary: ys) simp_all |
141 by (induct xs arbitrary: ys) simp_all |
142 text{*\noindent The annotation @{text"arbitrary:"}~\emph{vars} |
142 text{*\noindent The annotation @{text"arbitrary:"}~\emph{vars} |
143 universally quantifies all \emph{vars} before the induction. Hence |
143 universally quantifies all \emph{vars} before the induction. Hence |
144 they can be replaced by \emph{arbitrary} values in the proof. |
144 they can be replaced by \emph{arbitrary} values in the proof. |
145 |
145 |
146 The nice thing about generalization via @{text"arbitrary:"} is that in |
146 Generalization via @{text"arbitrary"} is particularly convenient |
147 the induction step the claim is available in unquantified form but |
147 if the induction step is a structured proof as opposed to the automatic |
|
148 example above. Then the claim is available in unquantified form but |
148 with the generalized variables replaced by @{text"?"}-variables, ready |
149 with the generalized variables replaced by @{text"?"}-variables, ready |
149 for instantiation. In the above example the |
150 for instantiation. In the above example, in the @{const[source] Cons} case the |
150 induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"}. |
151 induction hypothesis is @{text"itrev xs ?ys = rev xs @ ?ys"} (available |
151 |
152 under the name @{const[source] Cons}). |
152 For the curious: @{text"arbitrary:"} introduces @{text"\<And>"} |
153 |
153 behind the scenes. |
|
154 |
154 |
155 \subsection{Inductive proofs of conditional formulae} |
155 \subsection{Inductive proofs of conditional formulae} |
156 \label{sec:full-Ind} |
156 \label{sec:full-Ind} |
157 |
157 |
158 Induction also copes well with formulae involving @{text"\<Longrightarrow>"}, for example |
158 Induction also copes well with formulae involving @{text"\<Longrightarrow>"}, for example |