Re: [isabelle] Definition in (and of) Isabelle/HOL
On Fri, 11 Apr 2014, Rob Arthan wrote:
Do you do anything to avoid the potential problem whereby two calls of
new_specification with the same predicate will result in provably equal
constants if you implement new_specification naively with Hilbert
choice. E.g., ?x.1 < x < 10 used to define c and d? This is addressed
in HOL Light along the following lines: it defines a function on the
natural numbers such that 1 < x(n) < 10 for all n, and then defines c =
x(42) and d = x(43), assuming that c is the 42nd constant that HOL Light
has been asked to define.
There is nothing like this in the 'specification' command of Isabelle/HOL,
but that add-on feature from 2004 got hardly ever used in practice. It
also fell behind a lot concerning general system infrastructure for
I have recently asked around the canonical question if 'specification'
should be be removed or renovated, and it came out a slight tendency
towards renovation (after removal of some of its obsolete sub-features).
Locales are indeed better in most situations to work in a context of
abstract term parameters with some logical premises in the local context.
Almost all specification mechanisms in Isabelle/HOL are now "localized",
i.e. work in such hypothetical situations of "fixes" and "assumes", so
that is a real practical benefit. The cost for it is increasingly complex
system infrastructure (outside the core logical framework).
This archive was generated by a fusion of
Pipermail (Mailman edition) and