*To*: Tobias Nipkow <nipkow at in.tum.de>, Isabelle Users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] inductive_set and ordinal induction*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 26 Oct 2015 18:15:57 +0100*In-reply-to*: <562E5D96.9010402@in.tum.de>*References*: <561F736D.9070902@yozora.eu> <562E25F4.2070509@yozora.eu> <562E580C.3020305@in.tum.de> <562E5B48.5070703@inf.ethz.ch> <562E5D96.9010402@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Andreas On 26/10/15 18:06, Tobias Nipkow wrote:

Bummer! Is there any reason not to make the monotonicity theorem availble in user space? If not... Tobias On 26/10/2015 17:56, Andreas Lochbihler wrote:Indeed, inductive does not bind the monotonicity theorem to a theorem name and so the monotonicity theorem is not accessible from user space. Moreover, the monotonicity prover is not exported in the ML interface either, so you cannot even state the monotonicity theorem yourself and have the monotonicity prover solve the goal once more. Andreas On 26/10/15 17:42, Tobias Nipkow wrote:Hopefully one can get access to the monotonicity theorem proved internally in the cause of an inductive definition. But I don't know how. It is not called X_mono or X.mono. In the worst case it is hidden... Tobias On 26/10/2015 14:09, Christoph Dittmann wrote:Hi, after investigating a little, I learned that inductive_set builds on inductive. The same question applies to inductive: For an inductive predicate X, can I somehow get an induction schema like "[| ... |] ==> P X" as opposed to "[| X x; ... |] ==> P x" ? If there is no way to get this automatically, is there maybe a way to access the monotonicity rule of an inductive predicate, so that I can apply lfp_ordinal_induct? Christoph On 10/15/2015 11:35 AM, Christoph Dittmann wrote:Hi, I would like to use lfp_ordinal_induct_set with inductive_set. When I define: inductive_set X where "â âb. f a b â b â X â â a â X" I get an induction theorem X.induct for free. However, X.induct talks about elements, not sets. The following induction schema based on least fixed points also works: lemma X_lfp_induct: assumes step: "âS. P S â P (S â {a. âb. f a b â b â S})" and union: "âM. âS â M. P S â P (âM)" shows "P X" oops I managed to prove X_lfp_induct (see attachment) by redefining X manually via the lfp function and then showing that this definition is equivalent to the inductive_set. Then X_lfp_induct follows from lfp_ordinal_induct_set from ~~/src/HOL/Inductive.thy. For this I needed to prove things like monotonicity, which I assume inductive_set already proves internally. So my approach seems a little redundant and I think there could be a better way. Is there an easier way to get a least fixed point induction schema like this for inductive_sets in general, maybe even fully automatic? Thanks, Christoph

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

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

- Previous by Date: Re: [isabelle] inductive_set and ordinal induction
- Next by Date: [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