src/HOLCF/UpperPD.thy
changeset 27405 785f5dbec8f4
parent 27373 5794a0e3e26c
child 29138 661a8db7e647
child 29237 e90d9d51106b
     1.1 --- a/src/HOLCF/UpperPD.thy	Tue Jul 01 00:52:46 2008 +0200
     1.2 +++ b/src/HOLCF/UpperPD.thy	Tue Jul 01 00:58:19 2008 +0200
     1.3 @@ -70,21 +70,21 @@
     1.4  apply (simp add: upper_le_PDPlus_iff 3)
     1.5  done
     1.6  
     1.7 -lemma approx_pd_upper_chain:
     1.8 -  "approx_pd n t \<le>\<sharp> approx_pd (Suc n) t"
     1.9 +lemma pd_take_upper_chain:
    1.10 +  "pd_take n t \<le>\<sharp> pd_take (Suc n) t"
    1.11  apply (induct t rule: pd_basis_induct)
    1.12  apply (simp add: compact_basis.take_chain)
    1.13  apply (simp add: PDPlus_upper_mono)
    1.14  done
    1.15  
    1.16 -lemma approx_pd_upper_le: "approx_pd i t \<le>\<sharp> t"
    1.17 +lemma pd_take_upper_le: "pd_take i t \<le>\<sharp> t"
    1.18  apply (induct t rule: pd_basis_induct)
    1.19  apply (simp add: compact_basis.take_less)
    1.20  apply (simp add: PDPlus_upper_mono)
    1.21  done
    1.22  
    1.23 -lemma approx_pd_upper_mono:
    1.24 -  "t \<le>\<sharp> u \<Longrightarrow> approx_pd n t \<le>\<sharp> approx_pd n u"
    1.25 +lemma pd_take_upper_mono:
    1.26 +  "t \<le>\<sharp> u \<Longrightarrow> pd_take n t \<le>\<sharp> pd_take n u"
    1.27  apply (erule upper_le_induct)
    1.28  apply (simp add: compact_basis.take_mono)
    1.29  apply (simp add: upper_le_PDPlus_PDUnit_iff)
    1.30 @@ -133,14 +133,14 @@
    1.31  by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
    1.32  
    1.33  interpretation upper_pd:
    1.34 -  ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd]
    1.35 +  ideal_completion [upper_le pd_take upper_principal Rep_upper_pd]
    1.36  apply unfold_locales
    1.37 -apply (rule approx_pd_upper_le)
    1.38 -apply (rule approx_pd_idem)
    1.39 -apply (erule approx_pd_upper_mono)
    1.40 -apply (rule approx_pd_upper_chain)
    1.41 -apply (rule finite_range_approx_pd)
    1.42 -apply (rule approx_pd_covers)
    1.43 +apply (rule pd_take_upper_le)
    1.44 +apply (rule pd_take_idem)
    1.45 +apply (erule pd_take_upper_mono)
    1.46 +apply (rule pd_take_upper_chain)
    1.47 +apply (rule finite_range_pd_take)
    1.48 +apply (rule pd_take_covers)
    1.49  apply (rule ideal_Rep_upper_pd)
    1.50  apply (erule Rep_upper_pd_lub)
    1.51  apply (rule Rep_upper_principal)
    1.52 @@ -179,12 +179,12 @@
    1.53  instance upper_pd :: (bifinite) bifinite ..
    1.54  
    1.55  lemma approx_upper_principal [simp]:
    1.56 -  "approx n\<cdot>(upper_principal t) = upper_principal (approx_pd n t)"
    1.57 +  "approx n\<cdot>(upper_principal t) = upper_principal (pd_take n t)"
    1.58  unfolding approx_upper_pd_def
    1.59  by (rule upper_pd.completion_approx_principal)
    1.60  
    1.61  lemma approx_eq_upper_principal:
    1.62 -  "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
    1.63 +  "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (pd_take n t)"
    1.64  unfolding approx_upper_pd_def
    1.65  by (rule upper_pd.completion_approx_eq_principal)
    1.66