theory Exercise8 imports Main begin

constdefs
  closed :: "('a set \<Rightarrow> 'a set) \<Rightarrow> 'a set \<Rightarrow> bool"
  "closed f B \<equiv> f B \<subseteq> B"

lemma closed_int:
  "\<lbrakk> mono f; closed f A; closed f B \<rbrakk> \<Longrightarrow> closed f (A \<inter> B)"
  apply (unfold closed_def mono_def)
  apply blast
  done

constdefs
  lfpt :: "('a set \<Rightarrow> 'a set) \<Rightarrow> 'a set"
  "lfpt f \<equiv> \<Inter> {B. closed f B}"

text {* lfpt is the greatest lower bound: *}

lemma lfpt_lower: "closed f B \<Longrightarrow> lfpt f \<subseteq> B"
  apply (unfold lfpt_def)
  apply blast
  done

lemma lfpt_greatest:
  assumes A_smaller: "\<And>B. closed f B \<Longrightarrow> A \<subseteq> B"
  shows "A \<subseteq> lfpt f"
  apply (unfold lfpt_def)
  apply (insert A_smaller)
  apply blast
  done

section {* Fix Point *}

lemma 1:
  "mono f \<Longrightarrow> f (lfpt f) \<subseteq> lfpt f"
  apply (rule lfpt_greatest)
  apply (frule lfpt_lower) 
  apply (drule monoD, assumption)
  apply (simp add: closed_def)
  done
  
lemma 2:
  "mono f \<Longrightarrow> lfpt f \<subseteq> (f (lfpt f) :: 'a set)"
  apply (rule lfpt_lower)
  apply (unfold closed_def) 
  apply (rule monoD [where f=f], assumption)
  apply (erule 1)
  done

lemma lfpt_fixpoint:
  "mono f \<Longrightarrow> f (lfpt f) = lfpt f"
  by (blast intro!: 1 2)

text {* lfpt is the least fix point *}

lemma lfpt_least:
  assumes A: "f A = A"
  shows "lfpt f \<subseteq> A"
  apply (rule lfpt_lower)
  apply (unfold closed_def)
  apply (simp add: A) 
  done

section {* Rule Induction *}

consts R :: "('a set \<times> 'a) set"

constdefs
  R_hat :: "'a set \<Rightarrow> 'a set"
  "R_hat A \<equiv> {x. \<exists>H. (H,x) \<in> R \<and> H \<subseteq> A}"

lemma monoR': "mono R_hat"
  apply (unfold mono_def)
  apply (unfold R_hat_def)
  apply blast
  done

lemma sound:
  assumes hyp: "\<forall>(H,x) \<in> R. ((\<forall>h \<in> H. P h) \<longrightarrow> P x)" 
  shows "\<forall>x \<in> lfpt R_hat. P x"
proof -
  from hyp
  have "closed R_hat {x. P x}"
    unfolding closed_def R_hat_def by blast
  hence "lfpt R_hat \<subseteq> {x. P x}"
    by (rule lfpt_lower)
  thus ?thesis
    by blast
qed
  

end