69 by (erule contrapos_nn, erule abs_defin') |
69 by (erule contrapos_nn, erule abs_defin') |
70 |
70 |
71 lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>" |
71 lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>" |
72 by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms) |
72 by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms) |
73 |
73 |
74 lemma abs_defined_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)" |
74 lemma abs_bottom_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)" |
75 by (auto elim: abs_defin' intro: abs_strict) |
75 by (auto elim: abs_defin' intro: abs_strict) |
76 |
76 |
77 lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)" |
77 lemma rep_bottom_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)" |
78 by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms) |
78 by (rule iso.abs_bottom_iff [OF iso.swap]) (rule iso_axioms) |
79 |
79 |
80 lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P" |
80 lemma casedist_rule: "rep\<cdot>x = \<bottom> \<or> P \<Longrightarrow> x = \<bottom> \<or> P" |
81 by (simp add: rep_defined_iff) |
81 by (simp add: rep_bottom_iff) |
82 |
82 |
83 lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x" |
83 lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x" |
84 proof (unfold compact_def) |
84 proof (unfold compact_def) |
85 assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)" |
85 assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)" |
86 with cont_Rep_CFun2 |
86 with cont_Rep_CFun2 |