Re: [isabelle] inductive_set and ordinal induction



As far as I understood Stefan, the _def theorems are actually internal.

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.