--- a/src/HOLCF/Cont.thy Thu Mar 27 19:22:24 2008 +0100
+++ b/src/HOLCF/Cont.thy Thu Mar 27 19:49:24 2008 +0100
@@ -186,7 +186,8 @@
text {* if-then-else is continuous *}
-lemma cont_if: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)"
+lemma cont_if [simp]:
+ "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)"
by (induct b) simp_all
subsection {* Finite chains and flat pcpos *}
--- a/src/HOLCF/Ffun.thy Thu Mar 27 19:22:24 2008 +0100
+++ b/src/HOLCF/Ffun.thy Thu Mar 27 19:49:24 2008 +0100
@@ -240,21 +240,23 @@
text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *}
-lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun f"
+lemma mono2mono_lambda:
+ assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
apply (rule monofunI)
apply (rule less_fun_ext)
-apply (blast dest: monofunE)
+apply (erule monofunE [OF f])
done
-lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f"
+lemma cont2cont_lambda [simp]:
+ assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
apply (subgoal_tac "monofun f")
apply (rule monocontlub2cont)
apply assumption
apply (rule contlubI)
apply (rule ext)
apply (simp add: thelub_fun ch2ch_monofun)
-apply (blast dest: cont2contlubE)
-apply (simp add: mono2mono_lambda cont2mono)
+apply (erule cont2contlubE [OF f])
+apply (simp add: mono2mono_lambda cont2mono f)
done
text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
@@ -268,9 +270,7 @@
"\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow>
(\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))"
apply (rule thelub_fun [symmetric])
-apply (rule ch2ch_cont)
-apply (simp add: cont2cont_lambda)
-apply assumption
+apply (simp add: ch2ch_cont)
done
lemma mono2mono_app:
--- a/src/HOLCF/Lift.thy Thu Mar 27 19:22:24 2008 +0100
+++ b/src/HOLCF/Lift.thy Thu Mar 27 19:49:24 2008 +0100
@@ -105,10 +105,10 @@
terms.
*}
-lemma cont_Rep_CFun_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)"
+lemma cont_Rep_CFun_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s)"
by (rule cont2cont_Rep_CFun [THEN cont2cont_fun])
-lemma cont_Rep_CFun_app_app: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)"
+lemma cont_Rep_CFun_app_app [simp]: "\<lbrakk>cont g; cont f\<rbrakk> \<Longrightarrow> cont(\<lambda>x. ((f x)\<cdot>(g x)) s t)"
by (rule cont_Rep_CFun_app [THEN cont2cont_fun])
subsection {* Further operations *}
@@ -148,17 +148,17 @@
apply (rule cont_lift_case1)
done
-lemma cont2cont_flift1:
+lemma cont2cont_flift1 [simp]:
"\<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 add: cont2cont_lambda)
+apply simp
done
-lemma cont2cont_lift_case:
+lemma cont2cont_lift_case [simp]:
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))"
apply (subgoal_tac "cont (\<lambda>x. (FLIFT y. f x y)\<cdot>(g x))")
apply (simp add: flift1_def cont_lift_case2)
-apply (simp add: cont2cont_flift1)
+apply simp
done
text {* rewrites for @{term flift1}, @{term flift2} *}
@@ -185,7 +185,7 @@
\medskip Extension of @{text cont_tac} and installation of simplifier.
*}
-lemmas cont_lemmas_ext [simp] =
+lemmas cont_lemmas_ext =
cont2cont_flift1 cont2cont_lift_case cont2cont_lambda
cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if