src/HOLCF/UpperPD.thy
changeset 31076 99fe356cbbc2
parent 30729 461ee3e49ad3
child 33585 8d39394fe5cf
     1.1 --- a/src/HOLCF/UpperPD.thy	Fri May 08 19:28:11 2009 +0100
     1.2 +++ b/src/HOLCF/UpperPD.thy	Fri May 08 16:19:51 2009 -0700
     1.3 @@ -23,7 +23,7 @@
     1.4  apply (drule (1) bspec, erule bexE)
     1.5  apply (drule (1) bspec, erule bexE)
     1.6  apply (erule rev_bexI)
     1.7 -apply (erule (1) trans_less)
     1.8 +apply (erule (1) below_trans)
     1.9  done
    1.10  
    1.11  interpretation upper_le: preorder upper_le
    1.12 @@ -38,7 +38,7 @@
    1.13  lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v"
    1.14  unfolding upper_le_def Rep_PDPlus by fast
    1.15  
    1.16 -lemma PDPlus_upper_less: "PDPlus t u \<le>\<sharp> t"
    1.17 +lemma PDPlus_upper_le: "PDPlus t u \<le>\<sharp> t"
    1.18  unfolding upper_le_def Rep_PDPlus by fast
    1.19  
    1.20  lemma upper_le_PDUnit_PDUnit_iff [simp]:
    1.21 @@ -97,7 +97,7 @@
    1.22    "{S::'a pd_basis set. upper_le.ideal S}"
    1.23  by (fast intro: upper_le.ideal_principal)
    1.24  
    1.25 -instantiation upper_pd :: (profinite) sq_ord
    1.26 +instantiation upper_pd :: (profinite) below
    1.27  begin
    1.28  
    1.29  definition
    1.30 @@ -108,16 +108,16 @@
    1.31  
    1.32  instance upper_pd :: (profinite) po
    1.33  by (rule upper_le.typedef_ideal_po
    1.34 -    [OF type_definition_upper_pd sq_le_upper_pd_def])
    1.35 +    [OF type_definition_upper_pd below_upper_pd_def])
    1.36  
    1.37  instance upper_pd :: (profinite) cpo
    1.38  by (rule upper_le.typedef_ideal_cpo
    1.39 -    [OF type_definition_upper_pd sq_le_upper_pd_def])
    1.40 +    [OF type_definition_upper_pd below_upper_pd_def])
    1.41  
    1.42  lemma Rep_upper_pd_lub:
    1.43    "chain Y \<Longrightarrow> Rep_upper_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_upper_pd (Y i))"
    1.44  by (rule upper_le.typedef_ideal_rep_contlub
    1.45 -    [OF type_definition_upper_pd sq_le_upper_pd_def])
    1.46 +    [OF type_definition_upper_pd below_upper_pd_def])
    1.47  
    1.48  lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd xs)"
    1.49  by (rule Rep_upper_pd [unfolded mem_Collect_eq])
    1.50 @@ -143,7 +143,7 @@
    1.51  apply (rule ideal_Rep_upper_pd)
    1.52  apply (erule Rep_upper_pd_lub)
    1.53  apply (rule Rep_upper_principal)
    1.54 -apply (simp only: sq_le_upper_pd_def)
    1.55 +apply (simp only: below_upper_pd_def)
    1.56  done
    1.57  
    1.58  text {* Upper powerdomain is pointed *}
    1.59 @@ -262,28 +262,28 @@
    1.60  lemmas upper_plus_aci =
    1.61    upper_plus_ac upper_plus_absorb upper_plus_left_absorb
    1.62  
    1.63 -lemma upper_plus_less1: "xs +\<sharp> ys \<sqsubseteq> xs"
    1.64 +lemma upper_plus_below1: "xs +\<sharp> ys \<sqsubseteq> xs"
    1.65  apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
    1.66 -apply (simp add: PDPlus_upper_less)
    1.67 +apply (simp add: PDPlus_upper_le)
    1.68  done
    1.69  
    1.70 -lemma upper_plus_less2: "xs +\<sharp> ys \<sqsubseteq> ys"
    1.71 -by (subst upper_plus_commute, rule upper_plus_less1)
    1.72 +lemma upper_plus_below2: "xs +\<sharp> ys \<sqsubseteq> ys"
    1.73 +by (subst upper_plus_commute, rule upper_plus_below1)
    1.74  
    1.75  lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys +\<sharp> zs"
    1.76  apply (subst upper_plus_absorb [of xs, symmetric])
    1.77  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
    1.78  done
    1.79  
    1.80 -lemma upper_less_plus_iff:
    1.81 +lemma upper_below_plus_iff:
    1.82    "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
    1.83  apply safe
    1.84 -apply (erule trans_less [OF _ upper_plus_less1])
    1.85 -apply (erule trans_less [OF _ upper_plus_less2])
    1.86 +apply (erule below_trans [OF _ upper_plus_below1])
    1.87 +apply (erule below_trans [OF _ upper_plus_below2])
    1.88  apply (erule (1) upper_plus_greatest)
    1.89  done
    1.90  
    1.91 -lemma upper_plus_less_unit_iff:
    1.92 +lemma upper_plus_below_unit_iff:
    1.93    "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
    1.94   apply (rule iffI)
    1.95    apply (subgoal_tac
    1.96 @@ -297,13 +297,13 @@
    1.97     apply simp
    1.98    apply simp
    1.99   apply (erule disjE)
   1.100 -  apply (erule trans_less [OF upper_plus_less1])
   1.101 - apply (erule trans_less [OF upper_plus_less2])
   1.102 +  apply (erule below_trans [OF upper_plus_below1])
   1.103 + apply (erule below_trans [OF upper_plus_below2])
   1.104  done
   1.105  
   1.106 -lemma upper_unit_less_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
   1.107 +lemma upper_unit_below_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
   1.108   apply (rule iffI)
   1.109 -  apply (rule profinite_less_ext)
   1.110 +  apply (rule profinite_below_ext)
   1.111    apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   1.112    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   1.113    apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
   1.114 @@ -311,10 +311,10 @@
   1.115   apply (erule monofun_cfun_arg)
   1.116  done
   1.117  
   1.118 -lemmas upper_pd_less_simps =
   1.119 -  upper_unit_less_iff
   1.120 -  upper_less_plus_iff
   1.121 -  upper_plus_less_unit_iff
   1.122 +lemmas upper_pd_below_simps =
   1.123 +  upper_unit_below_iff
   1.124 +  upper_below_plus_iff
   1.125 +  upper_plus_below_unit_iff
   1.126  
   1.127  lemma upper_unit_eq_iff [simp]: "{x}\<sharp> = {y}\<sharp> \<longleftrightarrow> x = y"
   1.128  unfolding po_eq_conv by simp
   1.129 @@ -323,10 +323,10 @@
   1.130  unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
   1.131  
   1.132  lemma upper_plus_strict1 [simp]: "\<bottom> +\<sharp> ys = \<bottom>"
   1.133 -by (rule UU_I, rule upper_plus_less1)
   1.134 +by (rule UU_I, rule upper_plus_below1)
   1.135  
   1.136  lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
   1.137 -by (rule UU_I, rule upper_plus_less2)
   1.138 +by (rule UU_I, rule upper_plus_below2)
   1.139  
   1.140  lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
   1.141  unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
   1.142 @@ -407,11 +407,11 @@
   1.143  
   1.144  lemma upper_bind_basis_mono:
   1.145    "t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u"
   1.146 -unfolding expand_cfun_less
   1.147 +unfolding expand_cfun_below
   1.148  apply (erule upper_le_induct, safe)
   1.149  apply (simp add: monofun_cfun)
   1.150 -apply (simp add: trans_less [OF upper_plus_less1])
   1.151 -apply (simp add: upper_less_plus_iff)
   1.152 +apply (simp add: below_trans [OF upper_plus_below1])
   1.153 +apply (simp add: upper_below_plus_iff)
   1.154  done
   1.155  
   1.156  definition