author huffman Tue, 01 Jul 2008 01:09:03 +0200 changeset 27406 3897988917a3 parent 27405 785f5dbec8f4 child 27407 68e111812b83
rename compact_approx to compact_take
```--- 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

-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 (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)
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_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))"])