renamed to Ffun (full function space)

--- a/src/HOLCF/FunCpo.ML	Fri Jun 03 23:13:08 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-
-(* legacy ML bindings *)
-
-val less_fun_def = thm "less_fun_def";
-val refl_less_fun = thm "refl_less_fun";
-val antisym_less_fun = thm "antisym_less_fun";
-val trans_less_fun = thm "trans_less_fun";
-val minimal_fun = thm "minimal_fun";
-val least_fun = thm "least_fun";
-val less_fun = thm "less_fun";
-val ch2ch_fun = thm "ch2ch_fun";
-val ub2ub_fun = thm "ub2ub_fun";
-val lub_fun = thm "lub_fun";
-val thelub_fun = thm "thelub_fun";
-val cpo_fun = thm "cpo_fun";
-val inst_fun_pcpo = thm "inst_fun_pcpo";

--- a/src/HOLCF/FunCpo.thy	Fri Jun 03 23:13:08 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,114 +0,0 @@
-(*  Title:      HOLCF/FunCpo.thy
-    ID:         $Id$
-    Author:     Franz Regensburger
-
-Definition of the partial ordering for the type of all functions => (fun)
-
-Class instance of  => (fun) for class pcpo.
-*)
-
-header {* Class instances for the type of all functions *}
-
-theory FunCpo
-imports Pcpo
-begin
-
-subsection {* Type @{typ "'a => 'b"} is a partial order *}
-
-instance fun  :: (type, sq_ord) sq_ord ..
-
-defs (overloaded)
-  less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  
-
-lemma refl_less_fun: "(f::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f"
-by (simp add: less_fun_def)
-
-lemma antisym_less_fun:
-  "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f1\<rbrakk> \<Longrightarrow> f1 = f2"
-by (simp add: less_fun_def expand_fun_eq antisym_less)
-
-lemma trans_less_fun:
-  "\<lbrakk>(f1::'a::type \<Rightarrow> 'b::po) \<sqsubseteq> f2; f2 \<sqsubseteq> f3\<rbrakk> \<Longrightarrow> f1 \<sqsubseteq> f3"
-apply (unfold less_fun_def)
-apply clarify
-apply (rule trans_less)
-apply (erule spec)
-apply (erule spec)
-done
-
-instance fun  :: (type, po) po
-by intro_classes
-  (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+
-
-text {* make the symbol @{text "<<"} accessible for type fun *}
-
-lemma less_fun: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
-by (simp add: less_fun_def)
-
-lemma less_funI: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: less_fun_def)
-
-subsection {* Type @{typ "'a::type => 'b::pcpo"} is pointed *}
-
-lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
-by (simp add: less_fun_def)
-
-lemma least_fun: "\<exists>x::'a \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
-apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
-apply (rule minimal_fun [THEN allI])
-done
-
-subsection {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
-
-text {* chains of functions yield chains in the po range *}
-
-lemma ch2ch_fun:
-  "chain (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) \<Longrightarrow> chain (\<lambda>i. S i x)"
-by (simp add: chain_def less_fun_def)
-
-text {* upper bounds of function chains yield upper bound in the po range *}
-
-lemma ub2ub_fun:
-  "range (S::nat \<Rightarrow> 'a \<Rightarrow> 'b::po) <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
-by (auto simp add: is_ub_def less_fun_def)
-
-text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
-
-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_lubI)
-apply (rule ub_rangeI)
-apply (rule less_funI)
-apply (rule is_ub_thelub)
-apply (erule ch2ch_fun)
-apply (rule less_funI)
-apply (rule is_lub_thelub)
-apply (erule ch2ch_fun)
-apply (erule ub2ub_fun)
-done
-
-lemma thelub_fun:
-  "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
-    \<Longrightarrow> lub (range S) = (\<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  :: (type, pcpo) pcpo
-by intro_classes (rule least_fun)
-
-text {* for compatibility with old HOLCF-Version *}
-lemma inst_fun_pcpo: "UU = (%x. UU)"
-by (rule minimal_fun [THEN UU_I, symmetric])
-
-lemma UU_app [simp]: "\<bottom> x = \<bottom>"
-by (simp add: inst_fun_pcpo)
-
-end
-