src/HOLCF/Cfun.thy

 
 instance "->" :: (finite_po, finite_po) finite_po
 by (rule typedef_finite_po [OF type_definition_CFun])
 
 instance "->" :: (finite_po, chfin) chfin
-by (rule typedef_chfin [OF type_definition_CFun less_CFun_def])
+by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
 
 instance "->" :: (cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: less_CFun_def Rep_CFun_inject)
+by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
 
 instance "->" :: (cpo, pcpo) pcpo
-by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun])
+by (rule typedef_pcpo [OF type_definition_CFun below_CFun_def UU_CFun])
 
 lemmas Rep_CFun_strict =
-  typedef_Rep_strict [OF type_definition_CFun less_CFun_def UU_CFun]
+  typedef_Rep_strict [OF type_definition_CFun below_CFun_def UU_CFun]
 
 lemmas Abs_CFun_strict =
-  typedef_Abs_strict [OF type_definition_CFun less_CFun_def UU_CFun]
+  typedef_Abs_strict [OF type_definition_CFun below_CFun_def UU_CFun]
 
 text {* function application is strict in its first argument *}
 
 lemma Rep_CFun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
 by (simp add: Rep_CFun_strict)

 lemma ext_cfun: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
 by (simp add: expand_cfun_eq)
 
 text {* Extensionality wrt. ordering for continuous functions *}
 
-lemma expand_cfun_less: "f \<sqsubseteq> g = (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
-by (simp add: less_CFun_def expand_fun_less)
-
-lemma less_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: expand_cfun_less)
+lemma expand_cfun_below: "f \<sqsubseteq> g = (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
+by (simp add: below_CFun_def expand_fun_below)
+
+lemma below_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
+by (simp add: expand_cfun_below)
 
 text {* Congruence for continuous function application *}
 
 lemma cfun_cong: "\<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> f\<cdot>x = g\<cdot>y"
 by simp

 by (rule cont_Rep_CFun1 [THEN contE])
 
 text {* monotonicity of application *}
 
 lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
-by (simp add: expand_cfun_less)
+by (simp add: expand_cfun_below)
 
 lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
 by (rule monofun_Rep_CFun2 [THEN monofunE])
 
 lemma monofun_cfun: "\<lbrakk>f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y"
-by (rule trans_less [OF monofun_cfun_fun monofun_cfun_arg])
+by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])
 
 text {* ch2ch - rules for the type @{typ "'a -> 'b"} *}
 
 lemma chain_monofun: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
 by (erule monofun_Rep_CFun2 [THEN ch2ch_monofun])

   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>(Y i))"
 by (simp add: chain_def monofun_cfun)
 
 lemma ch2ch_LAM [simp]:
   "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
-by (simp add: chain_def expand_cfun_less)
+by (simp add: chain_def expand_cfun_below)
 
 text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
 
 lemma contlub_cfun: 
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. F i\<cdot>(Y i))"

 text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
 
 lemma cont2mono_LAM:
   "\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
     \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
-  unfolding monofun_def expand_cfun_less by simp
+  unfolding monofun_def expand_cfun_below by simp
 
 text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
 
 text {*
   Not suitable as a cont2cont rule, because on nested lambdas

 
 text {* Monotonicity of @{term Abs_CFun} *}
 
 lemma semi_monofun_Abs_CFun:
   "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_CFun f \<sqsubseteq> Abs_CFun g"
-by (simp add: less_CFun_def Abs_CFun_inverse2)
+by (simp add: below_CFun_def Abs_CFun_inverse2)
 
 text {* some lemmata for functions with flat/chfin domain/range types *}
 
 lemma chfin_Rep_CFunR: "chain (Y::nat => 'a::cpo->'b::chfin)  
       ==> !s. ? n. (LUB i. Y i)$s = Y n$s"

 apply (drule_tac f=f in cfun_arg_cong)
 apply simp
 apply simp
 done
 
-lemma injection_less:
+lemma injection_below:
   "\<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)