*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Induction starting from 1 and beyond*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Wed, 25 Mar 2015 13:50:59 +0100*In-reply-to*: <1427234535.23788.4.camel@kit.edu>*References*: <a06200795d1377a9cc56c@[192.168.1.20]> <1427234535.23788.4.camel@kit.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.5.0

lemma ind_from_2 [case_names 0 1 2 many]: fixes P :: "nat â bool" assumes "P 0" and "P 1" and "P 2" and "âk. k â 2 â P k â P (Suc k)" shows "P n" using assms apply (induction_schema) apply (case_tac n, force, force) apply (lexicographic_order) done

cheers chris On 03/24/2015 11:02 PM, Joachim Breitner wrote:

Dear Douglas, Am Dienstag, den 24.03.2015, 15:37 -0500 schrieb W. Douglas Maurer:P. S. While I was still in graduate school I co-wrote a paper containing an inductive proof in which the inductive step, P(k-1) implies P(k), depended on the fact that k >= 3. Therefore I needed two basis steps, one for k = 1, which was trivial, and one for k = 2, which my co-author supplied. How would you do something like that in Isar?remember that inductions schemes are just regular lemmas, so you can always define precisely the induction rule that you need, and use that: lemma ind_from_2[case_names 0 1 2 many]: assumes "P 0" assumes "P 1" assumes "P 2" assumes "â k. k â 2 â P k â P (Suc k)" shows "P n" proof(induction n) case 0 thus ?case by fact next case (Suc k) have "k = 0 â k = 1 â k â 2" by auto with Suc.IH assms show ?case by (auto simp add: numeral_eq_Suc) qed And later lemma "foo n" proof(induction n rule: ind_from_2) case 0 show ?case... next case 1 show ?case... next case 2 show ?case... next case many show ?case... qed I find this separation of concerns makes your proofs much easier to read and understand. Greetings, Joachim

**References**:**[isabelle] Induction starting from 1 and beyond***From:*W. Douglas Maurer

**Re: [isabelle] Induction starting from 1 and beyond***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Induction starting from 1 and beyond
- Next by Date: [isabelle] _graph _grap_aux and _sumC
- Previous by Thread: Re: [isabelle] Induction starting from 1 and beyond
- Next by Thread: Re: [isabelle] Induction starting from 1 and beyond
- Cl-isabelle-users March 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list