# 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)
fix n
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)
qed

`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
``"Isarish", e.g.,
`
lemma strange_induct:
assumes "P (0::nat)"
and "âj > 0. âi < j. P i â P j"
shows "P n"
proof (induct rule: nat_less_induct)
fix n
assume " âm < n. P m"
with assms show "P n" by (cases n) auto
qed

`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"
proof -
{
fix 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
qed

`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.
`
cheers
chris

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*