rename Ffun.thy to Fun_Cpo.thy
authorhuffman
Mon Oct 11 16:24:44 2010 -0700 (2010-10-11)
changeset 40001666c3751227c
parent 40000 9c6ad000dc89
child 40002 c5b5f7a3a3b1
rename Ffun.thy to Fun_Cpo.thy
src/HOLCF/Cfun.thy
src/HOLCF/Ffun.thy
src/HOLCF/Fun_Cpo.thy
src/HOLCF/IsaMakefile
     1.1 --- a/src/HOLCF/Cfun.thy	Mon Oct 11 16:14:15 2010 -0700
     1.2 +++ b/src/HOLCF/Cfun.thy	Mon Oct 11 16:24:44 2010 -0700
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* The type of continuous functions *}
     1.5  
     1.6  theory Cfun
     1.7 -imports Pcpodef Ffun Product_Cpo
     1.8 +imports Pcpodef Fun_Cpo Product_Cpo
     1.9  begin
    1.10  
    1.11  default_sort cpo
     2.1 --- a/src/HOLCF/Ffun.thy	Mon Oct 11 16:14:15 2010 -0700
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,273 +0,0 @@
     2.4 -(*  Title:      HOLCF/FunCpo.thy
     2.5 -    Author:     Franz Regensburger
     2.6 -*)
     2.7 -
     2.8 -header {* Class instances for the full function space *}
     2.9 -
    2.10 -theory Ffun
    2.11 -imports Cont
    2.12 -begin
    2.13 -
    2.14 -subsection {* Full function space is a partial order *}
    2.15 -
    2.16 -instantiation "fun"  :: (type, below) below
    2.17 -begin
    2.18 -
    2.19 -definition
    2.20 -  below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
    2.21 -
    2.22 -instance ..
    2.23 -end
    2.24 -
    2.25 -instance "fun" :: (type, po) po
    2.26 -proof
    2.27 -  fix f :: "'a \<Rightarrow> 'b"
    2.28 -  show "f \<sqsubseteq> f"
    2.29 -    by (simp add: below_fun_def)
    2.30 -next
    2.31 -  fix f g :: "'a \<Rightarrow> 'b"
    2.32 -  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
    2.33 -    by (simp add: below_fun_def fun_eq_iff below_antisym)
    2.34 -next
    2.35 -  fix f g h :: "'a \<Rightarrow> 'b"
    2.36 -  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
    2.37 -    unfolding below_fun_def by (fast elim: below_trans)
    2.38 -qed
    2.39 -
    2.40 -text {* make the symbol @{text "<<"} accessible for type fun *}
    2.41 -
    2.42 -lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
    2.43 -by (simp add: below_fun_def)
    2.44 -
    2.45 -lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
    2.46 -by (simp add: below_fun_def)
    2.47 -
    2.48 -subsection {* Full function space is chain complete *}
    2.49 -
    2.50 -text {* function application is monotone *}
    2.51 -
    2.52 -lemma monofun_app: "monofun (\<lambda>f. f x)"
    2.53 -by (rule monofunI, simp add: below_fun_def)
    2.54 -
    2.55 -text {* chains of functions yield chains in the po range *}
    2.56 -
    2.57 -lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
    2.58 -by (simp add: chain_def below_fun_def)
    2.59 -
    2.60 -lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
    2.61 -by (simp add: chain_def below_fun_def)
    2.62 -
    2.63 -text {* upper bounds of function chains yield upper bound in the po range *}
    2.64 -
    2.65 -lemma ub2ub_fun:
    2.66 -  "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
    2.67 -by (auto simp add: is_ub_def below_fun_def)
    2.68 -
    2.69 -text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
    2.70 -
    2.71 -lemma is_lub_lambda:
    2.72 -  assumes f: "\<And>x. range (\<lambda>i. Y i x) <<| f x"
    2.73 -  shows "range Y <<| f"
    2.74 -apply (rule is_lubI)
    2.75 -apply (rule ub_rangeI)
    2.76 -apply (rule below_fun_ext)
    2.77 -apply (rule is_ub_lub [OF f])
    2.78 -apply (rule below_fun_ext)
    2.79 -apply (rule is_lub_lub [OF f])
    2.80 -apply (erule ub2ub_fun)
    2.81 -done
    2.82 -
    2.83 -lemma lub_fun:
    2.84 -  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    2.85 -    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
    2.86 -apply (rule is_lub_lambda)
    2.87 -apply (rule cpo_lubI)
    2.88 -apply (erule ch2ch_fun)
    2.89 -done
    2.90 -
    2.91 -lemma thelub_fun:
    2.92 -  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    2.93 -    \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
    2.94 -by (rule lub_fun [THEN thelubI])
    2.95 -
    2.96 -lemma cpo_fun:
    2.97 -  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
    2.98 -by (rule exI, erule lub_fun)
    2.99 -
   2.100 -instance "fun"  :: (type, cpo) cpo
   2.101 -by intro_classes (rule cpo_fun)
   2.102 -
   2.103 -instance "fun" :: (finite, finite_po) finite_po ..
   2.104 -
   2.105 -instance "fun" :: (type, discrete_cpo) discrete_cpo
   2.106 -proof
   2.107 -  fix f g :: "'a \<Rightarrow> 'b"
   2.108 -  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
   2.109 -    unfolding expand_fun_below fun_eq_iff
   2.110 -    by simp
   2.111 -qed
   2.112 -
   2.113 -text {* chain-finite function spaces *}
   2.114 -
   2.115 -lemma maxinch2maxinch_lambda:
   2.116 -  "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
   2.117 -unfolding max_in_chain_def fun_eq_iff by simp
   2.118 -
   2.119 -lemma maxinch_mono:
   2.120 -  "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
   2.121 -unfolding max_in_chain_def
   2.122 -proof (intro allI impI)
   2.123 -  fix k
   2.124 -  assume Y: "\<forall>n\<ge>i. Y i = Y n"
   2.125 -  assume ij: "i \<le> j"
   2.126 -  assume jk: "j \<le> k"
   2.127 -  from ij jk have ik: "i \<le> k" by simp
   2.128 -  from Y ij have Yij: "Y i = Y j" by simp
   2.129 -  from Y ik have Yik: "Y i = Y k" by simp
   2.130 -  from Yij Yik show "Y j = Y k" by auto
   2.131 -qed
   2.132 -
   2.133 -instance "fun" :: (finite, chfin) chfin
   2.134 -proof
   2.135 -  fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
   2.136 -  let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
   2.137 -  assume "chain Y"
   2.138 -  hence "\<And>x. chain (\<lambda>i. Y i x)"
   2.139 -    by (rule ch2ch_fun)
   2.140 -  hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
   2.141 -    by (rule chfin)
   2.142 -  hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
   2.143 -    by (rule LeastI_ex)
   2.144 -  hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
   2.145 -    by (rule maxinch_mono [OF _ Max_ge], simp_all)
   2.146 -  hence "max_in_chain (Max (range ?n)) Y"
   2.147 -    by (rule maxinch2maxinch_lambda)
   2.148 -  thus "\<exists>n. max_in_chain n Y" ..
   2.149 -qed
   2.150 -
   2.151 -subsection {* Full function space is pointed *}
   2.152 -
   2.153 -lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
   2.154 -by (simp add: below_fun_def)
   2.155 -
   2.156 -lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
   2.157 -apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
   2.158 -apply (rule minimal_fun [THEN allI])
   2.159 -done
   2.160 -
   2.161 -instance "fun"  :: (type, pcpo) pcpo
   2.162 -by intro_classes (rule least_fun)
   2.163 -
   2.164 -text {* for compatibility with old HOLCF-Version *}
   2.165 -lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
   2.166 -by (rule minimal_fun [THEN UU_I, symmetric])
   2.167 -
   2.168 -text {* function application is strict in the left argument *}
   2.169 -lemma app_strict [simp]: "\<bottom> x = \<bottom>"
   2.170 -by (simp add: inst_fun_pcpo)
   2.171 -
   2.172 -text {*
   2.173 -  The following results are about application for functions in @{typ "'a=>'b"}
   2.174 -*}
   2.175 -
   2.176 -lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
   2.177 -by (simp add: below_fun_def)
   2.178 -
   2.179 -lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
   2.180 -by (rule monofunE)
   2.181 -
   2.182 -lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
   2.183 -by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
   2.184 -
   2.185 -subsection {* Propagation of monotonicity and continuity *}
   2.186 -
   2.187 -text {* the lub of a chain of monotone functions is monotone *}
   2.188 -
   2.189 -lemma monofun_lub_fun:
   2.190 -  "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
   2.191 -    \<Longrightarrow> monofun (\<Squnion>i. F i)"
   2.192 -apply (rule monofunI)
   2.193 -apply (simp add: thelub_fun)
   2.194 -apply (rule lub_mono)
   2.195 -apply (erule ch2ch_fun)
   2.196 -apply (erule ch2ch_fun)
   2.197 -apply (simp add: monofunE)
   2.198 -done
   2.199 -
   2.200 -text {* the lub of a chain of continuous functions is continuous *}
   2.201 -
   2.202 -lemma cont_lub_fun:
   2.203 -  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
   2.204 -apply (rule contI2)
   2.205 -apply (erule monofun_lub_fun)
   2.206 -apply (simp add: cont2mono)
   2.207 -apply (simp add: thelub_fun cont2contlubE)
   2.208 -apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
   2.209 -done
   2.210 -
   2.211 -lemma cont2cont_lub:
   2.212 -  "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
   2.213 -by (simp add: thelub_fun [symmetric] cont_lub_fun)
   2.214 -
   2.215 -lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
   2.216 -apply (rule monofunI)
   2.217 -apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
   2.218 -done
   2.219 -
   2.220 -lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
   2.221 -apply (rule contI2)
   2.222 -apply (erule cont2mono [THEN mono2mono_fun])
   2.223 -apply (simp add: cont2contlubE)
   2.224 -apply (simp add: thelub_fun ch2ch_cont)
   2.225 -done
   2.226 -
   2.227 -text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
   2.228 -
   2.229 -lemma mono2mono_lambda:
   2.230 -  assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
   2.231 -apply (rule monofunI)
   2.232 -apply (rule below_fun_ext)
   2.233 -apply (erule monofunE [OF f])
   2.234 -done
   2.235 -
   2.236 -lemma cont2cont_lambda [simp]:
   2.237 -  assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
   2.238 -apply (rule contI2)
   2.239 -apply (simp add: mono2mono_lambda cont2mono f)
   2.240 -apply (rule below_fun_ext)
   2.241 -apply (simp add: thelub_fun cont2contlubE [OF f])
   2.242 -done
   2.243 -
   2.244 -text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
   2.245 -
   2.246 -lemma contlub_lambda:
   2.247 -  "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
   2.248 -    \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
   2.249 -by (simp add: thelub_fun ch2ch_lambda)
   2.250 -
   2.251 -lemma contlub_abstraction:
   2.252 -  "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
   2.253 -    (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
   2.254 -apply (rule thelub_fun [symmetric])
   2.255 -apply (simp add: ch2ch_cont)
   2.256 -done
   2.257 -
   2.258 -lemma mono2mono_app:
   2.259 -  "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
   2.260 -apply (rule monofunI)
   2.261 -apply (simp add: monofun_fun monofunE)
   2.262 -done
   2.263 -
   2.264 -lemma cont2cont_app:
   2.265 -  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
   2.266 -apply (erule cont_apply [where t=t])
   2.267 -apply (erule spec)
   2.268 -apply (erule cont2cont_fun)
   2.269 -done
   2.270 -
   2.271 -lemmas cont2cont_app2 = cont2cont_app [rule_format]
   2.272 -
   2.273 -lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
   2.274 -by (rule cont2cont_app2 [OF cont_const])
   2.275 -
   2.276 -end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOLCF/Fun_Cpo.thy	Mon Oct 11 16:24:44 2010 -0700
     3.3 @@ -0,0 +1,274 @@
     3.4 +(*  Title:      HOLCF/Fun_Cpo.thy
     3.5 +    Author:     Franz Regensburger
     3.6 +    Author:     Brian Huffman
     3.7 +*)
     3.8 +
     3.9 +header {* Class instances for the full function space *}
    3.10 +
    3.11 +theory Fun_Cpo
    3.12 +imports Cont
    3.13 +begin
    3.14 +
    3.15 +subsection {* Full function space is a partial order *}
    3.16 +
    3.17 +instantiation "fun"  :: (type, below) below
    3.18 +begin
    3.19 +
    3.20 +definition
    3.21 +  below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
    3.22 +
    3.23 +instance ..
    3.24 +end
    3.25 +
    3.26 +instance "fun" :: (type, po) po
    3.27 +proof
    3.28 +  fix f :: "'a \<Rightarrow> 'b"
    3.29 +  show "f \<sqsubseteq> f"
    3.30 +    by (simp add: below_fun_def)
    3.31 +next
    3.32 +  fix f g :: "'a \<Rightarrow> 'b"
    3.33 +  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
    3.34 +    by (simp add: below_fun_def fun_eq_iff below_antisym)
    3.35 +next
    3.36 +  fix f g h :: "'a \<Rightarrow> 'b"
    3.37 +  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
    3.38 +    unfolding below_fun_def by (fast elim: below_trans)
    3.39 +qed
    3.40 +
    3.41 +text {* make the symbol @{text "<<"} accessible for type fun *}
    3.42 +
    3.43 +lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
    3.44 +by (simp add: below_fun_def)
    3.45 +
    3.46 +lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
    3.47 +by (simp add: below_fun_def)
    3.48 +
    3.49 +subsection {* Full function space is chain complete *}
    3.50 +
    3.51 +text {* function application is monotone *}
    3.52 +
    3.53 +lemma monofun_app: "monofun (\<lambda>f. f x)"
    3.54 +by (rule monofunI, simp add: below_fun_def)
    3.55 +
    3.56 +text {* chains of functions yield chains in the po range *}
    3.57 +
    3.58 +lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
    3.59 +by (simp add: chain_def below_fun_def)
    3.60 +
    3.61 +lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
    3.62 +by (simp add: chain_def below_fun_def)
    3.63 +
    3.64 +text {* upper bounds of function chains yield upper bound in the po range *}
    3.65 +
    3.66 +lemma ub2ub_fun:
    3.67 +  "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
    3.68 +by (auto simp add: is_ub_def below_fun_def)
    3.69 +
    3.70 +text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
    3.71 +
    3.72 +lemma is_lub_lambda:
    3.73 +  assumes f: "\<And>x. range (\<lambda>i. Y i x) <<| f x"
    3.74 +  shows "range Y <<| f"
    3.75 +apply (rule is_lubI)
    3.76 +apply (rule ub_rangeI)
    3.77 +apply (rule below_fun_ext)
    3.78 +apply (rule is_ub_lub [OF f])
    3.79 +apply (rule below_fun_ext)
    3.80 +apply (rule is_lub_lub [OF f])
    3.81 +apply (erule ub2ub_fun)
    3.82 +done
    3.83 +
    3.84 +lemma lub_fun:
    3.85 +  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    3.86 +    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
    3.87 +apply (rule is_lub_lambda)
    3.88 +apply (rule cpo_lubI)
    3.89 +apply (erule ch2ch_fun)
    3.90 +done
    3.91 +
    3.92 +lemma thelub_fun:
    3.93 +  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
    3.94 +    \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
    3.95 +by (rule lub_fun [THEN thelubI])
    3.96 +
    3.97 +lemma cpo_fun:
    3.98 +  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
    3.99 +by (rule exI, erule lub_fun)
   3.100 +
   3.101 +instance "fun"  :: (type, cpo) cpo
   3.102 +by intro_classes (rule cpo_fun)
   3.103 +
   3.104 +instance "fun" :: (finite, finite_po) finite_po ..
   3.105 +
   3.106 +instance "fun" :: (type, discrete_cpo) discrete_cpo
   3.107 +proof
   3.108 +  fix f g :: "'a \<Rightarrow> 'b"
   3.109 +  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
   3.110 +    unfolding expand_fun_below fun_eq_iff
   3.111 +    by simp
   3.112 +qed
   3.113 +
   3.114 +text {* chain-finite function spaces *}
   3.115 +
   3.116 +lemma maxinch2maxinch_lambda:
   3.117 +  "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
   3.118 +unfolding max_in_chain_def fun_eq_iff by simp
   3.119 +
   3.120 +lemma maxinch_mono:
   3.121 +  "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
   3.122 +unfolding max_in_chain_def
   3.123 +proof (intro allI impI)
   3.124 +  fix k
   3.125 +  assume Y: "\<forall>n\<ge>i. Y i = Y n"
   3.126 +  assume ij: "i \<le> j"
   3.127 +  assume jk: "j \<le> k"
   3.128 +  from ij jk have ik: "i \<le> k" by simp
   3.129 +  from Y ij have Yij: "Y i = Y j" by simp
   3.130 +  from Y ik have Yik: "Y i = Y k" by simp
   3.131 +  from Yij Yik show "Y j = Y k" by auto
   3.132 +qed
   3.133 +
   3.134 +instance "fun" :: (finite, chfin) chfin
   3.135 +proof
   3.136 +  fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
   3.137 +  let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
   3.138 +  assume "chain Y"
   3.139 +  hence "\<And>x. chain (\<lambda>i. Y i x)"
   3.140 +    by (rule ch2ch_fun)
   3.141 +  hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
   3.142 +    by (rule chfin)
   3.143 +  hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
   3.144 +    by (rule LeastI_ex)
   3.145 +  hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
   3.146 +    by (rule maxinch_mono [OF _ Max_ge], simp_all)
   3.147 +  hence "max_in_chain (Max (range ?n)) Y"
   3.148 +    by (rule maxinch2maxinch_lambda)
   3.149 +  thus "\<exists>n. max_in_chain n Y" ..
   3.150 +qed
   3.151 +
   3.152 +subsection {* Full function space is pointed *}
   3.153 +
   3.154 +lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
   3.155 +by (simp add: below_fun_def)
   3.156 +
   3.157 +lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
   3.158 +apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
   3.159 +apply (rule minimal_fun [THEN allI])
   3.160 +done
   3.161 +
   3.162 +instance "fun"  :: (type, pcpo) pcpo
   3.163 +by intro_classes (rule least_fun)
   3.164 +
   3.165 +text {* for compatibility with old HOLCF-Version *}
   3.166 +lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
   3.167 +by (rule minimal_fun [THEN UU_I, symmetric])
   3.168 +
   3.169 +text {* function application is strict in the left argument *}
   3.170 +lemma app_strict [simp]: "\<bottom> x = \<bottom>"
   3.171 +by (simp add: inst_fun_pcpo)
   3.172 +
   3.173 +text {*
   3.174 +  The following results are about application for functions in @{typ "'a=>'b"}
   3.175 +*}
   3.176 +
   3.177 +lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
   3.178 +by (simp add: below_fun_def)
   3.179 +
   3.180 +lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
   3.181 +by (rule monofunE)
   3.182 +
   3.183 +lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
   3.184 +by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
   3.185 +
   3.186 +subsection {* Propagation of monotonicity and continuity *}
   3.187 +
   3.188 +text {* the lub of a chain of monotone functions is monotone *}
   3.189 +
   3.190 +lemma monofun_lub_fun:
   3.191 +  "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
   3.192 +    \<Longrightarrow> monofun (\<Squnion>i. F i)"
   3.193 +apply (rule monofunI)
   3.194 +apply (simp add: thelub_fun)
   3.195 +apply (rule lub_mono)
   3.196 +apply (erule ch2ch_fun)
   3.197 +apply (erule ch2ch_fun)
   3.198 +apply (simp add: monofunE)
   3.199 +done
   3.200 +
   3.201 +text {* the lub of a chain of continuous functions is continuous *}
   3.202 +
   3.203 +lemma cont_lub_fun:
   3.204 +  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
   3.205 +apply (rule contI2)
   3.206 +apply (erule monofun_lub_fun)
   3.207 +apply (simp add: cont2mono)
   3.208 +apply (simp add: thelub_fun cont2contlubE)
   3.209 +apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
   3.210 +done
   3.211 +
   3.212 +lemma cont2cont_lub:
   3.213 +  "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
   3.214 +by (simp add: thelub_fun [symmetric] cont_lub_fun)
   3.215 +
   3.216 +lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
   3.217 +apply (rule monofunI)
   3.218 +apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
   3.219 +done
   3.220 +
   3.221 +lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
   3.222 +apply (rule contI2)
   3.223 +apply (erule cont2mono [THEN mono2mono_fun])
   3.224 +apply (simp add: cont2contlubE)
   3.225 +apply (simp add: thelub_fun ch2ch_cont)
   3.226 +done
   3.227 +
   3.228 +text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
   3.229 +
   3.230 +lemma mono2mono_lambda:
   3.231 +  assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
   3.232 +apply (rule monofunI)
   3.233 +apply (rule below_fun_ext)
   3.234 +apply (erule monofunE [OF f])
   3.235 +done
   3.236 +
   3.237 +lemma cont2cont_lambda [simp]:
   3.238 +  assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
   3.239 +apply (rule contI2)
   3.240 +apply (simp add: mono2mono_lambda cont2mono f)
   3.241 +apply (rule below_fun_ext)
   3.242 +apply (simp add: thelub_fun cont2contlubE [OF f])
   3.243 +done
   3.244 +
   3.245 +text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
   3.246 +
   3.247 +lemma contlub_lambda:
   3.248 +  "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
   3.249 +    \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
   3.250 +by (simp add: thelub_fun ch2ch_lambda)
   3.251 +
   3.252 +lemma contlub_abstraction:
   3.253 +  "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
   3.254 +    (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
   3.255 +apply (rule thelub_fun [symmetric])
   3.256 +apply (simp add: ch2ch_cont)
   3.257 +done
   3.258 +
   3.259 +lemma mono2mono_app:
   3.260 +  "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
   3.261 +apply (rule monofunI)
   3.262 +apply (simp add: monofun_fun monofunE)
   3.263 +done
   3.264 +
   3.265 +lemma cont2cont_app:
   3.266 +  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
   3.267 +apply (erule cont_apply [where t=t])
   3.268 +apply (erule spec)
   3.269 +apply (erule cont2cont_fun)
   3.270 +done
   3.271 +
   3.272 +lemmas cont2cont_app2 = cont2cont_app [rule_format]
   3.273 +
   3.274 +lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
   3.275 +by (rule cont2cont_app2 [OF cont_const])
   3.276 +
   3.277 +end
     4.1 --- a/src/HOLCF/IsaMakefile	Mon Oct 11 16:14:15 2010 -0700
     4.2 +++ b/src/HOLCF/IsaMakefile	Mon Oct 11 16:24:44 2010 -0700
     4.3 @@ -48,9 +48,9 @@
     4.4    Deflation.thy \
     4.5    Domain.thy \
     4.6    Domain_Aux.thy \
     4.7 -  Ffun.thy \
     4.8    Fixrec.thy \
     4.9    Fix.thy \
    4.10 +  Fun_Cpo.thy \
    4.11    HOLCF.thy \
    4.12    Lift.thy \
    4.13    LowerPD.thy \