# Re: [isabelle] inductive_set and ordinal induction

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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.