1.1 --- a/src/HOLCF/Bifinite.thy	Fri Jun 20 22:41:41 2008 +0200
     1.2 +++ b/src/HOLCF/Bifinite.thy	Fri Jun 20 22:51:50 2008 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  apply (rule is_ub_thelub, simp)
     1.5  done
     1.6  
     1.7 -lemma approx_strict [simp]: "approx i\<cdot>(\<bottom>::'a::bifinite) = \<bottom>"
     1.8 +lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>"
     1.9  by (rule UU_I, rule approx_less)
    1.10  
    1.11  lemma approx_approx1:
    1.12 @@ -113,23 +113,12 @@
    1.13    thus "\<exists>j. approx n\<cdot>x \<sqsubseteq> Y j" ..
    1.14  qed
    1.15  
    1.16 -lemma bifinite_compact_eq_approx:
    1.17 -  assumes x: "compact x"
    1.18 -  shows "\<exists>i. approx i\<cdot>x = x"
    1.19 -proof -
    1.20 -  have chain: "chain (\<lambda>i. approx i\<cdot>x)" by simp
    1.21 -  have less: "x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by simp
    1.22 -  obtain i where i: "x \<sqsubseteq> approx i\<cdot>x"
    1.23 -    using compactD2 [OF x chain less] ..
    1.24 -  with approx_less have "approx i\<cdot>x = x"
    1.25 -    by (rule antisym_less)
    1.26 -  thus "\<exists>i. approx i\<cdot>x = x" ..
    1.27 -qed
    1.28 +lemma profinite_compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
    1.29 +by (rule admD2) simp_all
    1.30  
    1.31 -lemma bifinite_compact_iff:
    1.32 -  "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)"
    1.33 +lemma profinite_compact_iff: "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)"
    1.34   apply (rule iffI)
    1.35 -  apply (erule bifinite_compact_eq_approx)
    1.36 +  apply (erule profinite_compact_eq_approx)
    1.37   apply (erule exE)
    1.38   apply (erule subst)
    1.39   apply (rule compact_approx)
    1.40 @@ -144,7 +133,7 @@
    1.41    thus "P x" by simp
    1.42  qed
    1.43  
    1.44 -lemma bifinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
    1.45 +lemma profinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
    1.46  apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
    1.47  apply (rule lub_mono, simp, simp, simp)
    1.48  done