*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Wed, 23 Apr 2008 21:48:49 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <D581C5B5-1579-4B3F-8B73-44D59FEE298B@cam.ac.uk>*References*: <480E1A5F.6050500@cse.unsw.edu.au> <D581C5B5-1579-4B3F-8B73-44D59FEE298B@cam.ac.uk>*User-agent*: Thunderbird 2.0.0.12 (X11/20080227)

Hi,

Sincerely, Rafal Kolanski. Lawrence Paulson wrote:

It looks like that is indeed a bug. Meanwhile, the following ugly hackwill let you substitute in an assumption until the bug can be fixed.apply (erule rev_mp) apply (rule sep_conj_pop_r_left [THEN ssubst]) Larry Paulson On 22 Apr 2008, at 18:03, Rafal Kolanski wrote:I have encountered what seemed to be a really simple concept in myproof. When I see this:((\<lambda>(h, r). (ass1 (v r) (p r)) (h, r)) &&& (\<lambda>(h, r). (ass2 (p r)) (h, r)) &&& P) (h, r)I know, that due to the implementation of &&&, the external r will bepassed down to all the internal states, making all the lambdas in thatstatement completely redundant. However I cannot make any genericrules such as:"((\<lambda>(h,r). (P r) (h,r)) &&& Q) = (\<lambda>(h,r). (P r &&& Q)(h,r))"and have them substitute. Worse yet, attempting to substitute theabove results in:*** exception TYPE raised: Variable "?Q" has two distinct types *** At command "apply"This really seemed a simple thing to do, and now I'm not sure what onearth is going on. Please find attached a simplified theory file builton WordMain which illustrates this problem, with commentary.I would love some advice on how to get that to work, even if itinvolves ugly ML code.

**References**:**[isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method***From:*Rafal Kolanski

**Re: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method
- Next by Date: [isabelle] Partial functions
- Previous by Thread: Re: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method
- Next by Thread: [isabelle] TPHOLs'2009 Host Selection
- Cl-isabelle-users April 2008 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