79 |
79 |
80 \subsection{Structural induction} |
80 \subsection{Structural induction} |
81 |
81 |
82 We start with an inductive proof where both cases are proved automatically: *} |
82 We start with an inductive proof where both cases are proved automatically: *} |
83 lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)" |
83 lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)" |
84 by (induct n, simp_all) |
84 by (induct n) simp_all |
85 |
85 |
86 text{*\noindent The constraint @{text"::nat"} is needed because all of |
86 text{*\noindent The constraint @{text"::nat"} is needed because all of |
87 the operations involved are overloaded. |
87 the operations involved are overloaded. |
|
88 This proof also demonstrates that \isakeyword{by} can take two arguments, |
|
89 one to start and one to finish the proof --- the latter is optional. |
88 |
90 |
89 If we want to expose more of the structure of the |
91 If we want to expose more of the structure of the |
90 proof, we can use pattern matching to avoid having to repeat the goal |
92 proof, we can use pattern matching to avoid having to repeat the goal |
91 statement: *} |
93 statement: *} |
92 lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)" (is "?P n") |
94 lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)" (is "?P n") |
134 needs to be universally quantified before induction succeeds.\footnote{@{thm rev.simps(1)},\quad @{thm rev.simps(2)[no_vars]},\\ @{thm itrev.simps(1)[no_vars]},\quad @{thm itrev.simps(2)[no_vars]}} But |
136 needs to be universally quantified before induction succeeds.\footnote{@{thm rev.simps(1)},\quad @{thm rev.simps(2)[no_vars]},\\ @{thm itrev.simps(1)[no_vars]},\quad @{thm itrev.simps(2)[no_vars]}} But |
135 strictly speaking, this quantification step is already part of the |
137 strictly speaking, this quantification step is already part of the |
136 proof and the quantifiers should not clutter the original claim. This |
138 proof and the quantifiers should not clutter the original claim. This |
137 is how the quantification step can be combined with induction: *} |
139 is how the quantification step can be combined with induction: *} |
138 lemma "itrev xs ys = rev xs @ ys" |
140 lemma "itrev xs ys = rev xs @ ys" |
139 by (induct xs arbitrary: ys) auto |
141 by (induct xs arbitrary: ys) simp_all |
140 text{*\noindent The annotation @{text"arbitrary:"}~\emph{vars} |
142 text{*\noindent The annotation @{text"arbitrary:"}~\emph{vars} |
141 universally quantifies all \emph{vars} before the induction. Hence |
143 universally quantifies all \emph{vars} before the induction. Hence |
142 they can be replaced by \emph{arbitrary} values in the proof. |
144 they can be replaced by \emph{arbitrary} values in the proof. |
143 This proof also demonstrates that \isakeyword{by} can take two arguments, |
|
144 one to start and one to finish the proof --- the latter is optional. |
|
145 |
145 |
146 The nice thing about generalization via @{text"arbitrary:"} is that in |
146 The nice thing about generalization via @{text"arbitrary:"} is that in |
147 the induction step the claim is available in unquantified form but |
147 the induction step the claim is available in unquantified form but |
148 with the generalized variables replaced by @{text"?"}-variables, ready |
148 with the generalized variables replaced by @{text"?"}-variables, ready |
149 for instantiation. In the above example the |
149 for instantiation. In the above example the |
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 |
159 *} |
159 *} |
160 |
160 |
161 lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs" |
161 lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs" |
162 by (induct xs) auto |
162 by (induct xs) simp_all |
163 |
163 |
164 text{*\noindent This is an improvement over that style the |
164 text{*\noindent This is an improvement over that style the |
165 tutorial~\cite{LNCS2283} advises, which requires @{text"\<longrightarrow>"}. |
165 tutorial~\cite{LNCS2283} advises, which requires @{text"\<longrightarrow>"}. |
166 A further improvement is shown in the following proof: |
166 A further improvement is shown in the following proof: |
167 *} |
167 *} |