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.