equal
deleted
inserted
replaced
189 done |
189 done |
190 |
190 |
191 lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d" |
191 lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d" |
192 apply (rule iffI) |
192 apply (rule iffI) |
193 apply (simp only: compact_def cast_below_cast [symmetric]) |
193 apply (simp only: compact_def cast_below_cast [symmetric]) |
194 apply (erule adm_subst [OF cont_Rep_CFun2]) |
194 apply (erule adm_subst [OF cont_Rep_cfun2]) |
195 apply (erule compact_cast) |
195 apply (erule compact_cast) |
196 done |
196 done |
197 |
197 |
198 lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B" |
198 lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B" |
199 by (simp only: cast_below_cast) |
199 by (simp only: cast_below_cast) |