theory week06B_demo
imports Main
begin

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

print_theorems


-- ---------------------------------------------------

text {* Cases (rule inversion) in Isar *}


lemma "Ev n \<Longrightarrow> n = 0 \<or> (\<exists>Ev n'. n = Suc (Suc n'))"
proof -
  assume "Ev n"
  from this show "n = 0 \<or> (\<exists>Ev n'. n = Suc (Suc n'))"
  proof cases
    assume "n = 0"
    thus ?thesis ..
  next
    fix n' 
    assume "n = Suc (Suc n')" and "Ev n'"
    thus ?thesis by blast
  qed
qed


lemma 
  assumes n: "Ev n" 
  shows "n = 0 \<or> (\<exists>Ev n'. n = Suc (Suc n'))" 
using n proof cases
  case ZeroI
  thus ?thesis ..
next
  case (Add2I n')
  thus ?thesis by blast
qed
  

text {* Rule induction in Isar *}

lemma "Ev n \<Longrightarrow> \<exists>k. n = 2*k"
proof (induct rule: Ev.induct)
  case ZeroI thus ?case by simp
next
  case Add2I thus ?case by arith
qed


lemma assumes n: "Ev n" shows "\<exists>k. n = 2*k"
using n proof induct
  case ZeroI thus ?case by simp
next
  case Add2I thus ?case by arith
qed


lemma assumes n: "Ev n" shows "\<exists>k. n = 2*k"
using n proof induct
  case ZeroI thus ?case by simp
next
  case (Add2I m)
  then obtain k where "m = 2*k" by blast
  hence "Suc (Suc m) = 2*(k+1)" by simp
  thus "\<exists>k. Suc (Suc m) = 2*k" ..
qed


-- ----------------------------------------------

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 {* 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"

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