--- 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
--- 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";
--- 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 *}
--- 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";