Email Gateway (Aug 22 2022 at 14:02): Email Gateway (Aug 22 2022 at 14:02):From: Giuliano Losa <giuliano@losa.fr>
Hello,
in the following theory, the processing of the definition of x2 takes
minutes on my machine.
theory Test
imports Main
begin
abbreviation x1 where "x1 f ≡ f"
definition x2 where "x2 ≡ x"
end
If I remove the abbreviation, it becomes instantaneous.
I came across this problem because I made the following abbreviation:
abbreviation flip where "flip f ≡ λ x y . f y x"
It rendered Isabelle unusable, as the processing of some commands (not
only definition, but also other commands) started to take minutes.
I fixed the problem by using a definition instead of an abbreviation,
but there might be something worth investigating going on here.
I observed this behavior using Isabelle-2016 and Isabelle_15-Aug-2016.
Giuliano
signature.asc
Email Gateway (Aug 22 2022 at 14:02):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hello Giuliano.
The problem, of course, is that abbreviations are unfolded for term
parsing and folded for term printing. Unfolding these simple
abbreviations is no problem. But abbreviations as general as these could
be folded anywhere, making it impossible to print.
I think you might want to try abbreviation(input) rather than
abbreviation. You can define any of these abbreviations safely for input.
That will allow you to type "flip" wherever you like, but it will
disappear in output.
In general, I find abbreviation(input) a very useful mechanism, and I
use it by default rather than abbreviation.
Cheers,
Thomas.
Last updated: Apr 26 2024 at 01:06 UTC