[isabelle-dev] 'specification' and 'ax_specification'

[Makarius]

On Fri, 14 Mar 2014, Jasmin Blanchette wrote:

>>  * HOL/Tools/choice_specification.ML which is loaded into
>>    HOL/Hilbert_Choice.thy -- really old stuff that would require serious
>>    renovation if actually used: 'ax_specification' with its unchecked
>>    axiomatization is actually unsed, and 'specification' only by
>>    HOL-Auth (and its many clones).
>>
>>    A candidate for HOL-Library, after removing the axiomatic part?
>>    Nitpick seems to have special tricks to cope with it, though.
>
> These special tricks could be taken out. They're not vital in any way.

(This deserves its own mail thread.)

Motivated by the surprise about ``"code_pred" introduces axioms?'' from 
last October 
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-October/msg00228.html
I've checked the situation more systematically some weeks ago.

Spurious axiomatizations can lead to unpleasant surprises to users that 
are unaware of the danger.  We probably can't do anything about code_pred 
now, but check the general situations about further such trapdoors.


So how about 'ax_specification'?  It is an alternate personality of 
'specification' that would make it very hard to renovate the latter, if 
that is desirable at all: 'ax_specification' is unused and 'specification' 
only used in HOL-Auth and its derivatives, which appears to have been a 
demo for that.

There are various possibilities:

   (a) Do nothing and let this old stuff collect more dust.

   (b) Remove 'ax_specification' and brush-up 'specification' a little
       (proper local contexts, PIDE markup etc.).

   (c) Remove both 'ax_specification' and 'specification', and do the
       HOL-Auth applications with a hypothetical context, potentially
       with a proven interpretation of the assumptions.


 	Makarius