(*<*)
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
(*>*)