1.1 --- a/src/HOLCF/CompactBasis.thy	Tue Nov 25 23:26:44 2008 +0100
     1.2 +++ b/src/HOLCF/CompactBasis.thy	Tue Nov 25 23:28:06 2008 +0100
     1.3 @@ -90,25 +90,25 @@
     1.4  text {* Ideal completion *}
     1.5  
     1.6  definition
     1.7 -  compacts :: "'a \<Rightarrow> 'a compact_basis set" where
     1.8 -  "compacts = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
     1.9 +  approximants :: "'a \<Rightarrow> 'a compact_basis set" where
    1.10 +  "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
    1.11  
    1.12  interpretation compact_basis:
    1.13 -  ideal_completion [sq_le compact_take Rep_compact_basis compacts]
    1.14 +  ideal_completion [sq_le compact_take Rep_compact_basis approximants]
    1.15  proof
    1.16    fix w :: 'a
    1.17 -  show "preorder.ideal sq_le (compacts w)"
    1.18 +  show "preorder.ideal sq_le (approximants w)"
    1.19    proof (rule sq_le.idealI)
    1.20 -    show "\<exists>x. x \<in> compacts w"
    1.21 -      unfolding compacts_def
    1.22 +    show "\<exists>x. x \<in> approximants w"
    1.23 +      unfolding approximants_def
    1.24        apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
    1.25        apply (simp add: Abs_compact_basis_inverse approx_less)
    1.26        done
    1.27    next
    1.28      fix x y :: "'a compact_basis"
    1.29 -    assume "x \<in> compacts w" "y \<in> compacts w"
    1.30 -    thus "\<exists>z \<in> compacts w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    1.31 -      unfolding compacts_def
    1.32 +    assume "x \<in> approximants w" "y \<in> approximants w"
    1.33 +    thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    1.34 +      unfolding approximants_def
    1.35        apply simp
    1.36        apply (cut_tac a=x in compact_Rep_compact_basis)
    1.37        apply (cut_tac a=y in compact_Rep_compact_basis)
    1.38 @@ -123,8 +123,8 @@
    1.39        done
    1.40    next
    1.41      fix x y :: "'a compact_basis"
    1.42 -    assume "x \<sqsubseteq> y" "y \<in> compacts w" thus "x \<in> compacts w"
    1.43 -      unfolding compacts_def
    1.44 +    assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w"
    1.45 +      unfolding approximants_def
    1.46        apply simp
    1.47        apply (simp add: compact_le_def)
    1.48        apply (erule (1) trans_less)
    1.49 @@ -133,24 +133,24 @@
    1.50  next
    1.51    fix Y :: "nat \<Rightarrow> 'a"
    1.52    assume Y: "chain Y"
    1.53 -  show "compacts (\<Squnion>i. Y i) = (\<Union>i. compacts (Y i))"
    1.54 -    unfolding compacts_def
    1.55 +  show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
    1.56 +    unfolding approximants_def
    1.57      apply safe
    1.58      apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
    1.59      apply (erule trans_less, rule is_ub_thelub [OF Y])
    1.60      done
    1.61  next
    1.62    fix a :: "'a compact_basis"
    1.63 -  show "compacts (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
    1.64 -    unfolding compacts_def compact_le_def ..
    1.65 +  show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
    1.66 +    unfolding approximants_def compact_le_def ..
    1.67  next
    1.68    fix x y :: "'a"
    1.69 -  assume "compacts x \<subseteq> compacts y" thus "x \<sqsubseteq> y"
    1.70 +  assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y"
    1.71      apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
    1.72      apply (rule admD, simp, simp)
    1.73      apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
    1.74 -    apply (simp add: compacts_def Abs_compact_basis_inverse approx_less)
    1.75 -    apply (simp add: compacts_def Abs_compact_basis_inverse)
    1.76 +    apply (simp add: approximants_def Abs_compact_basis_inverse approx_less)
    1.77 +    apply (simp add: approximants_def Abs_compact_basis_inverse)
    1.78      done
    1.79  qed
    1.80  
    1.81 @@ -163,7 +163,7 @@
    1.82  lemma Rep_compact_bot: "Rep_compact_basis compact_bot = \<bottom>"
    1.83  unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
    1.84  
    1.85 -lemma compact_minimal [simp]: "compact_bot \<sqsubseteq> a"
    1.86 +lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a"
    1.87  unfolding compact_le_def Rep_compact_bot by simp
    1.88  
    1.89