Re: [isabelle] inductive_set and ordinal induction



Yes, it should be considered fixed, and I support Andreas' idea of
exporting the monotonicity theorem. 

 - Johannes

Am Dienstag, den 27.10.2015, 16:27 +0100 schrieb Tobias Nipkow:
> On 27/10/2015 16:16, Johannes HÃlzl wrote:
> > As far as I understood Stefan, the _def theorems are actually internal.
> 
> But it is exported, and hasn't changed over many years and I don't see any 
> impending change there either.
> 
> Tobias
> 
> > I think you should be on the save side with your last suggestion, i.e.
> > defining the functional F_def and then prove:
> >
> > inductive X ...
> >
> > definition F where
> >    "F = ..."
> >
> > lemma "X = lfp F"
> >    unfolding X_def F_def by simp
> >
> > Then you should be on the save side if we change the internals of the
> > inductive package.
> >
> >   - Johannes
> >
> > Am Dienstag, den 27.10.2015, 15:22 +0100 schrieb Christoph Dittmann:
> >> Dear Johannes,
> >>
> >> thank you, and also Andreas for your answers.
> >>
> >> On 10/27/2015 02:26 PM, Johannes HÃlzl wrote:
> >>> As Andreas points out, you can directly use the definition of the
> >>> predicate (<inductive pred>_def) and then manually prove monotonicity.
> >>> Then you can apply lfp_ordinal_induct.
> >>
> >> <inductive_pred>_def is "<inductive_pred> == lfp <something_very_long>".
> >> Can I somehow bind <something_very_long> to a name so that I do not need
> >> to copy&paste it?
> >>
> >> I tried pattern matching like
> >>    note X_def (is "_ == lfp ?f")
> >> but this doesn't work (the isar manual agrees).
> >>
> >> Is <inductive_pred>_def considered part of the stable interface to the
> >> inductive package?  If not, maybe my approach of redefining the
> >> inductive predicate explicitly via lfp and proving equality could be
> >> more robust against changes in the inductive package?
> >>
> >> Best,
> >> Christoph
> >>
> >
> >
> >
> 






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