Re: [isabelle] Simplifying split lambda terms and (maybe) a bug in the "subst" method
Thanks for that. If/when the bug gets fixed, would I have the slightest
chance of using things like sep_conj_pop_r_left as a simp rule? Or am I
limited to subst or constructing my own tactic?
As for WordMain, I thought that was the main include of HOL-word? We
have our own expanded version of HOL-word, so I might've made a mistake
Lawrence Paulson wrote:
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 &&& Q)
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