theory week05B_demo_withproofs 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)" 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" apply (unfold lfpt_def) apply blast done lemma lfpt_greatest: assumes A_smaller: "\B. closed f B \ A \ B" shows "A \ lfpt f" apply (unfold lfpt_def) apply (insert A_smaller) apply blast done section {* Fix Point *} lemma lfpt_fixpoint1: "mono f \ f (lfpt f) \ 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 \ lfpt f \ (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 \ f (lfpt f) = lfpt f" by (blast intro!: lfpt_fixpoint1 lfpt_fixpoint2) text {* lfpt is the least fix point *} lemma lfpt_least: assumes A: "f A = A" shows "lfpt f \ A" apply (rule lfpt_lower) apply (unfold closed_def) apply (simp add: A) done text {* Formalising applying a function multiple times *} primrec appl :: "('a \ 'a) \ nat \ ('a \ 'a)" where "appl f 0 = id" | "appl f (Suc n) = f \ (appl f n)" text {* Any fixed point is not smaller than applying the function multiple times to the smallest element *} lemma appl_less_fp: assumes fp: "f d = d" assumes mo: "mono f" shows "appl f n {} \ d" proof(induct n) case 0 show ?case proof - have "{} \ d" .. thus ?case by simp qed next case (Suc n) show ?case proof - have a: "appl f (Suc n) {} \ f d" proof (simp) have h: "appl f n {} \ d" by(rule Suc.hyps) from mo and h show "f (appl f n {}) \ f d" by(rule monoD) qed moreover from fp have b: "f d \ d" by(rule equalityD1) ultimately show ?case by(rule subset_trans) qed qed lemma appl_subset: assumes m: "mono f" shows "appl f n {} \ 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 {}) \ f (appl f (Suc n) {})" by (rule monoD[OF m Suc.hyps]) thus ?case by simp qed qed lemma UN_split: "(\i\{0..Suc y}. P i) = ((\i\{0..y}. P i) \ P (Suc y))" apply(auto simp: atLeastAtMostSuc_conv) done lemma UN_appl: assumes m: "mono f" shows "(\i\{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 "(\i\{0..Suc n}. appl f i {}) = (\i\{0..n}. appl f i {}) \ (appl f (Suc n) {})" by (rule UN_split) hence "(\i\{0..Suc n}. appl f i {}) = (appl f n {}) \ (appl f (Suc n) {})" by (simp add: Suc.hyps) moreover have "((appl f n {}) \ (appl f (Suc n) {})) = appl f (Suc n) {}" proof - from m have "appl f n {} \ 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 {* Rule Induction *} consts R :: "('a set \ 'a) set" definition R_hat :: "'a set \ 'a set" where "R_hat A \ {x. \H. (H,x) \ R \ H \ A}" lemma monoR': "mono R_hat" apply (unfold mono_def) apply (unfold R_hat_def) apply blast done lemma sound: assumes hyp: "\(H,x) \ R. ((\h \ H. P h) \ P x)" shows "\x \ 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 \ {x. P x}" by (rule lfpt_lower) thus ?thesis by blast qed end