Re: [isabelle] Strong Induction

```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?
>
> --
> 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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.