(*<*)
theory sol12
imports "~~/src/HOL/IMP/VCG" "~~/src/HOL/IMP/Hoare_Total" Complex_Main
"~~/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"
(*<*)
proof
fix x y :: 'a
assume "x\y"
let ?C = "\n::nat. if n = 0 then x else y"
from `x\y` have "chain ?C" unfolding chain_def by auto
have range_C: "range ?C = {x, y}" by auto
have "f x \ Sup (f ` range ?C)" by (simp add: range_C)
also have "\ = f (Sup (range ?C))" using `continuous f` `chain ?C`
by (rule continuousD [symmetric])
also have "Sup (range ?C) = y" using `x\y`
unfolding range_C by (simp add: sup_absorb2)
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" (*<*)
unfolding chain_def
proof
fix i
show "(f^^i) bot \ (f^^Suc i) bot"
by (induct i) (auto intro: monoD[OF MONO])
qed (*>*)
show ?thesis
proof (rule antisym)
show "Sup (range ?C) \ lfp f" (*<*)
proof -
{
fix i
have "(f^^i) bot \ lfp f"
apply (induct i)
apply simp
apply simp
by (metis MONO lfp_unfold monoD)
} thus "Sup (range ?C) \ lfp f" by (blast intro: Sup_least)
qed (*>*)
next
show "lfp f \ Sup (range ?C)" (*<*)
apply (rule lfp_lowerbound)
apply (simp only: continuousD[OF CONT CHAIN])
apply (rule Sup_subset_mono)
apply (auto)
apply (rule_tac x="Suc i" in range_eqI)
apply auto
done
(*>*)
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". *}
(* Fill in the gaps marked with "!" - Everything else is provided *)
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
proof
case goal1 show ?case by(simp add: less_list_def) (* ! *)
next
case goal2 thus ?case by(auto simp: less_eq_list_def) (* ! *)
next
case goal3 thus ?case by(fastforce simp: less_eq_list_def) (* ! *)
next
case goal4 thus ?case
by (simp add: antisym less_eq_list_def nth_equalityI) (* ! *)
qed
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 = map (\p. INF C:M. C ! p) [0..*)
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
(*<*)
proof
case goal1 thus ?case
by(auto simp: Inf_list_def less_eq_list_def intro:INF_lower) (* ! *)
next
case goal2 thus ?case
by(auto simp: Inf_list_def less_eq_list_def intro:INF_greatest) (* ! *)
next
case goal3 thus ?case by(auto simp: Inf_list_def) (* ! *)
qed
(*>*)
(*<*)
end
(*>*)