[isabelle-dev] 'specification' and 'ax_specification'
andreas.lochbihler at inf.ethz.ch
Fri Mar 14 15:10:29 CET 2014
I myself found specification quite convenient and use it occasionally, e.g., in
AFP/Containers/Set_Linorder and a number of my private developments. It's a useful
shortcut to a definition with SOME and deriving the properties later with someI. It would
be good if it works with contexts. I have never used ax_specification, though.
On 14/03/14 14:44, Makarius wrote:
> 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
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev