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.

Best,
Christoph




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