Re: [isabelle] inductive_set and ordinal induction



Dear Stefan,

You are right in that the rules generated by the inductive package suffice for proving. However, sometimes it is easier to prove some statement using a higher-level reasoning principle than with the point-wise rules for inductive predicates. Thus, there may be cases where it is easier to derive a property from the internal construction than from what is exposed. 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. In principle, such rules could be derived from the induction rule provided, but I would have to do the derivation for each function. By using the internal derivation, I can do the derivation once and just instantiate the appropriate lemma. Of course, I know that I have to change my proofs when partial_function changes, but as I am using the internal definition only in a principled way, the required adaptations should also be canonical.

Something similar can also be useful for the inductive package, as this request shows.

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.

Best,
Andreas


On 27/10/15 09:37, Stefan Berghofer wrote:
On 10/26/2015 06:15 PM, Andreas Lochbihler wrote:
No, I'd be glad if it was made available. Probably nobody ever invested the time to
adapt the code base.

Andreas

On 26/10/15 18:06, Tobias Nipkow wrote:
Bummer! Is there any reason not to make the monotonicity theorem availble in user space?
If not...

Tobias

Hi all,

monotonicity and similar theorems are not made available to the user because this would
expose
the inner workings of the inductive definition package, which can change without prior
notice.
For a more detailed discussion of this problem, see e.g. this thread:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-May/msg00079.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-June/msg00013.html

Greetings,
Stefan




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