Re: [isabelle] inductive_set and ordinal induction



Dear Christoph,

the prove using lfp_ordinal_induct is quite different, the inductive
package does not produce it for you.

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. 

 - Johannes

Am Dienstag, den 27.10.2015, 13:20 +0100 schrieb Andreas Lochbihler:
> Dear Christoph,
> 
> The general answer first:
> The rules generated by the inductive package suffice to prove that the predicate equals 
> the internal construction. Thus, you can prove the same as you can prove with access the 
> internal construction. However, this proof of equivalence can be quite tedious (which is 
> why I support making the internal construction accessible).
> 
> In the specific case of lfp_ordinal_induct, you just have to look at its proof. It uses 
> three properties of lfp and f:
> 1. Monotonicity of f: You have to prove this yourself manually, but this is doable.
> 2. lfp_unfold: This corresponds to X.simps[abs_def]
> 3. lfp_lowerbound: This corresponds to X.induct
> 
> Hope this helps,
> Andreas
> 
> On 27/10/15 11:01, Christoph Dittmann wrote:
> > On 10/27/2015 09:56 AM, Andreas Lochbihler wrote:
> >> You are right in that the rules generated by the inductive package
> >> suffice for proving.
> >
> > I don't see how ordinal induction (like lfp_ordinal_induct)
> >    "[| ... |] ==> P X"
> > is derivable from the pointwise induction rule
> >    "[| X x; ... |] ==> P x"
> > provided by the inductive package.
> >
> > Or is it derivable?
> >
> > Best,
> > Christoph
> >
> >
> 






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