--- a/src/HOLCF/Up.thy Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/Up.thy Mon May 19 23:49:20 2008 +0200
@@ -311,14 +311,14 @@
subsection {* Lifted cpo is a bifinite domain *}
-instance u :: (profinite) approx ..
+instantiation u :: (profinite) bifinite
+begin
-defs (overloaded)
+definition
approx_up_def:
- "approx \<equiv> \<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x))"
+ "approx = (\<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x)))"
-instance u :: (profinite) bifinite
-proof
+instance proof
fix i :: nat and x :: "'a u"
show "chain (\<lambda>i. approx i\<cdot>x)"
unfolding approx_up_def by simp
@@ -336,6 +336,8 @@
by (rule finite_subset, simp add: finite_fixes_approx)
qed
+end
+
lemma approx_up [simp]: "approx i\<cdot>(up\<cdot>x) = up\<cdot>(approx i\<cdot>x)"
unfolding approx_up_def by simp