Re: [isabelle] An induction rule
On 04/03/2015 06:04 AM, Elsa L. Gunter wrote:
lemma strange_induct[rule_format]: "(P (0::nat)) â (â j > 0. â i < j. P
i â P j) â P n"
proof (induct rule: nat_less_induct, auto)
assume A:" âm<n. P m" and B: "P 0" and C: " âj>0ânat. âi<j. P i â P j"
from A and B and C
show "P n"
by (case_tac "n = 0", auto)
Just for the record, it is bad style to start a proof with an automatic
method ("proof (..., auto)" above), since basically the resulting
subgoals can change at the whim of whoever is maintaining the theories
your own development is based on.
This can often be avoided by phrasing the lemma statement more
assumes "P (0::nat)"
and "âj > 0. âi < j. P i â P j"
shows "P n"
proof (induct rule: nat_less_induct)
assume " âm < n. P m"
with assms show "P n" by (cases n) auto
Another possibility is to use a combination of raw proof blocks and a
final application of an automatic method:
lemma strange_induct' [rule_format]:
"P (0::nat) â (â j > 0. â i < j. P i â P j) â P n"
assume "âm < n. P m" and "P 0" and " â j > 0. â i < j. P i â P j"
then have "P n" by (cases "n = 0") auto
then show ?thesis
by (induct rule: nat_less_induct) blast
In that way you can just state what you *want* (as opposed to what you
*have* to state according to the current subgoal) and rely on automatic
tools to make sure that this corresponds to the current subgoal.
This archive was generated by a fusion of
Pipermail (Mailman edition) and