[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.