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