Email Gateway (Aug 18 2022 at 11:46): Email Gateway (Aug 18 2022 at 11:46):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Dear Isabelle Wizards,
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.
Sincerely,
Rafal Kolanski.
Temp.thy
Email Gateway (Aug 18 2022 at 11:46):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 18 2022 at 11:47):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Hi,
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.
Sincerely,
Rafal Kolanski.
Lawrence Paulson wrote:
Last updated: May 03 2024 at 08:18 UTC