# HG changeset patch
# User huffman
# Date 1129065590 -7200
# Node ID 4a8c3f8b0a92a04f98e883a2b48364a56e5c72ed
# Parent  695a2365d32f7699417279ad1a062e8a8bf8f60c
cleaned up; renamed less_fun to expand_fun_less

diff -r 695a2365d32f -r 4a8c3f8b0a92 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Tue Oct 11 17:30:00 2005 +0200
+++ b/src/HOLCF/Cont.thy	Tue Oct 11 23:19:50 2005 +0200
@@ -215,7 +215,7 @@
 
 lemma mono2mono_MF1L_rev: "\<forall>y. monofun (\<lambda>x. f x y) \<Longrightarrow> monofun f"
 apply (rule monofunI)
-apply (rule less_fun [THEN iffD2])
+apply (rule less_fun_ext)
 apply (blast dest: monofunE)
 done
 
diff -r 695a2365d32f -r 4a8c3f8b0a92 src/HOLCF/Ffun.ML
--- a/src/HOLCF/Ffun.ML	Tue Oct 11 17:30:00 2005 +0200
+++ b/src/HOLCF/Ffun.ML	Tue Oct 11 23:19:50 2005 +0200
@@ -6,11 +6,11 @@
 val ch2ch_fun = thm "ch2ch_fun";
 val ch2ch_fun_rev = thm "ch2ch_fun_rev";
 val cpo_fun = thm "cpo_fun";
+val expand_fun_less = thm "expand_fun_less";
 val inst_fun_pcpo = thm "inst_fun_pcpo";
 val least_fun = thm "least_fun";
 val less_fun_def = thm "less_fun_def";
 val less_fun_ext = thm "less_fun_ext";
-val less_fun = thm "less_fun";
 val lub_fun = thm "lub_fun";
 val minimal_fun = thm "minimal_fun";
 val refl_less_fun = thm "refl_less_fun";
diff -r 695a2365d32f -r 4a8c3f8b0a92 src/HOLCF/Ffun.thy
--- a/src/HOLCF/Ffun.thy	Tue Oct 11 17:30:00 2005 +0200
+++ b/src/HOLCF/Ffun.thy	Tue Oct 11 23:19:50 2005 +0200
@@ -42,22 +42,12 @@
 
 text {* make the symbol @{text "<<"} accessible for type fun *}
 
-lemma less_fun: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
+lemma expand_fun_less: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
 by (simp add: less_fun_def)
 
 lemma less_fun_ext: "(\<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 *}
@@ -103,11 +93,21 @@
 instance fun  :: (type, cpo) cpo
 by intro_classes (rule cpo_fun)
 
+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
+
 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)"
+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 *}
diff -r 695a2365d32f -r 4a8c3f8b0a92 src/HOLCF/ex/loeckx.ML
--- a/src/HOLCF/ex/loeckx.ML	Tue Oct 11 17:30:00 2005 +0200
+++ b/src/HOLCF/ex/loeckx.ML	Tue Oct 11 23:19:50 2005 +0200
@@ -5,7 +5,7 @@
 Goalw [Ifix_def] "Ifix F= lub (range (%i.%G. iterate i G UU)) F";
 by (stac thelub_fun 1);
 by (rtac refl 2);
-by (blast_tac (claset() addIs [ch2ch_fun, chainI, less_fun RS iffD2,
+by (blast_tac (claset() addIs [ch2ch_fun, chainI, expand_fun_less RS iffD2,
                                chain_iterate RS chainE]) 1); 
 qed "loeckx_sieber";