Re: [isabelle] inductive_set and ordinal induction



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.

Andreas

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

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









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