--- a/src/HOLCF/Cfun.ML Tue Jun 07 20:04:41 2005 +0200
+++ b/src/HOLCF/Cfun.ML Wed Jun 08 00:04:38 2005 +0200
@@ -57,6 +57,7 @@
val chfin_Rep_CFunR = thm "chfin_Rep_CFunR";
val retraction_strict = thm "retraction_strict";
val injection_eq = thm "injection_eq";
+val injection_less = thm "injection_less";
val injection_defined_rev = thm "injection_defined_rev";
val injection_defined = thm "injection_defined";
val chfin2chfin = thm "chfin2chfin";
--- a/src/HOLCF/Cfun.thy Tue Jun 07 20:04:41 2005 +0200
+++ b/src/HOLCF/Cfun.thy Wed Jun 08 00:04:38 2005 +0200
@@ -336,6 +336,14 @@
apply simp
done
+lemma injection_less:
+ "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x \<sqsubseteq> g\<cdot>y) = (x \<sqsubseteq> y)"
+apply (rule iffI)
+apply (drule_tac f=f in monofun_cfun_arg)
+apply simp
+apply (erule monofun_cfun_arg)
+done
+
lemma injection_defined_rev:
"\<lbrakk>\<forall>x. f\<cdot>(g\<cdot>x) = x; g\<cdot>z = \<bottom>\<rbrakk> \<Longrightarrow> z = \<bottom>"
apply (drule_tac f=f in cfun_arg_cong)