theory week05B_demo
imports Main
begin

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

print_theorems


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

section "Formalising Least Fixpoints"


definition
  closed :: "('a set \<Rightarrow> 'a set) \<Rightarrow> 'a set \<Rightarrow> bool"
where
  "closed f B \<equiv> undefined"

lemma closed_int:
  "\<lbrakk> mono f; closed f A; closed f B \<rbrakk> \<Longrightarrow> closed f (A \<inter> B)"
  sorry

definition
  lfpt :: "('a set \<Rightarrow> 'a set) \<Rightarrow> 'a set" where
  "lfpt f \<equiv> undefined"

section {* Fix Point *}

lemma lfpt_fixpoint:
  "mono f \<Longrightarrow> f (lfpt f) = lfpt f"
  sorry

text {* lfpt is the least fix point *}

lemma lfpt_least:
  assumes A: "f A = A"
  shows "lfpt f \<subseteq> A"
  sorry


section {* Rule Induction *}

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

definition
  R_hat :: "'a set \<Rightarrow> 'a set" where
  "R_hat A \<equiv> undefined"

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"
  sorry

end