(*<*) theory tut12 imports "~~/src/HOL/IMP/Complete_Lattice" begin (*>*) text {* \ExerciseSheet{12}{12.~01.~2016}*} text {* \Exercise{Kleene fixed point theorem} Prove the Kleene fixed point theorem. We first introduce some auxiliary definitions: *} text {* A chain is a set such that any two elements are comparable. For the purposes of the Kleene fixed-point theorem, it is sufficient to consider only countable chains. It is easiest to formalize these as ascending sequences. (We can obtain the corresponding set using the function @{text "range :: ('a \ 'b) \ 'b set"}.) *} definition chain :: "(nat \ 'a::complete_lattice) \ bool" where "chain C \ (\n. C n \ C (Suc n))" lemma chainI[intro?]: assumes "\n. C n \ C (Suc n)" shows "chain C" using assms by (auto simp: chain_def) text {* A function is continuous, if it commutes with least upper bounds of chains.*} definition continuous :: "('a::complete_lattice \ 'b::complete_lattice) \ bool" where "continuous f \ (\C. chain C \ f (Sup (range C)) = Sup (f ` range C))" text {* The following lemma may be handy: *} lemma continuousD: "\continuous f; chain C\ \ f (Sup (range C)) = Sup (f ` range C)" unfolding continuous_def by auto text {* As warm-up, show that any continuous function is monotonic: *} lemma cont_imp_mono: fixes f :: "'a::complete_lattice \ 'b::complete_lattice" assumes CONT: "continuous f" shows "mono f" proof (rule monoI) fix x y :: 'a assume A: "x\y" let ?C = "\0\x | Suc _ \ y" from A have "chain ?C" by (auto simp: chain_def split: nat.split) have "f x \ Sup (f`{x,y})" by simp also have RC: "{x,y} = range ?C" apply (auto simp: image_def split: nat.splits) by presburger also have "Sup (f`range ?C) = f (Sup (range ?C))" using continuousD[OF CONT \chain ?C\] by simp also have "Sup (range ?C) = y" using A by (simp add: RC[symmetric] le_iff_sup) finally show "f x \ f y" . qed text {* Hint: The relevant lemmas are *} thm mono_def monoI monoD text {* Finally show the Kleene fixed point theorem. Note that this theorem is important, as it provides a way to compute least fixed points by iteration. *} theorem kleene_lfp: fixes f:: "'a::complete_lattice \ 'a" assumes CONT: "continuous f" shows "lfp f = Sup (range (\i. (f^^i) bot))" proof - txt {* We propose a proof structure here, however, you may deviate from this and use your own proof structure: *} let ?C = "\i. (f^^i) bot" note MONO=cont_imp_mono[OF CONT] have CHAIN: "chain ?C" proof (rule chainI) fix n show "(f ^^ n) bot \ (f ^^ Suc n) bot" apply (induction n) apply auto by (simp add: MONO monoD) qed show ?thesis proof (rule antisym) show "Sup (range ?C) \ lfp f" proof (rule Sup_least; clarsimp) fix i show "(f ^^ i) bot \ lfp f" apply (induction i) apply (auto dest: monoD[OF MONO] simp: lfp_unfold[OF MONO, symmetric]) done have "(f ^^ i) bot \ lfp f" apply (induction i) apply simp apply (drule monoD[OF MONO]) apply simp thm lfp_unfold[OF MONO, symmetric] apply (simp add: lfp_unfold[OF MONO, symmetric]) done have "(f ^^ i) bot \ lfp f" proof (induction i) case (Suc i) assume "(f ^^ i) bot \ lfp f" with monoD[OF MONO] have "(f ^^(Suc i)) bot \ f (lfp f)" by simp -- \Apply @{term f} on both sides\ also have "f (lfp f) = lfp f" by (simp add: lfp_unfold[OF MONO, symmetric]) -- \Contract fixed point\ finally show "(f ^^ Suc i) bot \ lfp f" . qed simp qed next have "f`range ?C \ range ?C" apply (auto simp: image_def) by (metis comp_apply funpow_Suc_right funpow_swap1) show "lfp f \ Sup (range ?C)" apply (rule lfp_lowerbound) thm continuousD[OF CONT \chain ?C\] apply (subst continuousD[OF CONT \chain ?C\]) apply (rule Sup_subset_mono) by fact qed qed text {* Hint: Some relevant lemmas are *} thm lfp_unfold lfp_lowerbound Sup_subset_mono range_eqI text \ \Exercise{Complete Lattice over Lists} \ text{* Show that lists of the same length ordered pointwise form a partial order if the element type is partially ordered. Partial orders are predefined as the type class "order". *} instantiation list :: (order) order (*<*) begin definition less_eq_list :: "('a::order)list \ 'a list \ bool" where "xs \ ys \ length xs = length ys \ (\p ys ! p)" definition less_list :: "'a list \ 'a list \ bool" where "less_list x y = (x \ y \ \ y \ x)" instance apply default (* You may also use an Isar-proof here *) sorry end (*>*) text{* Define the infimum operation for a set of lists. The first parameter is the length of the result list. *} definition Inf_list :: "nat \ ('a::complete_lattice) list set \ 'a list" where "Inf_list n M = undefined" text \Show that your ordering and the infimum operation indeed form a complete lattice: \ interpretation Complete_Lattice "{xs. length xs = n}" "Inf_list n" for n apply default (* Isar-proof also valid here ;) *) sorry (*<*) end (*>*)