src/HOLCF/Bifinite.thy
 changeset 31076 99fe356cbbc2 parent 30729 461ee3e49ad3 child 31113 15cf300a742f
```--- a/src/HOLCF/Bifinite.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Bifinite.thy	Fri May 08 16:19:51 2009 -0700
@@ -19,7 +19,7 @@

class bifinite = profinite + pcpo

-lemma approx_less: "approx i\<cdot>x \<sqsubseteq> x"
+lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
proof -
have "chain (\<lambda>i. approx i\<cdot>x)" by simp
hence "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by (rule is_ub_thelub)
@@ -32,7 +32,7 @@
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
by (rule approx_idem)
show "approx i\<cdot>x \<sqsubseteq> x"
-    by (rule approx_less)
+    by (rule approx_below)
show "finite {x. approx i\<cdot>x = x}"
by (rule finite_fixes_approx)
qed
@@ -49,17 +49,17 @@
by (rule ext_cfun, simp add: contlub_cfun_fun)

lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>"
-by (rule UU_I, rule approx_less)
+by (rule UU_I, rule approx_below)

lemma approx_approx1:
"i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>x"
-apply (rule deflation_less_comp1 [OF deflation_approx deflation_approx])
+apply (rule deflation_below_comp1 [OF deflation_approx deflation_approx])
apply (erule chain_mono [OF chain_approx])
done

lemma approx_approx2:
"j \<le> i \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx j\<cdot>x"
-apply (rule deflation_less_comp2 [OF deflation_approx deflation_approx])
+apply (rule deflation_below_comp2 [OF deflation_approx deflation_approx])
apply (erule chain_mono [OF chain_approx])
done

@@ -99,7 +99,7 @@
thus "P x" by simp
qed

-lemma profinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
+lemma profinite_below_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```