*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] inductive_set and ordinal induction*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Tue, 27 Oct 2015 14:26:23 +0100*In-reply-to*: <562F6C19.1000101@inf.ethz.ch>*Organization*: TU München*References*: <561F736D.9070902@yozora.eu> <562E25F4.2070509@yozora.eu> <562E580C.3020305@in.tum.de> <562E5B48.5070703@inf.ethz.ch> <562E5D96.9010402@in.tum.de> <562E5FCD.4040802@inf.ethz.ch> <562F37C2.5000308@in.tum.de> <562F3C4D.3070109@inf.ethz.ch> <562F4B63.4080402@yozora.eu> <562F6C19.1000101@inf.ethz.ch>

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 > > > > >

**Follow-Ups**:**Re: [isabelle] inductive_set and ordinal induction***From:*Christoph Dittmann

**References**:**[isabelle] inductive_set and ordinal induction***From:*Christoph Dittmann

**Re: [isabelle] inductive_set and ordinal induction***From:*Christoph Dittmann

**Re: [isabelle] inductive_set and ordinal induction***From:*Tobias Nipkow

**Re: [isabelle] inductive_set and ordinal induction***From:*Andreas Lochbihler

**Re: [isabelle] inductive_set and ordinal induction***From:*Tobias Nipkow

**Re: [isabelle] inductive_set and ordinal induction***From:*Andreas Lochbihler

**Re: [isabelle] inductive_set and ordinal induction***From:*Stefan Berghofer

**Re: [isabelle] inductive_set and ordinal induction***From:*Andreas Lochbihler

**Re: [isabelle] inductive_set and ordinal induction***From:*Christoph Dittmann

**Re: [isabelle] inductive_set and ordinal induction***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Common monadic programming idioms and termination
- Next by Date: Re: [isabelle] Bool cpo
- Previous by Thread: Re: [isabelle] inductive_set and ordinal induction
- Next by Thread: Re: [isabelle] inductive_set and ordinal induction
- Cl-isabelle-users October 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list