*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] inductive_set and ordinal induction*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 27 Oct 2015 16:33:02 +0100*In-reply-to*: <1445958984.2334.181.camel@in.tum.de>*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> <562F4B63.4080402@yozora.eu> <562F6C19.1000101@inf.ethz.ch> <1445952383.2334.171.camel@in.tum.de> <562F88C1.5010208@yozora.eu> <1445958984.2334.181.camel@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

On 27/10/2015 16:16, Johannes HÃlzl wrote:

As far as I understood Stefan, the _def theorems are actually internal. I think you should be on the save side with your last suggestion, i.e. defining the functional F_def and then prove: inductive X ... definition F where "F = ..." lemma "X = lfp F" unfolding X_def F_def by simp Then you should be on the save side if we change the internals of the inductive package.

Tobias

- Johannes Am Dienstag, den 27.10.2015, 15:22 +0100 schrieb Christoph Dittmann:Dear Johannes, thank you, and also Andreas for your answers. On 10/27/2015 02:26 PM, Johannes HÃlzl wrote:As Andreas points out, you can directly use the definition of the predicate (<inductive pred>_def) and then manually prove monotonicity. Then you can apply lfp_ordinal_induct.<inductive_pred>_def is "<inductive_pred> == lfp <something_very_long>". Can I somehow bind <something_very_long> to a name so that I do not need to copy&paste it? I tried pattern matching like note X_def (is "_ == lfp ?f") but this doesn't work (the isar manual agrees). Is <inductive_pred>_def considered part of the stable interface to the inductive package? If not, maybe my approach of redefining the inductive predicate explicitly via lfp and proving equality could be more robust against changes in the inductive package? Best, Christoph

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] inductive_set and ordinal induction***From:*Johannes Hölzl

**References**:**[isabelle] inductive_set and ordinal induction***From:*Christoph Dittmann

**Re: [isabelle] inductive_set and ordinal induction***From:*Christoph Dittmann

**Re: [isabelle] inductive_set and ordinal induction***From:*Tobias Nipkow

**Re: [isabelle] inductive_set and ordinal induction***From:*Andreas Lochbihler

**Re: [isabelle] inductive_set and ordinal induction***From:*Tobias Nipkow

**Re: [isabelle] inductive_set and ordinal induction***From:*Andreas Lochbihler

**Re: [isabelle] inductive_set and ordinal induction***From:*Stefan Berghofer

**Re: [isabelle] inductive_set and ordinal induction***From:*Andreas Lochbihler

**Re: [isabelle] inductive_set and ordinal induction***From:*Christoph Dittmann

**Re: [isabelle] inductive_set and ordinal induction***From:*Andreas Lochbihler

**Re: [isabelle] inductive_set and ordinal induction***From:*Johannes Hölzl

**Re: [isabelle] inductive_set and ordinal induction***From:*Christoph Dittmann

**Re: [isabelle] inductive_set and ordinal induction***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] inductive_set and ordinal induction
- Next by Date: Re: [isabelle] inductive_set and ordinal induction
- Previous by Thread: Re: [isabelle] inductive_set and ordinal induction
- Next by Thread: Re: [isabelle] inductive_set and ordinal induction
- Cl-isabelle-users October 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