*To*: Christoph Dittmann <f-isabellelist at yozora.eu>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] inductive_set and ordinal induction*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 27 Oct 2015 13:20:41 +0100*In-reply-to*: <562F4B63.4080402@yozora.eu>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Dear Christoph, The general answer first:

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:*Johannes Hölzl

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

- Previous by Date: Re: [isabelle] Common monadic programming idioms and termination
- Next by Date: Re: [isabelle] Common monadic programming idioms and termination
- 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