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"

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





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



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