# Theory Fun_Cpo

theory Fun_Cpo
```(*  Title:      HOL/HOLCF/Fun_Cpo.thy
Author:     Franz Regensburger
Author:     Brian Huffman
*)

section ‹Class instances for the full function space›

theory Fun_Cpo
begin

subsection ‹Full function space is a partial order›

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"
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)"

lemma fun_belowI: "(⋀x. f x ⊑ g x) ⟹ f ⊑ g"

lemma fun_belowD: "f ⊑ g ⟹ f x ⊑ g x"

subsection ‹Full function space is chain complete›

text ‹Properties of chains of functions.›

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)"

lemma ch2ch_lambda: "(⋀x. chain (λi. S i x)) ⟹ chain S"

text ‹Type @{typ "'a::type ⇒ 'b::cpo"} is chain complete›

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"
qed

subsection ‹Full function space is pointed›

lemma minimal_fun: "(λx. ⊥) ⊑ f"

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 = ⊥"

lemma lambda_strict: "(λx. ⊥) = ⊥"
by (rule bottomI, rule minimal_fun)

subsection ‹Propagation of monotonicity and continuity›

text ‹The lub of a chain of monotone functions is monotone.›

text ‹The lub of a chain of continuous functions is continuous.›

text ‹Function application preserves monotonicity and continuity.›

lemma mono2mono_fun: "monofun f ⟹ monofun (λx. f x y)"

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 ‹
Lambda abstraction preserves monotonicity and continuity.
(Note ‹(λx. λy. f x y) = f›.)
›

lemma mono2mono_lambda: "(⋀y. monofun (λx. f x y)) ⟹ monofun f"

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 ‹What D.A.Schmidt calls continuity of abstraction; never used here›

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"