Email Gateway (Oct 26 2023 at 20:12): Email Gateway (Oct 26 2023 at 20:12):From: "Wickerson, John P" <j.wickerson@imperial.ac.uk>
Hi,
If I type the following into Isabelle2023 ...
... then the proof goes through fine. But it's highly misleading -- it looks like I've proved {} ⊇ {1} as a subgoal.
I think what's happening is that the "..." is being bound to the right-hand side of the previous line _after_ the abbreviation "{1,2} ⊇ {}" has been expanded to "{} ⊆ {1,2}". In other words, "..." is standing for {1,2}, not {}.
This is very confusing for the user. Can it be fixed so that the "..." is always bound to the right-hand side of the previous line _before_ any abbreviations are expanded?
Thanks,
John
Email Gateway (Oct 27 2023 at 04:19):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
My preferred solution to this recurring issue is to advise the confused
user that they should stop using the relation "superset_eq" (or
"superset", "greater", ...) which, strictly speaking, does not exist.
Stepan
Email Gateway (Oct 27 2023 at 12:20):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,
it does not resolve the confusion for the unexpecting user, but the
following trick can be helpful once you know about the issue:
Instead of
have "x >= y"
write
have "x >= y" (is "_ >= ...")
This pattern match overrides the default binding of ... to become the
actual rhs.
Then you can use also/finally normally.
Best wishes,
Dominique.
Last updated: Apr 28 2024 at 20:16 UTC