add lemmas finite_deflation_imp_compact, cast_below_cast_iff
authorBrian Huffman <brianh@cs.pdx.edu>
Tue Oct 05 17:36:45 2010 -0700 (2010-10-05)
changeset 399724244ff4f9649
parent 39971 2949af5e6b9c
child 39973 c62b4ff97bfc
add lemmas finite_deflation_imp_compact, cast_below_cast_iff
src/HOLCF/Algebraic.thy
src/HOLCF/Bifinite.thy
     1.1 --- a/src/HOLCF/Algebraic.thy	Tue Oct 05 17:32:02 2010 -0700
     1.2 +++ b/src/HOLCF/Algebraic.thy	Tue Oct 05 17:36:45 2010 -0700
     1.3 @@ -628,20 +628,16 @@
     1.4  lemma defl_approx_cast: "defl_approx i (cast\<cdot>A) = cast\<cdot>(approx i\<cdot>A)"
     1.5  by (rule cast_approx [symmetric])
     1.6  
     1.7 +lemma cast_below_cast_iff: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
     1.8 +apply (induct A rule: alg_defl.principal_induct, simp)
     1.9 +apply (induct B rule: alg_defl.principal_induct)
    1.10 +apply (simp add: cast_alg_defl_principal)
    1.11 +apply (simp add: finite_deflation_imp_compact finite_deflation_Rep_fin_defl)
    1.12 +apply (simp add: cast_alg_defl_principal below_fin_defl_def)
    1.13 +done
    1.14 +
    1.15  lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
    1.16 -apply (rule profinite_below_ext)
    1.17 -apply (drule_tac i=i in defl_approx_below)
    1.18 -apply (rule deflation_cast)
    1.19 -apply (rule deflation_cast)
    1.20 -apply (simp only: defl_approx_cast)
    1.21 -apply (cut_tac x="approx i\<cdot>A" in alg_defl.compact_imp_principal)
    1.22 -apply (rule compact_approx)
    1.23 -apply (cut_tac x="approx i\<cdot>B" in alg_defl.compact_imp_principal)
    1.24 -apply (rule compact_approx)
    1.25 -apply clarsimp
    1.26 -apply (simp add: cast_alg_defl_principal)
    1.27 -apply (simp add: below_fin_defl_def)
    1.28 -done
    1.29 +by (simp only: cast_below_cast_iff)
    1.30  
    1.31  lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
    1.32  by (simp add: below_antisym cast_below_imp_below)
     2.1 --- a/src/HOLCF/Bifinite.thy	Tue Oct 05 17:32:02 2010 -0700
     2.2 +++ b/src/HOLCF/Bifinite.thy	Tue Oct 05 17:36:45 2010 -0700
     2.3 @@ -295,6 +295,16 @@
     2.4      by (rule finite_range_imp_finite_fixes)
     2.5  qed
     2.6  
     2.7 +text {* Finite deflations are compact elements of the function space *}
     2.8 +
     2.9 +lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
    2.10 +apply (frule finite_deflation_imp_deflation)
    2.11 +apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
    2.12 +apply (simp add: cfun_map_def deflation.idem eta_cfun)
    2.13 +apply (rule finite_deflation.compact)
    2.14 +apply (simp only: finite_deflation_cfun_map)
    2.15 +done
    2.16 +
    2.17  instantiation cfun :: (profinite, profinite) profinite
    2.18  begin
    2.19