Re: [isabelle] inductive_set and ordinal induction



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.