declare a few more cont2cont rules
authorhuffman
Sun, 23 May 2010 19:30:14 -0700
changeset 37099 3636b08cbf51
parent 37098 b86d546c5282
child 37100 c11cdb5e7e97
declare a few more cont2cont rules
src/HOLCF/Cont.thy
src/HOLCF/Lift.thy
--- a/src/HOLCF/Cont.thy	Sat May 22 19:17:18 2010 -0700
+++ b/src/HOLCF/Cont.thy	Sun May 23 19:30:14 2010 -0700
@@ -178,7 +178,7 @@
 
 text {* if-then-else is continuous *}
 
-lemma cont_if [simp]:
+lemma cont_if [simp, cont2cont]:
   "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)"
 by (induct b) simp_all
 
--- a/src/HOLCF/Lift.thy	Sat May 22 19:17:18 2010 -0700
+++ b/src/HOLCF/Lift.thy	Sun May 23 19:30:14 2010 -0700
@@ -137,7 +137,7 @@
 apply (simp add: below_fun_ext)
 done
 
-lemma cont2cont_flift1 [simp]:
+lemma cont2cont_flift1 [simp, cont2cont]:
   "\<lbrakk>\<And>y. cont (\<lambda>x. f x y)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. FLIFT y. f x y)"
 apply (rule cont_flift1 [THEN cont2cont_app3])
 apply simp