Re: [isabelle] nat numerical constants simplifications



Am Montag, den 27.01.2014, 16:56 +0200 schrieb Viorel Preoteasa:
> I have the following two lemmas:
> 
> lemma "(2 + (Suc  n)) = (3 + n)"
>   by simp
> 
> lemma "f (2 + (Suc n)) = f (3 + n)"
>   by simp
> 
> The first one is proved by simp, but the proof on the 
> second lemma fails. How can I simplify numerical
> constants in context?
> 
> Best regards,
> 
> Viorel Preoteasa
> 

You can use numeral_eq_Suc to rewrite numerals into "Suc"s,
e.g. 3 into Suc (Suc (Suc 0)).

 - Johannes





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