# Re: [isabelle] An induction rule

`I don't know if that exact theorem is embedded in in Isabelle somewhere,
``but it can be derived from strong induction (aka nat_less_induct) as
``follows:
`

`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
---Elsa
On 4/2/15 10:32 PM, W. Douglas Maurer wrote:

`This seems like a really simple question, but after weeks of searching
``with no success I finally have to ask the list, since my student is
``waiting for the answer so he can finish his project: Where is (P(0)
``and (for all (j::nat > 0) there exists i < j such that (P(i) implies
``P(j)))) implies P(n) for all n? Many thanks! -WDMaurer
`

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