[isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Clemens Ballarin]

On 30 October, 2015 20:02 CET, Makarius <makarius at sketis.net> wrote: 
 
> Standard batch build prints relatively few terms, so this is not yet
> significant as a test.
> 
> The following change prints every intermediate Isar toplevel state.  With 
> that I get timeouts or interrupts due to out-of-memory situation in
> various sessions, e.g. HOL-Nominal-Examples or Jinja.

Unfortunately this already fails without my patch, so it cannot be used as a test.

I'm not familiar with the termination argument for abbreviations, but certainly we can say that abbreviations define a reduction system (in fact a rewrite system), and I would assume that there are no cycles and infinite paths.  Now my patch will clone part of this system, introducing additional nodes and transitions, but I don't see how it would introduce cycles if there were no cycles without it.  It could introduce infinite chains, but only for infinite chains of interpretations.  The latter are not allowed by the roundup algorithm.  Am I missing something?

Clemens