Re: [isabelle] Failing simproc

On 18.07.2012 10:55, Dmitriy Traytel wrote:
Hi *,

I stumbled upon some funny behaviour which prevents the simplifier in
proving "True" in Isabelle2012 (also in 8a1ef12f7e6d). The reduced
example is attached.

This exception is thrown by the simproc natless_cancel_sums (in Nat_Arith.nat_cancel_sums), as the following succeeds:

  ML_prf {* Delsimprocs [nth Nat_Arith.nat_cancel_sums 1] *}
  have "(\<And>ys zs. length ys < Suc (length zs + length ys))" by simp
  hence True
    by simp

The other simprocs in Nat_Arith also seem to be affected.

  -- Lars

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