# Re: [isabelle] Strong Induction

Technically speaking, "strong induction" (also called "complete induction") is
exactly the induction principle less_induct, which you can use the way René has
shown. However, you do not need to derive a separate induction rule first, it
can be just as easy to use less_induct directly.
Tobias
Am 09/09/2012 00:37, schrieb René Neumann:
> 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é
>

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