[isabelle-dev] 'specification' and 'ax_specification'
hoelzl at in.tum.de
Fri Mar 14 15:37:42 CET 2014
Yes, the same here. I would like to use specification sometimes, but
without supporting contexts it not as helpful as it could. I also do not
So my preference is option (b).
Am Freitag, den 14.03.2014, 15:10 +0100 schrieb Andreas Lochbihler:
> 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
> > 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-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev