[isabelle-dev] Speed of @{thm}

[Makarius]

On Fri, 10 Aug 2012, Jasmin Blanchette wrote:

> It's 20 times faster (!).
>
> This is mind-boggling. Looking at the code (correct me someone if I'm 
> wrong), it appears that @{thm} generate a variable that's bound in the 
> background and stores the looked up theorem. One would think this 
> ensures the lookup takes place only once, at compile time, even if 
> @{thm} occurs in a tight loop. But despite taking no special 
> precautions, @{fasthm} also has this property; the following is 
> lightning fast:
>
>   fun f n = @{fasthm "nibble.simps(1)"};
>   map f (1 upto 10000);
>
> The hg history did not reveal any insights into why theorems are handled 
> differently from (less efficiently than) @{term}, @{typ}, etc. Any idea?

The concepts are declared in the PLMMS 2007 paper by Wenzel/Chaieb.  The 
first public implementation was in Isabelle2007, which is not so immediate 
to find: 
http://isabelle.in.tum.de/repos/isabelle/annotate/Isabelle2007/src/Pure/ML/ml_context.ML#l230

That old version still had syntactic name lookup, not the abstract value 
business of the Isabelle2008 version.  Note that @{thm} is conceptually an 
abstract value, with externally available names for it being just an 
accident.  You don't have one for @{lemma}, for example.  BTW, @{term} and 
@{typ} are the main exceptions in LCF that have fully concrete syntax.


30ms for the conjuring trick with fully abstract @{thm} is odd, it should 
not happen.  Can you spend some time to figure out the time hole?

The antiquotation mechanism has been refined so many times, and acquired 
so many features, such that it should be able to produce ML source also 
for thousands of abstract theorems, not just tens or hundreds as until 
now.


 	Makarius