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.