*To*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Subject*: Re: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 23 Apr 2008 12:26:48 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <480E1A5F.6050500@cse.unsw.edu.au>*References*: <480E1A5F.6050500@cse.unsw.edu.au>

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 willbe passed down to all the internal states, making all the lambdas inthat statement completely redundant. However I cannot make anygeneric rules 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 whaton earth is going on. Please find attached a simplified theory filebuilt on 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.

**Follow-Ups**:

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

- Previous by Date: Re: [isabelle] LNCS format and isatool
- Next by Date: Re: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method
- Previous by Thread: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method
- Next by Thread: Re: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method
- 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