# [isabelle] Strong Induction

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

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