src/HOLCF/Bifinite.thy
changeset 39972 4244ff4f9649
parent 37678 0040bafffdef
child 39973 c62b4ff97bfc
     1.1 --- a/src/HOLCF/Bifinite.thy	Tue Oct 05 17:32:02 2010 -0700
     1.2 +++ b/src/HOLCF/Bifinite.thy	Tue Oct 05 17:36:45 2010 -0700
     1.3 @@ -295,6 +295,16 @@
     1.4      by (rule finite_range_imp_finite_fixes)
     1.5  qed
     1.6  
     1.7 +text {* Finite deflations are compact elements of the function space *}
     1.8 +
     1.9 +lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
    1.10 +apply (frule finite_deflation_imp_deflation)
    1.11 +apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
    1.12 +apply (simp add: cfun_map_def deflation.idem eta_cfun)
    1.13 +apply (rule finite_deflation.compact)
    1.14 +apply (simp only: finite_deflation_cfun_map)
    1.15 +done
    1.16 +
    1.17  instantiation cfun :: (profinite, profinite) profinite
    1.18  begin
    1.19