Re: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method
It looks like that is indeed a bug. Meanwhile, the following ugly hack
will 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])
On 22 Apr 2008, at 18:03, Rafal Kolanski wrote:
I have encountered what seemed to be a really simple concept in my
proof. 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
be passed down to all the internal states, making all the lambdas in
that statement completely redundant. However I cannot make any
generic rules such as:
"((\<lambda>(h,r). (P r) (h,r)) &&& Q) = (\<lambda>(h,r). (P r &&&
and have them substitute. Worse yet, attempting to substitute the
above 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
on earth is going on. Please find attached a simplified theory file
built on WordMain which illustrates this problem, with commentary.
I would love some advice on how to get that to work, even if it
involves ugly ML code.
This archive was generated by a fusion of
Pipermail (Mailman edition) and