[isabelle] inductive_set and ordinal induction


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"

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?

theory lfp imports Main begin

locale L =
  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

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

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)



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