theory week05B_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


text \<open>Formalising applying a function multiple times\<close>

primrec appl :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a)" where
  "appl f 0 = id" |
  "appl f (Suc n) = f \<circ> (appl f n)"


text \<open>Any fixed point is not smaller than applying the function multiple 
        times to the smallest element\<close>
lemma appl_less_fp:
  assumes fp: "f d = d"
  assumes mo: "mono f"   
  shows "appl f n {} \<subseteq> d"
  proof(induct n)
  case 0 show ?case
    proof -
    have "{} \<subseteq> d" ..
    thus ?case by simp
  qed
  next
  case (Suc n) show ?case
    proof -
    have a: "appl f (Suc n) {} \<subseteq> f d"
      proof (simp)
      have h: "appl f n {} \<subseteq> d" by(rule Suc.hyps)
      from mo and h show "f (appl f n {}) \<subseteq> f d" by(rule monoD)
      qed
    moreover from fp have b: "f d \<subseteq> d" by(rule equalityD1)
    ultimately show ?case by(rule subset_trans)
    qed
  qed

lemma appl_subset:
  assumes m: "mono f"
  shows "appl f n {} \<subseteq> appl f (Suc n) {}"
  proof(induct n)
  case 0
  show ?case by simp
  next
  case (Suc n)
  show ?case
    proof -
    have "f (appl f n {}) \<subseteq> f (appl f (Suc n) {})"
      by (rule monoD[OF m Suc.hyps])
    thus ?case by simp
    qed
  qed

lemma UN_split:
   "(\<Union>i\<in>{0..Suc y}. P i) = ((\<Union>i\<in>{0..y}. P i) \<union> P (Suc y))"
  apply(auto simp: atLeastAtMostSuc_conv)
  done
   
lemma UN_appl:
  assumes m: "mono f"
  shows "(\<Union>i\<in>{0..n}. appl f i {}) = appl f n {}"
  proof(induct n)
  case 0 show ?case by simp
  next
  case (Suc n) show ?case
    proof -
    have "(\<Union>i\<in>{0..Suc n}. appl f i {}) = (\<Union>i\<in>{0..n}. appl f i {}) \<union> (appl f (Suc n) {})" by (rule UN_split)
    hence "(\<Union>i\<in>{0..Suc n}. appl f i {}) = (appl f n {}) \<union> (appl f (Suc n) {})" by (simp add: Suc.hyps)
    moreover  have "((appl f n {}) \<union> (appl f (Suc n) {})) = appl f (Suc n) {}" 
      proof -
      from m have "appl f n {} \<subseteq> appl f (Suc n) {}" by(rule appl_subset)
      thus ?thesis by(simp add: subset_Un_eq)
      qed
    ultimately show ?thesis by(rule trans)
    qed
  qed

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