1.1 --- a/src/HOLCF/Domain.thy	Tue Oct 11 23:27:49 2005 +0200
     1.2 +++ b/src/HOLCF/Domain.thy	Tue Oct 11 23:47:29 2005 +0200
     1.3 @@ -86,6 +86,23 @@
     1.4  lemma (in iso) rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
     1.5  by (rule iso.abs_defined_iff [OF iso.swap])
     1.6  
     1.7 +lemma (in iso) compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
     1.8 +proof (unfold compact_def)
     1.9 +  assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
    1.10 +  with cont_Rep_CFun2
    1.11 +  have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
    1.12 +  thus "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_less by simp
    1.13 +qed
    1.14 +
    1.15 +lemma (in iso) compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
    1.16 +by (rule iso.compact_abs_rev [OF iso.swap])
    1.17 +
    1.18 +lemma (in iso) compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)"
    1.19 +by (rule compact_rep_rev, simp)
    1.20 +
    1.21 +lemma (in iso) compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)"
    1.22 +by (rule iso.compact_abs [OF iso.swap])
    1.23 +
    1.24  lemma (in iso) iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)"
    1.25  proof
    1.26    assume "x = abs\<cdot>y"