src/HOLCF/Up.thy
 changeset 25911 cc3f00949986 parent 25906 2179c6661218 child 25921 0ca392ab7f37
```     1.1 --- a/src/HOLCF/Up.thy	Mon Jan 14 21:16:06 2008 +0100
1.2 +++ b/src/HOLCF/Up.thy	Mon Jan 14 21:42:58 2008 +0100
1.3 @@ -8,7 +8,7 @@
1.4  header {* The type of lifted values *}
1.5
1.6  theory Up
1.7 -imports Cfun
1.8 +imports Bifinite
1.9  begin
1.10
1.11  defaultsort cpo
1.12 @@ -309,4 +309,34 @@
1.13  lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
1.14  by (cases x, simp_all)
1.15
1.16 +subsection {* Lifted cpo is a bifinite domain *}
1.17 +
1.18 +instance u :: (bifinite_cpo) approx ..
1.19 +
1.21 +  approx_up_def:
1.22 +    "approx \<equiv> \<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x))"
1.23 +
1.24 +instance u :: (bifinite_cpo) bifinite
1.25 +proof
1.26 +  fix i :: nat and x :: "'a u"
1.27 +  show "chain (\<lambda>i. approx i\<cdot>x)"
1.28 +    unfolding approx_up_def by simp
1.29 +  show "(\<Squnion>i. approx i\<cdot>x) = x"
1.30 +    unfolding approx_up_def
1.31 +    by (simp add: lub_distribs eta_cfun)
1.32 +  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
1.33 +    unfolding approx_up_def
1.34 +    by (induct x, simp, simp)
1.35 +  have "{x::'a u. approx i\<cdot>x = x} \<subseteq>
1.36 +        insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x::'a. approx i\<cdot>x = x})"
1.37 +    unfolding approx_up_def
1.38 +    by (rule subsetI, rule_tac p=x in upE, simp_all)
1.39 +  thus "finite {x::'a u. approx i\<cdot>x = x}"
1.40 +    by (rule finite_subset, simp add: finite_fixes_approx)
1.41 +qed
1.42 +
1.43 +lemma approx_up [simp]: "approx i\<cdot>(up\<cdot>x) = up\<cdot>(approx i\<cdot>x)"
1.44 +unfolding approx_up_def by simp
1.45 +
1.46  end
```