*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] inductive_set and ordinal induction*From*: Christoph Dittmann <f-isabellelist at yozora.eu>*Date*: Thu, 15 Oct 2015 11:35:41 +0200

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

theory lfp imports Main begin locale L = fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> bool" begin inductive_set X where X_intro: "\<lbrakk> \<And>b. f a b \<Longrightarrow> b \<in> X \<rbrakk> \<Longrightarrow> a \<in> X" definition X_step where [simp]: "X_step S \<equiv> S \<union> {a. \<forall>b. f a b \<longrightarrow> b \<in> S}" definition X_lfp where "X_lfp \<equiv> lfp X_step" lemma X_step_mono: "mono X_step" by (rule monoI) auto lemma X_lfp_equiv: "X = X_lfp" proof show "X \<subseteq> X_lfp" proof fix x assume "x \<in> X" thus "x \<in> X_lfp" proof (induct) case (X_intro a) have "a \<in> X_step X_lfp" unfolding X_step_def using X_intro(2) by auto thus ?case unfolding X_lfp_def using X_step_mono lfp_unfold by blast qed qed show "X_lfp \<subseteq> X" unfolding X_lfp_def using X_step_mono by (rule lfp_ordinal_induct_set) (auto intro: X_intro Sup_le_iff) qed lemma X_lfp_induct: assumes step: "\<And>S. P S \<Longrightarrow> P (S \<union> {a. \<forall>b. f a b \<longrightarrow> b \<in> S})" and union: "\<And>M. \<forall>S \<in> M. P S \<Longrightarrow> P (\<Union>M)" shows "P X" proof (subst X_lfp_equiv, unfold X_lfp_def, rule lfp_ordinal_induct_set) show "\<And>S. P S \<Longrightarrow> P (X_step S)" using step by auto qed (insert X_step_mono union) end end

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

- Previous by Date: Re: [isabelle] Code generation for reverse sorting
- Next by Date: [isabelle] tracing automatic datatype theorems
- Previous by Thread: Re: [isabelle] sublocale problem
- 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