(*<*)
theory ex12_tmpl
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))"
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 "continuous f"
shows "mono f"
sorry
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" sorry
show ?thesis
proof (rule antisym)
show "Sup (range ?C) \ lfp f" sorry
next
show "lfp f \ Sup (range ?C)" sorry
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
(*>*)