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

[Johannes Hölzl]

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
need ax_specification.

So my preference is option (b).

 - Johannes

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.
> 
> 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-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
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev