Re: [isabelle] inductive_set and ordinal induction



On Tue, 27 Oct 2015, Andreas Lochbihler wrote:

Most of the other Isabelle packages I know follow the same principle: the internal constructions are accessible, but normally not used. If anyone uses the internal constructions, it is obvious that the proofs will break if the implementation is changed.

For comparison, partial_function also exposes the internal definition and the monotonicity theorem and I actually use this frequently to derive better induction rules for my functions.

From what I saw in the Isabelle repository, this distinction between official and internal theorems might be more explicit in the next release. The internal theorems are only made available if a specific attribute is set at definition time. Something similar could also be done for inductive.

A few notes on these questions about internal construction vs. external results (or "interface") of derived definitional packages.

* Historically, constant definitions were always visible in the fact
  namespace.  A bit later, we introduced the "concealed" flag, as formal
  means to say that the accidental presence of such facts is better
  ignored (especially by tools like find_theorems of sledgehammer).  Only
  recently (i.e. some years ago) the namespaces for definitional axioms
  and facts (stored theorems) were clearly separated.  Thus it became
  possible to make formal definitions relatively hard to access by
  user-space tools.  (The 'private' modifier from Isabelle2015 has a
  similar effect.)

* Some weeks ago, I tried to make a few definitional packages more serious
  in this respect, by using an empty binding for the facts of the internal
  definitions.  Thus a few cases were exposed, where applications were
  actually using this, despite the original intentions.  So I added
  another configuration option to re-enable the lost definitional fact.

* I have now done the same for 'inductive', 'coinductive' etc. treating
  the "mono" rule like the internal definition.  This exposed surprisingly
  many cases where the definition was used in applications.  So the
  question, whether the "mono" rule is morally public or not is futile.


In conclusion, this is the relevant NEWS entry from Isabelle/ca53150406c9, which is meant for the coming release:

  * Inductive definitions ('inductive', 'coinductive', etc.) expose
  low-level facts of the internal construction only if the option
  "inductive_defs" is enabled. This refers to the internal predicate
  definition and its monotonicity result. Rare INCOMPATIBILITY.

  * Recursive function definitions ('fun', 'function', 'partial_function')
  expose low-level facts of the internal construction only if the option
  "function_defs" is enabled. Rare INCOMPATIBILITY.

This means the new situation is both more restrictive and more permissive.


There was also a discussion about the "stability of interfaces" in Isabelle. It does not really exist. Everything may change at some point. Of course, we don't change things at will, according to current weather conditions. But we are still moving conceptually forward to a hopefully better system.

A recent example for that is the upheaval of the 'datatype' package after many years.


	Makarius




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