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 Isabelle specifications.

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).


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.