src/HOLCF/LowerPD.thy
changeset 26420 57a626f64875
parent 26407 562a1d615336
child 26806 40b411ec05aa
     1.1 --- a/src/HOLCF/LowerPD.thy	Wed Mar 26 22:41:58 2008 +0100
     1.2 +++ b/src/HOLCF/LowerPD.thy	Thu Mar 27 00:27:16 2008 +0100
     1.3 @@ -13,10 +13,10 @@
     1.4  
     1.5  definition
     1.6    lower_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<flat>" 50) where
     1.7 -  "lower_le = (\<lambda>u v. \<forall>x\<in>Rep_pd_basis u. \<exists>y\<in>Rep_pd_basis v. compact_le x y)"
     1.8 +  "lower_le = (\<lambda>u v. \<forall>x\<in>Rep_pd_basis u. \<exists>y\<in>Rep_pd_basis v. x \<sqsubseteq> y)"
     1.9  
    1.10  lemma lower_le_refl [simp]: "t \<le>\<flat> t"
    1.11 -unfolding lower_le_def by (fast intro: compact_le_refl)
    1.12 +unfolding lower_le_def by fast
    1.13  
    1.14  lemma lower_le_trans: "\<lbrakk>t \<le>\<flat> u; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> t \<le>\<flat> v"
    1.15  unfolding lower_le_def
    1.16 @@ -24,7 +24,7 @@
    1.17  apply (drule (1) bspec, erule bexE)
    1.18  apply (drule (1) bspec, erule bexE)
    1.19  apply (erule rev_bexI)
    1.20 -apply (erule (1) compact_le_trans)
    1.21 +apply (erule (1) trans_less)
    1.22  done
    1.23  
    1.24  interpretation lower_le: preorder [lower_le]
    1.25 @@ -34,17 +34,17 @@
    1.26  unfolding lower_le_def Rep_PDUnit
    1.27  by (simp, rule Rep_pd_basis_nonempty [folded ex_in_conv])
    1.28  
    1.29 -lemma PDUnit_lower_mono: "compact_le x y \<Longrightarrow> PDUnit x \<le>\<flat> PDUnit y"
    1.30 +lemma PDUnit_lower_mono: "x \<sqsubseteq> y \<Longrightarrow> PDUnit x \<le>\<flat> PDUnit y"
    1.31  unfolding lower_le_def Rep_PDUnit by fast
    1.32  
    1.33  lemma PDPlus_lower_mono: "\<lbrakk>s \<le>\<flat> t; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<flat> PDPlus t v"
    1.34  unfolding lower_le_def Rep_PDPlus by fast
    1.35  
    1.36  lemma PDPlus_lower_less: "t \<le>\<flat> PDPlus t u"
    1.37 -unfolding lower_le_def Rep_PDPlus by (fast intro: compact_le_refl)
    1.38 +unfolding lower_le_def Rep_PDPlus by fast
    1.39  
    1.40  lemma lower_le_PDUnit_PDUnit_iff [simp]:
    1.41 -  "(PDUnit a \<le>\<flat> PDUnit b) = compact_le a b"
    1.42 +  "(PDUnit a \<le>\<flat> PDUnit b) = a \<sqsubseteq> b"
    1.43  unfolding lower_le_def Rep_PDUnit by fast
    1.44  
    1.45  lemma lower_le_PDUnit_PDPlus_iff:
    1.46 @@ -56,7 +56,7 @@
    1.47  
    1.48  lemma lower_le_induct [induct set: lower_le]:
    1.49    assumes le: "t \<le>\<flat> u"
    1.50 -  assumes 1: "\<And>a b. compact_le a b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
    1.51 +  assumes 1: "\<And>a b. a \<sqsubseteq> b \<Longrightarrow> P (PDUnit a) (PDUnit b)"
    1.52    assumes 2: "\<And>t u a. P (PDUnit a) t \<Longrightarrow> P (PDUnit a) (PDPlus t u)"
    1.53    assumes 3: "\<And>t u v. \<lbrakk>P t v; P u v\<rbrakk> \<Longrightarrow> P (PDPlus t u) v"
    1.54    shows "P t u"
    1.55 @@ -123,18 +123,18 @@
    1.56  done
    1.57  
    1.58  interpretation lower_pd:
    1.59 -  bifinite_basis [lower_le lower_principal Rep_lower_pd approx_pd]
    1.60 +  bifinite_basis [lower_le approx_pd lower_principal Rep_lower_pd]
    1.61  apply unfold_locales
    1.62 -apply (rule ideal_Rep_lower_pd)
    1.63 -apply (rule cont_Rep_lower_pd)
    1.64 -apply (rule Rep_lower_principal)
    1.65 -apply (simp only: less_lower_pd_def less_set_def)
    1.66  apply (rule approx_pd_lower_le)
    1.67  apply (rule approx_pd_idem)
    1.68  apply (erule approx_pd_lower_mono)
    1.69  apply (rule approx_pd_lower_mono1, simp)
    1.70  apply (rule finite_range_approx_pd)
    1.71  apply (rule ex_approx_pd_eq)
    1.72 +apply (rule ideal_Rep_lower_pd)
    1.73 +apply (rule cont_Rep_lower_pd)
    1.74 +apply (rule Rep_lower_principal)
    1.75 +apply (simp only: less_lower_pd_def less_set_def)
    1.76  done
    1.77  
    1.78  lemma lower_principal_less_iff [simp]: