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
  imports Adm

subsection ‹Full function space is a partial order›

instantiation "fun"  :: (type, below) below

definition below_fun_def: "(⊑)  (λf g. x. f x  g x)"

instance ..

instance "fun" :: (type, po) po
  fix f :: "'a  'b"
  show "f  f"
    by (simp add: below_fun_def)
  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)
  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)

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

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
  fix f g :: "'a  'b"
  show "f  g  f = g"
    by (simp add: fun_below_iff fun_eq_iff)

subsection ‹Full function space is pointed›

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 ‹Propagation of monotonicity and continuity›

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

lemma adm_monofun: "adm monofun"
  by (rule admI) (simp add: lub_fun fun_chain_iff monofun_def lub_mono)

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

lemma adm_cont: "adm cont"
  by (rule admI) (simp add: lub_fun fun_chain_iff)

text ‹Function application preserves monotonicity and continuity.›

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)

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"
  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 ‹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"
  by (simp add: lub_fun ch2ch_lambda)