[isabelle] natural number arithmetic normalisation

The following term arose inside a side-condition that the simplifier was attempting to discharge:

  (2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1)))))

The simp tactic being used included field_simps as a rewrite.

The result was an apparent "hang" as Isabelle attempted to calculate 2 ^ 32 in unary arithmetic. 

You can see the behaviour by doing

  lemma "(2::nat) ^ (2 * (2 * (2 * (2 * (2 * 1))))) = X"
  apply (simp add: field_simps)

It seems to me that this is yet more evidence that using 1 = Suc 0 as a rewrite is a bad idea.

That aside, it would be nice if the simp technology could allow the use of an innocuous rewrite (field_simps), one that doesn't even mention Suc, alongside perfectly reasonable terms such as the one above.


Attachment: signature.asc
Description: OpenPGP digital signature

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