# HG changeset patch
# User huffman
# Date 1286839484 25200
# Node ID 666c3751227c1275687819437aba9773bec0c527
# Parent  9c6ad000dc890923d775d7440213e040d8975703
rename Ffun.thy to Fun_Cpo.thy

diff -r 9c6ad000dc89 -r 666c3751227c src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Mon Oct 11 16:14:15 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Mon Oct 11 16:24:44 2010 -0700
@@ -6,7 +6,7 @@
 header {* The type of continuous functions *}
 
 theory Cfun
-imports Pcpodef Ffun Product_Cpo
+imports Pcpodef Fun_Cpo Product_Cpo
 begin
 
 default_sort cpo
diff -r 9c6ad000dc89 -r 666c3751227c src/HOLCF/Ffun.thy
--- a/src/HOLCF/Ffun.thy	Mon Oct 11 16:14:15 2010 -0700
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,273 +0,0 @@
-(*  Title:      HOLCF/FunCpo.thy
-    Author:     Franz Regensburger
-*)
-
-header {* Class instances for the full function space *}
-
-theory Ffun
-imports Cont
-begin
-
-subsection {* Full function space is a partial order *}
-
-instantiation "fun"  :: (type, below) below
-begin
-
-definition
-  below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
-
-instance ..
-end
-
-instance "fun" :: (type, po) po
-proof
-  fix f :: "'a \<Rightarrow> 'b"
-  show "f \<sqsubseteq> f"
-    by (simp add: below_fun_def)
-next
-  fix f g :: "'a \<Rightarrow> 'b"
-  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
-    by (simp add: below_fun_def fun_eq_iff below_antisym)
-next
-  fix f g h :: "'a \<Rightarrow> 'b"
-  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
-    unfolding below_fun_def by (fast elim: below_trans)
-qed
-
-text {* make the symbol @{text "<<"} accessible for type fun *}
-
-lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
-by (simp add: below_fun_def)
-
-lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: below_fun_def)
-
-subsection {* Full function space is chain complete *}
-
-text {* function application is monotone *}
-
-lemma monofun_app: "monofun (\<lambda>f. f x)"
-by (rule monofunI, simp add: below_fun_def)
-
-text {* chains of functions yield chains in the po range *}
-
-lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
-by (simp add: chain_def below_fun_def)
-
-lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
-by (simp add: chain_def below_fun_def)
-
-text {* upper bounds of function chains yield upper bound in the po range *}
-
-lemma ub2ub_fun:
-  "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
-by (auto simp add: is_ub_def below_fun_def)
-
-text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
-
-lemma is_lub_lambda:
-  assumes f: "\<And>x. range (\<lambda>i. Y i x) <<| f x"
-  shows "range Y <<| f"
-apply (rule is_lubI)
-apply (rule ub_rangeI)
-apply (rule below_fun_ext)
-apply (rule is_ub_lub [OF f])
-apply (rule below_fun_ext)
-apply (rule is_lub_lub [OF f])
-apply (erule ub2ub_fun)
-done
-
-lemma lub_fun:
-  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
-    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
-apply (rule is_lub_lambda)
-apply (rule cpo_lubI)
-apply (erule ch2ch_fun)
-done
-
-lemma thelub_fun:
-  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
-    \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
-by (rule lub_fun [THEN thelubI])
-
-lemma cpo_fun:
-  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
-by (rule exI, erule lub_fun)
-
-instance "fun"  :: (type, cpo) cpo
-by intro_classes (rule cpo_fun)
-
-instance "fun" :: (finite, finite_po) finite_po ..
-
-instance "fun" :: (type, discrete_cpo) discrete_cpo
-proof
-  fix f g :: "'a \<Rightarrow> 'b"
-  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
-    unfolding expand_fun_below fun_eq_iff
-    by simp
-qed
-
-text {* chain-finite function spaces *}
-
-lemma maxinch2maxinch_lambda:
-  "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
-unfolding max_in_chain_def fun_eq_iff by simp
-
-lemma maxinch_mono:
-  "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
-unfolding max_in_chain_def
-proof (intro allI impI)
-  fix k
-  assume Y: "\<forall>n\<ge>i. Y i = Y n"
-  assume ij: "i \<le> j"
-  assume jk: "j \<le> k"
-  from ij jk have ik: "i \<le> k" by simp
-  from Y ij have Yij: "Y i = Y j" by simp
-  from Y ik have Yik: "Y i = Y k" by simp
-  from Yij Yik show "Y j = Y k" by auto
-qed
-
-instance "fun" :: (finite, chfin) chfin
-proof
-  fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
-  let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
-  assume "chain Y"
-  hence "\<And>x. chain (\<lambda>i. Y i x)"
-    by (rule ch2ch_fun)
-  hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
-    by (rule chfin)
-  hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
-    by (rule LeastI_ex)
-  hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
-    by (rule maxinch_mono [OF _ Max_ge], simp_all)
-  hence "max_in_chain (Max (range ?n)) Y"
-    by (rule maxinch2maxinch_lambda)
-  thus "\<exists>n. max_in_chain n Y" ..
-qed
-
-subsection {* Full function space is pointed *}
-
-lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
-by (simp add: below_fun_def)
-
-lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
-apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
-apply (rule minimal_fun [THEN allI])
-done
-
-instance "fun"  :: (type, pcpo) pcpo
-by intro_classes (rule least_fun)
-
-text {* for compatibility with old HOLCF-Version *}
-lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
-by (rule minimal_fun [THEN UU_I, symmetric])
-
-text {* function application is strict in the left argument *}
-lemma app_strict [simp]: "\<bottom> x = \<bottom>"
-by (simp add: inst_fun_pcpo)
-
-text {*
-  The following results are about application for functions in @{typ "'a=>'b"}
-*}
-
-lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
-by (simp add: below_fun_def)
-
-lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
-by (rule monofunE)
-
-lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
-by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
-
-subsection {* Propagation of monotonicity and continuity *}
-
-text {* the lub of a chain of monotone functions is monotone *}
-
-lemma monofun_lub_fun:
-  "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
-    \<Longrightarrow> monofun (\<Squnion>i. F i)"
-apply (rule monofunI)
-apply (simp add: thelub_fun)
-apply (rule lub_mono)
-apply (erule ch2ch_fun)
-apply (erule ch2ch_fun)
-apply (simp add: monofunE)
-done
-
-text {* the lub of a chain of continuous functions is continuous *}
-
-lemma cont_lub_fun:
-  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
-apply (rule contI2)
-apply (erule monofun_lub_fun)
-apply (simp add: cont2mono)
-apply (simp add: thelub_fun cont2contlubE)
-apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
-done
-
-lemma cont2cont_lub:
-  "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
-by (simp add: thelub_fun [symmetric] cont_lub_fun)
-
-lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
-apply (rule monofunI)
-apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
-done
-
-lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
-apply (rule contI2)
-apply (erule cont2mono [THEN mono2mono_fun])
-apply (simp add: cont2contlubE)
-apply (simp add: thelub_fun ch2ch_cont)
-done
-
-text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
-
-lemma mono2mono_lambda:
-  assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
-apply (rule monofunI)
-apply (rule below_fun_ext)
-apply (erule monofunE [OF f])
-done
-
-lemma cont2cont_lambda [simp]:
-  assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
-apply (rule contI2)
-apply (simp add: mono2mono_lambda cont2mono f)
-apply (rule below_fun_ext)
-apply (simp add: thelub_fun cont2contlubE [OF f])
-done
-
-text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
-
-lemma contlub_lambda:
-  "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
-    \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
-by (simp add: thelub_fun ch2ch_lambda)
-
-lemma contlub_abstraction:
-  "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
-    (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
-apply (rule thelub_fun [symmetric])
-apply (simp add: ch2ch_cont)
-done
-
-lemma mono2mono_app:
-  "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
-apply (rule monofunI)
-apply (simp add: monofun_fun monofunE)
-done
-
-lemma cont2cont_app:
-  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
-apply (erule cont_apply [where t=t])
-apply (erule spec)
-apply (erule cont2cont_fun)
-done
-
-lemmas cont2cont_app2 = cont2cont_app [rule_format]
-
-lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
-by (rule cont2cont_app2 [OF cont_const])
-
-end
diff -r 9c6ad000dc89 -r 666c3751227c src/HOLCF/Fun_Cpo.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Fun_Cpo.thy	Mon Oct 11 16:24:44 2010 -0700
@@ -0,0 +1,274 @@
+(*  Title:      HOLCF/Fun_Cpo.thy
+    Author:     Franz Regensburger
+    Author:     Brian Huffman
+*)
+
+header {* Class instances for the full function space *}
+
+theory Fun_Cpo
+imports Cont
+begin
+
+subsection {* Full function space is a partial order *}
+
+instantiation "fun"  :: (type, below) below
+begin
+
+definition
+  below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
+
+instance ..
+end
+
+instance "fun" :: (type, po) po
+proof
+  fix f :: "'a \<Rightarrow> 'b"
+  show "f \<sqsubseteq> f"
+    by (simp add: below_fun_def)
+next
+  fix f g :: "'a \<Rightarrow> 'b"
+  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
+    by (simp add: below_fun_def fun_eq_iff below_antisym)
+next
+  fix f g h :: "'a \<Rightarrow> 'b"
+  assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
+    unfolding below_fun_def by (fast elim: below_trans)
+qed
+
+text {* make the symbol @{text "<<"} accessible for type fun *}
+
+lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
+by (simp add: below_fun_def)
+
+lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
+by (simp add: below_fun_def)
+
+subsection {* Full function space is chain complete *}
+
+text {* function application is monotone *}
+
+lemma monofun_app: "monofun (\<lambda>f. f x)"
+by (rule monofunI, simp add: below_fun_def)
+
+text {* chains of functions yield chains in the po range *}
+
+lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
+by (simp add: chain_def below_fun_def)
+
+lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
+by (simp add: chain_def below_fun_def)
+
+text {* upper bounds of function chains yield upper bound in the po range *}
+
+lemma ub2ub_fun:
+  "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
+by (auto simp add: is_ub_def below_fun_def)
+
+text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
+
+lemma is_lub_lambda:
+  assumes f: "\<And>x. range (\<lambda>i. Y i x) <<| f x"
+  shows "range Y <<| f"
+apply (rule is_lubI)
+apply (rule ub_rangeI)
+apply (rule below_fun_ext)
+apply (rule is_ub_lub [OF f])
+apply (rule below_fun_ext)
+apply (rule is_lub_lub [OF f])
+apply (erule ub2ub_fun)
+done
+
+lemma lub_fun:
+  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
+    \<Longrightarrow> range S <<| (\<lambda>x. \<Squnion>i. S i x)"
+apply (rule is_lub_lambda)
+apply (rule cpo_lubI)
+apply (erule ch2ch_fun)
+done
+
+lemma thelub_fun:
+  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
+    \<Longrightarrow> (\<Squnion>i. S i) = (\<lambda>x. \<Squnion>i. S i x)"
+by (rule lub_fun [THEN thelubI])
+
+lemma cpo_fun:
+  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
+by (rule exI, erule lub_fun)
+
+instance "fun"  :: (type, cpo) cpo
+by intro_classes (rule cpo_fun)
+
+instance "fun" :: (finite, finite_po) finite_po ..
+
+instance "fun" :: (type, discrete_cpo) discrete_cpo
+proof
+  fix f g :: "'a \<Rightarrow> 'b"
+  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
+    unfolding expand_fun_below fun_eq_iff
+    by simp
+qed
+
+text {* chain-finite function spaces *}
+
+lemma maxinch2maxinch_lambda:
+  "(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
+unfolding max_in_chain_def fun_eq_iff by simp
+
+lemma maxinch_mono:
+  "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
+unfolding max_in_chain_def
+proof (intro allI impI)
+  fix k
+  assume Y: "\<forall>n\<ge>i. Y i = Y n"
+  assume ij: "i \<le> j"
+  assume jk: "j \<le> k"
+  from ij jk have ik: "i \<le> k" by simp
+  from Y ij have Yij: "Y i = Y j" by simp
+  from Y ik have Yik: "Y i = Y k" by simp
+  from Yij Yik show "Y j = Y k" by auto
+qed
+
+instance "fun" :: (finite, chfin) chfin
+proof
+  fix Y :: "nat \<Rightarrow> 'a \<Rightarrow> 'b"
+  let ?n = "\<lambda>x. LEAST n. max_in_chain n (\<lambda>i. Y i x)"
+  assume "chain Y"
+  hence "\<And>x. chain (\<lambda>i. Y i x)"
+    by (rule ch2ch_fun)
+  hence "\<And>x. \<exists>n. max_in_chain n (\<lambda>i. Y i x)"
+    by (rule chfin)
+  hence "\<And>x. max_in_chain (?n x) (\<lambda>i. Y i x)"
+    by (rule LeastI_ex)
+  hence "\<And>x. max_in_chain (Max (range ?n)) (\<lambda>i. Y i x)"
+    by (rule maxinch_mono [OF _ Max_ge], simp_all)
+  hence "max_in_chain (Max (range ?n)) Y"
+    by (rule maxinch2maxinch_lambda)
+  thus "\<exists>n. max_in_chain n Y" ..
+qed
+
+subsection {* Full function space is pointed *}
+
+lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
+by (simp add: below_fun_def)
+
+lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
+apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
+apply (rule minimal_fun [THEN allI])
+done
+
+instance "fun"  :: (type, pcpo) pcpo
+by intro_classes (rule least_fun)
+
+text {* for compatibility with old HOLCF-Version *}
+lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
+by (rule minimal_fun [THEN UU_I, symmetric])
+
+text {* function application is strict in the left argument *}
+lemma app_strict [simp]: "\<bottom> x = \<bottom>"
+by (simp add: inst_fun_pcpo)
+
+text {*
+  The following results are about application for functions in @{typ "'a=>'b"}
+*}
+
+lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
+by (simp add: below_fun_def)
+
+lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
+by (rule monofunE)
+
+lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
+by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
+
+subsection {* Propagation of monotonicity and continuity *}
+
+text {* the lub of a chain of monotone functions is monotone *}
+
+lemma monofun_lub_fun:
+  "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk>
+    \<Longrightarrow> monofun (\<Squnion>i. F i)"
+apply (rule monofunI)
+apply (simp add: thelub_fun)
+apply (rule lub_mono)
+apply (erule ch2ch_fun)
+apply (erule ch2ch_fun)
+apply (simp add: monofunE)
+done
+
+text {* the lub of a chain of continuous functions is continuous *}
+
+lemma cont_lub_fun:
+  "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)"
+apply (rule contI2)
+apply (erule monofun_lub_fun)
+apply (simp add: cont2mono)
+apply (simp add: thelub_fun cont2contlubE)
+apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
+done
+
+lemma cont2cont_lub:
+  "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
+by (simp add: thelub_fun [symmetric] cont_lub_fun)
+
+lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
+apply (rule monofunI)
+apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])
+done
+
+lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)"
+apply (rule contI2)
+apply (erule cont2mono [THEN mono2mono_fun])
+apply (simp add: cont2contlubE)
+apply (simp add: thelub_fun ch2ch_cont)
+done
+
+text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
+
+lemma mono2mono_lambda:
+  assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
+apply (rule monofunI)
+apply (rule below_fun_ext)
+apply (erule monofunE [OF f])
+done
+
+lemma cont2cont_lambda [simp]:
+  assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
+apply (rule contI2)
+apply (simp add: mono2mono_lambda cont2mono f)
+apply (rule below_fun_ext)
+apply (simp add: thelub_fun cont2contlubE [OF f])
+done
+
+text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
+
+lemma contlub_lambda:
+  "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
+    \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))"
+by (simp add: thelub_fun ch2ch_lambda)
+
+lemma contlub_abstraction:
+  "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
+    (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
+apply (rule thelub_fun [symmetric])
+apply (simp add: ch2ch_cont)
+done
+
+lemma mono2mono_app:
+  "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))"
+apply (rule monofunI)
+apply (simp add: monofun_fun monofunE)
+done
+
+lemma cont2cont_app:
+  "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))"
+apply (erule cont_apply [where t=t])
+apply (erule spec)
+apply (erule cont2cont_fun)
+done
+
+lemmas cont2cont_app2 = cont2cont_app [rule_format]
+
+lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))"
+by (rule cont2cont_app2 [OF cont_const])
+
+end
diff -r 9c6ad000dc89 -r 666c3751227c src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Mon Oct 11 16:14:15 2010 -0700
+++ b/src/HOLCF/IsaMakefile	Mon Oct 11 16:24:44 2010 -0700
@@ -48,9 +48,9 @@
   Deflation.thy \
   Domain.thy \
   Domain_Aux.thy \
-  Ffun.thy \
   Fixrec.thy \
   Fix.thy \
+  Fun_Cpo.thy \
   HOLCF.thy \
   Lift.thy \
   LowerPD.thy \