# HG changeset patch
# User huffman
# Date 1214867343 -7200
# Node ID 3897988917a327d36dbcf8a6ddfe77db4f119a9e
# Parent  785f5dbec8f44f78cb60dff38acd29bfba8ee0e9
rename compact_approx to compact_take

diff -r 785f5dbec8f4 -r 3897988917a3 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Tue Jul 01 00:58:19 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy	Tue Jul 01 01:09:03 2008 +0200
@@ -37,51 +37,51 @@
 text {* Take function for compact basis *}
 
 definition
-  compact_approx :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where
-  "compact_approx = (\<lambda>n a. Abs_compact_basis (approx n\<cdot>(Rep_compact_basis a)))"
+  compact_take :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where
+  "compact_take = (\<lambda>n a. Abs_compact_basis (approx n\<cdot>(Rep_compact_basis a)))"
 
-lemma Rep_compact_approx:
-  "Rep_compact_basis (compact_approx n a) = approx n\<cdot>(Rep_compact_basis a)"
-unfolding compact_approx_def
+lemma Rep_compact_take:
+  "Rep_compact_basis (compact_take n a) = approx n\<cdot>(Rep_compact_basis a)"
+unfolding compact_take_def
 by (simp add: Abs_compact_basis_inverse)
 
-lemmas approx_Rep_compact_basis = Rep_compact_approx [symmetric]
+lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
 
 interpretation compact_basis:
-  basis_take [sq_le compact_approx]
+  basis_take [sq_le compact_take]
 proof
   fix n :: nat and a :: "'a compact_basis"
-  show "compact_approx n a \<sqsubseteq> a"
+  show "compact_take n a \<sqsubseteq> a"
     unfolding compact_le_def
-    by (simp add: Rep_compact_approx approx_less)
+    by (simp add: Rep_compact_take approx_less)
 next
   fix n :: nat and a :: "'a compact_basis"
-  show "compact_approx n (compact_approx n a) = compact_approx n a"
-    by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_approx)
+  show "compact_take n (compact_take n a) = compact_take n a"
+    by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_take)
 next
   fix n :: nat and a b :: "'a compact_basis"
-  assume "a \<sqsubseteq> b" thus "compact_approx n a \<sqsubseteq> compact_approx n b"
-    unfolding compact_le_def Rep_compact_approx
+  assume "a \<sqsubseteq> b" thus "compact_take n a \<sqsubseteq> compact_take n b"
+    unfolding compact_le_def Rep_compact_take
     by (rule monofun_cfun_arg)
 next
   fix n :: nat and a :: "'a compact_basis"
-  show "\<And>n a. compact_approx n a \<sqsubseteq> compact_approx (Suc n) a"
-    unfolding compact_le_def Rep_compact_approx
+  show "\<And>n a. compact_take n a \<sqsubseteq> compact_take (Suc n) a"
+    unfolding compact_le_def Rep_compact_take
     by (rule chainE, simp)
 next
   fix n :: nat
-  show "finite (range (compact_approx n))"
+  show "finite (range (compact_take n))"
     apply (rule finite_imageD [where f="Rep_compact_basis"])
     apply (rule finite_subset [where B="range (\<lambda>x. approx n\<cdot>x)"])
-    apply (clarsimp simp add: Rep_compact_approx)
+    apply (clarsimp simp add: Rep_compact_take)
     apply (rule finite_range_approx)
     apply (rule inj_onI, simp add: Rep_compact_basis_inject)
     done
 next
   fix a :: "'a compact_basis"
-  show "\<exists>n. compact_approx n a = a"
+  show "\<exists>n. compact_take n a = a"
     apply (simp add: Rep_compact_basis_inject [symmetric])
-    apply (simp add: Rep_compact_approx)
+    apply (simp add: Rep_compact_take)
     apply (rule profinite_compact_eq_approx)
     apply (rule compact_Rep_compact_basis)
     done
@@ -94,7 +94,7 @@
   "compacts = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
 
 interpretation compact_basis:
-  ideal_completion [sq_le compact_approx Rep_compact_basis compacts]
+  ideal_completion [sq_le compact_take Rep_compact_basis compacts]
 proof
   fix w :: 'a
   show "preorder.ideal sq_le (compacts w)"
@@ -250,17 +250,17 @@
 
 definition
   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))"
+  "pd_take n = (\<lambda>t. Abs_pd_basis (compact_take n ` Rep_pd_basis t))"
 
 lemma Rep_pd_take:
-  "Rep_pd_basis (pd_take n t) = compact_approx n ` Rep_pd_basis t"
+  "Rep_pd_basis (pd_take n t) = compact_take n ` Rep_pd_basis t"
 unfolding pd_take_def
 apply (rule Abs_pd_basis_inverse)
 apply (simp add: pd_basis_def)
 done
 
 lemma pd_take_simps [simp]:
-  "pd_take n (PDUnit a) = PDUnit (compact_approx n a)"
+  "pd_take n (PDUnit a) = PDUnit (compact_take 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_pd_take Rep_PDUnit Rep_PDPlus image_Un)
@@ -274,7 +274,7 @@
 
 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 (rule finite_subset [where B="Pow (range (compact_take n))"])
 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)