Email Gateway (Aug 23 2022 at 09:12): Email Gateway (Aug 23 2022 at 09:12):From: Dominique Unruh <unruh@ut.ee>
Hi,
I played around a bit, and while I don't understand the reason for the
problem, I managed to come up with a much smaller example that
illustrates the same(?) problem:
lemma "∀x::int. (length [y] = length [y])" for y :: int
apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps)
Note that when the allquantifier is remove, or when one of the y's is
replaced by 0, reification works. So the problem seems to be some subtle
interaction between the allquantifier and the fact that y occurs twice.
Best wishes,
Dominique.
Last updated: Nov 21 2024 at 12:39 UTC