src/HOLCF/UpperPD.thy
changeset 26407 562a1d615336
parent 26041 c2e15e65165f
child 26420 57a626f64875
     1.1 --- a/src/HOLCF/UpperPD.thy	Wed Mar 26 21:05:58 2008 +0100
     1.2 +++ b/src/HOLCF/UpperPD.thy	Wed Mar 26 22:38:17 2008 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4  subsection {* Type definition *}
     1.5  
     1.6  cpodef (open) 'a upper_pd =
     1.7 -  "{S::'a::bifinite pd_basis set. upper_le.ideal S}"
     1.8 +  "{S::'a::profinite pd_basis set. upper_le.ideal S}"
     1.9  apply (simp add: upper_le.adm_ideal)
    1.10  apply (fast intro: upper_le.ideal_principal)
    1.11  done
    1.12 @@ -153,7 +153,7 @@
    1.13  
    1.14  subsection {* Approximation *}
    1.15  
    1.16 -instance upper_pd :: (bifinite) approx ..
    1.17 +instance upper_pd :: (profinite) approx ..
    1.18  
    1.19  defs (overloaded)
    1.20    approx_upper_pd_def:
    1.21 @@ -192,7 +192,7 @@
    1.22  unfolding approx_upper_pd_def
    1.23  by (rule upper_pd.finite_fixes_basis_fun_take)
    1.24  
    1.25 -instance upper_pd :: (bifinite) bifinite
    1.26 +instance upper_pd :: (profinite) profinite
    1.27  apply intro_classes
    1.28  apply (simp add: chain_approx_upper_pd)
    1.29  apply (rule lub_approx_upper_pd)
    1.30 @@ -200,6 +200,8 @@
    1.31  apply (rule finite_fixes_approx_upper_pd)
    1.32  done
    1.33  
    1.34 +instance upper_pd :: (bifinite) bifinite ..
    1.35 +
    1.36  lemma compact_imp_upper_principal:
    1.37    "compact xs \<Longrightarrow> \<exists>t. xs = upper_principal t"
    1.38  apply (drule bifinite_compact_eq_approx)