Re: [isabelle] inductive_set and ordinal induction

Bummer! Is there any reason not to make the monotonicity theorem availble in user space? If not...


On 26/10/2015 17:56, Andreas Lochbihler wrote:
Indeed, inductive does not bind the monotonicity theorem to a theorem name and
so the monotonicity theorem is not accessible from user space. Moreover, the
monotonicity prover is not exported in the ML interface either, so you cannot
even state the monotonicity theorem yourself and have the monotonicity prover
solve the goal once more.


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


On 26/10/2015 14:09, Christoph Dittmann wrote:

after investigating a little, I learned that inductive_set builds on

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?


On 10/15/2015 11:35 AM, Christoph Dittmann wrote:

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"

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?


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

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