*To*: Tobias Nipkow <nipkow at in.tum.de>, Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] inductive_set and ordinal induction*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 26 Oct 2015 17:56:40 +0100*In-reply-to*: <562E580C.3020305@in.tum.de>*References*: <561F736D.9070902@yozora.eu> <562E25F4.2070509@yozora.eu> <562E580C.3020305@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Andreas On 26/10/15 17:42, Tobias Nipkow wrote:

Hopefully one can get access to the monotonicity theorem proved internally in the cause of an inductive definition. But I don't know how. It is not called X_mono or X.mono. In the worst case it is hidden... Tobias On 26/10/2015 14:09, Christoph Dittmann wrote:Hi, after investigating a little, I learned that inductive_set builds on inductive. The same question applies to inductive: For an inductive predicate X, can I somehow get an induction schema like "[| ... |] ==> P X" as opposed to "[| X x; ... |] ==> P x" ? If there is no way to get this automatically, is there maybe a way to access the monotonicity rule of an inductive predicate, so that I can apply lfp_ordinal_induct? Christoph On 10/15/2015 11:35 AM, Christoph Dittmann wrote:Hi, I would like to use lfp_ordinal_induct_set with inductive_set. When I define: inductive_set X where "â âb. f a b â b â X â â a â X" I get an induction theorem X.induct for free. However, X.induct talks about elements, not sets. The following induction schema based on least fixed points also works: lemma X_lfp_induct: assumes step: "âS. P S â P (S â {a. âb. f a b â b â S})" and union: "âM. âS â M. P S â P (âM)" shows "P X" oops I managed to prove X_lfp_induct (see attachment) by redefining X manually via the lfp function and then showing that this definition is equivalent to the inductive_set. Then X_lfp_induct follows from lfp_ordinal_induct_set from ~~/src/HOL/Inductive.thy. For this I needed to prove things like monotonicity, which I assume inductive_set already proves internally. So my approach seems a little redundant and I think there could be a better way. Is there an easier way to get a least fixed point induction schema like this for inductive_sets in general, maybe even fully automatic? Thanks, Christoph

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

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

- 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