Re: [isabelle] nat numerical constants simplifications



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.