src/HOL/HOLCF/Deflation.thy
changeset 41182 717404c7d59a
parent 40774 0437dbc127b3
child 41430 1aa23e9f2c87
     1.1 --- a/src/HOL/HOLCF/Deflation.thy	Wed Dec 15 20:52:20 2010 +0100
     1.2 +++ b/src/HOL/HOLCF/Deflation.thy	Wed Dec 15 19:15:06 2010 -0800
     1.3 @@ -206,18 +206,18 @@
     1.4  lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
     1.5  proof -
     1.6    assume "compact (e\<cdot>x)"
     1.7 -  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
     1.8 -  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
     1.9 -  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
    1.10 +  hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (rule compactD)
    1.11 +  hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
    1.12 +  hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by simp
    1.13    thus "compact x" by (rule compactI)
    1.14  qed
    1.15  
    1.16  lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
    1.17  proof -
    1.18    assume "compact x"
    1.19 -  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
    1.20 -  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
    1.21 -  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
    1.22 +  hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by (rule compactD)
    1.23 +  hence "adm (\<lambda>y. x \<notsqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
    1.24 +  hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (simp add: e_below_iff_below_p)
    1.25    thus "compact (e\<cdot>x)" by (rule compactI)
    1.26  qed
    1.27