added bifinite class instance
authorhuffman
Mon Jan 14 21:42:58 2008 +0100 (2008-01-14)
changeset 25911cc3f00949986
parent 25910 25533eb2b914
child 25912 a1a3f614dd86
added bifinite class instance
src/HOLCF/Up.thy
     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.20 +defs (overloaded)
    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