Re: [isabelle] inductive_set and ordinal induction
- To: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, Christoph Dittmann <f-isabellelist at yozora.eu>
- Subject: Re: [isabelle] inductive_set and ordinal induction
- From: Makarius <makarius at sketis.net>
- Date: Sun, 15 Nov 2015 20:30:27 +0100 (CET)
- Cc: Isabelle Users <isabelle-users at cl.cam.ac.uk>, Stefan Berghofer <berghofe at in.tum.de>
- In-reply-to: <562F3C4D.firstname.lastname@example.org>
- References: <561F736D.email@example.com> <562E25F4.firstname.lastname@example.org> <562E580C.email@example.com> <562E5B48.firstname.lastname@example.org> <562E5D96.email@example.com> <562E5FCD.firstname.lastname@example.org> <562F37C2.email@example.com> <562F3C4D.firstname.lastname@example.org>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
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
* 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
A recent example for that is the upheaval of the 'datatype' package after
This archive was generated by a fusion of
Pipermail (Mailman edition) and