theory week05A_demo_withproofs
imports Main
begin

inductive Ev :: "nat \<Rightarrow> bool"
where
ZeroI: "Ev 0" |
Add2I: "Ev n \<Longrightarrow> Ev (Suc(Suc n))"

print_theorems

\<comment> \<open>----------------------------------------------\<close>

section "Formalising Least Fixpoints"


definition
  closed :: "('a set \<Rightarrow> 'a set) \<Rightarrow> 'a set \<Rightarrow> bool"
where
  "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

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

text \<open>lfpt is the greatest lower bound:\<close>

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 \<open>Fix Point\<close>

lemma lfpt_fixpoint1:
  "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 lfpt_fixpoint2:
  "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 lfpt_fixpoint1)
  done

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

text \<open>lfpt is the least fix point\<close>

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 \<open>Rule Induction\<close>

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

definition
  R_hat :: "'a set \<Rightarrow> 'a set" where
  "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