# Re: [isabelle] inductive_set and ordinal induction

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"

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

```
```

```
```

```

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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