*To*: Felipe Magno de Almeida <felipe.m.almeida at gmail.com>*Subject*: Re: [isabelle] Strong Induction*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Sat, 8 Sep 2012 17:10:53 -0300*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <CADfx-VQj2eenBprqQGCk6z4ZvFin1+o68MJnLKNv=3eHAhfe0A@mail.gmail.com>*References*: <CADfx-VQj2eenBprqQGCk6z4ZvFin1+o68MJnLKNv=3eHAhfe0A@mail.gmail.com>*Sender*: alfio.martini at gmail.com

Hi Felipe, I am not with Gries book here, but It seems that you are looking for might be what is often called recursion [or computation] induction. Take a look at section 2.3.4, in the new Isabelle tutorial (here): http://isabelle.in.tum.de/dist/Isabelle2012/doc/prog-prove.pdf and also at section 3.5 of the traditional Isabelle tutorial here: http://isabelle.in.tum.de/dist/Isabelle2012/doc/tutorial.pdf Best! On Sat, Sep 8, 2012 at 2:49 PM, Felipe Magno de Almeida < felipe.m.almeida at gmail.com> wrote: > Hello, > > I'm studying the "A Logical Approach To Discrete Math" and am trying to use > Isabelle with solving a few exercises. I am in the Induction chapter, and > I'm > trying to prove: > > lemma > fixes x y h :: nat > shows "\<exists>x y. 2*(x::nat) + 5*(y::nat) = (h::nat)+4" > > Which would be the equivalent of the first exercise of the chapter which > is: > > P.n : (\<exists>h,k | 0 <= h /\ 0 <= k: 2*h + 5*k = n) for n>=4 > > I've searched the web for isabelle strong induction and cases, etc, I've > even > tried to read the src/HOL/Tools/inductive.ML but I'm not very proficient in > ML so I really couldn't understand much. So I really have no idea on how > to proceed. > > I wrote a proof in my notebook as: > > Proved P.0 and proved P.1, then proved that > P.n => P.n+2 > > But with Isabelle I have no idea how to transpose this. The induct proof > divides in cases 0 and Suc h. So all I have is until now: > > lemma > fixes x y h :: nat > shows "\<exists>x y. 2*(x::nat) + 5*(y::nat) = (h::nat)+4" > proof (induct h) > case 0 > have "\<exists> x y. 2*x + 5*y = (0::nat) + 4" > apply (rule_tac x = 2 in exI) > by simp > thus ?case . > next > case (Suc n) > and from here I have no idea how to continue. > > What I wanted was to: > > lemma > fixes x y h :: nat > shows "\<exists>x y. 2*(x::nat) + 5*(y::nat) = (h::nat)+4" > proof (induct h) > case 0 > have "\<exists> x y. 2*x + 5*y = (0::nat) + 4" > apply (rule_tac x = 2 in exI) > by simp > thus ?case . > next > case (Suc 0) > (* etc *) > thus ?case . > next > case (Suc (Suc n)) > (* prove P.n ==> P (Suc (Suc n)) *) > thus ?case . > qed > > Any pointers? > > Thanks in advance, > -- > Felipe Magno de Almeida > > -- 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] Strong Induction***From:*Felipe Magno de Almeida

- Previous by Date: [isabelle] Strong Induction
- Next by Date: Re: [isabelle] Strong Induction
- Previous by Thread: [isabelle] Strong Induction
- Next by Thread: Re: [isabelle] Strong Induction
- Cl-isabelle-users September 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