rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
authorhuffman
Fri May 08 16:19:51 2009 -0700 (2009-05-08)
changeset 3107699fe356cbbc2
parent 31075 a9d6cf6de9a8
child 31081 aee96acd5e79
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
src/HOLCF/Adm.thy
src/HOLCF/Algebraic.thy
src/HOLCF/Bifinite.thy
src/HOLCF/Cfun.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/Completion.thy
src/HOLCF/Cont.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/Cprod.thy
src/HOLCF/Deflation.thy
src/HOLCF/Discrete.thy
src/HOLCF/Domain.thy
src/HOLCF/Ffun.thy
src/HOLCF/Fix.thy
src/HOLCF/HOLCF.thy
src/HOLCF/Lift.thy
src/HOLCF/LowerPD.thy
src/HOLCF/One.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Pcpodef.thy
src/HOLCF/Porder.thy
src/HOLCF/Product_Cpo.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Sum_Cpo.thy
src/HOLCF/Tools/domain/domain_library.ML
src/HOLCF/Tools/domain/domain_theorems.ML
src/HOLCF/Tools/pcpodef_package.ML
src/HOLCF/Tr.thy
src/HOLCF/Universal.thy
src/HOLCF/Up.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/Adm.thy	Fri May 08 19:28:11 2009 +0100
     1.2 +++ b/src/HOLCF/Adm.thy	Fri May 08 16:19:51 2009 -0700
     1.3 @@ -78,7 +78,7 @@
     1.4    "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow> 
     1.5      (\<Squnion>i. Y i) = (\<Squnion>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
     1.6   apply (frule (1) adm_disj_lemma1)
     1.7 - apply (rule antisym_less)
     1.8 + apply (rule below_antisym)
     1.9    apply (rule lub_mono, assumption+)
    1.10    apply (erule chain_mono)
    1.11    apply (simp add: adm_disj_lemma2)
    1.12 @@ -122,7 +122,7 @@
    1.13  
    1.14  text {* admissibility and continuity *}
    1.15  
    1.16 -lemma adm_less: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
    1.17 +lemma adm_below: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
    1.18  apply (rule admI)
    1.19  apply (simp add: cont2contlubE)
    1.20  apply (rule lub_mono)
    1.21 @@ -132,7 +132,7 @@
    1.22  done
    1.23  
    1.24  lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
    1.25 -by (simp add: po_eq_conv adm_conj adm_less)
    1.26 +by (simp add: po_eq_conv adm_conj adm_below)
    1.27  
    1.28  lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
    1.29  apply (rule admI)
    1.30 @@ -142,11 +142,11 @@
    1.31  apply (erule spec)
    1.32  done
    1.33  
    1.34 -lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
    1.35 +lemma adm_not_below: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
    1.36  apply (rule admI)
    1.37  apply (drule_tac x=0 in spec)
    1.38  apply (erule contrapos_nn)
    1.39 -apply (erule rev_trans_less)
    1.40 +apply (erule rev_below_trans)
    1.41  apply (erule cont2mono [THEN monofunE])
    1.42  apply (erule is_ub_thelub)
    1.43  done
    1.44 @@ -179,21 +179,21 @@
    1.45  apply (drule (1) compactD2, simp)
    1.46  apply (erule exE, rule_tac x=i in exI)
    1.47  apply (rule max_in_chainI)
    1.48 -apply (rule antisym_less)
    1.49 +apply (rule below_antisym)
    1.50  apply (erule (1) chain_mono)
    1.51 -apply (erule (1) trans_less [OF is_ub_thelub])
    1.52 +apply (erule (1) below_trans [OF is_ub_thelub])
    1.53  done
    1.54  
    1.55  text {* admissibility and compactness *}
    1.56  
    1.57 -lemma adm_compact_not_less: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
    1.58 +lemma adm_compact_not_below: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
    1.59  unfolding compact_def by (rule adm_subst)
    1.60  
    1.61  lemma adm_neq_compact: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
    1.62 -by (simp add: po_eq_conv adm_imp adm_not_less adm_compact_not_less)
    1.63 +by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
    1.64  
    1.65  lemma adm_compact_neq: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
    1.66 -by (simp add: po_eq_conv adm_imp adm_not_less adm_compact_not_less)
    1.67 +by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
    1.68  
    1.69  lemma compact_UU [simp, intro]: "compact \<bottom>"
    1.70  by (rule compactI, simp add: adm_not_free)
    1.71 @@ -210,7 +210,7 @@
    1.72  
    1.73  lemmas adm_lemmas [simp] =
    1.74    adm_not_free adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
    1.75 -  adm_less adm_eq adm_not_less
    1.76 -  adm_compact_not_less adm_compact_neq adm_neq_compact adm_not_UU
    1.77 +  adm_below adm_eq adm_not_below
    1.78 +  adm_compact_not_below adm_compact_neq adm_neq_compact adm_not_UU
    1.79  
    1.80  end
     2.1 --- a/src/HOLCF/Algebraic.thy	Fri May 08 19:28:11 2009 +0100
     2.2 +++ b/src/HOLCF/Algebraic.thy	Fri May 08 16:19:51 2009 -0700
     2.3 @@ -33,21 +33,21 @@
     2.4  
     2.5  locale pre_deflation =
     2.6    fixes f :: "'a \<rightarrow> 'a::cpo"
     2.7 -  assumes less: "\<And>x. f\<cdot>x \<sqsubseteq> x"
     2.8 +  assumes below: "\<And>x. f\<cdot>x \<sqsubseteq> x"
     2.9    assumes finite_range: "finite (range (\<lambda>x. f\<cdot>x))"
    2.10  begin
    2.11  
    2.12 -lemma iterate_less: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
    2.13 -by (induct i, simp_all add: trans_less [OF less])
    2.14 +lemma iterate_below: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
    2.15 +by (induct i, simp_all add: below_trans [OF below])
    2.16  
    2.17  lemma iterate_fixed: "f\<cdot>x = x \<Longrightarrow> iterate i\<cdot>f\<cdot>x = x"
    2.18  by (induct i, simp_all)
    2.19  
    2.20  lemma antichain_iterate_app: "i \<le> j \<Longrightarrow> iterate j\<cdot>f\<cdot>x \<sqsubseteq> iterate i\<cdot>f\<cdot>x"
    2.21  apply (erule le_Suc_induct)
    2.22 -apply (simp add: less)
    2.23 -apply (rule refl_less)
    2.24 -apply (erule (1) trans_less)
    2.25 +apply (simp add: below)
    2.26 +apply (rule below_refl)
    2.27 +apply (erule (1) below_trans)
    2.28  done
    2.29  
    2.30  lemma finite_range_iterate_app: "finite (range (\<lambda>i. iterate i\<cdot>f\<cdot>x))"
    2.31 @@ -144,7 +144,7 @@
    2.32  next
    2.33    fix x :: 'a
    2.34    show "d\<cdot>x \<sqsubseteq> x"
    2.35 -    by (rule MOST_d, simp add: iterate_less)
    2.36 +    by (rule MOST_d, simp add: iterate_below)
    2.37  next
    2.38    from finite_range
    2.39    have "finite {x. f\<cdot>x = x}"
    2.40 @@ -163,7 +163,7 @@
    2.41    interpret d: finite_deflation d by fact
    2.42    fix x
    2.43    show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
    2.44 -    by (simp, rule trans_less [OF d.less f])
    2.45 +    by (simp, rule below_trans [OF d.below f])
    2.46    show "finite (range (\<lambda>x. (d oo f)\<cdot>x))"
    2.47      by (rule finite_subset [OF _ d.finite_range], auto)
    2.48  qed
    2.49 @@ -185,9 +185,9 @@
    2.50      apply safe
    2.51      apply (erule subst)
    2.52      apply (rule d.idem)
    2.53 -    apply (rule antisym_less)
    2.54 +    apply (rule below_antisym)
    2.55      apply (rule f)
    2.56 -    apply (erule subst, rule d.less)
    2.57 +    apply (erule subst, rule d.below)
    2.58      apply simp
    2.59      done
    2.60  qed
    2.61 @@ -199,18 +199,17 @@
    2.62  typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
    2.63  by (fast intro: finite_deflation_approx)
    2.64  
    2.65 -instantiation fin_defl :: (profinite) sq_ord
    2.66 +instantiation fin_defl :: (profinite) below
    2.67  begin
    2.68  
    2.69 -definition
    2.70 -  sq_le_fin_defl_def:
    2.71 +definition below_fin_defl_def:
    2.72      "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
    2.73  
    2.74  instance ..
    2.75  end
    2.76  
    2.77  instance fin_defl :: (profinite) po
    2.78 -by (rule typedef_po [OF type_definition_fin_defl sq_le_fin_defl_def])
    2.79 +by (rule typedef_po [OF type_definition_fin_defl below_fin_defl_def])
    2.80  
    2.81  lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
    2.82  using Rep_fin_defl by simp
    2.83 @@ -218,27 +217,27 @@
    2.84  interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
    2.85  by (rule finite_deflation_Rep_fin_defl)
    2.86  
    2.87 -lemma fin_defl_lessI:
    2.88 +lemma fin_defl_belowI:
    2.89    "(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
    2.90 -unfolding sq_le_fin_defl_def
    2.91 -by (rule Rep_fin_defl.lessI)
    2.92 +unfolding below_fin_defl_def
    2.93 +by (rule Rep_fin_defl.belowI)
    2.94  
    2.95 -lemma fin_defl_lessD:
    2.96 +lemma fin_defl_belowD:
    2.97    "\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x"
    2.98 -unfolding sq_le_fin_defl_def
    2.99 -by (rule Rep_fin_defl.lessD)
   2.100 +unfolding below_fin_defl_def
   2.101 +by (rule Rep_fin_defl.belowD)
   2.102  
   2.103  lemma fin_defl_eqI:
   2.104    "(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
   2.105 -apply (rule antisym_less)
   2.106 -apply (rule fin_defl_lessI, simp)
   2.107 -apply (rule fin_defl_lessI, simp)
   2.108 +apply (rule below_antisym)
   2.109 +apply (rule fin_defl_belowI, simp)
   2.110 +apply (rule fin_defl_belowI, simp)
   2.111  done
   2.112  
   2.113  lemma Abs_fin_defl_mono:
   2.114    "\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk>
   2.115      \<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
   2.116 -unfolding sq_le_fin_defl_def
   2.117 +unfolding below_fin_defl_def
   2.118  by (simp add: Abs_fin_defl_inverse)
   2.119  
   2.120  
   2.121 @@ -257,7 +256,7 @@
   2.122  apply (rule pre_deflation.finite_deflation_d)
   2.123  apply (rule pre_deflation_d_f)
   2.124  apply (rule finite_deflation_approx)
   2.125 -apply (rule Rep_fin_defl.less)
   2.126 +apply (rule Rep_fin_defl.below)
   2.127  done
   2.128  
   2.129  lemma fd_take_fixed_iff:
   2.130 @@ -265,10 +264,10 @@
   2.131      approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
   2.132  unfolding Rep_fin_defl_fd_take
   2.133  by (rule eventual_iterate_oo_fixed_iff
   2.134 -    [OF finite_deflation_approx Rep_fin_defl.less])
   2.135 +    [OF finite_deflation_approx Rep_fin_defl.below])
   2.136  
   2.137 -lemma fd_take_less: "fd_take n d \<sqsubseteq> d"
   2.138 -apply (rule fin_defl_lessI)
   2.139 +lemma fd_take_below: "fd_take n d \<sqsubseteq> d"
   2.140 +apply (rule fin_defl_belowI)
   2.141  apply (simp add: fd_take_fixed_iff)
   2.142  done
   2.143  
   2.144 @@ -278,16 +277,16 @@
   2.145  done
   2.146  
   2.147  lemma fd_take_mono: "a \<sqsubseteq> b \<Longrightarrow> fd_take n a \<sqsubseteq> fd_take n b"
   2.148 -apply (rule fin_defl_lessI)
   2.149 +apply (rule fin_defl_belowI)
   2.150  apply (simp add: fd_take_fixed_iff)
   2.151 -apply (simp add: fin_defl_lessD)
   2.152 +apply (simp add: fin_defl_belowD)
   2.153  done
   2.154  
   2.155  lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> approx j\<cdot>x = x"
   2.156  by (erule subst, simp add: min_def)
   2.157  
   2.158  lemma fd_take_chain: "m \<le> n \<Longrightarrow> fd_take m a \<sqsubseteq> fd_take n a"
   2.159 -apply (rule fin_defl_lessI)
   2.160 +apply (rule fin_defl_belowI)
   2.161  apply (simp add: fd_take_fixed_iff)
   2.162  apply (simp add: approx_fixed_le_lemma)
   2.163  done
   2.164 @@ -304,9 +303,9 @@
   2.165  lemma fd_take_covers: "\<exists>n. fd_take n a = a"
   2.166  apply (rule_tac x=
   2.167    "Max ((\<lambda>x. LEAST n. approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
   2.168 -apply (rule antisym_less)
   2.169 -apply (rule fd_take_less)
   2.170 -apply (rule fin_defl_lessI)
   2.171 +apply (rule below_antisym)
   2.172 +apply (rule fd_take_below)
   2.173 +apply (rule fin_defl_belowI)
   2.174  apply (simp add: fd_take_fixed_iff)
   2.175  apply (rule approx_fixed_le_lemma)
   2.176  apply (rule Max_ge)
   2.177 @@ -320,9 +319,9 @@
   2.178  apply (rule Rep_fin_defl.compact)
   2.179  done
   2.180  
   2.181 -interpretation fin_defl: basis_take sq_le fd_take
   2.182 +interpretation fin_defl: basis_take below fd_take
   2.183  apply default
   2.184 -apply (rule fd_take_less)
   2.185 +apply (rule fd_take_below)
   2.186  apply (rule fd_take_idem)
   2.187  apply (erule fd_take_mono)
   2.188  apply (rule fd_take_chain, simp)
   2.189 @@ -333,10 +332,10 @@
   2.190  subsection {* Defining algebraic deflations by ideal completion *}
   2.191  
   2.192  typedef (open) 'a alg_defl =
   2.193 -  "{S::'a fin_defl set. sq_le.ideal S}"
   2.194 -by (fast intro: sq_le.ideal_principal)
   2.195 +  "{S::'a fin_defl set. below.ideal S}"
   2.196 +by (fast intro: below.ideal_principal)
   2.197  
   2.198 -instantiation alg_defl :: (profinite) sq_ord
   2.199 +instantiation alg_defl :: (profinite) below
   2.200  begin
   2.201  
   2.202  definition
   2.203 @@ -346,19 +345,19 @@
   2.204  end
   2.205  
   2.206  instance alg_defl :: (profinite) po
   2.207 -by (rule sq_le.typedef_ideal_po
   2.208 -    [OF type_definition_alg_defl sq_le_alg_defl_def])
   2.209 +by (rule below.typedef_ideal_po
   2.210 +    [OF type_definition_alg_defl below_alg_defl_def])
   2.211  
   2.212  instance alg_defl :: (profinite) cpo
   2.213 -by (rule sq_le.typedef_ideal_cpo
   2.214 -    [OF type_definition_alg_defl sq_le_alg_defl_def])
   2.215 +by (rule below.typedef_ideal_cpo
   2.216 +    [OF type_definition_alg_defl below_alg_defl_def])
   2.217  
   2.218  lemma Rep_alg_defl_lub:
   2.219    "chain Y \<Longrightarrow> Rep_alg_defl (\<Squnion>i. Y i) = (\<Union>i. Rep_alg_defl (Y i))"
   2.220 -by (rule sq_le.typedef_ideal_rep_contlub
   2.221 -    [OF type_definition_alg_defl sq_le_alg_defl_def])
   2.222 +by (rule below.typedef_ideal_rep_contlub
   2.223 +    [OF type_definition_alg_defl below_alg_defl_def])
   2.224  
   2.225 -lemma ideal_Rep_alg_defl: "sq_le.ideal (Rep_alg_defl xs)"
   2.226 +lemma ideal_Rep_alg_defl: "below.ideal (Rep_alg_defl xs)"
   2.227  by (rule Rep_alg_defl [unfolded mem_Collect_eq])
   2.228  
   2.229  definition
   2.230 @@ -368,15 +367,15 @@
   2.231  lemma Rep_alg_defl_principal:
   2.232    "Rep_alg_defl (alg_defl_principal t) = {u. u \<sqsubseteq> t}"
   2.233  unfolding alg_defl_principal_def
   2.234 -by (simp add: Abs_alg_defl_inverse sq_le.ideal_principal)
   2.235 +by (simp add: Abs_alg_defl_inverse below.ideal_principal)
   2.236  
   2.237  interpretation alg_defl:
   2.238 -  ideal_completion sq_le fd_take alg_defl_principal Rep_alg_defl
   2.239 +  ideal_completion below fd_take alg_defl_principal Rep_alg_defl
   2.240  apply default
   2.241  apply (rule ideal_Rep_alg_defl)
   2.242  apply (erule Rep_alg_defl_lub)
   2.243  apply (rule Rep_alg_defl_principal)
   2.244 -apply (simp only: sq_le_alg_defl_def)
   2.245 +apply (simp only: below_alg_defl_def)
   2.246  done
   2.247  
   2.248  text {* Algebraic deflations are pointed *}
   2.249 @@ -443,7 +442,7 @@
   2.250    "cast\<cdot>(alg_defl_principal a) = Rep_fin_defl a"
   2.251  unfolding cast_def
   2.252  apply (rule alg_defl.basis_fun_principal)
   2.253 -apply (simp only: sq_le_fin_defl_def)
   2.254 +apply (simp only: below_fin_defl_def)
   2.255  done
   2.256  
   2.257  lemma deflation_cast: "deflation (cast\<cdot>d)"
   2.258 @@ -522,10 +521,10 @@
   2.259      apply (rule finite_deflation_p_d_e)
   2.260      apply (rule finite_deflation_cast)
   2.261      apply (rule compact_approx)
   2.262 -    apply (rule sq_ord_less_eq_trans [OF _ d])
   2.263 +    apply (rule below_eq_trans [OF _ d])
   2.264      apply (rule monofun_cfun_fun)
   2.265      apply (rule monofun_cfun_arg)
   2.266 -    apply (rule approx_less)
   2.267 +    apply (rule approx_below)
   2.268      done
   2.269    show "(\<Squnion>i. ?a i) = ID"
   2.270      apply (rule ext_cfun, simp)
     3.1 --- a/src/HOLCF/Bifinite.thy	Fri May 08 19:28:11 2009 +0100
     3.2 +++ b/src/HOLCF/Bifinite.thy	Fri May 08 16:19:51 2009 -0700
     3.3 @@ -19,7 +19,7 @@
     3.4  
     3.5  class bifinite = profinite + pcpo
     3.6  
     3.7 -lemma approx_less: "approx i\<cdot>x \<sqsubseteq> x"
     3.8 +lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
     3.9  proof -
    3.10    have "chain (\<lambda>i. approx i\<cdot>x)" by simp
    3.11    hence "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by (rule is_ub_thelub)
    3.12 @@ -32,7 +32,7 @@
    3.13    show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    3.14      by (rule approx_idem)
    3.15    show "approx i\<cdot>x \<sqsubseteq> x"
    3.16 -    by (rule approx_less)
    3.17 +    by (rule approx_below)
    3.18    show "finite {x. approx i\<cdot>x = x}"
    3.19      by (rule finite_fixes_approx)
    3.20  qed
    3.21 @@ -49,17 +49,17 @@
    3.22  by (rule ext_cfun, simp add: contlub_cfun_fun)
    3.23  
    3.24  lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>"
    3.25 -by (rule UU_I, rule approx_less)
    3.26 +by (rule UU_I, rule approx_below)
    3.27  
    3.28  lemma approx_approx1:
    3.29    "i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>x"
    3.30 -apply (rule deflation_less_comp1 [OF deflation_approx deflation_approx])
    3.31 +apply (rule deflation_below_comp1 [OF deflation_approx deflation_approx])
    3.32  apply (erule chain_mono [OF chain_approx])
    3.33  done
    3.34  
    3.35  lemma approx_approx2:
    3.36    "j \<le> i \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx j\<cdot>x"
    3.37 -apply (rule deflation_less_comp2 [OF deflation_approx deflation_approx])
    3.38 +apply (rule deflation_below_comp2 [OF deflation_approx deflation_approx])
    3.39  apply (erule chain_mono [OF chain_approx])
    3.40  done
    3.41  
    3.42 @@ -99,7 +99,7 @@
    3.43    thus "P x" by simp
    3.44  qed
    3.45  
    3.46 -lemma profinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
    3.47 +lemma profinite_below_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
    3.48  apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
    3.49  apply (rule lub_mono, simp, simp, simp)
    3.50  done
     4.1 --- a/src/HOLCF/Cfun.thy	Fri May 08 19:28:11 2009 +0100
     4.2 +++ b/src/HOLCF/Cfun.thy	Fri May 08 16:19:51 2009 -0700
     4.3 @@ -105,19 +105,19 @@
     4.4  by (rule typedef_finite_po [OF type_definition_CFun])
     4.5  
     4.6  instance "->" :: (finite_po, chfin) chfin
     4.7 -by (rule typedef_chfin [OF type_definition_CFun less_CFun_def])
     4.8 +by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
     4.9  
    4.10  instance "->" :: (cpo, discrete_cpo) discrete_cpo
    4.11 -by intro_classes (simp add: less_CFun_def Rep_CFun_inject)
    4.12 +by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
    4.13  
    4.14  instance "->" :: (cpo, pcpo) pcpo
    4.15 -by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun])
    4.16 +by (rule typedef_pcpo [OF type_definition_CFun below_CFun_def UU_CFun])
    4.17  
    4.18  lemmas Rep_CFun_strict =
    4.19 -  typedef_Rep_strict [OF type_definition_CFun less_CFun_def UU_CFun]
    4.20 +  typedef_Rep_strict [OF type_definition_CFun below_CFun_def UU_CFun]
    4.21  
    4.22  lemmas Abs_CFun_strict =
    4.23 -  typedef_Abs_strict [OF type_definition_CFun less_CFun_def UU_CFun]
    4.24 +  typedef_Abs_strict [OF type_definition_CFun below_CFun_def UU_CFun]
    4.25  
    4.26  text {* function application is strict in its first argument *}
    4.27  
    4.28 @@ -153,11 +153,11 @@
    4.29  
    4.30  text {* Extensionality wrt. ordering for continuous functions *}
    4.31  
    4.32 -lemma expand_cfun_less: "f \<sqsubseteq> g = (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
    4.33 -by (simp add: less_CFun_def expand_fun_less)
    4.34 +lemma expand_cfun_below: "f \<sqsubseteq> g = (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
    4.35 +by (simp add: below_CFun_def expand_fun_below)
    4.36  
    4.37 -lemma less_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
    4.38 -by (simp add: expand_cfun_less)
    4.39 +lemma below_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
    4.40 +by (simp add: expand_cfun_below)
    4.41  
    4.42  text {* Congruence for continuous function application *}
    4.43  
    4.44 @@ -205,13 +205,13 @@
    4.45  text {* monotonicity of application *}
    4.46  
    4.47  lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
    4.48 -by (simp add: expand_cfun_less)
    4.49 +by (simp add: expand_cfun_below)
    4.50  
    4.51  lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
    4.52  by (rule monofun_Rep_CFun2 [THEN monofunE])
    4.53  
    4.54  lemma monofun_cfun: "\<lbrakk>f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y"
    4.55 -by (rule trans_less [OF monofun_cfun_fun monofun_cfun_arg])
    4.56 +by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])
    4.57  
    4.58  text {* ch2ch - rules for the type @{typ "'a -> 'b"} *}
    4.59  
    4.60 @@ -230,7 +230,7 @@
    4.61  
    4.62  lemma ch2ch_LAM [simp]:
    4.63    "\<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)"
    4.64 -by (simp add: chain_def expand_cfun_less)
    4.65 +by (simp add: chain_def expand_cfun_below)
    4.66  
    4.67  text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
    4.68  
    4.69 @@ -316,7 +316,7 @@
    4.70  lemma cont2mono_LAM:
    4.71    "\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
    4.72      \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
    4.73 -  unfolding monofun_def expand_cfun_less by simp
    4.74 +  unfolding monofun_def expand_cfun_below by simp
    4.75  
    4.76  text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
    4.77  
    4.78 @@ -365,7 +365,7 @@
    4.79  
    4.80  lemma semi_monofun_Abs_CFun:
    4.81    "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_CFun f \<sqsubseteq> Abs_CFun g"
    4.82 -by (simp add: less_CFun_def Abs_CFun_inverse2)
    4.83 +by (simp add: below_CFun_def Abs_CFun_inverse2)
    4.84  
    4.85  text {* some lemmata for functions with flat/chfin domain/range types *}
    4.86  
    4.87 @@ -401,7 +401,7 @@
    4.88  apply simp
    4.89  done
    4.90  
    4.91 -lemma injection_less:
    4.92 +lemma injection_below:
    4.93    "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x \<sqsubseteq> g\<cdot>y) = (x \<sqsubseteq> y)"
    4.94  apply (rule iffI)
    4.95  apply (drule_tac f=f in monofun_cfun_arg)
     5.1 --- a/src/HOLCF/CompactBasis.thy	Fri May 08 19:28:11 2009 +0100
     5.2 +++ b/src/HOLCF/CompactBasis.thy	Fri May 08 16:19:51 2009 -0700
     5.3 @@ -18,7 +18,7 @@
     5.4  lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
     5.5  by (rule Rep_compact_basis [unfolded mem_Collect_eq])
     5.6  
     5.7 -instantiation compact_basis :: (profinite) sq_ord
     5.8 +instantiation compact_basis :: (profinite) below
     5.9  begin
    5.10  
    5.11  definition
    5.12 @@ -47,12 +47,12 @@
    5.13  lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
    5.14  
    5.15  interpretation compact_basis:
    5.16 -  basis_take sq_le compact_take
    5.17 +  basis_take below compact_take
    5.18  proof
    5.19    fix n :: nat and a :: "'a compact_basis"
    5.20    show "compact_take n a \<sqsubseteq> a"
    5.21      unfolding compact_le_def
    5.22 -    by (simp add: Rep_compact_take approx_less)
    5.23 +    by (simp add: Rep_compact_take approx_below)
    5.24  next
    5.25    fix n :: nat and a :: "'a compact_basis"
    5.26    show "compact_take n (compact_take n a) = compact_take n a"
    5.27 @@ -93,15 +93,15 @@
    5.28    "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
    5.29  
    5.30  interpretation compact_basis:
    5.31 -  ideal_completion sq_le compact_take Rep_compact_basis approximants
    5.32 +  ideal_completion below compact_take Rep_compact_basis approximants
    5.33  proof
    5.34    fix w :: 'a
    5.35 -  show "preorder.ideal sq_le (approximants w)"
    5.36 -  proof (rule sq_le.idealI)
    5.37 +  show "preorder.ideal below (approximants w)"
    5.38 +  proof (rule below.idealI)
    5.39      show "\<exists>x. x \<in> approximants w"
    5.40        unfolding approximants_def
    5.41        apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
    5.42 -      apply (simp add: Abs_compact_basis_inverse approx_less)
    5.43 +      apply (simp add: Abs_compact_basis_inverse approx_below)
    5.44        done
    5.45    next
    5.46      fix x y :: "'a compact_basis"
    5.47 @@ -116,7 +116,7 @@
    5.48        apply (clarify, rename_tac i j)
    5.49        apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
    5.50        apply (simp add: compact_le_def)
    5.51 -      apply (simp add: Abs_compact_basis_inverse approx_less)
    5.52 +      apply (simp add: Abs_compact_basis_inverse approx_below)
    5.53        apply (erule subst, erule subst)
    5.54        apply (simp add: monofun_cfun chain_mono [OF chain_approx])
    5.55        done
    5.56 @@ -126,7 +126,7 @@
    5.57        unfolding approximants_def
    5.58        apply simp
    5.59        apply (simp add: compact_le_def)
    5.60 -      apply (erule (1) trans_less)
    5.61 +      apply (erule (1) below_trans)
    5.62        done
    5.63    qed
    5.64  next
    5.65 @@ -136,7 +136,7 @@
    5.66      unfolding approximants_def
    5.67      apply safe
    5.68      apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
    5.69 -    apply (erule trans_less, rule is_ub_thelub [OF Y])
    5.70 +    apply (erule below_trans, rule is_ub_thelub [OF Y])
    5.71      done
    5.72  next
    5.73    fix a :: "'a compact_basis"
    5.74 @@ -148,7 +148,7 @@
    5.75      apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
    5.76      apply (rule admD, simp, simp)
    5.77      apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
    5.78 -    apply (simp add: approximants_def Abs_compact_basis_inverse approx_less)
    5.79 +    apply (simp add: approximants_def Abs_compact_basis_inverse approx_below)
    5.80      apply (simp add: approximants_def Abs_compact_basis_inverse)
    5.81      done
    5.82  qed
    5.83 @@ -288,7 +288,7 @@
    5.84  apply (cut_tac a=a in compact_basis.take_covers)
    5.85  apply (clarify, rule_tac x=n in exI)
    5.86  apply (clarify, simp)
    5.87 -apply (rule antisym_less)
    5.88 +apply (rule below_antisym)
    5.89  apply (rule compact_basis.take_less)
    5.90  apply (drule_tac a=a in compact_basis.take_chain_le)
    5.91  apply simp
     6.1 --- a/src/HOLCF/Completion.thy	Fri May 08 19:28:11 2009 +0100
     6.2 +++ b/src/HOLCF/Completion.thy	Fri May 08 16:19:51 2009 -0700
     6.3 @@ -108,11 +108,11 @@
     6.4  done
     6.5  
     6.6  lemma typedef_ideal_po:
     6.7 -  fixes Abs :: "'a set \<Rightarrow> 'b::sq_ord"
     6.8 +  fixes Abs :: "'a set \<Rightarrow> 'b::below"
     6.9    assumes type: "type_definition Rep Abs {S. ideal S}"
    6.10 -  assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
    6.11 +  assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
    6.12    shows "OFCLASS('b, po_class)"
    6.13 - apply (intro_classes, unfold less)
    6.14 + apply (intro_classes, unfold below)
    6.15     apply (rule subset_refl)
    6.16    apply (erule (1) subset_trans)
    6.17   apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
    6.18 @@ -122,7 +122,7 @@
    6.19  lemma
    6.20    fixes Abs :: "'a set \<Rightarrow> 'b::po"
    6.21    assumes type: "type_definition Rep Abs {S. ideal S}"
    6.22 -  assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
    6.23 +  assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
    6.24    assumes S: "chain S"
    6.25    shows typedef_ideal_lub: "range S <<| Abs (\<Union>i. Rep (S i))"
    6.26      and typedef_ideal_rep_contlub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
    6.27 @@ -130,7 +130,7 @@
    6.28    have 1: "ideal (\<Union>i. Rep (S i))"
    6.29      apply (rule ideal_UN)
    6.30       apply (rule type_definition.Rep [OF type, unfolded mem_Collect_eq])
    6.31 -    apply (subst less [symmetric])
    6.32 +    apply (subst below [symmetric])
    6.33      apply (erule chain_mono [OF S])
    6.34      done
    6.35    hence 2: "Rep (Abs (\<Union>i. Rep (S i))) = (\<Union>i. Rep (S i))"
    6.36 @@ -138,8 +138,8 @@
    6.37    show 3: "range S <<| Abs (\<Union>i. Rep (S i))"
    6.38      apply (rule is_lubI)
    6.39       apply (rule is_ubI)
    6.40 -     apply (simp add: less 2, fast)
    6.41 -    apply (simp add: less 2 is_ub_def, fast)
    6.42 +     apply (simp add: below 2, fast)
    6.43 +    apply (simp add: below 2 is_ub_def, fast)
    6.44      done
    6.45    hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))"
    6.46      by (rule thelubI)
    6.47 @@ -150,16 +150,16 @@
    6.48  lemma typedef_ideal_cpo:
    6.49    fixes Abs :: "'a set \<Rightarrow> 'b::po"
    6.50    assumes type: "type_definition Rep Abs {S. ideal S}"
    6.51 -  assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
    6.52 +  assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
    6.53    shows "OFCLASS('b, cpo_class)"
    6.54 -by (default, rule exI, erule typedef_ideal_lub [OF type less])
    6.55 +by (default, rule exI, erule typedef_ideal_lub [OF type below])
    6.56  
    6.57  end
    6.58  
    6.59 -interpretation sq_le: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
    6.60 +interpretation below: preorder "below :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
    6.61  apply unfold_locales
    6.62 -apply (rule refl_less)
    6.63 -apply (erule (1) trans_less)
    6.64 +apply (rule below_refl)
    6.65 +apply (erule (1) below_trans)
    6.66  done
    6.67  
    6.68  subsection {* Lemmas about least upper bounds *}
    6.69 @@ -229,43 +229,43 @@
    6.70  apply (rule subsetI, rule UN_I [where a=0], simp_all)
    6.71  done
    6.72  
    6.73 -lemma less_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
    6.74 +lemma below_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
    6.75  by (rule iffI [OF rep_mono subset_repD])
    6.76  
    6.77  lemma rep_eq: "rep x = {a. principal a \<sqsubseteq> x}"
    6.78 -unfolding less_def rep_principal
    6.79 +unfolding below_def rep_principal
    6.80  apply safe
    6.81  apply (erule (1) idealD3 [OF ideal_rep])
    6.82  apply (erule subsetD, simp add: r_refl)
    6.83  done
    6.84  
    6.85 -lemma mem_rep_iff_principal_less: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
    6.86 +lemma mem_rep_iff_principal_below: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
    6.87  by (simp add: rep_eq)
    6.88  
    6.89 -lemma principal_less_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
    6.90 +lemma principal_below_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
    6.91  by (simp add: rep_eq)
    6.92  
    6.93 -lemma principal_less_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
    6.94 -by (simp add: principal_less_iff_mem_rep rep_principal)
    6.95 +lemma principal_below_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
    6.96 +by (simp add: principal_below_iff_mem_rep rep_principal)
    6.97  
    6.98  lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> a \<preceq> b \<and> b \<preceq> a"
    6.99 -unfolding po_eq_conv [where 'a='b] principal_less_iff ..
   6.100 +unfolding po_eq_conv [where 'a='b] principal_below_iff ..
   6.101  
   6.102  lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
   6.103  by (simp add: rep_eq)
   6.104  
   6.105  lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b"
   6.106 -by (simp only: principal_less_iff)
   6.107 +by (simp only: principal_below_iff)
   6.108  
   6.109 -lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
   6.110 -unfolding principal_less_iff_mem_rep
   6.111 -by (simp add: less_def subset_eq)
   6.112 +lemma belowI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
   6.113 +unfolding principal_below_iff_mem_rep
   6.114 +by (simp add: below_def subset_eq)
   6.115  
   6.116  lemma lub_principal_rep: "principal ` rep x <<| x"
   6.117  apply (rule is_lubI)
   6.118  apply (rule ub_imageI)
   6.119  apply (erule repD)
   6.120 -apply (subst less_def)
   6.121 +apply (subst below_def)
   6.122  apply (rule subsetI)
   6.123  apply (drule (1) ub_imageD)
   6.124  apply (simp add: rep_eq)
   6.125 @@ -299,7 +299,7 @@
   6.126   apply (rule is_lub_thelub0)
   6.127    apply (rule basis_fun_lemma0, erule f_mono)
   6.128   apply (rule is_ubI, clarsimp, rename_tac a)
   6.129 - apply (rule trans_less [OF f_mono [OF take_chain]])
   6.130 + apply (rule below_trans [OF f_mono [OF take_chain]])
   6.131   apply (rule is_ub_thelub0)
   6.132    apply (rule basis_fun_lemma0, erule f_mono)
   6.133   apply simp
   6.134 @@ -313,7 +313,7 @@
   6.135   apply (rule ub_imageI, rename_tac a)
   6.136    apply (cut_tac a=a in take_covers, erule exE, rename_tac i)
   6.137    apply (erule subst)
   6.138 -  apply (rule rev_trans_less)
   6.139 +  apply (rule rev_below_trans)
   6.140     apply (rule_tac x=i in is_ub_thelub)
   6.141     apply (rule basis_fun_lemma1, erule f_mono)
   6.142    apply (rule is_ub_thelub0)
   6.143 @@ -324,7 +324,7 @@
   6.144   apply (rule is_lub_thelub0)
   6.145    apply (rule basis_fun_lemma0, erule f_mono)
   6.146   apply (rule is_ubI, clarsimp, rename_tac a)
   6.147 - apply (rule trans_less [OF f_mono [OF take_less]])
   6.148 + apply (rule below_trans [OF f_mono [OF take_less]])
   6.149   apply (erule (1) ub_imageD)
   6.150  done
   6.151  
   6.152 @@ -350,7 +350,7 @@
   6.153       apply (erule (1) subsetD [OF rep_mono])
   6.154      apply (rule is_lub_thelub0 [OF lub ub_imageI])
   6.155      apply (simp add: rep_contlub, clarify)
   6.156 -    apply (erule rev_trans_less [OF is_ub_thelub])
   6.157 +    apply (erule rev_below_trans [OF is_ub_thelub])
   6.158      apply (erule is_ub_thelub0 [OF lub imageI])
   6.159      done
   6.160  qed
   6.161 @@ -367,21 +367,21 @@
   6.162  lemma basis_fun_mono:
   6.163    assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   6.164    assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
   6.165 -  assumes less: "\<And>a. f a \<sqsubseteq> g a"
   6.166 +  assumes below: "\<And>a. f a \<sqsubseteq> g a"
   6.167    shows "basis_fun f \<sqsubseteq> basis_fun g"
   6.168 - apply (rule less_cfun_ext)
   6.169 + apply (rule below_cfun_ext)
   6.170   apply (simp only: basis_fun_beta f_mono g_mono)
   6.171   apply (rule is_lub_thelub0)
   6.172    apply (rule basis_fun_lemma, erule f_mono)
   6.173   apply (rule ub_imageI, rename_tac a)
   6.174 - apply (rule trans_less [OF less])
   6.175 + apply (rule below_trans [OF below])
   6.176   apply (rule is_ub_thelub0)
   6.177    apply (rule basis_fun_lemma, erule g_mono)
   6.178   apply (erule imageI)
   6.179  done
   6.180  
   6.181  lemma compact_principal [simp]: "compact (principal a)"
   6.182 -by (rule compactI2, simp add: principal_less_iff_mem_rep rep_contlub)
   6.183 +by (rule compactI2, simp add: principal_below_iff_mem_rep rep_contlub)
   6.184  
   6.185  subsection {* Bifiniteness of ideal completions *}
   6.186  
     7.1 --- a/src/HOLCF/Cont.thy	Fri May 08 19:28:11 2009 +0100
     7.2 +++ b/src/HOLCF/Cont.thy	Fri May 08 16:19:51 2009 -0700
     7.3 @@ -121,14 +121,14 @@
     7.4  
     7.5  lemma contI2:
     7.6    assumes mono: "monofun f"
     7.7 -  assumes less: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
     7.8 +  assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
     7.9       \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
    7.10    shows "cont f"
    7.11  apply (rule monocontlub2cont)
    7.12  apply (rule mono)
    7.13  apply (rule contlubI)
    7.14 -apply (rule antisym_less)
    7.15 -apply (rule less, assumption)
    7.16 +apply (rule below_antisym)
    7.17 +apply (rule below, assumption)
    7.18  apply (erule ch2ch_monofun [OF mono])
    7.19  apply (rule is_lub_thelub)
    7.20  apply (erule ch2ch_monofun [OF mono])
    7.21 @@ -192,7 +192,7 @@
    7.22      by (auto intro: cont2monofunE [OF 1]
    7.23                      cont2monofunE [OF 2]
    7.24                      cont2monofunE [OF 3]
    7.25 -                    trans_less)
    7.26 +                    below_trans)
    7.27  next
    7.28    fix Y :: "nat \<Rightarrow> 'a" assume "chain Y"
    7.29    then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) = (\<Squnion>i. f (Y i) (t (Y i)))"
     8.1 --- a/src/HOLCF/ConvexPD.thy	Fri May 08 19:28:11 2009 +0100
     8.2 +++ b/src/HOLCF/ConvexPD.thy	Fri May 08 16:19:51 2009 -0700
     8.3 @@ -144,7 +144,7 @@
     8.4    "{S::'a pd_basis set. convex_le.ideal S}"
     8.5  by (fast intro: convex_le.ideal_principal)
     8.6  
     8.7 -instantiation convex_pd :: (profinite) sq_ord
     8.8 +instantiation convex_pd :: (profinite) below
     8.9  begin
    8.10  
    8.11  definition
    8.12 @@ -155,16 +155,16 @@
    8.13  
    8.14  instance convex_pd :: (profinite) po
    8.15  by (rule convex_le.typedef_ideal_po
    8.16 -    [OF type_definition_convex_pd sq_le_convex_pd_def])
    8.17 +    [OF type_definition_convex_pd below_convex_pd_def])
    8.18  
    8.19  instance convex_pd :: (profinite) cpo
    8.20  by (rule convex_le.typedef_ideal_cpo
    8.21 -    [OF type_definition_convex_pd sq_le_convex_pd_def])
    8.22 +    [OF type_definition_convex_pd below_convex_pd_def])
    8.23  
    8.24  lemma Rep_convex_pd_lub:
    8.25    "chain Y \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_convex_pd (Y i))"
    8.26  by (rule convex_le.typedef_ideal_rep_contlub
    8.27 -    [OF type_definition_convex_pd sq_le_convex_pd_def])
    8.28 +    [OF type_definition_convex_pd below_convex_pd_def])
    8.29  
    8.30  lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
    8.31  by (rule Rep_convex_pd [unfolded mem_Collect_eq])
    8.32 @@ -190,7 +190,7 @@
    8.33  apply (rule ideal_Rep_convex_pd)
    8.34  apply (erule Rep_convex_pd_lub)
    8.35  apply (rule Rep_convex_principal)
    8.36 -apply (simp only: sq_le_convex_pd_def)
    8.37 +apply (simp only: below_convex_pd_def)
    8.38  done
    8.39  
    8.40  text {* Convex powerdomain is pointed *}
    8.41 @@ -311,7 +311,7 @@
    8.42  lemmas convex_plus_aci =
    8.43    convex_plus_ac convex_plus_absorb convex_plus_left_absorb
    8.44  
    8.45 -lemma convex_unit_less_plus_iff [simp]:
    8.46 +lemma convex_unit_below_plus_iff [simp]:
    8.47    "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
    8.48   apply (rule iffI)
    8.49    apply (subgoal_tac
    8.50 @@ -329,7 +329,7 @@
    8.51   apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
    8.52  done
    8.53  
    8.54 -lemma convex_plus_less_unit_iff [simp]:
    8.55 +lemma convex_plus_below_unit_iff [simp]:
    8.56    "xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
    8.57   apply (rule iffI)
    8.58    apply (subgoal_tac
    8.59 @@ -347,9 +347,9 @@
    8.60   apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
    8.61  done
    8.62  
    8.63 -lemma convex_unit_less_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
    8.64 +lemma convex_unit_below_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
    8.65   apply (rule iffI)
    8.66 -  apply (rule profinite_less_ext)
    8.67 +  apply (rule profinite_below_ext)
    8.68    apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
    8.69    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
    8.70    apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
    8.71 @@ -433,12 +433,12 @@
    8.72  
    8.73  lemma monofun_LAM:
    8.74    "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
    8.75 -by (simp add: expand_cfun_less)
    8.76 +by (simp add: expand_cfun_below)
    8.77  
    8.78  lemma convex_bind_basis_mono:
    8.79    "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
    8.80  apply (erule convex_le_induct)
    8.81 -apply (erule (1) trans_less)
    8.82 +apply (erule (1) below_trans)
    8.83  apply (simp add: monofun_LAM monofun_cfun)
    8.84  apply (simp add: monofun_LAM monofun_cfun)
    8.85  done
    8.86 @@ -606,12 +606,12 @@
    8.87  
    8.88  text {* Ordering property *}
    8.89  
    8.90 -lemma convex_pd_less_iff:
    8.91 +lemma convex_pd_below_iff:
    8.92    "(xs \<sqsubseteq> ys) =
    8.93      (convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and>
    8.94       convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)"
    8.95   apply (safe elim!: monofun_cfun_arg)
    8.96 - apply (rule profinite_less_ext)
    8.97 + apply (rule profinite_below_ext)
    8.98   apply (drule_tac f="approx i" in monofun_cfun_arg)
    8.99   apply (drule_tac f="approx i" in monofun_cfun_arg)
   8.100   apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
   8.101 @@ -620,19 +620,19 @@
   8.102   apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
   8.103  done
   8.104  
   8.105 -lemmas convex_plus_less_plus_iff =
   8.106 -  convex_pd_less_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
   8.107 +lemmas convex_plus_below_plus_iff =
   8.108 +  convex_pd_below_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
   8.109  
   8.110 -lemmas convex_pd_less_simps =
   8.111 -  convex_unit_less_plus_iff
   8.112 -  convex_plus_less_unit_iff
   8.113 -  convex_plus_less_plus_iff
   8.114 -  convex_unit_less_iff
   8.115 +lemmas convex_pd_below_simps =
   8.116 +  convex_unit_below_plus_iff
   8.117 +  convex_plus_below_unit_iff
   8.118 +  convex_plus_below_plus_iff
   8.119 +  convex_unit_below_iff
   8.120    convex_to_upper_unit
   8.121    convex_to_upper_plus
   8.122    convex_to_lower_unit
   8.123    convex_to_lower_plus
   8.124 -  upper_pd_less_simps
   8.125 -  lower_pd_less_simps
   8.126 +  upper_pd_below_simps
   8.127 +  lower_pd_below_simps
   8.128  
   8.129  end
     9.1 --- a/src/HOLCF/Cprod.thy	Fri May 08 19:28:11 2009 +0100
     9.2 +++ b/src/HOLCF/Cprod.thy	Fri May 08 16:19:51 2009 -0700
     9.3 @@ -68,7 +68,7 @@
     9.4  lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')"
     9.5  by (simp add: cpair_eq_pair)
     9.6  
     9.7 -lemma cpair_less [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
     9.8 +lemma cpair_below [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
     9.9  by (simp add: cpair_eq_pair)
    9.10  
    9.11  lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
    9.12 @@ -107,23 +107,23 @@
    9.13  
    9.14  lemmas surjective_pairing_Cprod2 = cpair_cfst_csnd
    9.15  
    9.16 -lemma less_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
    9.17 -by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
    9.18 +lemma below_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
    9.19 +by (simp add: below_prod_def cfst_def csnd_def cont_fst cont_snd)
    9.20  
    9.21  lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
    9.22 -by (auto simp add: po_eq_conv less_cprod)
    9.23 +by (auto simp add: po_eq_conv below_cprod)
    9.24  
    9.25 -lemma cfst_less_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
    9.26 -by (simp add: less_cprod)
    9.27 +lemma cfst_below_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
    9.28 +by (simp add: below_cprod)
    9.29  
    9.30 -lemma csnd_less_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
    9.31 -by (simp add: less_cprod)
    9.32 +lemma csnd_below_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
    9.33 +by (simp add: below_cprod)
    9.34  
    9.35  lemma compact_cfst: "compact x \<Longrightarrow> compact (cfst\<cdot>x)"
    9.36 -by (rule compactI, simp add: cfst_less_iff)
    9.37 +by (rule compactI, simp add: cfst_below_iff)
    9.38  
    9.39  lemma compact_csnd: "compact x \<Longrightarrow> compact (csnd\<cdot>x)"
    9.40 -by (rule compactI, simp add: csnd_less_iff)
    9.41 +by (rule compactI, simp add: csnd_below_iff)
    9.42  
    9.43  lemma compact_cpair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
    9.44  by (simp add: cpair_eq_pair)
    10.1 --- a/src/HOLCF/Deflation.thy	Fri May 08 19:28:11 2009 +0100
    10.2 +++ b/src/HOLCF/Deflation.thy	Fri May 08 16:19:51 2009 -0700
    10.3 @@ -15,11 +15,11 @@
    10.4  locale deflation =
    10.5    fixes d :: "'a \<rightarrow> 'a"
    10.6    assumes idem: "\<And>x. d\<cdot>(d\<cdot>x) = d\<cdot>x"
    10.7 -  assumes less: "\<And>x. d\<cdot>x \<sqsubseteq> x"
    10.8 +  assumes below: "\<And>x. d\<cdot>x \<sqsubseteq> x"
    10.9  begin
   10.10  
   10.11 -lemma less_ID: "d \<sqsubseteq> ID"
   10.12 -by (rule less_cfun_ext, simp add: less)
   10.13 +lemma below_ID: "d \<sqsubseteq> ID"
   10.14 +by (rule below_cfun_ext, simp add: below)
   10.15  
   10.16  text {* The set of fixed points is the same as the range. *}
   10.17  
   10.18 @@ -34,18 +34,18 @@
   10.19    the subset ordering of their sets of fixed-points.
   10.20  *}
   10.21  
   10.22 -lemma lessI:
   10.23 +lemma belowI:
   10.24    assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
   10.25 -proof (rule less_cfun_ext)
   10.26 +proof (rule below_cfun_ext)
   10.27    fix x
   10.28 -  from less have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
   10.29 +  from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
   10.30    also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
   10.31    finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" .
   10.32  qed
   10.33  
   10.34 -lemma lessD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
   10.35 -proof (rule antisym_less)
   10.36 -  from less show "d\<cdot>x \<sqsubseteq> x" .
   10.37 +lemma belowD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
   10.38 +proof (rule below_antisym)
   10.39 +  from below show "d\<cdot>x \<sqsubseteq> x" .
   10.40  next
   10.41    assume "f \<sqsubseteq> d"
   10.42    hence "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
   10.43 @@ -64,11 +64,11 @@
   10.44  lemma deflation_UU: "deflation \<bottom>"
   10.45  by (simp add: deflation.intro)
   10.46  
   10.47 -lemma deflation_less_iff:
   10.48 +lemma deflation_below_iff:
   10.49    "\<lbrakk>deflation p; deflation q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
   10.50   apply safe
   10.51 -  apply (simp add: deflation.lessD)
   10.52 - apply (simp add: deflation.lessI)
   10.53 +  apply (simp add: deflation.belowD)
   10.54 + apply (simp add: deflation.belowI)
   10.55  done
   10.56  
   10.57  text {*
   10.58 @@ -76,13 +76,13 @@
   10.59    the lesser of the two (if they are comparable).
   10.60  *}
   10.61  
   10.62 -lemma deflation_less_comp1:
   10.63 +lemma deflation_below_comp1:
   10.64    assumes "deflation f"
   10.65    assumes "deflation g"
   10.66    shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
   10.67 -proof (rule antisym_less)
   10.68 +proof (rule below_antisym)
   10.69    interpret g: deflation g by fact
   10.70 -  from g.less show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
   10.71 +  from g.below show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
   10.72  next
   10.73    interpret f: deflation f by fact
   10.74    assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
   10.75 @@ -91,9 +91,9 @@
   10.76    finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" .
   10.77  qed
   10.78  
   10.79 -lemma deflation_less_comp2:
   10.80 +lemma deflation_below_comp2:
   10.81    "\<lbrakk>deflation f; deflation g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
   10.82 -by (simp only: deflation.lessD deflation.idem)
   10.83 +by (simp only: deflation.belowD deflation.idem)
   10.84  
   10.85  
   10.86  subsection {* Deflations with finite range *}
   10.87 @@ -143,7 +143,7 @@
   10.88    hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)"
   10.89      using j by simp
   10.90    hence "d\<cdot>x \<sqsubseteq> Y j"
   10.91 -    using less by (rule trans_less)
   10.92 +    using below by (rule below_trans)
   10.93    thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
   10.94  qed
   10.95  
   10.96 @@ -155,10 +155,10 @@
   10.97  locale ep_pair =
   10.98    fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a"
   10.99    assumes e_inverse [simp]: "\<And>x. p\<cdot>(e\<cdot>x) = x"
  10.100 -  and e_p_less: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
  10.101 +  and e_p_below: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
  10.102  begin
  10.103  
  10.104 -lemma e_less_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
  10.105 +lemma e_below_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
  10.106  proof
  10.107    assume "e\<cdot>x \<sqsubseteq> e\<cdot>y"
  10.108    hence "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
  10.109 @@ -169,7 +169,7 @@
  10.110  qed
  10.111  
  10.112  lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y"
  10.113 -unfolding po_eq_conv e_less_iff ..
  10.114 +unfolding po_eq_conv e_below_iff ..
  10.115  
  10.116  lemma p_eq_iff:
  10.117    "\<lbrakk>e\<cdot>(p\<cdot>x) = x; e\<cdot>(p\<cdot>y) = y\<rbrakk> \<Longrightarrow> p\<cdot>x = p\<cdot>y \<longleftrightarrow> x = y"
  10.118 @@ -178,7 +178,7 @@
  10.119  lemma p_inverse: "(\<exists>x. y = e\<cdot>x) = (e\<cdot>(p\<cdot>y) = y)"
  10.120  by (auto, rule exI, erule sym)
  10.121  
  10.122 -lemma e_less_iff_less_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
  10.123 +lemma e_below_iff_below_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
  10.124  proof
  10.125    assume "e\<cdot>x \<sqsubseteq> y"
  10.126    then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>y" by (rule monofun_cfun_arg)
  10.127 @@ -186,7 +186,7 @@
  10.128  next
  10.129    assume "x \<sqsubseteq> p\<cdot>y"
  10.130    then have "e\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>y)" by (rule monofun_cfun_arg)
  10.131 -  then show "e\<cdot>x \<sqsubseteq> y" using e_p_less by (rule trans_less)
  10.132 +  then show "e\<cdot>x \<sqsubseteq> y" using e_p_below by (rule below_trans)
  10.133  qed
  10.134  
  10.135  lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
  10.136 @@ -203,7 +203,7 @@
  10.137    assume "compact x"
  10.138    hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
  10.139    hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
  10.140 -  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_less_iff_less_p)
  10.141 +  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
  10.142    thus "compact (e\<cdot>x)" by (rule compactI)
  10.143  qed
  10.144  
  10.145 @@ -213,7 +213,7 @@
  10.146  text {* Deflations from ep-pairs *}
  10.147  
  10.148  lemma deflation_e_p: "deflation (e oo p)"
  10.149 -by (simp add: deflation.intro e_p_less)
  10.150 +by (simp add: deflation.intro e_p_below)
  10.151  
  10.152  lemma deflation_e_d_p:
  10.153    assumes "deflation d"
  10.154 @@ -224,7 +224,7 @@
  10.155    show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
  10.156      by (simp add: idem)
  10.157    show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
  10.158 -    by (simp add: e_less_iff_less_p less)
  10.159 +    by (simp add: e_below_iff_below_p below)
  10.160  qed
  10.161  
  10.162  lemma finite_deflation_e_d_p:
  10.163 @@ -236,7 +236,7 @@
  10.164    show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
  10.165      by (simp add: idem)
  10.166    show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
  10.167 -    by (simp add: e_less_iff_less_p less)
  10.168 +    by (simp add: e_below_iff_below_p below)
  10.169    have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))"
  10.170      by (simp add: finite_image)
  10.171    hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
  10.172 @@ -254,24 +254,24 @@
  10.173    {
  10.174      fix x
  10.175      have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
  10.176 -      by (rule d.less)
  10.177 +      by (rule d.below)
  10.178      hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)"
  10.179        by (rule monofun_cfun_arg)
  10.180      hence "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
  10.181        by simp
  10.182    }
  10.183 -  note p_d_e_less = this
  10.184 +  note p_d_e_below = this
  10.185    show ?thesis
  10.186    proof
  10.187      fix x
  10.188      show "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
  10.189 -      by (rule p_d_e_less)
  10.190 +      by (rule p_d_e_below)
  10.191    next
  10.192      fix x
  10.193      show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x"
  10.194 -    proof (rule antisym_less)
  10.195 +    proof (rule below_antisym)
  10.196        show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) \<sqsubseteq> (p oo d oo e)\<cdot>x"
  10.197 -        by (rule p_d_e_less)
  10.198 +        by (rule p_d_e_below)
  10.199        have "p\<cdot>(d\<cdot>(d\<cdot>(d\<cdot>(e\<cdot>x)))) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
  10.200          by (intro monofun_cfun_arg d)
  10.201        hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
  10.202 @@ -315,29 +315,29 @@
  10.203  lemma ep_pair_unique_e_lemma:
  10.204    assumes "ep_pair e1 p" and "ep_pair e2 p"
  10.205    shows "e1 \<sqsubseteq> e2"
  10.206 -proof (rule less_cfun_ext)
  10.207 +proof (rule below_cfun_ext)
  10.208    interpret e1: ep_pair e1 p by fact
  10.209    interpret e2: ep_pair e2 p by fact
  10.210    fix x
  10.211    have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
  10.212 -    by (rule e1.e_p_less)
  10.213 +    by (rule e1.e_p_below)
  10.214    thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
  10.215      by (simp only: e2.e_inverse)
  10.216  qed
  10.217  
  10.218  lemma ep_pair_unique_e:
  10.219    "\<lbrakk>ep_pair e1 p; ep_pair e2 p\<rbrakk> \<Longrightarrow> e1 = e2"
  10.220 -by (fast intro: antisym_less elim: ep_pair_unique_e_lemma)
  10.221 +by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
  10.222  
  10.223  lemma ep_pair_unique_p_lemma:
  10.224    assumes "ep_pair e p1" and "ep_pair e p2"
  10.225    shows "p1 \<sqsubseteq> p2"
  10.226 -proof (rule less_cfun_ext)
  10.227 +proof (rule below_cfun_ext)
  10.228    interpret p1: ep_pair e p1 by fact
  10.229    interpret p2: ep_pair e p2 by fact
  10.230    fix x
  10.231    have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
  10.232 -    by (rule p1.e_p_less)
  10.233 +    by (rule p1.e_p_below)
  10.234    hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
  10.235      by (rule monofun_cfun_arg)
  10.236    thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
  10.237 @@ -346,7 +346,7 @@
  10.238  
  10.239  lemma ep_pair_unique_p:
  10.240    "\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
  10.241 -by (fast intro: antisym_less elim: ep_pair_unique_p_lemma)
  10.242 +by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
  10.243  
  10.244  subsection {* Composing ep-pairs *}
  10.245  
  10.246 @@ -363,11 +363,11 @@
  10.247    show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
  10.248      by simp
  10.249    have "e1\<cdot>(p1\<cdot>(p2\<cdot>y)) \<sqsubseteq> p2\<cdot>y"
  10.250 -    by (rule ep1.e_p_less)
  10.251 +    by (rule ep1.e_p_below)
  10.252    hence "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)"
  10.253      by (rule monofun_cfun_arg)
  10.254    also have "e2\<cdot>(p2\<cdot>y) \<sqsubseteq> y"
  10.255 -    by (rule ep2.e_p_less)
  10.256 +    by (rule ep2.e_p_below)
  10.257    finally show "(e2 oo e1)\<cdot>((p1 oo p2)\<cdot>y) \<sqsubseteq> y"
  10.258      by simp
  10.259  qed
  10.260 @@ -381,7 +381,7 @@
  10.261  proof -
  10.262    have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal)
  10.263    hence "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
  10.264 -  also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_less)
  10.265 +  also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_below)
  10.266    finally show "e\<cdot>\<bottom> = \<bottom>" by simp
  10.267  qed
  10.268  
    11.1 --- a/src/HOLCF/Discrete.thy	Fri May 08 19:28:11 2009 +0100
    11.2 +++ b/src/HOLCF/Discrete.thy	Fri May 08 16:19:51 2009 -0700
    11.3 @@ -12,21 +12,21 @@
    11.4  
    11.5  subsection {* Type @{typ "'a discr"} is a discrete cpo *}
    11.6  
    11.7 -instantiation discr :: (type) sq_ord
    11.8 +instantiation discr :: (type) below
    11.9  begin
   11.10  
   11.11  definition
   11.12 -  less_discr_def:
   11.13 +  below_discr_def:
   11.14      "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
   11.15  
   11.16  instance ..
   11.17  end
   11.18  
   11.19  instance discr :: (type) discrete_cpo
   11.20 -by intro_classes (simp add: less_discr_def)
   11.21 +by intro_classes (simp add: below_discr_def)
   11.22  
   11.23 -lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
   11.24 -by simp
   11.25 +lemma discr_below_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
   11.26 +by simp (* FIXME: same discrete_cpo - remove? is [iff] important? *)
   11.27  
   11.28  subsection {* Type @{typ "'a discr"} is a cpo *}
   11.29  
    12.1 --- a/src/HOLCF/Domain.thy	Fri May 08 19:28:11 2009 +0100
    12.2 +++ b/src/HOLCF/Domain.thy	Fri May 08 16:19:51 2009 -0700
    12.3 @@ -33,7 +33,7 @@
    12.4  lemma swap: "iso rep abs"
    12.5    by (rule iso.intro [OF rep_iso abs_iso])
    12.6  
    12.7 -lemma abs_less: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
    12.8 +lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
    12.9  proof
   12.10    assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y"
   12.11    then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg)
   12.12 @@ -43,11 +43,11 @@
   12.13    then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg)
   12.14  qed
   12.15  
   12.16 -lemma rep_less: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
   12.17 -  by (rule iso.abs_less [OF swap])
   12.18 +lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
   12.19 +  by (rule iso.abs_below [OF swap])
   12.20  
   12.21  lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)"
   12.22 -  by (simp add: po_eq_conv abs_less)
   12.23 +  by (simp add: po_eq_conv abs_below)
   12.24  
   12.25  lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)"
   12.26    by (rule iso.abs_eq [OF swap])
   12.27 @@ -91,7 +91,7 @@
   12.28    assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
   12.29    with cont_Rep_CFun2
   12.30    have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
   12.31 -  then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_less by simp
   12.32 +  then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
   12.33  qed
   12.34  
   12.35  lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
    13.1 --- a/src/HOLCF/Ffun.thy	Fri May 08 19:28:11 2009 +0100
    13.2 +++ b/src/HOLCF/Ffun.thy	Fri May 08 16:19:51 2009 -0700
    13.3 @@ -10,11 +10,11 @@
    13.4  
    13.5  subsection {* Full function space is a partial order *}
    13.6  
    13.7 -instantiation "fun"  :: (type, sq_ord) sq_ord
    13.8 +instantiation "fun"  :: (type, below) below
    13.9  begin
   13.10  
   13.11  definition
   13.12 -  less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  
   13.13 +  below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
   13.14  
   13.15  instance ..
   13.16  end
   13.17 @@ -23,45 +23,45 @@
   13.18  proof
   13.19    fix f :: "'a \<Rightarrow> 'b"
   13.20    show "f \<sqsubseteq> f"
   13.21 -    by (simp add: less_fun_def)
   13.22 +    by (simp add: below_fun_def)
   13.23  next
   13.24    fix f g :: "'a \<Rightarrow> 'b"
   13.25    assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
   13.26 -    by (simp add: less_fun_def expand_fun_eq antisym_less)
   13.27 +    by (simp add: below_fun_def expand_fun_eq below_antisym)
   13.28  next
   13.29    fix f g h :: "'a \<Rightarrow> 'b"
   13.30    assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
   13.31 -    unfolding less_fun_def by (fast elim: trans_less)
   13.32 +    unfolding below_fun_def by (fast elim: below_trans)
   13.33  qed
   13.34  
   13.35  text {* make the symbol @{text "<<"} accessible for type fun *}
   13.36  
   13.37 -lemma expand_fun_less: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
   13.38 -by (simp add: less_fun_def)
   13.39 +lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
   13.40 +by (simp add: below_fun_def)
   13.41  
   13.42 -lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
   13.43 -by (simp add: less_fun_def)
   13.44 +lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
   13.45 +by (simp add: below_fun_def)
   13.46  
   13.47  subsection {* Full function space is chain complete *}
   13.48  
   13.49  text {* function application is monotone *}
   13.50  
   13.51  lemma monofun_app: "monofun (\<lambda>f. f x)"
   13.52 -by (rule monofunI, simp add: less_fun_def)
   13.53 +by (rule monofunI, simp add: below_fun_def)
   13.54  
   13.55  text {* chains of functions yield chains in the po range *}
   13.56  
   13.57  lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
   13.58 -by (simp add: chain_def less_fun_def)
   13.59 +by (simp add: chain_def below_fun_def)
   13.60  
   13.61  lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
   13.62 -by (simp add: chain_def less_fun_def)
   13.63 +by (simp add: chain_def below_fun_def)
   13.64  
   13.65  text {* upper bounds of function chains yield upper bound in the po range *}
   13.66  
   13.67  lemma ub2ub_fun:
   13.68    "range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
   13.69 -by (auto simp add: is_ub_def less_fun_def)
   13.70 +by (auto simp add: is_ub_def below_fun_def)
   13.71  
   13.72  text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
   13.73  
   13.74 @@ -70,9 +70,9 @@
   13.75    shows "range Y <<| f"
   13.76  apply (rule is_lubI)
   13.77  apply (rule ub_rangeI)
   13.78 -apply (rule less_fun_ext)
   13.79 +apply (rule below_fun_ext)
   13.80  apply (rule is_ub_lub [OF f])
   13.81 -apply (rule less_fun_ext)
   13.82 +apply (rule below_fun_ext)
   13.83  apply (rule is_lub_lub [OF f])
   13.84  apply (erule ub2ub_fun)
   13.85  done
   13.86 @@ -103,7 +103,7 @@
   13.87  proof
   13.88    fix f g :: "'a \<Rightarrow> 'b"
   13.89    show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
   13.90 -    unfolding expand_fun_less expand_fun_eq
   13.91 +    unfolding expand_fun_below expand_fun_eq
   13.92      by simp
   13.93  qed
   13.94  
   13.95 @@ -148,7 +148,7 @@
   13.96  subsection {* Full function space is pointed *}
   13.97  
   13.98  lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
   13.99 -by (simp add: less_fun_def)
  13.100 +by (simp add: below_fun_def)
  13.101  
  13.102  lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
  13.103  apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
  13.104 @@ -171,13 +171,13 @@
  13.105  *}
  13.106  
  13.107  lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
  13.108 -by (simp add: less_fun_def)
  13.109 +by (simp add: below_fun_def)
  13.110  
  13.111  lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
  13.112  by (rule monofunE)
  13.113  
  13.114  lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
  13.115 -by (rule trans_less [OF monofun_fun_arg monofun_fun_fun])
  13.116 +by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
  13.117  
  13.118  subsection {* Propagation of monotonicity and continuity *}
  13.119  
  13.120 @@ -236,7 +236,7 @@
  13.121  lemma mono2mono_lambda:
  13.122    assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
  13.123  apply (rule monofunI)
  13.124 -apply (rule less_fun_ext)
  13.125 +apply (rule below_fun_ext)
  13.126  apply (erule monofunE [OF f])
  13.127  done
  13.128  
  13.129 @@ -296,4 +296,3 @@
  13.130  by (rule cont2cont_app2 [OF cont_const])
  13.131  
  13.132  end
  13.133 -
    14.1 --- a/src/HOLCF/Fix.thy	Fri May 08 19:28:11 2009 +0100
    14.2 +++ b/src/HOLCF/Fix.thy	Fri May 08 16:19:51 2009 -0700
    14.3 @@ -90,7 +90,7 @@
    14.4  apply simp
    14.5  done
    14.6  
    14.7 -lemma fix_least_less: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
    14.8 +lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
    14.9  apply (simp add: fix_def2)
   14.10  apply (rule is_lub_thelub)
   14.11  apply (rule chain_iterate)
   14.12 @@ -98,17 +98,17 @@
   14.13  apply (induct_tac i)
   14.14  apply simp
   14.15  apply simp
   14.16 -apply (erule rev_trans_less)
   14.17 +apply (erule rev_below_trans)
   14.18  apply (erule monofun_cfun_arg)
   14.19  done
   14.20  
   14.21  lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
   14.22 -by (rule fix_least_less, simp)
   14.23 +by (rule fix_least_below, simp)
   14.24  
   14.25  lemma fix_eqI:
   14.26    assumes fixed: "F\<cdot>x = x" and least: "\<And>z. F\<cdot>z = z \<Longrightarrow> x \<sqsubseteq> z"
   14.27    shows "fix\<cdot>F = x"
   14.28 -apply (rule antisym_less)
   14.29 +apply (rule below_antisym)
   14.30  apply (rule fix_least [OF fixed])
   14.31  apply (rule least [OF fix_eq [symmetric]])
   14.32  done
   14.33 @@ -230,10 +230,10 @@
   14.34    have "?y1 \<sqsubseteq> y" by (rule fix_least, simp add: F_y)
   14.35    hence "cfst\<cdot>(F\<cdot>\<langle>x, ?y1\<rangle>) \<sqsubseteq> cfst\<cdot>(F\<cdot>\<langle>x, y\<rangle>)" by (simp add: monofun_cfun)
   14.36    hence "cfst\<cdot>(F\<cdot>\<langle>x, ?y1\<rangle>) \<sqsubseteq> x" using F_x by simp
   14.37 -  hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_less)
   14.38 +  hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_below)
   14.39    hence "csnd\<cdot>(F\<cdot>\<langle>?x, y\<rangle>) \<sqsubseteq> csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)" by (simp add: monofun_cfun)
   14.40    hence "csnd\<cdot>(F\<cdot>\<langle>?x, y\<rangle>) \<sqsubseteq> y" using F_y by simp
   14.41 -  hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_less)
   14.42 +  hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_below)
   14.43    show "\<langle>?x, ?y\<rangle> \<sqsubseteq> z" using z 1 2 by simp
   14.44  qed
   14.45  
    15.1 --- a/src/HOLCF/HOLCF.thy	Fri May 08 19:28:11 2009 +0100
    15.2 +++ b/src/HOLCF/HOLCF.thy	Fri May 08 16:19:51 2009 -0700
    15.3 @@ -21,4 +21,58 @@
    15.4          (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
    15.5  *}
    15.6  
    15.7 +text {* Legacy theorem names *}
    15.8 +
    15.9 +lemmas sq_ord_less_eq_trans = below_eq_trans
   15.10 +lemmas sq_ord_eq_less_trans = eq_below_trans
   15.11 +lemmas refl_less = below_refl
   15.12 +lemmas trans_less = below_trans
   15.13 +lemmas antisym_less = below_antisym
   15.14 +lemmas antisym_less_inverse = below_antisym_inverse
   15.15 +lemmas box_less = box_below
   15.16 +lemmas rev_trans_less = rev_below_trans
   15.17 +lemmas not_less2not_eq = not_below2not_eq
   15.18 +lemmas less_UU_iff = below_UU_iff
   15.19 +lemmas flat_less_iff = flat_below_iff
   15.20 +lemmas adm_less = adm_below
   15.21 +lemmas adm_not_less = adm_not_below
   15.22 +lemmas adm_compact_not_less = adm_compact_not_below
   15.23 +lemmas less_fun_def = below_fun_def
   15.24 +lemmas expand_fun_less = expand_fun_below
   15.25 +lemmas less_fun_ext = below_fun_ext
   15.26 +lemmas less_discr_def = below_discr_def
   15.27 +lemmas discr_less_eq = discr_below_eq
   15.28 +lemmas less_unit_def = below_unit_def
   15.29 +lemmas less_cprod_def = below_prod_def
   15.30 +lemmas prod_lessI = prod_belowI
   15.31 +lemmas Pair_less_iff = Pair_below_iff
   15.32 +lemmas fst_less_iff = fst_below_iff
   15.33 +lemmas snd_less_iff = snd_below_iff
   15.34 +lemmas expand_cfun_less = expand_cfun_below
   15.35 +lemmas less_cfun_ext = below_cfun_ext
   15.36 +lemmas injection_less = injection_below
   15.37 +lemmas approx_less = approx_below
   15.38 +lemmas profinite_less_ext = profinite_below_ext
   15.39 +lemmas less_up_def = below_up_def
   15.40 +lemmas not_Iup_less = not_Iup_below
   15.41 +lemmas Iup_less = Iup_below
   15.42 +lemmas up_less = up_below
   15.43 +lemmas cpair_less = cpair_below
   15.44 +lemmas less_cprod = below_cprod
   15.45 +lemmas cfst_less_iff = cfst_below_iff
   15.46 +lemmas csnd_less_iff = csnd_below_iff
   15.47 +lemmas Def_inject_less_eq = Def_below_Def
   15.48 +lemmas Def_less_is_eq = Def_below_iff
   15.49 +lemmas spair_less_iff = spair_below_iff
   15.50 +lemmas less_sprod = below_sprod
   15.51 +lemmas spair_less = spair_below
   15.52 +lemmas sfst_less_iff = sfst_below_iff
   15.53 +lemmas ssnd_less_iff = ssnd_below_iff
   15.54 +lemmas fix_least_less = fix_least_below
   15.55 +lemmas dist_less_one = dist_below_one
   15.56 +lemmas less_ONE = below_ONE
   15.57 +lemmas ONE_less_iff = ONE_below_iff
   15.58 +lemmas less_sinlD = below_sinlD
   15.59 +lemmas less_sinrD = below_sinrD
   15.60 +
   15.61  end
    16.1 --- a/src/HOLCF/Lift.thy	Fri May 08 19:28:11 2009 +0100
    16.2 +++ b/src/HOLCF/Lift.thy	Fri May 08 16:19:51 2009 -0700
    16.3 @@ -70,11 +70,11 @@
    16.4  lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
    16.5    by simp
    16.6  
    16.7 -lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
    16.8 -by (simp add: less_lift_def Def_def Abs_lift_inverse lift_def)
    16.9 +lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
   16.10 +by (simp add: below_lift_def Def_def Abs_lift_inverse lift_def)
   16.11  
   16.12 -lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
   16.13 -by (induct y, simp, simp add: Def_inject_less_eq)
   16.14 +lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
   16.15 +by (induct y, simp, simp add: Def_below_Def)
   16.16  
   16.17  
   16.18  subsection {* Lift is flat *}
   16.19 @@ -134,7 +134,7 @@
   16.20    "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
   16.21  apply (rule monofunE [where f=flift1])
   16.22  apply (rule cont2mono [OF cont_flift1])
   16.23 -apply (simp add: less_fun_ext)
   16.24 +apply (simp add: below_fun_ext)
   16.25  done
   16.26  
   16.27  lemma cont2cont_flift1 [simp]:
   16.28 @@ -216,7 +216,7 @@
   16.29      apply (rule is_lubI)
   16.30       apply (rule ub_rangeI, simp)
   16.31      apply (drule ub_rangeD)
   16.32 -    apply (erule rev_trans_less)
   16.33 +    apply (erule rev_below_trans)
   16.34      apply simp
   16.35      apply (rule lessI)
   16.36      done
    17.1 --- a/src/HOLCF/LowerPD.thy	Fri May 08 19:28:11 2009 +0100
    17.2 +++ b/src/HOLCF/LowerPD.thy	Fri May 08 16:19:51 2009 -0700
    17.3 @@ -23,7 +23,7 @@
    17.4  apply (drule (1) bspec, erule bexE)
    17.5  apply (drule (1) bspec, erule bexE)
    17.6  apply (erule rev_bexI)
    17.7 -apply (erule (1) trans_less)
    17.8 +apply (erule (1) below_trans)
    17.9  done
   17.10  
   17.11  interpretation lower_le: preorder lower_le
   17.12 @@ -39,7 +39,7 @@
   17.13  lemma PDPlus_lower_mono: "\<lbrakk>s \<le>\<flat> t; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<flat> PDPlus t v"
   17.14  unfolding lower_le_def Rep_PDPlus by fast
   17.15  
   17.16 -lemma PDPlus_lower_less: "t \<le>\<flat> PDPlus t u"
   17.17 +lemma PDPlus_lower_le: "t \<le>\<flat> PDPlus t u"
   17.18  unfolding lower_le_def Rep_PDPlus by fast
   17.19  
   17.20  lemma lower_le_PDUnit_PDUnit_iff [simp]:
   17.21 @@ -99,7 +99,7 @@
   17.22    "{S::'a pd_basis set. lower_le.ideal S}"
   17.23  by (fast intro: lower_le.ideal_principal)
   17.24  
   17.25 -instantiation lower_pd :: (profinite) sq_ord
   17.26 +instantiation lower_pd :: (profinite) below
   17.27  begin
   17.28  
   17.29  definition
   17.30 @@ -110,16 +110,16 @@
   17.31  
   17.32  instance lower_pd :: (profinite) po
   17.33  by (rule lower_le.typedef_ideal_po
   17.34 -    [OF type_definition_lower_pd sq_le_lower_pd_def])
   17.35 +    [OF type_definition_lower_pd below_lower_pd_def])
   17.36  
   17.37  instance lower_pd :: (profinite) cpo
   17.38  by (rule lower_le.typedef_ideal_cpo
   17.39 -    [OF type_definition_lower_pd sq_le_lower_pd_def])
   17.40 +    [OF type_definition_lower_pd below_lower_pd_def])
   17.41  
   17.42  lemma Rep_lower_pd_lub:
   17.43    "chain Y \<Longrightarrow> Rep_lower_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_lower_pd (Y i))"
   17.44  by (rule lower_le.typedef_ideal_rep_contlub
   17.45 -    [OF type_definition_lower_pd sq_le_lower_pd_def])
   17.46 +    [OF type_definition_lower_pd below_lower_pd_def])
   17.47  
   17.48  lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd xs)"
   17.49  by (rule Rep_lower_pd [unfolded mem_Collect_eq])
   17.50 @@ -145,7 +145,7 @@
   17.51  apply (rule ideal_Rep_lower_pd)
   17.52  apply (erule Rep_lower_pd_lub)
   17.53  apply (rule Rep_lower_principal)
   17.54 -apply (simp only: sq_le_lower_pd_def)
   17.55 +apply (simp only: below_lower_pd_def)
   17.56  done
   17.57  
   17.58  text {* Lower powerdomain is pointed *}
   17.59 @@ -264,28 +264,28 @@
   17.60  lemmas lower_plus_aci =
   17.61    lower_plus_ac lower_plus_absorb lower_plus_left_absorb
   17.62  
   17.63 -lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
   17.64 +lemma lower_plus_below1: "xs \<sqsubseteq> xs +\<flat> ys"
   17.65  apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
   17.66 -apply (simp add: PDPlus_lower_less)
   17.67 +apply (simp add: PDPlus_lower_le)
   17.68  done
   17.69  
   17.70 -lemma lower_plus_less2: "ys \<sqsubseteq> xs +\<flat> ys"
   17.71 -by (subst lower_plus_commute, rule lower_plus_less1)
   17.72 +lemma lower_plus_below2: "ys \<sqsubseteq> xs +\<flat> ys"
   17.73 +by (subst lower_plus_commute, rule lower_plus_below1)
   17.74  
   17.75  lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs +\<flat> ys \<sqsubseteq> zs"
   17.76  apply (subst lower_plus_absorb [of zs, symmetric])
   17.77  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   17.78  done
   17.79  
   17.80 -lemma lower_plus_less_iff:
   17.81 +lemma lower_plus_below_iff:
   17.82    "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
   17.83  apply safe
   17.84 -apply (erule trans_less [OF lower_plus_less1])
   17.85 -apply (erule trans_less [OF lower_plus_less2])
   17.86 +apply (erule below_trans [OF lower_plus_below1])
   17.87 +apply (erule below_trans [OF lower_plus_below2])
   17.88  apply (erule (1) lower_plus_least)
   17.89  done
   17.90  
   17.91 -lemma lower_unit_less_plus_iff:
   17.92 +lemma lower_unit_below_plus_iff:
   17.93    "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
   17.94   apply (rule iffI)
   17.95    apply (subgoal_tac
   17.96 @@ -299,13 +299,13 @@
   17.97     apply simp
   17.98    apply simp
   17.99   apply (erule disjE)
  17.100 -  apply (erule trans_less [OF _ lower_plus_less1])
  17.101 - apply (erule trans_less [OF _ lower_plus_less2])
  17.102 +  apply (erule below_trans [OF _ lower_plus_below1])
  17.103 + apply (erule below_trans [OF _ lower_plus_below2])
  17.104  done
  17.105  
  17.106 -lemma lower_unit_less_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
  17.107 +lemma lower_unit_below_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
  17.108   apply (rule iffI)
  17.109 -  apply (rule profinite_less_ext)
  17.110 +  apply (rule profinite_below_ext)
  17.111    apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
  17.112    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
  17.113    apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
  17.114 @@ -313,10 +313,10 @@
  17.115   apply (erule monofun_cfun_arg)
  17.116  done
  17.117  
  17.118 -lemmas lower_pd_less_simps =
  17.119 -  lower_unit_less_iff
  17.120 -  lower_plus_less_iff
  17.121 -  lower_unit_less_plus_iff
  17.122 +lemmas lower_pd_below_simps =
  17.123 +  lower_unit_below_iff
  17.124 +  lower_plus_below_iff
  17.125 +  lower_unit_below_plus_iff
  17.126  
  17.127  lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
  17.128  by (simp add: po_eq_conv)
  17.129 @@ -330,18 +330,18 @@
  17.130  lemma lower_plus_strict_iff [simp]:
  17.131    "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
  17.132  apply safe
  17.133 -apply (rule UU_I, erule subst, rule lower_plus_less1)
  17.134 -apply (rule UU_I, erule subst, rule lower_plus_less2)
  17.135 +apply (rule UU_I, erule subst, rule lower_plus_below1)
  17.136 +apply (rule UU_I, erule subst, rule lower_plus_below2)
  17.137  apply (rule lower_plus_absorb)
  17.138  done
  17.139  
  17.140  lemma lower_plus_strict1 [simp]: "\<bottom> +\<flat> ys = ys"
  17.141 -apply (rule antisym_less [OF _ lower_plus_less2])
  17.142 +apply (rule below_antisym [OF _ lower_plus_below2])
  17.143  apply (simp add: lower_plus_least)
  17.144  done
  17.145  
  17.146  lemma lower_plus_strict2 [simp]: "xs +\<flat> \<bottom> = xs"
  17.147 -apply (rule antisym_less [OF _ lower_plus_less1])
  17.148 +apply (rule below_antisym [OF _ lower_plus_below1])
  17.149  apply (simp add: lower_plus_least)
  17.150  done
  17.151  
  17.152 @@ -412,11 +412,11 @@
  17.153  
  17.154  lemma lower_bind_basis_mono:
  17.155    "t \<le>\<flat> u \<Longrightarrow> lower_bind_basis t \<sqsubseteq> lower_bind_basis u"
  17.156 -unfolding expand_cfun_less
  17.157 +unfolding expand_cfun_below
  17.158  apply (erule lower_le_induct, safe)
  17.159  apply (simp add: monofun_cfun)
  17.160 -apply (simp add: rev_trans_less [OF lower_plus_less1])
  17.161 -apply (simp add: lower_plus_less_iff)
  17.162 +apply (simp add: rev_below_trans [OF lower_plus_below1])
  17.163 +apply (simp add: lower_plus_below_iff)
  17.164  done
  17.165  
  17.166  definition
    18.1 --- a/src/HOLCF/One.thy	Fri May 08 19:28:11 2009 +0100
    18.2 +++ b/src/HOLCF/One.thy	Fri May 08 16:19:51 2009 -0700
    18.3 @@ -28,13 +28,13 @@
    18.4  lemma one_induct: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
    18.5  by (cases x rule: oneE) simp_all
    18.6  
    18.7 -lemma dist_less_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
    18.8 +lemma dist_below_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
    18.9  unfolding ONE_def by simp
   18.10  
   18.11 -lemma less_ONE [simp]: "x \<sqsubseteq> ONE"
   18.12 +lemma below_ONE [simp]: "x \<sqsubseteq> ONE"
   18.13  by (induct x rule: one_induct) simp_all
   18.14  
   18.15 -lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
   18.16 +lemma ONE_below_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
   18.17  by (induct x rule: one_induct) simp_all
   18.18  
   18.19  lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"
    19.1 --- a/src/HOLCF/Pcpo.thy	Fri May 08 19:28:11 2009 +0100
    19.2 +++ b/src/HOLCF/Pcpo.thy	Fri May 08 16:19:51 2009 -0700
    19.3 @@ -46,7 +46,7 @@
    19.4  
    19.5  lemma lub_range_shift:
    19.6    "chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)"
    19.7 -apply (rule antisym_less)
    19.8 +apply (rule below_antisym)
    19.9  apply (rule lub_range_mono)
   19.10  apply    fast
   19.11  apply   assumption
   19.12 @@ -54,7 +54,7 @@
   19.13  apply (rule is_lub_thelub)
   19.14  apply assumption
   19.15  apply (rule ub_rangeI)
   19.16 -apply (rule_tac y="Y (i + j)" in trans_less)
   19.17 +apply (rule_tac y="Y (i + j)" in below_trans)
   19.18  apply (erule chain_mono)
   19.19  apply (rule le_add1)
   19.20  apply (rule is_ub_thelub)
   19.21 @@ -66,7 +66,7 @@
   19.22  apply (rule iffI)
   19.23  apply (fast intro!: thelubI lub_finch1)
   19.24  apply (unfold max_in_chain_def)
   19.25 -apply (safe intro!: antisym_less)
   19.26 +apply (safe intro!: below_antisym)
   19.27  apply (fast elim!: chain_mono)
   19.28  apply (drule sym)
   19.29  apply (force elim!: is_ub_thelub)
   19.30 @@ -79,7 +79,7 @@
   19.31      \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
   19.32  apply (erule is_lub_thelub)
   19.33  apply (rule ub_rangeI)
   19.34 -apply (rule trans_less)
   19.35 +apply (rule below_trans)
   19.36  apply (erule meta_spec)
   19.37  apply (erule is_ub_thelub)
   19.38  done
   19.39 @@ -106,7 +106,7 @@
   19.40  lemma lub_equal2:
   19.41    "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
   19.42      \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
   19.43 -  by (blast intro: antisym_less lub_mono2 sym)
   19.44 +  by (blast intro: below_antisym lub_mono2 sym)
   19.45  
   19.46  lemma lub_mono3:
   19.47    "\<lbrakk>chain Y; chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk>
   19.48 @@ -115,7 +115,7 @@
   19.49  apply (rule ub_rangeI)
   19.50  apply (erule allE)
   19.51  apply (erule exE)
   19.52 -apply (erule trans_less)
   19.53 +apply (erule below_trans)
   19.54  apply (erule is_ub_thelub)
   19.55  done
   19.56  
   19.57 @@ -132,10 +132,10 @@
   19.58    assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
   19.59    assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
   19.60    shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)"
   19.61 -proof (rule antisym_less)
   19.62 +proof (rule below_antisym)
   19.63    have 3: "chain (\<lambda>i. Y i i)"
   19.64      apply (rule chainI)
   19.65 -    apply (rule trans_less)
   19.66 +    apply (rule below_trans)
   19.67      apply (rule chainE [OF 1])
   19.68      apply (rule chainE [OF 2])
   19.69      done
   19.70 @@ -146,7 +146,7 @@
   19.71      apply (rule ub_rangeI)
   19.72      apply (rule lub_mono3 [rule_format, OF 2 3])
   19.73      apply (rule exI)
   19.74 -    apply (rule trans_less)
   19.75 +    apply (rule below_trans)
   19.76      apply (rule chain_mono [OF 1 le_maxI1])
   19.77      apply (rule chain_mono [OF 2 le_maxI2])
   19.78      done
   19.79 @@ -185,7 +185,7 @@
   19.80  apply (rule theI')
   19.81  apply (rule ex_ex1I)
   19.82  apply (rule least)
   19.83 -apply (blast intro: antisym_less)
   19.84 +apply (blast intro: below_antisym)
   19.85  done
   19.86  
   19.87  lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
   19.88 @@ -207,7 +207,7 @@
   19.89  
   19.90  text {* useful lemmas about @{term \<bottom>} *}
   19.91  
   19.92 -lemma less_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
   19.93 +lemma below_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
   19.94  by (simp add: po_eq_conv)
   19.95  
   19.96  lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
   19.97 @@ -287,7 +287,7 @@
   19.98  apply (blast dest: chain_mono ax_flat)
   19.99  done
  19.100  
  19.101 -lemma flat_less_iff:
  19.102 +lemma flat_below_iff:
  19.103    shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
  19.104    by (safe dest!: ax_flat)
  19.105  
  19.106 @@ -298,7 +298,7 @@
  19.107  
  19.108  text {* Discrete cpos *}
  19.109  
  19.110 -class discrete_cpo = sq_ord +
  19.111 +class discrete_cpo = below +
  19.112    assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
  19.113  begin
  19.114  
    20.1 --- a/src/HOLCF/Pcpodef.thy	Fri May 08 19:28:11 2009 +0100
    20.2 +++ b/src/HOLCF/Pcpodef.thy	Fri May 08 16:19:51 2009 -0700
    20.3 @@ -16,22 +16,22 @@
    20.4    if the ordering is defined in the standard way.
    20.5  *}
    20.6  
    20.7 -setup {* Sign.add_const_constraint (@{const_name Porder.sq_le}, NONE) *}
    20.8 +setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
    20.9  
   20.10  theorem typedef_po:
   20.11    fixes Abs :: "'a::po \<Rightarrow> 'b::type"
   20.12    assumes type: "type_definition Rep Abs A"
   20.13 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   20.14 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   20.15    shows "OFCLASS('b, po_class)"
   20.16 - apply (intro_classes, unfold less)
   20.17 -   apply (rule refl_less)
   20.18 -  apply (erule (1) trans_less)
   20.19 + apply (intro_classes, unfold below)
   20.20 +   apply (rule below_refl)
   20.21 +  apply (erule (1) below_trans)
   20.22   apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
   20.23 - apply (erule (1) antisym_less)
   20.24 + apply (erule (1) below_antisym)
   20.25  done
   20.26  
   20.27 -setup {* Sign.add_const_constraint (@{const_name Porder.sq_le},
   20.28 -  SOME @{typ "'a::sq_ord \<Rightarrow> 'a::sq_ord \<Rightarrow> bool"}) *}
   20.29 +setup {* Sign.add_const_constraint (@{const_name Porder.below},
   20.30 +  SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
   20.31  
   20.32  subsection {* Proving a subtype is finite *}
   20.33  
   20.34 @@ -58,9 +58,9 @@
   20.35  subsection {* Proving a subtype is chain-finite *}
   20.36  
   20.37  lemma monofun_Rep:
   20.38 -  assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   20.39 +  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   20.40    shows "monofun Rep"
   20.41 -by (rule monofunI, unfold less)
   20.42 +by (rule monofunI, unfold below)
   20.43  
   20.44  lemmas ch2ch_Rep = ch2ch_monofun [OF monofun_Rep]
   20.45  lemmas ub2ub_Rep = ub2ub_monofun [OF monofun_Rep]
   20.46 @@ -68,10 +68,10 @@
   20.47  theorem typedef_chfin:
   20.48    fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
   20.49    assumes type: "type_definition Rep Abs A"
   20.50 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   20.51 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   20.52    shows "OFCLASS('b, chfin_class)"
   20.53   apply intro_classes
   20.54 - apply (drule ch2ch_Rep [OF less])
   20.55 + apply (drule ch2ch_Rep [OF below])
   20.56   apply (drule chfin)
   20.57   apply (unfold max_in_chain_def)
   20.58   apply (simp add: type_definition.Rep_inject [OF type])
   20.59 @@ -90,28 +90,28 @@
   20.60  lemma Abs_inverse_lub_Rep:
   20.61    fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
   20.62    assumes type: "type_definition Rep Abs A"
   20.63 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   20.64 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   20.65      and adm:  "adm (\<lambda>x. x \<in> A)"
   20.66    shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
   20.67   apply (rule type_definition.Abs_inverse [OF type])
   20.68 - apply (erule admD [OF adm ch2ch_Rep [OF less]])
   20.69 + apply (erule admD [OF adm ch2ch_Rep [OF below]])
   20.70   apply (rule type_definition.Rep [OF type])
   20.71  done
   20.72  
   20.73  theorem typedef_lub:
   20.74    fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
   20.75    assumes type: "type_definition Rep Abs A"
   20.76 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   20.77 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   20.78      and adm: "adm (\<lambda>x. x \<in> A)"
   20.79    shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
   20.80 - apply (frule ch2ch_Rep [OF less])
   20.81 + apply (frule ch2ch_Rep [OF below])
   20.82   apply (rule is_lubI)
   20.83    apply (rule ub_rangeI)
   20.84 -  apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])
   20.85 +  apply (simp only: below Abs_inverse_lub_Rep [OF type below adm])
   20.86    apply (erule is_ub_thelub)
   20.87 - apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])
   20.88 + apply (simp only: below Abs_inverse_lub_Rep [OF type below adm])
   20.89   apply (erule is_lub_thelub)
   20.90 - apply (erule ub2ub_Rep [OF less])
   20.91 + apply (erule ub2ub_Rep [OF below])
   20.92  done
   20.93  
   20.94  lemmas typedef_thelub = typedef_lub [THEN thelubI, standard]
   20.95 @@ -119,13 +119,13 @@
   20.96  theorem typedef_cpo:
   20.97    fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
   20.98    assumes type: "type_definition Rep Abs A"
   20.99 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.100 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.101      and adm: "adm (\<lambda>x. x \<in> A)"
  20.102    shows "OFCLASS('b, cpo_class)"
  20.103  proof
  20.104    fix S::"nat \<Rightarrow> 'b" assume "chain S"
  20.105    hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
  20.106 -    by (rule typedef_lub [OF type less adm])
  20.107 +    by (rule typedef_lub [OF type below adm])
  20.108    thus "\<exists>x. range S <<| x" ..
  20.109  qed
  20.110  
  20.111 @@ -136,14 +136,14 @@
  20.112  theorem typedef_cont_Rep:
  20.113    fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
  20.114    assumes type: "type_definition Rep Abs A"
  20.115 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.116 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.117      and adm: "adm (\<lambda>x. x \<in> A)"
  20.118    shows "cont Rep"
  20.119   apply (rule contI)
  20.120 - apply (simp only: typedef_thelub [OF type less adm])
  20.121 - apply (simp only: Abs_inverse_lub_Rep [OF type less adm])
  20.122 + apply (simp only: typedef_thelub [OF type below adm])
  20.123 + apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
  20.124   apply (rule cpo_lubI)
  20.125 - apply (erule ch2ch_Rep [OF less])
  20.126 + apply (erule ch2ch_Rep [OF below])
  20.127  done
  20.128  
  20.129  text {*
  20.130 @@ -153,28 +153,28 @@
  20.131  *}
  20.132  
  20.133  theorem typedef_is_lubI:
  20.134 -  assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.135 +  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.136    shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
  20.137   apply (rule is_lubI)
  20.138    apply (rule ub_rangeI)
  20.139 -  apply (subst less)
  20.140 +  apply (subst below)
  20.141    apply (erule is_ub_lub)
  20.142 - apply (subst less)
  20.143 + apply (subst below)
  20.144   apply (erule is_lub_lub)
  20.145 - apply (erule ub2ub_Rep [OF less])
  20.146 + apply (erule ub2ub_Rep [OF below])
  20.147  done
  20.148  
  20.149  theorem typedef_cont_Abs:
  20.150    fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
  20.151    fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
  20.152    assumes type: "type_definition Rep Abs A"
  20.153 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.154 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.155      and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
  20.156      and f_in_A: "\<And>x. f x \<in> A"
  20.157      and cont_f: "cont f"
  20.158    shows "cont (\<lambda>x. Abs (f x))"
  20.159   apply (rule contI)
  20.160 - apply (rule typedef_is_lubI [OF less])
  20.161 + apply (rule typedef_is_lubI [OF below])
  20.162   apply (simp only: type_definition.Abs_inverse [OF type f_in_A])
  20.163   apply (erule cont_f [THEN contE])
  20.164  done
  20.165 @@ -184,15 +184,15 @@
  20.166  theorem typedef_compact:
  20.167    fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
  20.168    assumes type: "type_definition Rep Abs A"
  20.169 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.170 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.171      and adm: "adm (\<lambda>x. x \<in> A)"
  20.172    shows "compact (Rep k) \<Longrightarrow> compact k"
  20.173  proof (unfold compact_def)
  20.174    have cont_Rep: "cont Rep"
  20.175 -    by (rule typedef_cont_Rep [OF type less adm])
  20.176 +    by (rule typedef_cont_Rep [OF type below adm])
  20.177    assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
  20.178    with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
  20.179 -  thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold less)
  20.180 +  thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
  20.181  qed
  20.182  
  20.183  subsection {* Proving a subtype is pointed *}
  20.184 @@ -205,13 +205,13 @@
  20.185  theorem typedef_pcpo_generic:
  20.186    fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
  20.187    assumes type: "type_definition Rep Abs A"
  20.188 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.189 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.190      and z_in_A: "z \<in> A"
  20.191      and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
  20.192    shows "OFCLASS('b, pcpo_class)"
  20.193   apply (intro_classes)
  20.194   apply (rule_tac x="Abs z" in exI, rule allI)
  20.195 - apply (unfold less)
  20.196 + apply (unfold below)
  20.197   apply (subst type_definition.Abs_inverse [OF type z_in_A])
  20.198   apply (rule z_least [OF type_definition.Rep [OF type]])
  20.199  done
  20.200 @@ -224,10 +224,10 @@
  20.201  theorem typedef_pcpo:
  20.202    fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
  20.203    assumes type: "type_definition Rep Abs A"
  20.204 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.205 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.206      and UU_in_A: "\<bottom> \<in> A"
  20.207    shows "OFCLASS('b, pcpo_class)"
  20.208 -by (rule typedef_pcpo_generic [OF type less UU_in_A], rule minimal)
  20.209 +by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
  20.210  
  20.211  subsubsection {* Strictness of @{term Rep} and @{term Abs} *}
  20.212  
  20.213 @@ -238,66 +238,66 @@
  20.214  
  20.215  theorem typedef_Abs_strict:
  20.216    assumes type: "type_definition Rep Abs A"
  20.217 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.218 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.219      and UU_in_A: "\<bottom> \<in> A"
  20.220    shows "Abs \<bottom> = \<bottom>"
  20.221 - apply (rule UU_I, unfold less)
  20.222 + apply (rule UU_I, unfold below)
  20.223   apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
  20.224  done
  20.225  
  20.226  theorem typedef_Rep_strict:
  20.227    assumes type: "type_definition Rep Abs A"
  20.228 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.229 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.230      and UU_in_A: "\<bottom> \<in> A"
  20.231    shows "Rep \<bottom> = \<bottom>"
  20.232 - apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
  20.233 + apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
  20.234   apply (rule type_definition.Abs_inverse [OF type UU_in_A])
  20.235  done
  20.236  
  20.237  theorem typedef_Abs_strict_iff:
  20.238    assumes type: "type_definition Rep Abs A"
  20.239 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.240 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.241      and UU_in_A: "\<bottom> \<in> A"
  20.242    shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
  20.243 - apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
  20.244 + apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
  20.245   apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
  20.246  done
  20.247  
  20.248  theorem typedef_Rep_strict_iff:
  20.249    assumes type: "type_definition Rep Abs A"
  20.250 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.251 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.252      and UU_in_A: "\<bottom> \<in> A"
  20.253    shows "(Rep x = \<bottom>) = (x = \<bottom>)"
  20.254 - apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst])
  20.255 + apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
  20.256   apply (simp add: type_definition.Rep_inject [OF type])
  20.257  done
  20.258  
  20.259  theorem typedef_Abs_defined:
  20.260    assumes type: "type_definition Rep Abs A"
  20.261 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.262 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.263      and UU_in_A: "\<bottom> \<in> A"
  20.264    shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
  20.265 -by (simp add: typedef_Abs_strict_iff [OF type less UU_in_A])
  20.266 +by (simp add: typedef_Abs_strict_iff [OF type below UU_in_A])
  20.267  
  20.268  theorem typedef_Rep_defined:
  20.269    assumes type: "type_definition Rep Abs A"
  20.270 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.271 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.272      and UU_in_A: "\<bottom> \<in> A"
  20.273    shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
  20.274 -by (simp add: typedef_Rep_strict_iff [OF type less UU_in_A])
  20.275 +by (simp add: typedef_Rep_strict_iff [OF type below UU_in_A])
  20.276  
  20.277  subsection {* Proving a subtype is flat *}
  20.278  
  20.279  theorem typedef_flat:
  20.280    fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
  20.281    assumes type: "type_definition Rep Abs A"
  20.282 -    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.283 +    and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
  20.284      and UU_in_A: "\<bottom> \<in> A"
  20.285    shows "OFCLASS('b, flat_class)"
  20.286   apply (intro_classes)
  20.287 - apply (unfold less)
  20.288 + apply (unfold below)
  20.289   apply (simp add: type_definition.Rep_inject [OF type, symmetric])
  20.290 - apply (simp add: typedef_Rep_strict [OF type less UU_in_A])
  20.291 + apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
  20.292   apply (simp add: ax_flat)
  20.293  done
  20.294  
    21.1 --- a/src/HOLCF/Porder.thy	Fri May 08 19:28:11 2009 +0100
    21.2 +++ b/src/HOLCF/Porder.thy	Fri May 08 16:19:51 2009 -0700
    21.3 @@ -10,59 +10,59 @@
    21.4  
    21.5  subsection {* Type class for partial orders *}
    21.6  
    21.7 -class sq_ord =
    21.8 -  fixes sq_le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    21.9 +class below =
   21.10 +  fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   21.11  begin
   21.12  
   21.13  notation
   21.14 -  sq_le (infixl "<<" 55)
   21.15 +  below (infixl "<<" 55)
   21.16  
   21.17  notation (xsymbols)
   21.18 -  sq_le (infixl "\<sqsubseteq>" 55)
   21.19 +  below (infixl "\<sqsubseteq>" 55)
   21.20  
   21.21 -lemma sq_ord_less_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
   21.22 +lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
   21.23    by (rule subst)
   21.24  
   21.25 -lemma sq_ord_eq_less_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
   21.26 +lemma eq_below_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
   21.27    by (rule ssubst)
   21.28  
   21.29  end
   21.30  
   21.31 -class po = sq_ord +
   21.32 -  assumes refl_less [iff]: "x \<sqsubseteq> x"
   21.33 -  assumes trans_less: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
   21.34 -  assumes antisym_less: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
   21.35 +class po = below +
   21.36 +  assumes below_refl [iff]: "x \<sqsubseteq> x"
   21.37 +  assumes below_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
   21.38 +  assumes below_antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
   21.39  begin
   21.40  
   21.41  text {* minimal fixes least element *}
   21.42  
   21.43  lemma minimal2UU[OF allI] : "\<forall>x. uu \<sqsubseteq> x \<Longrightarrow> uu = (THE u. \<forall>y. u \<sqsubseteq> y)"
   21.44 -  by (blast intro: theI2 antisym_less)
   21.45 +  by (blast intro: theI2 below_antisym)
   21.46  
   21.47  text {* the reverse law of anti-symmetry of @{term "op <<"} *}
   21.48 -
   21.49 -lemma antisym_less_inverse: "x = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
   21.50 +(* Is this rule ever useful? *)
   21.51 +lemma below_antisym_inverse: "x = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
   21.52    by simp
   21.53  
   21.54 -lemma box_less: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d"
   21.55 -  by (rule trans_less [OF trans_less])
   21.56 +lemma box_below: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d"
   21.57 +  by (rule below_trans [OF below_trans])
   21.58  
   21.59  lemma po_eq_conv: "x = y \<longleftrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
   21.60 -  by (fast elim!: antisym_less_inverse intro!: antisym_less)
   21.61 +  by (fast intro!: below_antisym)
   21.62  
   21.63 -lemma rev_trans_less: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z"
   21.64 -  by (rule trans_less)
   21.65 +lemma rev_below_trans: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z"
   21.66 +  by (rule below_trans)
   21.67  
   21.68 -lemma not_less2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
   21.69 +lemma not_below2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
   21.70    by auto
   21.71  
   21.72  end
   21.73  
   21.74  lemmas HOLCF_trans_rules [trans] =
   21.75 -  trans_less
   21.76 -  antisym_less
   21.77 -  sq_ord_less_eq_trans
   21.78 -  sq_ord_eq_less_trans
   21.79 +  below_trans
   21.80 +  below_antisym
   21.81 +  below_eq_trans
   21.82 +  eq_below_trans
   21.83  
   21.84  context po
   21.85  begin
   21.86 @@ -97,7 +97,7 @@
   21.87    unfolding is_ub_def by fast
   21.88  
   21.89  lemma is_ub_upward: "\<lbrakk>S <| x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S <| y"
   21.90 -  unfolding is_ub_def by (fast intro: trans_less)
   21.91 +  unfolding is_ub_def by (fast intro: below_trans)
   21.92  
   21.93  subsection {* Least upper bounds *}
   21.94  
   21.95 @@ -143,7 +143,7 @@
   21.96  
   21.97  lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
   21.98  apply (unfold is_lub_def is_ub_def)
   21.99 -apply (blast intro: antisym_less)
  21.100 +apply (blast intro: below_antisym)
  21.101  done
  21.102  
  21.103  text {* technical lemmas about @{term lub} and @{term is_lub} *}
  21.104 @@ -191,7 +191,7 @@
  21.105  text {* chains are monotone functions *}
  21.106  
  21.107  lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
  21.108 -  by (erule less_Suc_induct, erule chainE, erule trans_less)
  21.109 +  by (erule less_Suc_induct, erule chainE, erule below_trans)
  21.110  
  21.111  lemma chain_mono: "\<lbrakk>chain Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
  21.112    by (cases "i = j", simp, simp add: chain_mono_less)
  21.113 @@ -208,7 +208,7 @@
  21.114    "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x"
  21.115  apply (rule iffI)
  21.116  apply (rule ub_rangeI)
  21.117 -apply (rule_tac y="S (i + j)" in trans_less)
  21.118 +apply (rule_tac y="S (i + j)" in below_trans)
  21.119  apply (erule chain_mono)
  21.120  apply (rule le_add1)
  21.121  apply (erule ub_rangeD)
  21.122 @@ -313,7 +313,7 @@
  21.123    apply (erule exE)
  21.124    apply (rule finite_chainI, assumption)
  21.125    apply (rule max_in_chainI)
  21.126 -  apply (rule antisym_less)
  21.127 +  apply (rule below_antisym)
  21.128     apply (erule (1) chain_mono)
  21.129    apply (erule spec)
  21.130   apply (rule finite_range_has_max)
  21.131 @@ -451,4 +451,4 @@
  21.132  
  21.133  end
  21.134  
  21.135 -end
  21.136 \ No newline at end of file
  21.137 +end
    22.1 --- a/src/HOLCF/Product_Cpo.thy	Fri May 08 19:28:11 2009 +0100
    22.2 +++ b/src/HOLCF/Product_Cpo.thy	Fri May 08 16:19:51 2009 -0700
    22.3 @@ -12,11 +12,11 @@
    22.4  
    22.5  subsection {* Type @{typ unit} is a pcpo *}
    22.6  
    22.7 -instantiation unit :: sq_ord
    22.8 +instantiation unit :: below
    22.9  begin
   22.10  
   22.11  definition
   22.12 -  less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
   22.13 +  below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
   22.14  
   22.15  instance ..
   22.16  end
   22.17 @@ -32,11 +32,11 @@
   22.18  
   22.19  subsection {* Product type is a partial order *}
   22.20  
   22.21 -instantiation "*" :: (sq_ord, sq_ord) sq_ord
   22.22 +instantiation "*" :: (below, below) below
   22.23  begin
   22.24  
   22.25  definition
   22.26 -  less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
   22.27 +  below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
   22.28  
   22.29  instance ..
   22.30  end
   22.31 @@ -45,26 +45,26 @@
   22.32  proof
   22.33    fix x :: "'a \<times> 'b"
   22.34    show "x \<sqsubseteq> x"
   22.35 -    unfolding less_cprod_def by simp
   22.36 +    unfolding below_prod_def by simp
   22.37  next
   22.38    fix x y :: "'a \<times> 'b"
   22.39    assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
   22.40 -    unfolding less_cprod_def Pair_fst_snd_eq
   22.41 -    by (fast intro: antisym_less)
   22.42 +    unfolding below_prod_def Pair_fst_snd_eq
   22.43 +    by (fast intro: below_antisym)
   22.44  next
   22.45    fix x y z :: "'a \<times> 'b"
   22.46    assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
   22.47 -    unfolding less_cprod_def
   22.48 -    by (fast intro: trans_less)
   22.49 +    unfolding below_prod_def
   22.50 +    by (fast intro: below_trans)
   22.51  qed
   22.52  
   22.53  subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
   22.54  
   22.55 -lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
   22.56 -unfolding less_cprod_def by simp
   22.57 +lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
   22.58 +unfolding below_prod_def by simp
   22.59  
   22.60 -lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
   22.61 -unfolding less_cprod_def by simp
   22.62 +lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
   22.63 +unfolding below_prod_def by simp
   22.64  
   22.65  text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
   22.66  
   22.67 @@ -81,20 +81,20 @@
   22.68  text {* @{term fst} and @{term snd} are monotone *}
   22.69  
   22.70  lemma monofun_fst: "monofun fst"
   22.71 -by (simp add: monofun_def less_cprod_def)
   22.72 +by (simp add: monofun_def below_prod_def)
   22.73  
   22.74  lemma monofun_snd: "monofun snd"
   22.75 -by (simp add: monofun_def less_cprod_def)
   22.76 +by (simp add: monofun_def below_prod_def)
   22.77  
   22.78  subsection {* Product type is a cpo *}
   22.79  
   22.80  lemma is_lub_Pair:
   22.81    "\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)"
   22.82  apply (rule is_lubI [OF ub_rangeI])
   22.83 -apply (simp add: less_cprod_def is_ub_lub)
   22.84 +apply (simp add: below_prod_def is_ub_lub)
   22.85  apply (frule ub2ub_monofun [OF monofun_fst])
   22.86  apply (drule ub2ub_monofun [OF monofun_snd])
   22.87 -apply (simp add: less_cprod_def is_lub_lub)
   22.88 +apply (simp add: below_prod_def is_lub_lub)
   22.89  done
   22.90  
   22.91  lemma lub_cprod:
   22.92 @@ -134,14 +134,14 @@
   22.93  proof
   22.94    fix x y :: "'a \<times> 'b"
   22.95    show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
   22.96 -    unfolding less_cprod_def Pair_fst_snd_eq
   22.97 +    unfolding below_prod_def Pair_fst_snd_eq
   22.98      by simp
   22.99  qed
  22.100  
  22.101  subsection {* Product type is pointed *}
  22.102  
  22.103  lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
  22.104 -by (simp add: less_cprod_def)
  22.105 +by (simp add: below_prod_def)
  22.106  
  22.107  instance "*" :: (pcpo, pcpo) pcpo
  22.108  by intro_classes (fast intro: minimal_cprod)
  22.109 @@ -257,20 +257,20 @@
  22.110  
  22.111  subsection {* Compactness and chain-finiteness *}
  22.112  
  22.113 -lemma fst_less_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
  22.114 -unfolding less_cprod_def by simp
  22.115 +lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
  22.116 +unfolding below_prod_def by simp
  22.117  
  22.118 -lemma snd_less_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y = x \<sqsubseteq> (fst x, y)"
  22.119 -unfolding less_cprod_def by simp
  22.120 +lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
  22.121 +unfolding below_prod_def by simp
  22.122  
  22.123  lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
  22.124 -by (rule compactI, simp add: fst_less_iff)
  22.125 +by (rule compactI, simp add: fst_below_iff)
  22.126  
  22.127  lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
  22.128 -by (rule compactI, simp add: snd_less_iff)
  22.129 +by (rule compactI, simp add: snd_below_iff)
  22.130  
  22.131  lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
  22.132 -by (rule compactI, simp add: less_cprod_def)
  22.133 +by (rule compactI, simp add: below_prod_def)
  22.134  
  22.135  lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
  22.136  apply (safe intro!: compact_Pair)
    23.1 --- a/src/HOLCF/Sprod.thy	Fri May 08 19:28:11 2009 +0100
    23.2 +++ b/src/HOLCF/Sprod.thy	Fri May 08 16:19:51 2009 -0700
    23.3 @@ -20,7 +20,7 @@
    23.4  by (rule typedef_finite_po [OF type_definition_Sprod])
    23.5  
    23.6  instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    23.7 -by (rule typedef_chfin [OF type_definition_Sprod less_Sprod_def])
    23.8 +by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
    23.9  
   23.10  syntax (xsymbols)
   23.11    "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
   23.12 @@ -67,7 +67,7 @@
   23.13  by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
   23.14  
   23.15  lemmas Rep_Sprod_simps =
   23.16 -  Rep_Sprod_inject [symmetric] less_Sprod_def
   23.17 +  Rep_Sprod_inject [symmetric] below_Sprod_def
   23.18    Rep_Sprod_strict Rep_Sprod_spair
   23.19  
   23.20  lemma Exh_Sprod:
   23.21 @@ -99,7 +99,7 @@
   23.22  lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
   23.23  by (simp add: Rep_Sprod_simps strictify_conv_if)
   23.24  
   23.25 -lemma spair_less_iff:
   23.26 +lemma spair_below_iff:
   23.27    "((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
   23.28  by (simp add: Rep_Sprod_simps strictify_conv_if)
   23.29  
   23.30 @@ -160,38 +160,38 @@
   23.31  lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
   23.32  by (cases p, simp_all)
   23.33  
   23.34 -lemma less_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
   23.35 -apply (simp add: less_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
   23.36 -apply (rule less_cprod)
   23.37 +lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
   23.38 +apply (simp add: below_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
   23.39 +apply (rule below_cprod)
   23.40  done
   23.41  
   23.42  lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)"
   23.43 -by (auto simp add: po_eq_conv less_sprod)
   23.44 +by (auto simp add: po_eq_conv below_sprod)
   23.45  
   23.46 -lemma spair_less:
   23.47 +lemma spair_below:
   23.48    "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
   23.49  apply (cases "a = \<bottom>", simp)
   23.50  apply (cases "b = \<bottom>", simp)
   23.51 -apply (simp add: less_sprod)
   23.52 +apply (simp add: below_sprod)
   23.53  done
   23.54  
   23.55 -lemma sfst_less_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
   23.56 +lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
   23.57  apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
   23.58 -apply (simp add: less_sprod)
   23.59 +apply (simp add: below_sprod)
   23.60  done
   23.61  
   23.62 -lemma ssnd_less_iff: "ssnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:sfst\<cdot>x, y:)"
   23.63 +lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:sfst\<cdot>x, y:)"
   23.64  apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
   23.65 -apply (simp add: less_sprod)
   23.66 +apply (simp add: below_sprod)
   23.67  done
   23.68  
   23.69  subsection {* Compactness *}
   23.70  
   23.71  lemma compact_sfst: "compact x \<Longrightarrow> compact (sfst\<cdot>x)"
   23.72 -by (rule compactI, simp add: sfst_less_iff)
   23.73 +by (rule compactI, simp add: sfst_below_iff)
   23.74  
   23.75  lemma compact_ssnd: "compact x \<Longrightarrow> compact (ssnd\<cdot>x)"
   23.76 -by (rule compactI, simp add: ssnd_less_iff)
   23.77 +by (rule compactI, simp add: ssnd_below_iff)
   23.78  
   23.79  lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
   23.80  by (rule compact_Sprod, simp add: Rep_Sprod_spair strictify_conv_if)
   23.81 @@ -224,7 +224,7 @@
   23.82    assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
   23.83      apply (induct x, simp)
   23.84      apply (induct y, simp)
   23.85 -    apply (simp add: spair_less_iff flat_less_iff)
   23.86 +    apply (simp add: spair_below_iff flat_below_iff)
   23.87      done
   23.88  qed
   23.89  
    24.1 --- a/src/HOLCF/Ssum.thy	Fri May 08 19:28:11 2009 +0100
    24.2 +++ b/src/HOLCF/Ssum.thy	Fri May 08 16:19:51 2009 -0700
    24.3 @@ -22,7 +22,7 @@
    24.4  by (rule typedef_finite_po [OF type_definition_Ssum])
    24.5  
    24.6  instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    24.7 -by (rule typedef_chfin [OF type_definition_Ssum less_Ssum_def])
    24.8 +by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
    24.9  
   24.10  syntax (xsymbols)
   24.11    "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
   24.12 @@ -61,17 +61,17 @@
   24.13  
   24.14  text {* Ordering *}
   24.15  
   24.16 -lemma sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
   24.17 -by (simp add: less_Ssum_def Rep_Ssum_sinl strictify_conv_if)
   24.18 +lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
   24.19 +by (simp add: below_Ssum_def Rep_Ssum_sinl strictify_conv_if)
   24.20  
   24.21 -lemma sinr_less [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
   24.22 -by (simp add: less_Ssum_def Rep_Ssum_sinr strictify_conv_if)
   24.23 +lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
   24.24 +by (simp add: below_Ssum_def Rep_Ssum_sinr strictify_conv_if)
   24.25  
   24.26 -lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
   24.27 -by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
   24.28 +lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
   24.29 +by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
   24.30  
   24.31 -lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
   24.32 -by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
   24.33 +lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
   24.34 +by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
   24.35  
   24.36  text {* Equality *}
   24.37  
   24.38 @@ -167,10 +167,10 @@
   24.39    "\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
   24.40  by (cases p, simp only: sinl_strict [symmetric], simp, simp)
   24.41  
   24.42 -lemma less_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
   24.43 +lemma below_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
   24.44  by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
   24.45  
   24.46 -lemma less_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
   24.47 +lemma below_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
   24.48  by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
   24.49  
   24.50  subsection {* Case analysis combinator *}
   24.51 @@ -207,8 +207,8 @@
   24.52  instance "++" :: (flat, flat) flat
   24.53  apply (intro_classes, clarify)
   24.54  apply (rule_tac p=x in ssumE, simp)
   24.55 -apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
   24.56 -apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
   24.57 +apply (rule_tac p=y in ssumE, simp_all add: flat_below_iff)
   24.58 +apply (rule_tac p=y in ssumE, simp_all add: flat_below_iff)
   24.59  done
   24.60  
   24.61  subsection {* Strict sum is a bifinite domain *}
    25.1 --- a/src/HOLCF/Sum_Cpo.thy	Fri May 08 19:28:11 2009 +0100
    25.2 +++ b/src/HOLCF/Sum_Cpo.thy	Fri May 08 16:19:51 2009 -0700
    25.3 @@ -10,28 +10,28 @@
    25.4  
    25.5  subsection {* Ordering on type @{typ "'a + 'b"} *}
    25.6  
    25.7 -instantiation "+" :: (sq_ord, sq_ord) sq_ord
    25.8 +instantiation "+" :: (below, below) below
    25.9  begin
   25.10  
   25.11 -definition
   25.12 -  less_sum_def: "x \<sqsubseteq> y \<equiv> case x of
   25.13 +definition below_sum_def:
   25.14 +  "x \<sqsubseteq> y \<equiv> case x of
   25.15           Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
   25.16           Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
   25.17  
   25.18  instance ..
   25.19  end
   25.20  
   25.21 -lemma Inl_less_iff [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
   25.22 -unfolding less_sum_def by simp
   25.23 +lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
   25.24 +unfolding below_sum_def by simp
   25.25  
   25.26 -lemma Inr_less_iff [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
   25.27 -unfolding less_sum_def by simp
   25.28 +lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
   25.29 +unfolding below_sum_def by simp
   25.30  
   25.31 -lemma Inl_less_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
   25.32 -unfolding less_sum_def by simp
   25.33 +lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
   25.34 +unfolding below_sum_def by simp
   25.35  
   25.36 -lemma Inr_less_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
   25.37 -unfolding less_sum_def by simp
   25.38 +lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
   25.39 +unfolding below_sum_def by simp
   25.40  
   25.41  lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
   25.42  by simp
   25.43 @@ -39,20 +39,20 @@
   25.44  lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
   25.45  by simp
   25.46  
   25.47 -lemma Inl_lessE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   25.48 +lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   25.49  by (cases x, simp_all)
   25.50  
   25.51 -lemma Inr_lessE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   25.52 +lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   25.53  by (cases x, simp_all)
   25.54  
   25.55 -lemmas sum_less_elims = Inl_lessE Inr_lessE
   25.56 +lemmas sum_below_elims = Inl_belowE Inr_belowE
   25.57  
   25.58 -lemma sum_less_cases:
   25.59 +lemma sum_below_cases:
   25.60    "\<lbrakk>x \<sqsubseteq> y;
   25.61      \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
   25.62      \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
   25.63        \<Longrightarrow> R"
   25.64 -by (cases x, safe elim!: sum_less_elims, auto)
   25.65 +by (cases x, safe elim!: sum_below_elims, auto)
   25.66  
   25.67  subsection {* Sum type is a complete partial order *}
   25.68  
   25.69 @@ -64,18 +64,18 @@
   25.70  next
   25.71    fix x y :: "'a + 'b"
   25.72    assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
   25.73 -    by (induct x, auto elim!: sum_less_elims intro: antisym_less)
   25.74 +    by (induct x, auto elim!: sum_below_elims intro: below_antisym)
   25.75  next
   25.76    fix x y z :: "'a + 'b"
   25.77    assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
   25.78 -    by (induct x, auto elim!: sum_less_elims intro: trans_less)
   25.79 +    by (induct x, auto elim!: sum_below_elims intro: below_trans)
   25.80  qed
   25.81  
   25.82  lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
   25.83 -by (rule monofunI, erule sum_less_cases, simp_all)
   25.84 +by (rule monofunI, erule sum_below_cases, simp_all)
   25.85  
   25.86  lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
   25.87 -by (rule monofunI, erule sum_less_cases, simp_all)
   25.88 +by (rule monofunI, erule sum_below_cases, simp_all)
   25.89  
   25.90  lemma sum_chain_cases:
   25.91    assumes Y: "chain Y"
   25.92 @@ -87,12 +87,12 @@
   25.93     apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
   25.94    apply (rule ext)
   25.95    apply (cut_tac j=i in chain_mono [OF Y le0], simp)
   25.96 -  apply (erule Inl_lessE, simp)
   25.97 +  apply (erule Inl_belowE, simp)
   25.98   apply (rule B)
   25.99    apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
  25.100   apply (rule ext)
  25.101   apply (cut_tac j=i in chain_mono [OF Y le0], simp)
  25.102 - apply (erule Inr_lessE, simp)
  25.103 + apply (erule Inr_belowE, simp)
  25.104  done
  25.105  
  25.106  lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
  25.107 @@ -100,7 +100,7 @@
  25.108    apply (rule ub_rangeI)
  25.109    apply (simp add: is_ub_lub)
  25.110   apply (frule ub_rangeD [where i=arbitrary])
  25.111 - apply (erule Inl_lessE, simp)
  25.112 + apply (erule Inl_belowE, simp)
  25.113   apply (erule is_lub_lub)
  25.114   apply (rule ub_rangeI)
  25.115   apply (drule ub_rangeD, simp)
  25.116 @@ -111,7 +111,7 @@
  25.117    apply (rule ub_rangeI)
  25.118    apply (simp add: is_ub_lub)
  25.119   apply (frule ub_rangeD [where i=arbitrary])
  25.120 - apply (erule Inr_lessE, simp)
  25.121 + apply (erule Inr_belowE, simp)
  25.122   apply (erule is_lub_lub)
  25.123   apply (rule ub_rangeI)
  25.124   apply (drule ub_rangeD, simp)
  25.125 @@ -226,7 +226,7 @@
  25.126  instance "+" :: (finite_po, finite_po) finite_po ..
  25.127  
  25.128  instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
  25.129 -by intro_classes (simp add: less_sum_def split: sum.split)
  25.130 +by intro_classes (simp add: below_sum_def split: sum.split)
  25.131  
  25.132  subsection {* Sum type is a bifinite domain *}
  25.133  
    26.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Fri May 08 19:28:11 2009 +0100
    26.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Fri May 08 16:19:51 2009 -0700
    26.3 @@ -257,7 +257,7 @@
    26.4  infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
    26.5  infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
    26.6  infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
    26.7 -infix 1 <<;     fun S <<  T = %%: @{const_name Porder.sq_le} $ S $ T;
    26.8 +infix 1 <<;     fun S <<  T = %%: @{const_name Porder.below} $ S $ T;
    26.9  infix 1 ~<<;    fun S ~<< T = HOLogic.mk_not (S << T);
   26.10  
   26.11  infix 9 `  ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;
    27.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Fri May 08 19:28:11 2009 +0100
    27.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Fri May 08 16:19:51 2009 -0700
    27.3 @@ -29,7 +29,7 @@
    27.4  val adm_all = @{thm adm_all};
    27.5  val adm_conj = @{thm adm_conj};
    27.6  val adm_subst = @{thm adm_subst};
    27.7 -val antisym_less_inverse = @{thm antisym_less_inverse};
    27.8 +val antisym_less_inverse = @{thm below_antisym_inverse};
    27.9  val beta_cfun = @{thm beta_cfun};
   27.10  val cfun_arg_cong = @{thm cfun_arg_cong};
   27.11  val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL};
   27.12 @@ -44,12 +44,12 @@
   27.13  val contlub_cfun_fun = @{thm contlub_cfun_fun};
   27.14  val fix_def2 = @{thm fix_def2};
   27.15  val injection_eq = @{thm injection_eq};
   27.16 -val injection_less = @{thm injection_less};
   27.17 +val injection_less = @{thm injection_below};
   27.18  val lub_equal = @{thm lub_equal};
   27.19  val monofun_cfun_arg = @{thm monofun_cfun_arg};
   27.20  val retraction_strict = @{thm retraction_strict};
   27.21  val spair_eq = @{thm spair_eq};
   27.22 -val spair_less = @{thm spair_less};
   27.23 +val spair_less = @{thm spair_below};
   27.24  val sscase1 = @{thm sscase1};
   27.25  val ssplit1 = @{thm ssplit1};
   27.26  val strictify1 = @{thm strictify1};
   27.27 @@ -121,7 +121,7 @@
   27.28  
   27.29  val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
   27.30  
   27.31 -val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: antisym_less_inverse)}
   27.32 +val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)}
   27.33  
   27.34  in
   27.35  
    28.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Fri May 08 19:28:11 2009 +0100
    28.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Fri May 08 16:19:51 2009 -0700
    28.3 @@ -66,9 +66,9 @@
    28.4          NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
    28.5        | SOME morphs => morphs);
    28.6      val RepC = Const (full Rep_name, newT --> oldT);
    28.7 -    fun lessC T = Const (@{const_name sq_le}, T --> T --> HOLogic.boolT);
    28.8 -    val less_def = Logic.mk_equals (lessC newT,
    28.9 -      Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
   28.10 +    fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
   28.11 +    val below_def = Logic.mk_equals (belowC newT,
   28.12 +      Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
   28.13  
   28.14      fun make_po tac thy1 =
   28.15        let
   28.16 @@ -76,22 +76,22 @@
   28.17            |> TypedefPackage.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
   28.18          val lthy3 = thy2
   28.19            |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
   28.20 -        val less_def' = Syntax.check_term lthy3 less_def;
   28.21 -        val ((_, (_, less_definition')), lthy4) = lthy3
   28.22 +        val below_def' = Syntax.check_term lthy3 below_def;
   28.23 +        val ((_, (_, below_definition')), lthy4) = lthy3
   28.24            |> Specification.definition (NONE,
   28.25 -              ((Binding.prefix_name "less_" (Binding.suffix_name "_def" name), []), less_def'));
   28.26 +              ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
   28.27          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
   28.28 -        val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
   28.29 +        val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
   28.30          val thy5 = lthy4
   28.31            |> Class.prove_instantiation_instance
   28.32 -              (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, less_definition]) 1))
   28.33 +              (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
   28.34            |> LocalTheory.exit_global;
   28.35 -      in ((type_definition, less_definition, set_def), thy5) end;
   28.36 +      in ((type_definition, below_definition, set_def), thy5) end;
   28.37  
   28.38 -    fun make_cpo admissible (type_def, less_def, set_def) theory =
   28.39 +    fun make_cpo admissible (type_def, below_def, set_def) theory =
   28.40        let
   28.41          val admissible' = fold_rule (the_list set_def) admissible;
   28.42 -        val cpo_thms = map (Thm.transfer theory) [type_def, less_def, admissible'];
   28.43 +        val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
   28.44          val theory' = theory
   28.45            |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
   28.46              (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
   28.47 @@ -110,10 +110,10 @@
   28.48          |> Sign.parent_path
   28.49        end;
   28.50  
   28.51 -    fun make_pcpo UU_mem (type_def, less_def, set_def) theory =
   28.52 +    fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
   28.53        let
   28.54          val UU_mem' = fold_rule (the_list set_def) UU_mem;
   28.55 -        val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UU_mem'];
   28.56 +        val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
   28.57          val theory' = theory
   28.58            |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
   28.59              (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
    29.1 --- a/src/HOLCF/Tr.thy	Fri May 08 19:28:11 2009 +0100
    29.2 +++ b/src/HOLCF/Tr.thy	Fri May 08 16:19:51 2009 -0700
    29.3 @@ -37,7 +37,7 @@
    29.4  
    29.5  text {* distinctness for type @{typ tr} *}
    29.6  
    29.7 -lemma dist_less_tr [simp]:
    29.8 +lemma dist_below_tr [simp]:
    29.9    "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
   29.10  unfolding TT_def FF_def by simp_all
   29.11  
   29.12 @@ -45,16 +45,16 @@
   29.13    "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
   29.14  unfolding TT_def FF_def by simp_all
   29.15  
   29.16 -lemma TT_less_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
   29.17 +lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
   29.18  by (induct x rule: tr_induct) simp_all
   29.19  
   29.20 -lemma FF_less_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
   29.21 +lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
   29.22  by (induct x rule: tr_induct) simp_all
   29.23  
   29.24 -lemma not_less_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
   29.25 +lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
   29.26  by (induct x rule: tr_induct) simp_all
   29.27  
   29.28 -lemma not_less_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
   29.29 +lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
   29.30  by (induct x rule: tr_induct) simp_all
   29.31  
   29.32  
    30.1 --- a/src/HOLCF/Universal.thy	Fri May 08 19:28:11 2009 +0100
    30.2 +++ b/src/HOLCF/Universal.thy	Fri May 08 16:19:51 2009 -0700
    30.3 @@ -251,7 +251,7 @@
    30.4  typedef (open) udom = "{S. udom.ideal S}"
    30.5  by (fast intro: udom.ideal_principal)
    30.6  
    30.7 -instantiation udom :: sq_ord
    30.8 +instantiation udom :: below
    30.9  begin
   30.10  
   30.11  definition
   30.12 @@ -262,16 +262,16 @@
   30.13  
   30.14  instance udom :: po
   30.15  by (rule udom.typedef_ideal_po
   30.16 -    [OF type_definition_udom sq_le_udom_def])
   30.17 +    [OF type_definition_udom below_udom_def])
   30.18  
   30.19  instance udom :: cpo
   30.20  by (rule udom.typedef_ideal_cpo
   30.21 -    [OF type_definition_udom sq_le_udom_def])
   30.22 +    [OF type_definition_udom below_udom_def])
   30.23  
   30.24  lemma Rep_udom_lub:
   30.25    "chain Y \<Longrightarrow> Rep_udom (\<Squnion>i. Y i) = (\<Union>i. Rep_udom (Y i))"
   30.26  by (rule udom.typedef_ideal_rep_contlub
   30.27 -    [OF type_definition_udom sq_le_udom_def])
   30.28 +    [OF type_definition_udom below_udom_def])
   30.29  
   30.30  lemma ideal_Rep_udom: "udom.ideal (Rep_udom xs)"
   30.31  by (rule Rep_udom [unfolded mem_Collect_eq])
   30.32 @@ -291,7 +291,7 @@
   30.33  apply (rule ideal_Rep_udom)
   30.34  apply (erule Rep_udom_lub)
   30.35  apply (rule Rep_udom_principal)
   30.36 -apply (simp only: sq_le_udom_def)
   30.37 +apply (simp only: below_udom_def)
   30.38  done
   30.39  
   30.40  text {* Universal domain is pointed *}
   30.41 @@ -359,9 +359,9 @@
   30.42      assume "y \<in> insert a A" and "(if x \<sqsubseteq> a then a else x) \<sqsubseteq> y"
   30.43      thus "(if x \<sqsubseteq> a then a else x) = y"
   30.44        apply auto
   30.45 -      apply (frule (1) trans_less)
   30.46 +      apply (frule (1) below_trans)
   30.47        apply (frule (1) x_eq)
   30.48 -      apply (rule antisym_less, assumption)
   30.49 +      apply (rule below_antisym, assumption)
   30.50        apply simp
   30.51        apply (erule (1) x_eq)
   30.52        done
   30.53 @@ -503,7 +503,7 @@
   30.54  done
   30.55  
   30.56  lemma rank_leD: "rank x \<le> n \<Longrightarrow> cb_take n x = x"
   30.57 -apply (rule antisym_less [OF cb_take_less])
   30.58 +apply (rule below_antisym [OF cb_take_less])
   30.59  apply (subst compact_approx_rank [symmetric])
   30.60  apply (erule cb_take_chain_le)
   30.61  done
   30.62 @@ -727,7 +727,7 @@
   30.63        apply (rule IH)
   30.64         apply (simp add: less_max_iff_disj)
   30.65         apply (erule place_sub_less)
   30.66 -      apply (erule rev_trans_less)
   30.67 +      apply (erule rev_below_trans)
   30.68        apply (rule sub_below)
   30.69        done
   30.70    qed
   30.71 @@ -779,9 +779,9 @@
   30.72  
   30.73  lemma basis_prj_mono: "ubasis_le a b \<Longrightarrow> basis_prj a \<sqsubseteq> basis_prj b"
   30.74  proof (induct a b rule: ubasis_le.induct)
   30.75 -  case (ubasis_le_refl a) show ?case by (rule refl_less)
   30.76 +  case (ubasis_le_refl a) show ?case by (rule below_refl)
   30.77  next
   30.78 -  case (ubasis_le_trans a b c) thus ?case by - (rule trans_less)
   30.79 +  case (ubasis_le_trans a b c) thus ?case by - (rule below_trans)
   30.80  next
   30.81    case (ubasis_le_lower S a i) thus ?case
   30.82      apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
    31.1 --- a/src/HOLCF/Up.thy	Fri May 08 19:28:11 2009 +0100
    31.2 +++ b/src/HOLCF/Up.thy	Fri May 08 16:19:51 2009 -0700
    31.3 @@ -26,11 +26,11 @@
    31.4  
    31.5  subsection {* Ordering on lifted cpo *}
    31.6  
    31.7 -instantiation u :: (cpo) sq_ord
    31.8 +instantiation u :: (cpo) below
    31.9  begin
   31.10  
   31.11  definition
   31.12 -  less_up_def:
   31.13 +  below_up_def:
   31.14      "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
   31.15        (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
   31.16  
   31.17 @@ -38,13 +38,13 @@
   31.18  end
   31.19  
   31.20  lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
   31.21 -by (simp add: less_up_def)
   31.22 +by (simp add: below_up_def)
   31.23  
   31.24 -lemma not_Iup_less [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
   31.25 -by (simp add: less_up_def)
   31.26 +lemma not_Iup_below [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
   31.27 +by (simp add: below_up_def)
   31.28  
   31.29 -lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
   31.30 -by (simp add: less_up_def)
   31.31 +lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
   31.32 +by (simp add: below_up_def)
   31.33  
   31.34  subsection {* Lifted cpo is a partial order *}
   31.35  
   31.36 @@ -52,17 +52,17 @@
   31.37  proof
   31.38    fix x :: "'a u"
   31.39    show "x \<sqsubseteq> x"
   31.40 -    unfolding less_up_def by (simp split: u.split)
   31.41 +    unfolding below_up_def by (simp split: u.split)
   31.42  next
   31.43    fix x y :: "'a u"
   31.44    assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
   31.45 -    unfolding less_up_def
   31.46 -    by (auto split: u.split_asm intro: antisym_less)
   31.47 +    unfolding below_up_def
   31.48 +    by (auto split: u.split_asm intro: below_antisym)
   31.49  next
   31.50    fix x y z :: "'a u"
   31.51    assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
   31.52 -    unfolding less_up_def
   31.53 -    by (auto split: u.split_asm intro: trans_less)
   31.54 +    unfolding below_up_def
   31.55 +    by (auto split: u.split_asm intro: below_trans)
   31.56  qed
   31.57  
   31.58  lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
   31.59 @@ -78,7 +78,7 @@
   31.60    "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
   31.61  apply (rule is_lubI)
   31.62  apply (rule ub_rangeI)
   31.63 -apply (subst Iup_less)
   31.64 +apply (subst Iup_below)
   31.65  apply (erule is_ub_lub)
   31.66  apply (case_tac u)
   31.67  apply (drule ub_rangeD)
   31.68 @@ -112,7 +112,7 @@
   31.69  lemma up_lemma4:
   31.70    "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
   31.71  apply (rule chainI)
   31.72 -apply (rule Iup_less [THEN iffD1])
   31.73 +apply (rule Iup_below [THEN iffD1])
   31.74  apply (subst up_lemma3, assumption+)+
   31.75  apply (simp add: chainE)
   31.76  done
   31.77 @@ -235,9 +235,9 @@
   31.78  by (simp add: up_def cont_Iup inst_up_pcpo)
   31.79  
   31.80  lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
   31.81 -by simp
   31.82 +by simp (* FIXME: remove? *)
   31.83  
   31.84 -lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
   31.85 +lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
   31.86  by (simp add: up_def cont_Iup)
   31.87  
   31.88  lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    32.1 --- a/src/HOLCF/UpperPD.thy	Fri May 08 19:28:11 2009 +0100
    32.2 +++ b/src/HOLCF/UpperPD.thy	Fri May 08 16:19:51 2009 -0700
    32.3 @@ -23,7 +23,7 @@
    32.4  apply (drule (1) bspec, erule bexE)
    32.5  apply (drule (1) bspec, erule bexE)
    32.6  apply (erule rev_bexI)
    32.7 -apply (erule (1) trans_less)
    32.8 +apply (erule (1) below_trans)
    32.9  done
   32.10  
   32.11  interpretation upper_le: preorder upper_le
   32.12 @@ -38,7 +38,7 @@
   32.13  lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v"
   32.14  unfolding upper_le_def Rep_PDPlus by fast
   32.15  
   32.16 -lemma PDPlus_upper_less: "PDPlus t u \<le>\<sharp> t"
   32.17 +lemma PDPlus_upper_le: "PDPlus t u \<le>\<sharp> t"
   32.18  unfolding upper_le_def Rep_PDPlus by fast
   32.19  
   32.20  lemma upper_le_PDUnit_PDUnit_iff [simp]:
   32.21 @@ -97,7 +97,7 @@
   32.22    "{S::'a pd_basis set. upper_le.ideal S}"
   32.23  by (fast intro: upper_le.ideal_principal)
   32.24  
   32.25 -instantiation upper_pd :: (profinite) sq_ord
   32.26 +instantiation upper_pd :: (profinite) below
   32.27  begin
   32.28  
   32.29  definition
   32.30 @@ -108,16 +108,16 @@
   32.31  
   32.32  instance upper_pd :: (profinite) po
   32.33  by (rule upper_le.typedef_ideal_po
   32.34 -    [OF type_definition_upper_pd sq_le_upper_pd_def])
   32.35 +    [OF type_definition_upper_pd below_upper_pd_def])
   32.36  
   32.37  instance upper_pd :: (profinite) cpo
   32.38  by (rule upper_le.typedef_ideal_cpo
   32.39 -    [OF type_definition_upper_pd sq_le_upper_pd_def])
   32.40 +    [OF type_definition_upper_pd below_upper_pd_def])
   32.41  
   32.42  lemma Rep_upper_pd_lub:
   32.43    "chain Y \<Longrightarrow> Rep_upper_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_upper_pd (Y i))"
   32.44  by (rule upper_le.typedef_ideal_rep_contlub
   32.45 -    [OF type_definition_upper_pd sq_le_upper_pd_def])
   32.46 +    [OF type_definition_upper_pd below_upper_pd_def])
   32.47  
   32.48  lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd xs)"
   32.49  by (rule Rep_upper_pd [unfolded mem_Collect_eq])
   32.50 @@ -143,7 +143,7 @@
   32.51  apply (rule ideal_Rep_upper_pd)
   32.52  apply (erule Rep_upper_pd_lub)
   32.53  apply (rule Rep_upper_principal)
   32.54 -apply (simp only: sq_le_upper_pd_def)
   32.55 +apply (simp only: below_upper_pd_def)
   32.56  done
   32.57  
   32.58  text {* Upper powerdomain is pointed *}
   32.59 @@ -262,28 +262,28 @@
   32.60  lemmas upper_plus_aci =
   32.61    upper_plus_ac upper_plus_absorb upper_plus_left_absorb
   32.62  
   32.63 -lemma upper_plus_less1: "xs +\<sharp> ys \<sqsubseteq> xs"
   32.64 +lemma upper_plus_below1: "xs +\<sharp> ys \<sqsubseteq> xs"
   32.65  apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
   32.66 -apply (simp add: PDPlus_upper_less)
   32.67 +apply (simp add: PDPlus_upper_le)
   32.68  done
   32.69  
   32.70 -lemma upper_plus_less2: "xs +\<sharp> ys \<sqsubseteq> ys"
   32.71 -by (subst upper_plus_commute, rule upper_plus_less1)
   32.72 +lemma upper_plus_below2: "xs +\<sharp> ys \<sqsubseteq> ys"
   32.73 +by (subst upper_plus_commute, rule upper_plus_below1)
   32.74  
   32.75  lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys +\<sharp> zs"
   32.76  apply (subst upper_plus_absorb [of xs, symmetric])
   32.77  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   32.78  done
   32.79  
   32.80 -lemma upper_less_plus_iff:
   32.81 +lemma upper_below_plus_iff:
   32.82    "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
   32.83  apply safe
   32.84 -apply (erule trans_less [OF _ upper_plus_less1])
   32.85 -apply (erule trans_less [OF _ upper_plus_less2])
   32.86 +apply (erule below_trans [OF _ upper_plus_below1])
   32.87 +apply (erule below_trans [OF _ upper_plus_below2])
   32.88  apply (erule (1) upper_plus_greatest)
   32.89  done
   32.90  
   32.91 -lemma upper_plus_less_unit_iff:
   32.92 +lemma upper_plus_below_unit_iff:
   32.93    "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
   32.94   apply (rule iffI)
   32.95    apply (subgoal_tac
   32.96 @@ -297,13 +297,13 @@
   32.97     apply simp
   32.98    apply simp
   32.99   apply (erule disjE)
  32.100 -  apply (erule trans_less [OF upper_plus_less1])
  32.101 - apply (erule trans_less [OF upper_plus_less2])
  32.102 +  apply (erule below_trans [OF upper_plus_below1])
  32.103 + apply (erule below_trans [OF upper_plus_below2])
  32.104  done
  32.105  
  32.106 -lemma upper_unit_less_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
  32.107 +lemma upper_unit_below_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
  32.108   apply (rule iffI)
  32.109 -  apply (rule profinite_less_ext)
  32.110 +  apply (rule profinite_below_ext)
  32.111    apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
  32.112    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
  32.113    apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
  32.114 @@ -311,10 +311,10 @@
  32.115   apply (erule monofun_cfun_arg)
  32.116  done
  32.117  
  32.118 -lemmas upper_pd_less_simps =
  32.119 -  upper_unit_less_iff
  32.120 -  upper_less_plus_iff
  32.121 -  upper_plus_less_unit_iff
  32.122 +lemmas upper_pd_below_simps =
  32.123 +  upper_unit_below_iff
  32.124 +  upper_below_plus_iff
  32.125 +  upper_plus_below_unit_iff
  32.126  
  32.127  lemma upper_unit_eq_iff [simp]: "{x}\<sharp> = {y}\<sharp> \<longleftrightarrow> x = y"
  32.128  unfolding po_eq_conv by simp
  32.129 @@ -323,10 +323,10 @@
  32.130  unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
  32.131  
  32.132  lemma upper_plus_strict1 [simp]: "\<bottom> +\<sharp> ys = \<bottom>"
  32.133 -by (rule UU_I, rule upper_plus_less1)
  32.134 +by (rule UU_I, rule upper_plus_below1)
  32.135  
  32.136  lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
  32.137 -by (rule UU_I, rule upper_plus_less2)
  32.138 +by (rule UU_I, rule upper_plus_below2)
  32.139  
  32.140  lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
  32.141  unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
  32.142 @@ -407,11 +407,11 @@
  32.143  
  32.144  lemma upper_bind_basis_mono:
  32.145    "t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u"
  32.146 -unfolding expand_cfun_less
  32.147 +unfolding expand_cfun_below
  32.148  apply (erule upper_le_induct, safe)
  32.149  apply (simp add: monofun_cfun)
  32.150 -apply (simp add: trans_less [OF upper_plus_less1])
  32.151 -apply (simp add: upper_less_plus_iff)
  32.152 +apply (simp add: below_trans [OF upper_plus_below1])
  32.153 +apply (simp add: upper_below_plus_iff)
  32.154  done
  32.155  
  32.156  definition