75 of this. *} |
75 of this. *} |
76 |
76 |
77 subsection{*Structural induction*} |
77 subsection{*Structural induction*} |
78 |
78 |
79 text{* We start with an inductive proof where both cases are proved automatically: *} |
79 text{* We start with an inductive proof where both cases are proved automatically: *} |
80 lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)" |
80 lemma "2 * (\<Sum>i::nat = 0..<n+1. i) = n*(n+1)" |
81 by (induct n, simp_all) |
81 by (induct n, simp_all) |
82 |
82 |
83 text{*\noindent If we want to expose more of the structure of the |
83 text{*\noindent The constraint @{text"::nat"} is needed because all of |
|
84 the operations involved are overloaded. |
|
85 |
|
86 If we want to expose more of the structure of the |
84 proof, we can use pattern matching to avoid having to repeat the goal |
87 proof, we can use pattern matching to avoid having to repeat the goal |
85 statement: *} |
88 statement: *} |
86 lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)" (is "?P n") |
89 lemma "2 * (\<Sum>i::nat = 0..<n+1. i) = n*(n+1)" (is "?P n") |
87 proof (induct n) |
90 proof (induct n) |
88 show "?P 0" by simp |
91 show "?P 0" by simp |
89 next |
92 next |
90 fix n assume "?P n" |
93 fix n assume "?P n" |
91 thus "?P(Suc n)" by simp |
94 thus "?P(Suc n)" by simp |
92 qed |
95 qed |
93 |
96 |
94 text{* \noindent We could refine this further to show more of the equational |
97 text{* \noindent We could refine this further to show more of the equational |
95 proof. Instead we explore the same avenue as for case distinctions: |
98 proof. Instead we explore the same avenue as for case distinctions: |
96 introducing context via the \isakeyword{case} command: *} |
99 introducing context via the \isakeyword{case} command: *} |
97 lemma "2 * (\<Sum>i<n+1. i) = n*(n+1)" |
100 lemma "2 * (\<Sum>i::nat = 0..<n+1. i) = n*(n+1)" |
98 proof (induct n) |
101 proof (induct n) |
99 case 0 show ?case by simp |
102 case 0 show ?case by simp |
100 next |
103 next |
101 case Suc thus ?case by simp |
104 case Suc thus ?case by simp |
102 qed |
105 qed |