# HG changeset patch
# User wenzelm
# Date 1290971542 -3600
# Node ID 0562a0a5bb9339138375b05040d1b4d07f53bcc0
# Parent  1b15d1805b7288be80a2886ccc3ac6c5f4145907# Parent  d21aedaa91e7470a139d0aba868d7cc190c46728
merged

diff -r d21aedaa91e7 -r 0562a0a5bb93 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Sun Nov 28 20:03:19 2010 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Sun Nov 28 20:12:22 2010 +0100
@@ -481,12 +481,19 @@
   seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" where
   "seq = (\<Lambda> x. if x = \<bottom> then \<bottom> else ID)"
 
-lemma cont_seq: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else y)"
-unfolding cont_def is_lub_def is_ub_def ball_simps
-by (simp add: lub_eq_bottom_iff)
+lemma cont2cont_if_bottom [cont2cont, simp]:
+  assumes f: "cont (\<lambda>x. f x)" and g: "cont (\<lambda>x. g x)"
+  shows "cont (\<lambda>x. if f x = \<bottom> then \<bottom> else g x)"
+proof (rule cont_apply [OF f])
+  show "\<And>x. cont (\<lambda>y. if y = \<bottom> then \<bottom> else g x)"
+    unfolding cont_def is_lub_def is_ub_def ball_simps
+    by (simp add: lub_eq_bottom_iff)
+  show "\<And>y. cont (\<lambda>x. if y = \<bottom> then \<bottom> else g x)"
+    by (simp add: g)
+qed
 
 lemma seq_conv_if: "seq\<cdot>x = (if x = \<bottom> then \<bottom> else ID)"
-unfolding seq_def by (simp add: cont_seq)
+unfolding seq_def by simp
 
 lemma seq1 [simp]: "seq\<cdot>\<bottom> = \<bottom>"
 by (simp add: seq_conv_if)
diff -r d21aedaa91e7 -r 0562a0a5bb93 src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Sun Nov 28 20:03:19 2010 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy	Sun Nov 28 20:12:22 2010 +0100
@@ -150,9 +150,8 @@
   "match_FF = (\<Lambda> x k. If x then fail else k)"
 
 lemma match_bottom_simps [simp]:
-  "match_bottom\<cdot>\<bottom>\<cdot>k = \<bottom>"
-  "x \<noteq> \<bottom> \<Longrightarrow> match_bottom\<cdot>x\<cdot>k = fail"
-by (simp_all add: match_bottom_def)
+  "match_bottom\<cdot>x\<cdot>k = (if x = \<bottom> then \<bottom> else fail)"
+by (simp add: match_bottom_def)
 
 lemma match_Pair_simps [simp]:
   "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"