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

Dear Brian, That was really a great hint. Exactly what I wanted! I was not aware of this "lemmas" command. I will look into into in more detail. All the Best! On Tue, May 15, 2012 at 3:32 AM, Brian Huffman <huffman at in.tum.de> wrote: > 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! > >> > > > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Coordenador do Curso de Ciência da Computação Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática 90619-900 -Porto Alegre - RS - Brasil

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

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

**Re: [isabelle] Case distinction with Recursion Induction***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Case distinction with Recursion Induction
- Next by Date: Re: [isabelle] schematic variables and assumption
- 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