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.