[isabelle-dev] Circular reasoning via multithreading seems too easy

[Makarius]

On 03/12/16 14:57, Peter Lammich wrote:
> 
> the attached theory is accepted by all Isabelle's from 2015 to the
> latest 2016-1-RC4, without any complaints, even in batch mode 
> (isabelle build). 
> It just uses a prove_future, and proves the theorem with itself!

Here is the main result of investigating the sources and their entangled
history:

changeset:   64570:1134e4d5e5b7
user:        wenzelm
date:        Fri Dec 16 19:07:16 2016 +0100
files:       src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
src/HOL/SPARK/Tools/spark_vcs.ML src/Pure/Thy/thy_info.ML
src/Pure/more_thm.ML src/Pure/proofterm.ML src/Pure/thm.ML
description:
consolidate nested thms with persistent result, for improved performance;
always consolidate parts of fulfill_norm_proof: important to exhibit
cyclic thms (via non-termination as officially published), but this was
lost in f33d5a00c25d;


There was actually a second drop-out of formerly working behaviour (see
a2e7862e7dd5), but the changeset 1134e4d5e5b7 subsumes both, because the
consolidation of type thm/theory is now done a bit differently.

General concepts behind all that are described in section 3.2 in my
paper at ITP 2013, see especially the last two paragraphs.



Dropouts of this category belong to the normal routine in Isabelle,
according to its design principles in the last 10 years -- when we moved
from a research experiment towards a serious system. System reliability
has already reached a stage where most users never see it break down, so
any sense of what can go wrong is lost.

Hopefully this synthetic example helps to return to a better
understanding of what Isabelle really is: an increasing approximation of
ultimate perfection.

Whenever we reach that, the system will be discarded :-)


	Makarius