# HG changeset patch
# User huffman
# Date 1213995110 -7200
# Node ID c74270fd72a8d35db12b8ace09f2b40ece7c4e5e
# Parent  b915a10a616a51fde2b901af42465ebb8fa9ba64
clean up and rename some profinite lemmas

diff -r b915a10a616a -r c74270fd72a8 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Fri Jun 20 22:41:41 2008 +0200
+++ b/src/HOLCF/Bifinite.thy	Fri Jun 20 22:51:50 2008 +0200
@@ -42,7 +42,7 @@
 apply (rule is_ub_thelub, simp)
 done
 
-lemma approx_strict [simp]: "approx i\<cdot>(\<bottom>::'a::bifinite) = \<bottom>"
+lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>"
 by (rule UU_I, rule approx_less)
 
 lemma approx_approx1:
@@ -113,23 +113,12 @@
   thus "\<exists>j. approx n\<cdot>x \<sqsubseteq> Y j" ..
 qed
 
-lemma bifinite_compact_eq_approx:
-  assumes x: "compact x"
-  shows "\<exists>i. approx i\<cdot>x = x"
-proof -
-  have chain: "chain (\<lambda>i. approx i\<cdot>x)" by simp
-  have less: "x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by simp
-  obtain i where i: "x \<sqsubseteq> approx i\<cdot>x"
-    using compactD2 [OF x chain less] ..
-  with approx_less have "approx i\<cdot>x = x"
-    by (rule antisym_less)
-  thus "\<exists>i. approx i\<cdot>x = x" ..
-qed
+lemma profinite_compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
+by (rule admD2) simp_all
 
-lemma bifinite_compact_iff:
-  "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)"
+lemma profinite_compact_iff: "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)"
  apply (rule iffI)
-  apply (erule bifinite_compact_eq_approx)
+  apply (erule profinite_compact_eq_approx)
  apply (erule exE)
  apply (erule subst)
  apply (rule compact_approx)
@@ -144,7 +133,7 @@
   thus "P x" by simp
 qed
 
-lemma bifinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
+lemma profinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
 apply (rule lub_mono, simp, simp, simp)
 done
diff -r b915a10a616a -r c74270fd72a8 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Fri Jun 20 22:41:41 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy	Fri Jun 20 22:51:50 2008 +0200
@@ -493,7 +493,7 @@
   show "\<exists>n. compact_approx n a = a"
     apply (simp add: Rep_compact_basis_inject [symmetric])
     apply (simp add: Rep_compact_approx)
-    apply (rule bifinite_compact_eq_approx)
+    apply (rule profinite_compact_eq_approx)
     apply (rule compact_Rep_compact_basis)
     done
 qed
@@ -523,8 +523,8 @@
       apply simp
       apply (cut_tac a=x in compact_Rep_compact_basis)
       apply (cut_tac a=y in compact_Rep_compact_basis)
-      apply (drule bifinite_compact_eq_approx)
-      apply (drule bifinite_compact_eq_approx)
+      apply (drule profinite_compact_eq_approx)
+      apply (drule profinite_compact_eq_approx)
       apply (clarify, rename_tac i j)
       apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
       apply (simp add: compact_le_def)
diff -r b915a10a616a -r c74270fd72a8 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Fri Jun 20 22:41:41 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy	Fri Jun 20 22:51:50 2008 +0200
@@ -327,7 +327,7 @@
 
 lemma convex_unit_less_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
  apply (rule iffI)
-  apply (rule bifinite_less_ext)
+  apply (rule profinite_less_ext)
   apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
@@ -346,7 +346,7 @@
 
 lemma compact_convex_unit_iff [simp]:
   "compact {x}\<natural> \<longleftrightarrow> compact x"
-unfolding bifinite_compact_iff by simp
+unfolding profinite_compact_iff by simp
 
 lemma compact_convex_plus [simp]:
   "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<natural> ys)"
@@ -589,7 +589,7 @@
     (convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and>
      convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)"
  apply (safe elim!: monofun_cfun_arg)
- apply (rule bifinite_less_ext)
+ apply (rule profinite_less_ext)
  apply (drule_tac f="approx i" in monofun_cfun_arg)
  apply (drule_tac f="approx i" in monofun_cfun_arg)
  apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
diff -r b915a10a616a -r c74270fd72a8 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Fri Jun 20 22:41:41 2008 +0200
+++ b/src/HOLCF/LowerPD.thy	Fri Jun 20 22:51:50 2008 +0200
@@ -284,7 +284,7 @@
 
 lemma lower_unit_less_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
  apply (rule iffI)
-  apply (rule bifinite_less_ext)
+  apply (rule profinite_less_ext)
   apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
@@ -331,7 +331,7 @@
 done
 
 lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x"
-unfolding bifinite_compact_iff by simp
+unfolding profinite_compact_iff by simp
 
 lemma compact_lower_plus [simp]:
   "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"
diff -r b915a10a616a -r c74270fd72a8 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Fri Jun 20 22:41:41 2008 +0200
+++ b/src/HOLCF/UpperPD.thy	Fri Jun 20 22:51:50 2008 +0200
@@ -282,7 +282,7 @@
 
 lemma upper_unit_less_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
  apply (rule iffI)
-  apply (rule bifinite_less_ext)
+  apply (rule profinite_less_ext)
   apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
   apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
@@ -321,7 +321,7 @@
 done
 
 lemma compact_upper_unit_iff [simp]: "compact {x}\<sharp> \<longleftrightarrow> compact x"
-unfolding bifinite_compact_iff by simp
+unfolding profinite_compact_iff by simp
 
 lemma compact_upper_plus [simp]:
   "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<sharp> ys)"