Re: [isabelle] inductive_set and ordinal induction
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
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.
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.
On 26/10/15 18:06, Tobias Nipkow wrote:
Bummer! Is there any reason not to make the monotonicity theorem availble in user space?
monotonicity and similar theorems are not made available to the user because this would
the inner workings of the inductive definition package, which can change without prior
For a more detailed discussion of this problem, see e.g. this thread:
This archive was generated by a fusion of
Pipermail (Mailman edition) and