src/HOL/HOLCF/Cpodef.thy
changeset 40834 a1249aeff5b6
parent 40774 0437dbc127b3
child 41029 f7d8cfa6e7fc
     1.1 --- a/src/HOL/HOLCF/Cpodef.thy	Tue Nov 30 15:34:51 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Tue Nov 30 15:56:19 2010 -0800
     1.3 @@ -131,7 +131,8 @@
     1.4    assumes type: "type_definition Rep Abs A"
     1.5      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     1.6      and adm: "adm (\<lambda>x. x \<in> A)"
     1.7 -  shows "cont Rep"
     1.8 +  shows "cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. Rep (f x))"
     1.9 + apply (erule cont_apply [OF _ _ cont_const])
    1.10   apply (rule contI)
    1.11   apply (simp only: typedef_lub [OF type below adm])
    1.12   apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
    1.13 @@ -166,7 +167,7 @@
    1.14    shows "compact (Rep k) \<Longrightarrow> compact k"
    1.15  proof (unfold compact_def)
    1.16    have cont_Rep: "cont Rep"
    1.17 -    by (rule typedef_cont_Rep [OF type below adm])
    1.18 +    by (rule typedef_cont_Rep [OF type below adm cont_id])
    1.19    assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
    1.20    with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
    1.21    thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)