# HG changeset patch
# User huffman
# Date 1118181878 -7200
# Node ID 7102a1aaecfd9ff53658b6c6f8bd474d620b13ab
# Parent  79b37d5e50b128c37dc864a005e561761c7ed74b
added theorem injection_less

diff -r 79b37d5e50b1 -r 7102a1aaecfd src/HOLCF/Cfun.ML
--- 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";
diff -r 79b37d5e50b1 -r 7102a1aaecfd src/HOLCF/Cfun.thy
--- 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)