Email Gateway (Aug 19 2022 at 17:20): Email Gateway (Aug 19 2022 at 17:20):From: Tobias Nipkow <nipkow@in.tum.de>
Thank you for that bug-report. It lookes like the simplifier expected a certain
invariant to hold which doesn't. I have just pushed a modification that no
longer makes that assumption. It surprises me that this situation hadn't arisen
before.
Thanks!
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 09:02):From: Ognjen Maric <ognjen.maric@gmail.com>
Hi,
in the following example, the simplifier raises a Bind exception.
lemma
"{(s1, s2). s2 = (if z then undefined else s1)} `` { x } = S"
apply(simp)
oops
The check_conv function fails and complains about proving the wrong
goal, but I do not really understand what the error is. Moreover, if I
explicitly add an:
apply(subst Image_Collect_split)
before applying the simp tactic, the error goes away - even though this
rule is already in the simpset and simp applies it before throwing the
exception, and both variants seem to yield the same pair of a term and a
rewrite rule.
Ognjen
Last updated: Apr 23 2024 at 16:19 UTC