# HG changeset patch
# User Brian Huffman <brianh@cs.pdx.edu>
# Date 1286325405 25200
# Node ID 4244ff4f964919346b28861c0926acb227aaf205
# Parent  2949af5e6b9c3883df76d8571d90a94cf5f90321
add lemmas finite_deflation_imp_compact, cast_below_cast_iff

diff -r 2949af5e6b9c -r 4244ff4f9649 src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Tue Oct 05 17:32:02 2010 -0700
+++ b/src/HOLCF/Algebraic.thy	Tue Oct 05 17:36:45 2010 -0700
@@ -628,20 +628,16 @@
 lemma defl_approx_cast: "defl_approx i (cast\<cdot>A) = cast\<cdot>(approx i\<cdot>A)"
 by (rule cast_approx [symmetric])
 
+lemma cast_below_cast_iff: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<longleftrightarrow> A \<sqsubseteq> B"
+apply (induct A rule: alg_defl.principal_induct, simp)
+apply (induct B rule: alg_defl.principal_induct)
+apply (simp add: cast_alg_defl_principal)
+apply (simp add: finite_deflation_imp_compact finite_deflation_Rep_fin_defl)
+apply (simp add: cast_alg_defl_principal below_fin_defl_def)
+done
+
 lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
-apply (rule profinite_below_ext)
-apply (drule_tac i=i in defl_approx_below)
-apply (rule deflation_cast)
-apply (rule deflation_cast)
-apply (simp only: defl_approx_cast)
-apply (cut_tac x="approx i\<cdot>A" in alg_defl.compact_imp_principal)
-apply (rule compact_approx)
-apply (cut_tac x="approx i\<cdot>B" in alg_defl.compact_imp_principal)
-apply (rule compact_approx)
-apply clarsimp
-apply (simp add: cast_alg_defl_principal)
-apply (simp add: below_fin_defl_def)
-done
+by (simp only: cast_below_cast_iff)
 
 lemma cast_eq_imp_eq: "cast\<cdot>A = cast\<cdot>B \<Longrightarrow> A = B"
 by (simp add: below_antisym cast_below_imp_below)
diff -r 2949af5e6b9c -r 4244ff4f9649 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Tue Oct 05 17:32:02 2010 -0700
+++ b/src/HOLCF/Bifinite.thy	Tue Oct 05 17:36:45 2010 -0700
@@ -295,6 +295,16 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
+text {* Finite deflations are compact elements of the function space *}
+
+lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
+apply (frule finite_deflation_imp_deflation)
+apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)")
+apply (simp add: cfun_map_def deflation.idem eta_cfun)
+apply (rule finite_deflation.compact)
+apply (simp only: finite_deflation_cfun_map)
+done
+
 instantiation cfun :: (profinite, profinite) profinite
 begin