Re: [isabelle] Abbreviation makes Isabelle/HOL very slow



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.

On 24/08/16 00:00, Giuliano Losa wrote:
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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.