[isabelle-dev] blast flexflex pairs

[Makarius]

This is the continuation / conclusion of the pending thread about flexflex 
pairs in blast, see also 
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-December/msg00085.html

In Isabelle/b45b1b217f43 from 01-Jan-2014 the smashing of flexflex pairs 
is already removed, just like for any other proof tools.  The general idea 
is that global goal information like maxidx and flexflex pairs (called 
tpairs internally) accumulates monotonically, without any premature 
censorship by proof tools.  Instead the cleanup is deferred to certain 
checkpoints of the system infrastructure, e.g. the goal wrappers 
Goal.prove or goals in Isar proof text.


Here is also an exhaustive list of places where flexflex pairs accumulate 
in practice due to "blast" (or indirectly via "auto"):

Isabelle/9a52ee8cae9b
AFP/4fbb736e4e28

(line 99 of "~~/src/HOL/Cardinals/Wellorder_Embedding.thy")
(line 406 of "~~/src/HOL/Library/Ramsey.thy")
(line 408 of "~~/src/HOL/Library/Ramsey.thy")
(line 318 of "$AFP/Markov_Models/ex/PCTL.thy")
(line 1162 of "$AFP/Nat-Interval-Logic/IL_TemporalOperators.thy")
(line 376 of "$AFP/Stuttering_Equivalence/PLTL.thy")
(line 384 of "$AFP/Stuttering_Equivalence/PLTL.thy")
(line 534 of "$AFP/Stuttering_Equivalence/PLTL.thy")

These incidents are rather unexciting.  I have occasionally seen other 
proof tools like "fast" produce spurious flexflex pairs as well, without 
doing any immediate harm.


I was about to push b45b1b217f43 already last year, but it was delayed by 
mysterious total failure of existence of the test environment for 
JinjaThreads.  It is still unclear what actually happened.  It might have 
been just due to extra tracing messages emitted in the test, which are 
occasionally deadly as we know already.  JinjaThread has always defined 
the edge of what is possible at all, and thus might occasionally fall off 
that edge.

So for my part, this thread can be closed now.


 	Makarius