*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] inductive_set and ordinal induction*From*: Christoph Dittmann <f-isabellelist at yozora.eu>*Date*: Mon, 26 Oct 2015 14:09:08 +0100*In-reply-to*: <561F736D.9070902@yozora.eu>*References*: <561F736D.9070902@yozora.eu>

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

- Previous by Date: Re: [isabelle] Locales: Interpretation changes behaviour of locale expression
- Next by Date: Re: [isabelle] inductive_set and ordinal induction
- Previous by Thread: [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