--- a/src/HOLCF/Lift.thy Mon May 19 23:49:20 2008 +0200
+++ b/src/HOLCF/Lift.thy Mon May 19 23:50:06 2008 +0200
@@ -6,7 +6,7 @@
header {* Lifting types of class type to flat pcpo's *}
theory Lift
-imports Discrete Up Cprod
+imports Discrete Up Cprod Countable
begin
defaultsort type
@@ -204,4 +204,51 @@
end;
*}
+subsection {* Lifted countable types are bifinite *}
+
+instantiation lift :: (countable) bifinite
+begin
+
+definition
+ approx_lift_def:
+ "approx = (\<lambda>n. FLIFT x. if to_nat x < n then Def x else \<bottom>)"
+
+instance proof
+ fix x :: "'a lift"
+ show "chain (\<lambda>i. approx i\<cdot>x)"
+ unfolding approx_lift_def
+ by (rule chainI, cases x, simp_all)
+next
+ fix x :: "'a lift"
+ show "(\<Squnion>i. approx i\<cdot>x) = x"
+ unfolding approx_lift_def
+ apply (cases x, simp)
+ apply (rule thelubI)
+ apply (rule is_lubI)
+ apply (rule ub_rangeI, simp)
+ apply (drule ub_rangeD)
+ apply (erule rev_trans_less)
+ apply simp
+ apply (rule lessI)
+ done
+next
+ fix i :: nat and x :: "'a lift"
+ show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
+ unfolding approx_lift_def
+ by (cases x, simp, simp)
+next
+ fix i :: nat
+ show "finite {x::'a lift. approx i\<cdot>x = x}"
+ proof (rule finite_subset)
+ let ?S = "insert (\<bottom>::'a lift) (Def ` to_nat -` {..<i})"
+ show "{x::'a lift. approx i\<cdot>x = x} \<subseteq> ?S"
+ unfolding approx_lift_def
+ by (rule subsetI, case_tac x, simp, simp split: split_if_asm)
+ show "finite ?S"
+ by (simp add: finite_vimageI)
+ qed
+qed
+
end
+
+end