# 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.