--- a/src/HOLCF/CompactBasis.thy Tue Jul 01 00:52:46 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy Tue Jul 01 00:58:19 2008 +0200
@@ -246,42 +246,42 @@
shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
-text {* approx-pd *}
+text {* Take function for powerdomain basis *}
definition
- approx_pd :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
- "approx_pd n = (\<lambda>t. Abs_pd_basis (compact_approx n ` Rep_pd_basis t))"
+ pd_take :: "nat \<Rightarrow> 'a pd_basis \<Rightarrow> 'a pd_basis" where
+ "pd_take n = (\<lambda>t. Abs_pd_basis (compact_approx n ` Rep_pd_basis t))"
-lemma Rep_approx_pd:
- "Rep_pd_basis (approx_pd n t) = compact_approx n ` Rep_pd_basis t"
-unfolding approx_pd_def
+lemma Rep_pd_take:
+ "Rep_pd_basis (pd_take n t) = compact_approx n ` Rep_pd_basis t"
+unfolding pd_take_def
apply (rule Abs_pd_basis_inverse)
apply (simp add: pd_basis_def)
done
-lemma approx_pd_simps [simp]:
- "approx_pd n (PDUnit a) = PDUnit (compact_approx n a)"
- "approx_pd n (PDPlus t u) = PDPlus (approx_pd n t) (approx_pd n u)"
+lemma pd_take_simps [simp]:
+ "pd_take n (PDUnit a) = PDUnit (compact_approx n a)"
+ "pd_take n (PDPlus t u) = PDPlus (pd_take n t) (pd_take n u)"
apply (simp_all add: Rep_pd_basis_inject [symmetric])
-apply (simp_all add: Rep_approx_pd Rep_PDUnit Rep_PDPlus image_Un)
+apply (simp_all add: Rep_pd_take Rep_PDUnit Rep_PDPlus image_Un)
done
-lemma approx_pd_idem: "approx_pd n (approx_pd n t) = approx_pd n t"
+lemma pd_take_idem: "pd_take n (pd_take n t) = pd_take n t"
apply (induct t rule: pd_basis_induct)
apply (simp add: compact_basis.take_take)
apply simp
done
-lemma finite_range_approx_pd: "finite (range (approx_pd n))"
+lemma finite_range_pd_take: "finite (range (pd_take n))"
apply (rule finite_imageD [where f="Rep_pd_basis"])
apply (rule finite_subset [where B="Pow (range (compact_approx n))"])
-apply (clarsimp simp add: Rep_approx_pd)
+apply (clarsimp simp add: Rep_pd_take)
apply (simp add: compact_basis.finite_range_take)
apply (rule inj_onI, simp add: Rep_pd_basis_inject)
done
-lemma approx_pd_covers: "\<exists>n. approx_pd n t = t"
-apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. approx_pd m t = t", fast)
+lemma pd_take_covers: "\<exists>n. pd_take n t = t"
+apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. pd_take m t = t", fast)
apply (induct t rule: pd_basis_induct)
apply (cut_tac a=a in compact_basis.take_covers)
apply (clarify, rule_tac x=n in exI)
--- a/src/HOLCF/ConvexPD.thy Tue Jul 01 00:52:46 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy Tue Jul 01 00:58:19 2008 +0200
@@ -117,21 +117,21 @@
apply (simp add: 4)
done
-lemma approx_pd_convex_chain:
- "approx_pd n t \<le>\<natural> approx_pd (Suc n) t"
+lemma pd_take_convex_chain:
+ "pd_take n t \<le>\<natural> pd_take (Suc n) t"
apply (induct t rule: pd_basis_induct)
apply (simp add: compact_basis.take_chain)
apply (simp add: PDPlus_convex_mono)
done
-lemma approx_pd_convex_le: "approx_pd i t \<le>\<natural> t"
+lemma pd_take_convex_le: "pd_take i t \<le>\<natural> t"
apply (induct t rule: pd_basis_induct)
apply (simp add: compact_basis.take_less)
apply (simp add: PDPlus_convex_mono)
done
-lemma approx_pd_convex_mono:
- "t \<le>\<natural> u \<Longrightarrow> approx_pd n t \<le>\<natural> approx_pd n u"
+lemma pd_take_convex_mono:
+ "t \<le>\<natural> u \<Longrightarrow> pd_take n t \<le>\<natural> pd_take n u"
apply (erule convex_le_induct)
apply (erule (1) convex_le_trans)
apply (simp add: compact_basis.take_mono)
@@ -180,14 +180,14 @@
by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
interpretation convex_pd:
- ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
+ ideal_completion [convex_le pd_take convex_principal Rep_convex_pd]
apply unfold_locales
-apply (rule approx_pd_convex_le)
-apply (rule approx_pd_idem)
-apply (erule approx_pd_convex_mono)
-apply (rule approx_pd_convex_chain)
-apply (rule finite_range_approx_pd)
-apply (rule approx_pd_covers)
+apply (rule pd_take_convex_le)
+apply (rule pd_take_idem)
+apply (erule pd_take_convex_mono)
+apply (rule pd_take_convex_chain)
+apply (rule finite_range_pd_take)
+apply (rule pd_take_covers)
apply (rule ideal_Rep_convex_pd)
apply (erule Rep_convex_pd_lub)
apply (rule Rep_convex_principal)
@@ -226,12 +226,12 @@
instance convex_pd :: (bifinite) bifinite ..
lemma approx_convex_principal [simp]:
- "approx n\<cdot>(convex_principal t) = convex_principal (approx_pd n t)"
+ "approx n\<cdot>(convex_principal t) = convex_principal (pd_take n t)"
unfolding approx_convex_pd_def
by (rule convex_pd.completion_approx_principal)
lemma approx_eq_convex_principal:
- "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
+ "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (pd_take n t)"
unfolding approx_convex_pd_def
by (rule convex_pd.completion_approx_eq_principal)
--- a/src/HOLCF/LowerPD.thy Tue Jul 01 00:52:46 2008 +0200
+++ b/src/HOLCF/LowerPD.thy Tue Jul 01 00:58:19 2008 +0200
@@ -72,21 +72,21 @@
apply (simp add: lower_le_PDPlus_iff 3)
done
-lemma approx_pd_lower_chain:
- "approx_pd n t \<le>\<flat> approx_pd (Suc n) t"
+lemma pd_take_lower_chain:
+ "pd_take n t \<le>\<flat> pd_take (Suc n) t"
apply (induct t rule: pd_basis_induct)
apply (simp add: compact_basis.take_chain)
apply (simp add: PDPlus_lower_mono)
done
-lemma approx_pd_lower_le: "approx_pd i t \<le>\<flat> t"
+lemma pd_take_lower_le: "pd_take i t \<le>\<flat> t"
apply (induct t rule: pd_basis_induct)
apply (simp add: compact_basis.take_less)
apply (simp add: PDPlus_lower_mono)
done
-lemma approx_pd_lower_mono:
- "t \<le>\<flat> u \<Longrightarrow> approx_pd n t \<le>\<flat> approx_pd n u"
+lemma pd_take_lower_mono:
+ "t \<le>\<flat> u \<Longrightarrow> pd_take n t \<le>\<flat> pd_take n u"
apply (erule lower_le_induct)
apply (simp add: compact_basis.take_mono)
apply (simp add: lower_le_PDUnit_PDPlus_iff)
@@ -135,14 +135,14 @@
by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
interpretation lower_pd:
- ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd]
+ ideal_completion [lower_le pd_take lower_principal Rep_lower_pd]
apply unfold_locales
-apply (rule approx_pd_lower_le)
-apply (rule approx_pd_idem)
-apply (erule approx_pd_lower_mono)
-apply (rule approx_pd_lower_chain)
-apply (rule finite_range_approx_pd)
-apply (rule approx_pd_covers)
+apply (rule pd_take_lower_le)
+apply (rule pd_take_idem)
+apply (erule pd_take_lower_mono)
+apply (rule pd_take_lower_chain)
+apply (rule finite_range_pd_take)
+apply (rule pd_take_covers)
apply (rule ideal_Rep_lower_pd)
apply (erule Rep_lower_pd_lub)
apply (rule Rep_lower_principal)
@@ -181,12 +181,12 @@
instance lower_pd :: (bifinite) bifinite ..
lemma approx_lower_principal [simp]:
- "approx n\<cdot>(lower_principal t) = lower_principal (approx_pd n t)"
+ "approx n\<cdot>(lower_principal t) = lower_principal (pd_take n t)"
unfolding approx_lower_pd_def
by (rule lower_pd.completion_approx_principal)
lemma approx_eq_lower_principal:
- "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
+ "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (pd_take n t)"
unfolding approx_lower_pd_def
by (rule lower_pd.completion_approx_eq_principal)
--- a/src/HOLCF/UpperPD.thy Tue Jul 01 00:52:46 2008 +0200
+++ b/src/HOLCF/UpperPD.thy Tue Jul 01 00:58:19 2008 +0200
@@ -70,21 +70,21 @@
apply (simp add: upper_le_PDPlus_iff 3)
done
-lemma approx_pd_upper_chain:
- "approx_pd n t \<le>\<sharp> approx_pd (Suc n) t"
+lemma pd_take_upper_chain:
+ "pd_take n t \<le>\<sharp> pd_take (Suc n) t"
apply (induct t rule: pd_basis_induct)
apply (simp add: compact_basis.take_chain)
apply (simp add: PDPlus_upper_mono)
done
-lemma approx_pd_upper_le: "approx_pd i t \<le>\<sharp> t"
+lemma pd_take_upper_le: "pd_take i t \<le>\<sharp> t"
apply (induct t rule: pd_basis_induct)
apply (simp add: compact_basis.take_less)
apply (simp add: PDPlus_upper_mono)
done
-lemma approx_pd_upper_mono:
- "t \<le>\<sharp> u \<Longrightarrow> approx_pd n t \<le>\<sharp> approx_pd n u"
+lemma pd_take_upper_mono:
+ "t \<le>\<sharp> u \<Longrightarrow> pd_take n t \<le>\<sharp> pd_take n u"
apply (erule upper_le_induct)
apply (simp add: compact_basis.take_mono)
apply (simp add: upper_le_PDPlus_PDUnit_iff)
@@ -133,14 +133,14 @@
by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
interpretation upper_pd:
- ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd]
+ ideal_completion [upper_le pd_take upper_principal Rep_upper_pd]
apply unfold_locales
-apply (rule approx_pd_upper_le)
-apply (rule approx_pd_idem)
-apply (erule approx_pd_upper_mono)
-apply (rule approx_pd_upper_chain)
-apply (rule finite_range_approx_pd)
-apply (rule approx_pd_covers)
+apply (rule pd_take_upper_le)
+apply (rule pd_take_idem)
+apply (erule pd_take_upper_mono)
+apply (rule pd_take_upper_chain)
+apply (rule finite_range_pd_take)
+apply (rule pd_take_covers)
apply (rule ideal_Rep_upper_pd)
apply (erule Rep_upper_pd_lub)
apply (rule Rep_upper_principal)
@@ -179,12 +179,12 @@
instance upper_pd :: (bifinite) bifinite ..
lemma approx_upper_principal [simp]:
- "approx n\<cdot>(upper_principal t) = upper_principal (approx_pd n t)"
+ "approx n\<cdot>(upper_principal t) = upper_principal (pd_take n t)"
unfolding approx_upper_pd_def
by (rule upper_pd.completion_approx_principal)
lemma approx_eq_upper_principal:
- "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
+ "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (pd_take n t)"
unfolding approx_upper_pd_def
by (rule upper_pd.completion_approx_eq_principal)