# HG changeset patch # User huffman # Date 1214866699 -7200 # Node ID 785f5dbec8f44f78cb60dff38acd29bfba8ee0e9 # Parent 62171da527d6101b318b328fcad82103c74b464b rename approx_pd to pd_take diff -r 62171da527d6 -r 785f5dbec8f4 src/HOLCF/CompactBasis.thy --- 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 \ 'a pd_basis \ 'a pd_basis" where - "approx_pd n = (\t. Abs_pd_basis (compact_approx n ` Rep_pd_basis t))" + pd_take :: "nat \ 'a pd_basis \ 'a pd_basis" where + "pd_take n = (\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: "\n. approx_pd n t = t" -apply (subgoal_tac "\n. \m\n. approx_pd m t = t", fast) +lemma pd_take_covers: "\n. pd_take n t = t" +apply (subgoal_tac "\n. \m\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) diff -r 62171da527d6 -r 785f5dbec8f4 src/HOLCF/ConvexPD.thy --- 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 \\ approx_pd (Suc n) t" +lemma pd_take_convex_chain: + "pd_take n t \\ 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 \\ t" +lemma pd_take_convex_le: "pd_take i t \\ 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 \\ u \ approx_pd n t \\ approx_pd n u" +lemma pd_take_convex_mono: + "t \\ u \ pd_take n t \\ 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\(convex_principal t) = convex_principal (approx_pd n t)" + "approx n\(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: - "\t\Rep_convex_pd xs. approx n\xs = convex_principal (approx_pd n t)" + "\t\Rep_convex_pd xs. approx n\xs = convex_principal (pd_take n t)" unfolding approx_convex_pd_def by (rule convex_pd.completion_approx_eq_principal) diff -r 62171da527d6 -r 785f5dbec8f4 src/HOLCF/LowerPD.thy --- 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 \\ approx_pd (Suc n) t" +lemma pd_take_lower_chain: + "pd_take n t \\ 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 \\ t" +lemma pd_take_lower_le: "pd_take i t \\ 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 \\ u \ approx_pd n t \\ approx_pd n u" +lemma pd_take_lower_mono: + "t \\ u \ pd_take n t \\ 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\(lower_principal t) = lower_principal (approx_pd n t)" + "approx n\(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: - "\t\Rep_lower_pd xs. approx n\xs = lower_principal (approx_pd n t)" + "\t\Rep_lower_pd xs. approx n\xs = lower_principal (pd_take n t)" unfolding approx_lower_pd_def by (rule lower_pd.completion_approx_eq_principal) diff -r 62171da527d6 -r 785f5dbec8f4 src/HOLCF/UpperPD.thy --- 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 \\ approx_pd (Suc n) t" +lemma pd_take_upper_chain: + "pd_take n t \\ 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 \\ t" +lemma pd_take_upper_le: "pd_take i t \\ 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 \\ u \ approx_pd n t \\ approx_pd n u" +lemma pd_take_upper_mono: + "t \\ u \ pd_take n t \\ 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\(upper_principal t) = upper_principal (approx_pd n t)" + "approx n\(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: - "\t\Rep_upper_pd xs. approx n\xs = upper_principal (approx_pd n t)" + "\t\Rep_upper_pd xs. approx n\xs = upper_principal (pd_take n t)" unfolding approx_upper_pd_def by (rule upper_pd.completion_approx_eq_principal)