*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.3070109@inf.ethz.ch>*References*: <561F736D.9070902@yozora.eu> <562E25F4.2070509@yozora.eu> <562E580C.3020305@in.tum.de> <562E5B48.5070703@inf.ethz.ch> <562E5D96.9010402@in.tum.de> <562E5FCD.4040802@inf.ethz.ch> <562F37C2.5000308@in.tum.de> <562F3C4D.3070109@inf.ethz.ch>*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. Ifanyone uses the internal constructions, it is obvious that the proofswill break if the implementation is changed.

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

From what I saw in the Isabelle repository, this distinction betweenofficial and internal theorems might be more explicit in the nextrelease. The internal theorems are only made available if a specificattribute is set at definition time. Something similar could also bedone for inductive.

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

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

Makarius

- Previous by Date: Re: [isabelle] Interpretation problems of locales with datatype declarations
- Next by Date: Re: [isabelle] Running Isabelle in batch mode
- Previous by Thread: Re: [isabelle] Juxtaposed cartouche error in session run; okay in PIDE
- Next by Thread: Re: [isabelle] Running Isabelle in batch mode
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list