Re: [isabelle] nat numerical constants simplifications





On 01/28/2014 10:45 AM, Viorel Preoteasa wrote:
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.
I see.


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).
For this case (i.e., commutativity) it might help to add "ac_simps" to the "simp" or "auto".

cheers

chris


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.