*To*: Ognjen Maric <ognjen.maric at gmail.com>*Subject*: Re: [isabelle] Product_Type.split_beta fails*From*: Makarius <makarius at sketis.net>*Date*: Mon, 10 Feb 2014 13:28:58 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <52716B5A.5010604@gmail.com>*References*: <52716B5A.5010604@gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 30 Oct 2013, Ognjen Maric wrote:

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) = cSetting the depth limit to 2 or higher makes the error go away. Glancingat the simproc, it seems that its local function "meta_eq" assumes thatrewriting with just "cond_split_eta" will work, but this fails at lowsimp depths.

Thanks for working out a well-defined example for this incident.

Makarius

- Previous by Date: [isabelle] Show types of constants?
- Next by Date: [isabelle] type variable and locales extension
- Previous by Thread: [isabelle] Show types of constants?
- Next by Thread: [isabelle] type variable and locales extension
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list