rename approx_pd to pd_take
authorhuffman
Tue Jul 01 00:58:19 2008 +0200 (2008-07-01)
changeset 27405785f5dbec8f4
parent 27404 62171da527d6
child 27406 3897988917a3
rename approx_pd to pd_take
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/CompactBasis.thy	Tue Jul 01 00:52:46 2008 +0200
     1.2 +++ b/src/HOLCF/CompactBasis.thy	Tue Jul 01 00:58:19 2008 +0200
     1.3 @@ -246,42 +246,42 @@
     1.4    shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
     1.5  unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
     1.6  
     1.7 -text {* approx-pd *}
     1.8 +text {* Take function for powerdomain basis *}
     1.9  
    1.10  definition
    1.11 -  approx_pd :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
    1.12 -  "approx_pd n = (\<lambda>t. Abs_pd_basis (compact_approx n ` Rep_pd_basis t))"
    1.13 +  pd_take :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
    1.14 +  "pd_take n = (\<lambda>t. Abs_pd_basis (compact_approx n ` Rep_pd_basis t))"
    1.15  
    1.16 -lemma Rep_approx_pd:
    1.17 -  "Rep_pd_basis (approx_pd n t) = compact_approx n ` Rep_pd_basis t"
    1.18 -unfolding approx_pd_def
    1.19 +lemma Rep_pd_take:
    1.20 +  "Rep_pd_basis (pd_take n t) = compact_approx n ` Rep_pd_basis t"
    1.21 +unfolding pd_take_def
    1.22  apply (rule Abs_pd_basis_inverse)
    1.23  apply (simp add: pd_basis_def)
    1.24  done
    1.25  
    1.26 -lemma approx_pd_simps [simp]:
    1.27 -  "approx_pd n (PDUnit a) = PDUnit (compact_approx n a)"
    1.28 -  "approx_pd n (PDPlus t u) = PDPlus (approx_pd n t) (approx_pd n u)"
    1.29 +lemma pd_take_simps [simp]:
    1.30 +  "pd_take n (PDUnit a) = PDUnit (compact_approx n a)"
    1.31 +  "pd_take n (PDPlus t u) = PDPlus (pd_take n t) (pd_take n u)"
    1.32  apply (simp_all add: Rep_pd_basis_inject [symmetric])
    1.33 -apply (simp_all add: Rep_approx_pd Rep_PDUnit Rep_PDPlus image_Un)
    1.34 +apply (simp_all add: Rep_pd_take Rep_PDUnit Rep_PDPlus image_Un)
    1.35  done
    1.36  
    1.37 -lemma approx_pd_idem: "approx_pd n (approx_pd n t) = approx_pd n t"
    1.38 +lemma pd_take_idem: "pd_take n (pd_take n t) = pd_take n t"
    1.39  apply (induct t rule: pd_basis_induct)
    1.40  apply (simp add: compact_basis.take_take)
    1.41  apply simp
    1.42  done
    1.43  
    1.44 -lemma finite_range_approx_pd: "finite (range (approx_pd n))"
    1.45 +lemma finite_range_pd_take: "finite (range (pd_take n))"
    1.46  apply (rule finite_imageD [where f="Rep_pd_basis"])
    1.47  apply (rule finite_subset [where B="Pow (range (compact_approx n))"])
    1.48 -apply (clarsimp simp add: Rep_approx_pd)
    1.49 +apply (clarsimp simp add: Rep_pd_take)
    1.50  apply (simp add: compact_basis.finite_range_take)
    1.51  apply (rule inj_onI, simp add: Rep_pd_basis_inject)
    1.52  done
    1.53  
    1.54 -lemma approx_pd_covers: "\<exists>n. approx_pd n t = t"
    1.55 -apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. approx_pd m t = t", fast)
    1.56 +lemma pd_take_covers: "\<exists>n. pd_take n t = t"
    1.57 +apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. pd_take m t = t", fast)
    1.58  apply (induct t rule: pd_basis_induct)
    1.59  apply (cut_tac a=a in compact_basis.take_covers)
    1.60  apply (clarify, rule_tac x=n in exI)
     2.1 --- a/src/HOLCF/ConvexPD.thy	Tue Jul 01 00:52:46 2008 +0200
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Tue Jul 01 00:58:19 2008 +0200
     2.3 @@ -117,21 +117,21 @@
     2.4  apply (simp add: 4)
     2.5  done
     2.6  
     2.7 -lemma approx_pd_convex_chain:
     2.8 -  "approx_pd n t \<le>\<natural> approx_pd (Suc n) t"
     2.9 +lemma pd_take_convex_chain:
    2.10 +  "pd_take n t \<le>\<natural> pd_take (Suc n) t"
    2.11  apply (induct t rule: pd_basis_induct)
    2.12  apply (simp add: compact_basis.take_chain)
    2.13  apply (simp add: PDPlus_convex_mono)
    2.14  done
    2.15  
    2.16 -lemma approx_pd_convex_le: "approx_pd i t \<le>\<natural> t"
    2.17 +lemma pd_take_convex_le: "pd_take i t \<le>\<natural> t"
    2.18  apply (induct t rule: pd_basis_induct)
    2.19  apply (simp add: compact_basis.take_less)
    2.20  apply (simp add: PDPlus_convex_mono)
    2.21  done
    2.22  
    2.23 -lemma approx_pd_convex_mono:
    2.24 -  "t \<le>\<natural> u \<Longrightarrow> approx_pd n t \<le>\<natural> approx_pd n u"
    2.25 +lemma pd_take_convex_mono:
    2.26 +  "t \<le>\<natural> u \<Longrightarrow> pd_take n t \<le>\<natural> pd_take n u"
    2.27  apply (erule convex_le_induct)
    2.28  apply (erule (1) convex_le_trans)
    2.29  apply (simp add: compact_basis.take_mono)
    2.30 @@ -180,14 +180,14 @@
    2.31  by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
    2.32  
    2.33  interpretation convex_pd:
    2.34 -  ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
    2.35 +  ideal_completion [convex_le pd_take convex_principal Rep_convex_pd]
    2.36  apply unfold_locales
    2.37 -apply (rule approx_pd_convex_le)
    2.38 -apply (rule approx_pd_idem)
    2.39 -apply (erule approx_pd_convex_mono)
    2.40 -apply (rule approx_pd_convex_chain)
    2.41 -apply (rule finite_range_approx_pd)
    2.42 -apply (rule approx_pd_covers)
    2.43 +apply (rule pd_take_convex_le)
    2.44 +apply (rule pd_take_idem)
    2.45 +apply (erule pd_take_convex_mono)
    2.46 +apply (rule pd_take_convex_chain)
    2.47 +apply (rule finite_range_pd_take)
    2.48 +apply (rule pd_take_covers)
    2.49  apply (rule ideal_Rep_convex_pd)
    2.50  apply (erule Rep_convex_pd_lub)
    2.51  apply (rule Rep_convex_principal)
    2.52 @@ -226,12 +226,12 @@
    2.53  instance convex_pd :: (bifinite) bifinite ..
    2.54  
    2.55  lemma approx_convex_principal [simp]:
    2.56 -  "approx n\<cdot>(convex_principal t) = convex_principal (approx_pd n t)"
    2.57 +  "approx n\<cdot>(convex_principal t) = convex_principal (pd_take n t)"
    2.58  unfolding approx_convex_pd_def
    2.59  by (rule convex_pd.completion_approx_principal)
    2.60  
    2.61  lemma approx_eq_convex_principal:
    2.62 -  "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
    2.63 +  "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (pd_take n t)"
    2.64  unfolding approx_convex_pd_def
    2.65  by (rule convex_pd.completion_approx_eq_principal)
    2.66  
     3.1 --- a/src/HOLCF/LowerPD.thy	Tue Jul 01 00:52:46 2008 +0200
     3.2 +++ b/src/HOLCF/LowerPD.thy	Tue Jul 01 00:58:19 2008 +0200
     3.3 @@ -72,21 +72,21 @@
     3.4  apply (simp add: lower_le_PDPlus_iff 3)
     3.5  done
     3.6  
     3.7 -lemma approx_pd_lower_chain:
     3.8 -  "approx_pd n t \<le>\<flat> approx_pd (Suc n) t"
     3.9 +lemma pd_take_lower_chain:
    3.10 +  "pd_take n t \<le>\<flat> pd_take (Suc n) t"
    3.11  apply (induct t rule: pd_basis_induct)
    3.12  apply (simp add: compact_basis.take_chain)
    3.13  apply (simp add: PDPlus_lower_mono)
    3.14  done
    3.15  
    3.16 -lemma approx_pd_lower_le: "approx_pd i t \<le>\<flat> t"
    3.17 +lemma pd_take_lower_le: "pd_take i t \<le>\<flat> t"
    3.18  apply (induct t rule: pd_basis_induct)
    3.19  apply (simp add: compact_basis.take_less)
    3.20  apply (simp add: PDPlus_lower_mono)
    3.21  done
    3.22  
    3.23 -lemma approx_pd_lower_mono:
    3.24 -  "t \<le>\<flat> u \<Longrightarrow> approx_pd n t \<le>\<flat> approx_pd n u"
    3.25 +lemma pd_take_lower_mono:
    3.26 +  "t \<le>\<flat> u \<Longrightarrow> pd_take n t \<le>\<flat> pd_take n u"
    3.27  apply (erule lower_le_induct)
    3.28  apply (simp add: compact_basis.take_mono)
    3.29  apply (simp add: lower_le_PDUnit_PDPlus_iff)
    3.30 @@ -135,14 +135,14 @@
    3.31  by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
    3.32  
    3.33  interpretation lower_pd:
    3.34 -  ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd]
    3.35 +  ideal_completion [lower_le pd_take lower_principal Rep_lower_pd]
    3.36  apply unfold_locales
    3.37 -apply (rule approx_pd_lower_le)
    3.38 -apply (rule approx_pd_idem)
    3.39 -apply (erule approx_pd_lower_mono)
    3.40 -apply (rule approx_pd_lower_chain)
    3.41 -apply (rule finite_range_approx_pd)
    3.42 -apply (rule approx_pd_covers)
    3.43 +apply (rule pd_take_lower_le)
    3.44 +apply (rule pd_take_idem)
    3.45 +apply (erule pd_take_lower_mono)
    3.46 +apply (rule pd_take_lower_chain)
    3.47 +apply (rule finite_range_pd_take)
    3.48 +apply (rule pd_take_covers)
    3.49  apply (rule ideal_Rep_lower_pd)
    3.50  apply (erule Rep_lower_pd_lub)
    3.51  apply (rule Rep_lower_principal)
    3.52 @@ -181,12 +181,12 @@
    3.53  instance lower_pd :: (bifinite) bifinite ..
    3.54  
    3.55  lemma approx_lower_principal [simp]:
    3.56 -  "approx n\<cdot>(lower_principal t) = lower_principal (approx_pd n t)"
    3.57 +  "approx n\<cdot>(lower_principal t) = lower_principal (pd_take n t)"
    3.58  unfolding approx_lower_pd_def
    3.59  by (rule lower_pd.completion_approx_principal)
    3.60  
    3.61  lemma approx_eq_lower_principal:
    3.62 -  "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
    3.63 +  "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (pd_take n t)"
    3.64  unfolding approx_lower_pd_def
    3.65  by (rule lower_pd.completion_approx_eq_principal)
    3.66  
     4.1 --- a/src/HOLCF/UpperPD.thy	Tue Jul 01 00:52:46 2008 +0200
     4.2 +++ b/src/HOLCF/UpperPD.thy	Tue Jul 01 00:58:19 2008 +0200
     4.3 @@ -70,21 +70,21 @@
     4.4  apply (simp add: upper_le_PDPlus_iff 3)
     4.5  done
     4.6  
     4.7 -lemma approx_pd_upper_chain:
     4.8 -  "approx_pd n t \<le>\<sharp> approx_pd (Suc n) t"
     4.9 +lemma pd_take_upper_chain:
    4.10 +  "pd_take n t \<le>\<sharp> pd_take (Suc n) t"
    4.11  apply (induct t rule: pd_basis_induct)
    4.12  apply (simp add: compact_basis.take_chain)
    4.13  apply (simp add: PDPlus_upper_mono)
    4.14  done
    4.15  
    4.16 -lemma approx_pd_upper_le: "approx_pd i t \<le>\<sharp> t"
    4.17 +lemma pd_take_upper_le: "pd_take i t \<le>\<sharp> t"
    4.18  apply (induct t rule: pd_basis_induct)
    4.19  apply (simp add: compact_basis.take_less)
    4.20  apply (simp add: PDPlus_upper_mono)
    4.21  done
    4.22  
    4.23 -lemma approx_pd_upper_mono:
    4.24 -  "t \<le>\<sharp> u \<Longrightarrow> approx_pd n t \<le>\<sharp> approx_pd n u"
    4.25 +lemma pd_take_upper_mono:
    4.26 +  "t \<le>\<sharp> u \<Longrightarrow> pd_take n t \<le>\<sharp> pd_take n u"
    4.27  apply (erule upper_le_induct)
    4.28  apply (simp add: compact_basis.take_mono)
    4.29  apply (simp add: upper_le_PDPlus_PDUnit_iff)
    4.30 @@ -133,14 +133,14 @@
    4.31  by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
    4.32  
    4.33  interpretation upper_pd:
    4.34 -  ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd]
    4.35 +  ideal_completion [upper_le pd_take upper_principal Rep_upper_pd]
    4.36  apply unfold_locales
    4.37 -apply (rule approx_pd_upper_le)
    4.38 -apply (rule approx_pd_idem)
    4.39 -apply (erule approx_pd_upper_mono)
    4.40 -apply (rule approx_pd_upper_chain)
    4.41 -apply (rule finite_range_approx_pd)
    4.42 -apply (rule approx_pd_covers)
    4.43 +apply (rule pd_take_upper_le)
    4.44 +apply (rule pd_take_idem)
    4.45 +apply (erule pd_take_upper_mono)
    4.46 +apply (rule pd_take_upper_chain)
    4.47 +apply (rule finite_range_pd_take)
    4.48 +apply (rule pd_take_covers)
    4.49  apply (rule ideal_Rep_upper_pd)
    4.50  apply (erule Rep_upper_pd_lub)
    4.51  apply (rule Rep_upper_principal)
    4.52 @@ -179,12 +179,12 @@
    4.53  instance upper_pd :: (bifinite) bifinite ..
    4.54  
    4.55  lemma approx_upper_principal [simp]:
    4.56 -  "approx n\<cdot>(upper_principal t) = upper_principal (approx_pd n t)"
    4.57 +  "approx n\<cdot>(upper_principal t) = upper_principal (pd_take n t)"
    4.58  unfolding approx_upper_pd_def
    4.59  by (rule upper_pd.completion_approx_principal)
    4.60  
    4.61  lemma approx_eq_upper_principal:
    4.62 -  "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
    4.63 +  "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (pd_take n t)"
    4.64  unfolding approx_upper_pd_def
    4.65  by (rule upper_pd.completion_approx_eq_principal)
    4.66