*To*: Alfio Martini <alfio.martini at acm.org>, Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Case distinction with Recursion Induction*From*: Brian Huffman <huffman at in.tum.de>*Date*: Tue, 15 May 2012 08:32:28 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FB1F3D8.4010201@in.tum.de>*References*: <CAAPnxw1azJqxNQxrVQ9VWXb3iiT-2P2qBkQM4uBcxecBmrf3Yg@mail.gmail.com> <4FB1F3D8.4010201@in.tum.de>

On Tue, May 15, 2012 at 8:12 AM, Tobias Nipkow <nipkow at in.tum.de> wrote: > The names of the cases for recursive functions are 1, 2, .... > The reason is that fun may modify the input equations to disambiguate them. Thus > one equation may become two or more and one would need some clever naming scheme > to deal with that situation in inductions. Hi Alfio, Note that if you don't like the default case names, you can rename them using the "case_names" attribute on the induction rule. You can use the "lemmas" command to save the updated rule for reuse. For example: fun fib :: "nat => nat" where "fib 0 = 0" | "fib (Suc 0) = 1" | "fib n = fib (n - 1) + fib (n - 2)" lemmas fib_induct = fib.induct [case_names 0 Suc_0 Suc_Suc] lemma "fib n \<le> fib (Suc n)" proof (induct n rule: fib_induct) case 0 show ?case by simp next case Suc_0 show ?case by simp next case (Suc_Suc k) thus ?case by simp qed - Brian > Am 14/05/2012 22:50, schrieb Alfio Martini: >> Dear Isabelle Users, >> >> I was playing a bit with proofs with recursion induction in Isar and after >> a while, it >> became all too boring to type those long formulas so that I looked for some >> ways of improving this >> situation. >> >> Pattern-matching with meta-variables as unknowns was a huge improvement. >> But >> I tried also pattern matching via case distinction and did not succeed. >> Firstly, I thought case distinction >> was only possible with structural induction. But in the new tutorial >> (Programming and >> Proving) one sees that proofs using rule induction can be done via case >> distinction >> with respect to the name (labels) of the rules. >> >> Unfortunately, I did not succeed using this trick (of using a label) for >> recursion induction. >> Am I missing something very basic here? >> >> Best! >> >

**Follow-Ups**:**Re: [isabelle] Case distinction with Recursion Induction***From:*Alfio Martini

**References**:**[isabelle] Case distinction with Recursion Induction***From:*Alfio Martini

**Re: [isabelle] Case distinction with Recursion Induction***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Case distinction with Recursion Induction
- Next by Date: [isabelle] jedit
- Previous by Thread: Re: [isabelle] Case distinction with Recursion Induction
- Next by Thread: Re: [isabelle] Case distinction with Recursion Induction
- Cl-isabelle-users May 2012 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