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> f B \<subseteq> B"

lemma closed_int:
  "\<lbrakk> mono f; closed f A; closed f B \<rbrakk> \<Longrightarrow> closed f (A \<inter> B)"
  thm mono_def 
   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}"

section {* Fix Point *}

lemma blah1:
  "mono f \<Longrightarrow> closed f (f (lfpt f))"
  sorry
  
lemma blah2:
  "(\<forall> B. closed f B \<longrightarrow> A \<subseteq> B ) \<Longrightarrow>
    A \<subseteq> lfpt f"
  apply (simp add: lfpt_def closed_def) 
  apply blast
  done
  
lemma lfpt_fixpoint1:
  "mono f \<Longrightarrow> f (lfpt f) \<subseteq> lfpt f"
  apply (rule blah2)
  apply (clarsimp del: subsetI simp add: closed_def)
  apply (subgoal_tac "f (lfpt f) \<subseteq> f B")
   apply simp 
  apply (erule monoD) 
  apply (simp add: lfpt_def)
  apply (unfold closed_def)
  apply blast
  done
  
  
  
lemma lfpt_fixpoint2:
  "mono f \<Longrightarrow> lfpt f \<subseteq> f(lfpt f)"
  sorry

lemma lfpt_fixpoint:
  "mono f \<Longrightarrow> f (lfpt f) = lfpt f"
  apply (rule equalityI)
   apply (erule lfpt_fixpoint1)
  apply (erule lfpt_fixpoint2)
  done

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