Re: [isabelle] inductive_set and ordinal induction



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

Tobias

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.

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






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



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