Re: [isabelle] inductive_set and ordinal induction

On 10/27/2015 04:16 PM, Johannes HÃlzl wrote:
> 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.

I was thinking more of something like the proof of X_lfp_equiv I posted
in my original posting, without using X_def.

The only drawback is that I need to state the monotone function twice in
slightly different form, once for the inductive predicate and once again
to redefine it with lfp.


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