theory week05B_demo imports Main begin inductive Ev :: "nat \ bool" where ZeroI: "Ev 0" | Add2I: "Ev n \ Ev (Suc(Suc n))" print_theorems -- --------------------------------------------------- section "Formalising Least Fixpoints" definition closed :: "('a set \ 'a set) \ 'a set \ bool" where "closed f B \ f B \ B" lemma closed_int: "\ mono f; closed f A; closed f B \ \ closed f (A \ B)" thm mono_def apply (unfold closed_def mono_def) apply blast done definition lfpt :: "('a set \ 'a set) \ 'a set" where "lfpt f \ \ {B. closed f B}" text {* lfpt is the greatest lower bound: *} lemma lfpt_lower: "closed f B \ lfpt f \ B" sorry lemma lfpt_greatest: assumes A_smaller: "\B. closed f B \ A \ B" shows "A \ lfpt f" sorry section {* Fix Point *} lemma lfpt_fixpoint1: "mono f \ f (lfpt f) \ lfpt f" sorry lemma lfpt_fixpoint2: "mono f \ lfpt f \ f(lfpt f)" sorry lemma lfpt_fixpoint: "mono f \ 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 \ A" sorry section {* Rule Induction *} consts R :: "('a set \ 'a) set" definition R_hat :: "'a set \ 'a set" where "R_hat A \ undefined" lemma sound: assumes hyp: "\(H,x) \ R. (\h \ H. P h) \ P x" shows "\x \ lfpt R_hat. P x" sorry end