# HG changeset patch
# User huffman
# Date 1206643764 -3600
# Node ID ed657432b8b9870d071fe1e4aebfb11a0ebb0e42
# Parent  f8a615f3bb31a4631602bced9e100f87d448f987
declare cont_lemmas_ext as simp rules individually

diff -r f8a615f3bb31 -r ed657432b8b9 src/HOLCF/Cont.thy
--- 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 *}
diff -r f8a615f3bb31 -r ed657432b8b9 src/HOLCF/Ffun.thy
--- 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:
diff -r f8a615f3bb31 -r ed657432b8b9 src/HOLCF/Lift.thy
--- 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