--- a/src/HOL/HOLCF/Cfun.thy Tue Nov 30 15:34:51 2010 -0800
+++ b/src/HOL/HOLCF/Cfun.thy Tue Nov 30 15:56:19 2010 -0800
@@ -192,7 +192,7 @@
subsection {* Continuity of application *}
lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)"
-by (rule cont_Rep_cfun [THEN cont2cont_fun])
+by (rule cont_Rep_cfun [OF cont_id, THEN cont2cont_fun])
lemma cont_Rep_cfun2: "cont (\<lambda>x. f\<cdot>x)"
apply (cut_tac x=f in Rep_cfun)
--- a/src/HOL/HOLCF/Cpodef.thy Tue Nov 30 15:34:51 2010 -0800
+++ b/src/HOL/HOLCF/Cpodef.thy Tue Nov 30 15:56:19 2010 -0800
@@ -131,7 +131,8 @@
assumes type: "type_definition Rep Abs A"
and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
- shows "cont Rep"
+ shows "cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. Rep (f x))"
+ apply (erule cont_apply [OF _ _ cont_const])
apply (rule contI)
apply (simp only: typedef_lub [OF type below adm])
apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
@@ -166,7 +167,7 @@
shows "compact (Rep k) \<Longrightarrow> compact k"
proof (unfold compact_def)
have cont_Rep: "cont Rep"
- by (rule typedef_cont_Rep [OF type below adm])
+ by (rule typedef_cont_Rep [OF type below adm cont_id])
assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
--- a/src/HOL/HOLCF/Domain.thy Tue Nov 30 15:34:51 2010 -0800
+++ b/src/HOL/HOLCF/Domain.thy Tue Nov 30 15:56:19 2010 -0800
@@ -113,7 +113,7 @@
have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
unfolding emb
apply (rule beta_cfun)
- apply (rule typedef_cont_Rep [OF type below adm_defl_set])
+ apply (rule typedef_cont_Rep [OF type below adm_defl_set cont_id])
done
have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
unfolding prj
--- a/src/HOL/HOLCF/Fixrec.thy Tue Nov 30 15:34:51 2010 -0800
+++ b/src/HOL/HOLCF/Fixrec.thy Tue Nov 30 15:56:19 2010 -0800
@@ -80,19 +80,17 @@
text {* rewrite rules for mplus *}
-lemmas cont2cont_Rep_match = cont_Rep_match [THEN cont_compose]
-
lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
unfolding mplus_def
-by (simp add: cont2cont_Rep_match Rep_match_strict)
+by (simp add: cont_Rep_match Rep_match_strict)
lemma mplus_fail [simp]: "fail +++ m = m"
unfolding mplus_def fail_def
-by (simp add: cont2cont_Rep_match Abs_match_inverse)
+by (simp add: cont_Rep_match Abs_match_inverse)
lemma mplus_succeed [simp]: "succeed\<cdot>x +++ m = succeed\<cdot>x"
unfolding mplus_def succeed_def
-by (simp add: cont2cont_Rep_match cont_Abs_match Abs_match_inverse)
+by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)
lemma mplus_fail2 [simp]: "m +++ fail = m"
by (cases m, simp_all)
--- a/src/HOL/HOLCF/Lift.thy Tue Nov 30 15:34:51 2010 -0800
+++ b/src/HOL/HOLCF/Lift.thy Tue Nov 30 15:56:19 2010 -0800
@@ -87,7 +87,7 @@
lemma cont2cont_lift_case [simp]:
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case \<bottom> (f x) (g x))"
-unfolding lift_case_eq by (simp add: cont_Rep_lift [THEN cont_compose])
+unfolding lift_case_eq by (simp add: cont_Rep_lift)
subsection {* Further operations *}
--- a/src/HOL/HOLCF/Ssum.thy Tue Nov 30 15:34:51 2010 -0800
+++ b/src/HOL/HOLCF/Ssum.thy Tue Nov 30 15:56:19 2010 -0800
@@ -172,7 +172,7 @@
lemma beta_sscase:
"sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s)"
-unfolding sscase_def by (simp add: cont_Rep_ssum [THEN cont_compose])
+unfolding sscase_def by (simp add: cont_Rep_ssum)
lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
unfolding beta_sscase by (simp add: Rep_ssum_strict)
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Nov 30 15:34:51 2010 -0800
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Nov 30 15:56:19 2010 -0800
@@ -63,7 +63,7 @@
"match_bind\<cdot>fail\<cdot>k = fail"
"match_bind\<cdot>(succeed\<cdot>x)\<cdot>k = k\<cdot>x"
unfolding match_bind_def fail_def succeed_def
-by (simp_all add: cont2cont_Rep_match cont_Abs_match
+by (simp_all add: cont_Rep_match cont_Abs_match
Rep_match_strict Abs_match_inverse)
subsection {* Case branch combinator *}