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 there.


Rafal Kolanski.

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])

Larry Paulson

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) (h,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 MHonArc.