[isabelle] Product_Type.split_beta fails



Hi all,

I'm getting exceptions from the split_beta simproc which propagate to
the "user-level" (Isabelle 2013). Here's a minimal example:

lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))"
  using [[simp_depth_limit=0]]
  apply(simp)

This results in:
*** Proof failed.
*** (case :000 of (x, y) \<Rightarrow> c) = c
***  1. (case :000 of (x, y) \<Rightarrow> c) = c
*** The error(s) above occurred for the goal statement:
*** (case :000 of (x, y) \<Rightarrow> c) = c

Setting the depth limit to 2 or higher makes the error go away. Glancing
at the simproc, it seems that its local function "meta_eq" assumes that
rewriting with just "cond_split_eta" will work, but this fails at low
simp depths.

Cheers,
Ognjen




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