equal
deleted
inserted
replaced
82 \end{quote} |
82 \end{quote} |
83 This prevents trivial failures like the above and does not change the |
83 This prevents trivial failures like the above and does not change the |
84 provability of the goal. Because it is not always required, and may even |
84 provability of the goal. Because it is not always required, and may even |
85 complicate matters in some cases, this heuristic is often not |
85 complicate matters in some cases, this heuristic is often not |
86 applied blindly. |
86 applied blindly. |
|
87 |
|
88 In general, if you have tried the above heuristics and still find your |
|
89 induction does not go through, and no obvious lemma suggests itself, you may |
|
90 need to generalize your proposition even further. This requires insight into |
|
91 the problem at hand and is beyond simple rules of thumb. In a nutshell: you |
|
92 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} |
|
93 to learn about some advanced techniques for inductive proofs. |
87 *}; |
94 *}; |
88 |
95 |
89 (*<*) |
96 (*<*) |
90 by(induct_tac xs, simp, simp); |
97 by(induct_tac xs, simp, simp); |
91 end |
98 end |