equal
deleted
inserted
replaced
150 fixes f :: "'c::cpo \<Rightarrow> 'a::cpo" |
150 fixes f :: "'c::cpo \<Rightarrow> 'a::cpo" |
151 assumes type: "type_definition Rep Abs A" |
151 assumes type: "type_definition Rep Abs A" |
152 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
152 and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y" |
153 and adm: "adm (\<lambda>x. x \<in> A)" (* not used *) |
153 and adm: "adm (\<lambda>x. x \<in> A)" (* not used *) |
154 and f_in_A: "\<And>x. f x \<in> A" |
154 and f_in_A: "\<And>x. f x \<in> A" |
155 and cont_f: "cont f" |
155 shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))" |
156 shows "cont (\<lambda>x. Abs (f x))" |
156 unfolding cont_def is_lub_def is_ub_def ball_simps below |
157 apply (rule contI) |
157 by (simp add: type_definition.Abs_inverse [OF type f_in_A]) |
158 apply (rule typedef_is_lubI [OF below]) |
|
159 apply (simp only: type_definition.Abs_inverse [OF type f_in_A]) |
|
160 apply (erule cont_f [THEN contE]) |
|
161 done |
|
162 |
158 |
163 subsection {* Proving subtype elements are compact *} |
159 subsection {* Proving subtype elements are compact *} |
164 |
160 |
165 theorem typedef_compact: |
161 theorem typedef_compact: |
166 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |
162 fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo" |