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
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)
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