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.
Andreas
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
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
