Re: [isabelle] Strong Induction



Hi,

Am 08.09.2012 19:49, schrieb Felipe Magno de Almeida:
> 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:

If you don't find an induction rule that suits your needs, write one :)

lemma nat_plus2_induct [case_names Zero One SucSuc]:
  assumes "P 0"
  and "P (Suc 0)"
  and "\<And>n. P n \<Longrightarrow> P (Suc (Suc n))"
  shows "P (n::nat)"
proof (induct n rule: less_induct)
  case (less x) with assms show ?case
    by (cases x, simp) (metis less_Suc_eq_0_disj less_Suc_eq)
qed

lemma
  fixes x y h :: nat
  shows "\<exists>x y. 2*(x::nat) + 5*(y::nat) = (h::nat)+4"
proof (induct h rule: nat_plus2_induct)
  case Zero ...
next
  case One ...
next
  case (SucSuc n) ...
qed

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055





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