# Re: [isabelle] nat numerical constants simplifications

```Hi Chris,

My context is more complicated than f … = f …
I need to instantiate an assumption (forall n . …) with n, 1+n, 2+n, …, 10+n
and among other things I get
f (y (1 + n)) = 1 + f (y n) + 1
f (y (2 + n)) = 1 + f (y (1 + n)) + 1
…
I need to get all these simplified to
f (y (10 + n)) = f (y n) + 10 and ultimately prove f (y (10 + n)) >= 10 knowing
that  f (y n) >= 0.

The problem occurred when using 3 + n which was not simplified anymore
to Suc … . At first it seemed impossible to go forward, but then I remembered
sledgehammer, and I used it. It suggested the lemma Suc3_eq_add_3.
Using this lemma at the step (3+n), I could go forward. There were still
some problems because I mixed (… + n) and (n + …), but then they
were solved when changing everything to (… + n).

Best regards,

Viorel

On 28 Jan 2014, at 11:28, Christian Sternagel <c.sternagel at gmail.com> wrote:

> I would have suggested
>
> lemma "f (2 + (Suc n)) = f (3 + n)"
>  by (rule arg_cong) simp
>
> which works (thanks to backtracking?). Unfortunately, if you write the same as
>
>  lemma "f (2 + (Suc n)) = f (3 + n)"
>  apply (rule arg_cong)
>  apply (simp)
>  done
>
> in order to see the intermediate results, the prove fails, since "apply (rule arg_cong)" does not change the goal. Is this intended? Is "rule" allowed to leave a goal unchanged? (Btw: a little instantiation helps, e.g., "apply (rule arg_cong [of _ _ f])").
>
> cheers
>
> chris
>
> On 01/27/2014 03:56 PM, Viorel Preoteasa wrote:
>> 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
>>
>

```

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