# HG changeset patch
# User huffman
# Date 1200343378 -3600
# Node ID cc3f0094998629cc48e34b5fafeb860b72fd4ec9
# Parent  25533eb2b914c16516368229e62ab6c71d14d15d
added bifinite class instance

diff -r 25533eb2b914 -r cc3f00949986 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Mon Jan 14 21:16:06 2008 +0100
+++ b/src/HOLCF/Up.thy	Mon Jan 14 21:42:58 2008 +0100
@@ -8,7 +8,7 @@
 header {* The type of lifted values *}
 
 theory Up
-imports Cfun
+imports Bifinite
 begin
 
 defaultsort cpo
@@ -309,4 +309,34 @@
 lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
 by (cases x, simp_all)
 
+subsection {* Lifted cpo is a bifinite domain *}
+
+instance u :: (bifinite_cpo) approx ..
+
+defs (overloaded)
+  approx_up_def:
+    "approx \<equiv> \<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x))"
+
+instance u :: (bifinite_cpo) bifinite
+proof
+  fix i :: nat and x :: "'a u"
+  show "chain (\<lambda>i. approx i\<cdot>x)"
+    unfolding approx_up_def by simp
+  show "(\<Squnion>i. approx i\<cdot>x) = x"
+    unfolding approx_up_def
+    by (simp add: lub_distribs eta_cfun)
+  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+    unfolding approx_up_def
+    by (induct x, simp, simp)
+  have "{x::'a u. approx i\<cdot>x = x} \<subseteq>
+        insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x::'a. approx i\<cdot>x = x})"
+    unfolding approx_up_def
+    by (rule subsetI, rule_tac p=x in upE, simp_all)
+  thus "finite {x::'a u. approx i\<cdot>x = x}"
+    by (rule finite_subset, simp add: finite_fixes_approx)
+qed
+
+lemma approx_up [simp]: "approx i\<cdot>(up\<cdot>x) = up\<cdot>(approx i\<cdot>x)"
+unfolding approx_up_def by simp
+
 end