(* Title: HOL/HOLCF/Fun_Cpo.thy
Author: Franz Regensburger
Author: Brian Huffman
*)
section \<open>Class instances for the full function space\<close>
theory Fun_Cpo
imports Adm
begin
subsection \<open>Full function space is a partial order\<close>
instantiation "fun" :: (type, below) below
begin
definition below_fun_def: "(\) \ (\f g. \x. f x \ g x)"
instance ..
end
instance "fun" :: (type, po) po
proof
fix f :: "'a \ 'b"
show "f \ f"
by (simp add: below_fun_def)
next
fix f g :: "'a \ 'b"
assume "f \ g" and "g \ f" then show "f = g"
by (simp add: below_fun_def fun_eq_iff below_antisym)
next
fix f g h :: "'a \ 'b"
assume "f \ g" and "g \ h" then show "f \ h"
unfolding below_fun_def by (fast elim: below_trans)
qed
lemma fun_below_iff: "f \ g \ (\x. f x \ g x)"
by (simp add: below_fun_def)
lemma fun_belowI: "(\x. f x \ g x) \ f \ g"
by (simp add: below_fun_def)
lemma fun_belowD: "f \ g \ f x \ g x"
by (simp add: below_fun_def)
subsection \<open>Full function space is chain complete\<close>
text \<open>Properties of chains of functions.\<close>
lemma fun_chain_iff: "chain S \ (\x. chain (\i. S i x))"
by (auto simp: chain_def fun_below_iff)
lemma ch2ch_fun: "chain S \ chain (\i. S i x)"
by (simp add: chain_def below_fun_def)
lemma ch2ch_lambda: "(\x. chain (\i. S i x)) \ chain S"
by (simp add: chain_def below_fun_def)
text \<open>Type \<^typ>\<open>'a::type \<Rightarrow> 'b::cpo\<close> is chain complete\<close>
lemma is_lub_lambda: "(\x. range (\i. Y i x) <<| f x) \ range Y <<| f"
by (simp add: is_lub_def is_ub_def below_fun_def)
lemma is_lub_fun: "chain S \ range S <<| (\x. \i. S i x)"
for S :: "nat \ 'a::type \ 'b::cpo"
apply (rule is_lub_lambda)
apply (rule cpo_lubI)
apply (erule ch2ch_fun)
done
lemma lub_fun: "chain S \ (\i. S i) = (\x. \i. S i x)"
for S :: "nat \ 'a::type \ 'b::cpo"
by (rule is_lub_fun [THEN lub_eqI])
instance "fun" :: (type, cpo) cpo
by intro_classes (rule exI, erule is_lub_fun)
instance "fun" :: (type, discrete_cpo) discrete_cpo
proof
fix f g :: "'a \ 'b"
show "f \ g \ f = g"
by (simp add: fun_below_iff fun_eq_iff)
qed
subsection \<open>Full function space is pointed\<close>
lemma minimal_fun: "(\x. \) \ f"
by (simp add: below_fun_def)
instance "fun" :: (type, pcpo) pcpo
by standard (fast intro: minimal_fun)
lemma inst_fun_pcpo: "\ = (\x. \)"
by (rule minimal_fun [THEN bottomI, symmetric])
lemma app_strict [simp]: "\ x = \"
by (simp add: inst_fun_pcpo)
lemma lambda_strict: "(\x. \) = \"
by (rule bottomI, rule minimal_fun)
subsection \<open>Propagation of monotonicity and continuity\<close>
text \<open>The lub of a chain of monotone functions is monotone.\<close>
lemma adm_monofun: "adm monofun"
by (rule admI) (simp add: lub_fun fun_chain_iff monofun_def lub_mono)
text \<open>The lub of a chain of continuous functions is continuous.\<close>
lemma adm_cont: "adm cont"
by (rule admI) (simp add: lub_fun fun_chain_iff)
text \<open>Function application preserves monotonicity and continuity.\<close>
lemma mono2mono_fun: "monofun f \ monofun (\x. f x y)"
by (simp add: monofun_def fun_below_iff)
lemma cont2cont_fun: "cont f \ cont (\x. f x y)"
apply (rule contI2)
apply (erule cont2mono [THEN mono2mono_fun])
apply (simp add: cont2contlubE lub_fun ch2ch_cont)
done
lemma cont_fun: "cont (\f. f x)"
using cont_id by (rule cont2cont_fun)
text \<open>
Lambda abstraction preserves monotonicity and continuity.
(Note \<open>(\<lambda>x. \<lambda>y. f x y) = f\<close>.)
\<close>
lemma mono2mono_lambda: "(\y. monofun (\x. f x y)) \ monofun f"
by (simp add: monofun_def fun_below_iff)
lemma cont2cont_lambda [simp]:
assumes f: "\y. cont (\x. f x y)"
shows "cont f"
by (rule contI, rule is_lub_lambda, rule contE [OF f])
text \<open>What D.A.Schmidt calls continuity of abstraction; never used here\<close>
lemma contlub_lambda: "(\x. chain (\i. S i x)) \ (\x. \i. S i x) = (\i. (\x. S i x))"
for S :: "nat \ 'a::type \ 'b::cpo"
by (simp add: lub_fun ch2ch_lambda)
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
