theory Isar imports Sets begin

section{*A Taste of Structured Proofs in Isar*}

lemma [intro?]: "mono f \<Longrightarrow> x \<in> f (lfp f) \<Longrightarrow> x \<in> lfp f"

  by(simp only: lfp_unfold [symmetric])

lemma "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"

      (is "lfp ?F = ?toA")

proof

  show "lfp ?F \<subseteq> ?toA"

  by (blast intro!: lfp_lowerbound intro: rtrancl_trans)

next

  show "?toA \<subseteq> lfp ?F"

  proof

    fix s assume "s \<in> ?toA"

    then obtain t where stM: "(s,t) \<in> M\<^sup>*" and tA: "t \<in> A"

         by blast

    from stM show "s \<in> lfp ?F"

    proof (rule converse_rtrancl_induct)

      from tA have "t \<in> ?F (lfp ?F)" by blast

      with mono_ef show "t \<in> lfp ?F" ..

    next

      fix s s' assume "(s,s') \<in> M" and "(s',t) \<in> M\<^sup>*"

                  and "s' \<in> lfp ?F"

      then have "s \<in> ?F (lfp ?F)" by blast

      with mono_ef show "s \<in> lfp ?F" ..

    qed

  qed

qed

end