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