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

[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