--- a/src/HOLCF/Cfun.thy Sat May 22 08:30:40 2010 -0700
+++ b/src/HOLCF/Cfun.thy Sat May 22 10:02:07 2010 -0700
@@ -100,7 +100,7 @@
subsection {* Continuous function space is pointed *}
lemma UU_CFun: "\<bottom> \<in> CFun"
-by (simp add: CFun_def inst_fun_pcpo cont_const)
+by (simp add: CFun_def inst_fun_pcpo)
instance cfun :: (finite_po, finite_po) finite_po
by (rule typedef_finite_po [OF type_definition_CFun])
@@ -301,7 +301,7 @@
text {* cont2cont lemma for @{term Rep_CFun} *}
-lemma cont2cont_Rep_CFun [cont2cont]:
+lemma cont2cont_Rep_CFun [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes t: "cont (\<lambda>x. t x)"
shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
@@ -341,7 +341,7 @@
has only a single subgoal.
*}
-lemma cont2cont_LAM' [cont2cont]:
+lemma cont2cont_LAM' [simp, cont2cont]:
fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo"
assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
shows "cont (\<lambda>x. \<Lambda> y. f x y)"
@@ -353,7 +353,7 @@
using f by (rule cont_fst_snd_D1)
qed
-lemma cont2cont_LAM_discrete [cont2cont]:
+lemma cont2cont_LAM_discrete [simp, cont2cont]:
"(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
by (simp add: cont2cont_LAM)
@@ -556,7 +556,7 @@
shows "cont (\<lambda>x. let y = f x in g x y)"
unfolding Let_def using f g2 g1 by (rule cont_apply)
-lemma cont2cont_Let' [cont2cont]:
+lemma cont2cont_Let' [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
shows "cont (\<lambda>x. let y = f x in g x y)"
--- a/src/HOLCF/Cont.thy Sat May 22 08:30:40 2010 -0700
+++ b/src/HOLCF/Cont.thy Sat May 22 10:02:07 2010 -0700
@@ -120,7 +120,7 @@
apply (erule ch2ch_monofun [OF mono])
done
-subsection {* Continuity simproc *}
+subsection {* Collection of continuity rules *}
ML {*
structure Cont2ContData = Named_Thms
@@ -132,34 +132,18 @@
setup Cont2ContData.setup
-text {*
- Given the term @{term "cont f"}, the procedure tries to construct the
- theorem @{term "cont f == True"}. If this theorem cannot be completely
- solved by the introduction rules, then the procedure returns a
- conditional rewrite rule with the unsolved subgoals as premises.
-*}
-
-simproc_setup cont_proc ("cont f") = {*
- fn phi => fn ss => fn ct =>
- let
- val tr = instantiate' [] [SOME ct] @{thm Eq_TrueI};
- val rules = Cont2ContData.get (Simplifier.the_context ss);
- val tac = REPEAT_ALL_NEW (match_tac rules);
- in SINGLE (tac 1) tr end
-*}
-
subsection {* Continuity of basic functions *}
text {* The identity function is continuous *}
-lemma cont_id [cont2cont]: "cont (\<lambda>x. x)"
+lemma cont_id [simp, cont2cont]: "cont (\<lambda>x. x)"
apply (rule contI)
apply (erule cpo_lubI)
done
text {* constant functions are continuous *}
-lemma cont_const [cont2cont]: "cont (\<lambda>x. c)"
+lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)"
apply (rule contI)
apply (rule lub_const)
done
@@ -237,7 +221,7 @@
text {* functions with discrete domain *}
-lemma cont_discrete_cpo [cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
+lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
apply (rule contI)
apply (drule discrete_chain_const, clarify)
apply (simp add: lub_const)
--- a/src/HOLCF/Fixrec.thy Sat May 22 08:30:40 2010 -0700
+++ b/src/HOLCF/Fixrec.thy Sat May 22 10:02:07 2010 -0700
@@ -587,6 +587,7 @@
hide_const (open) return fail run cases
lemmas [fixrec_simp] =
+ beta_cfun cont2cont
run_strict run_fail run_return
mplus_strict mplus_fail mplus_return
spair_strict_iff
--- a/src/HOLCF/Product_Cpo.thy Sat May 22 08:30:40 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy Sat May 22 10:02:07 2010 -0700
@@ -221,7 +221,7 @@
apply (erule cpo_lubI [OF ch2ch_snd])
done
-lemma cont2cont_Pair [cont2cont]:
+lemma cont2cont_Pair [simp, cont2cont]:
assumes f: "cont (\<lambda>x. f x)"
assumes g: "cont (\<lambda>x. g x)"
shows "cont (\<lambda>x. (f x, g x))"
@@ -230,9 +230,9 @@
apply (rule cont_const)
done
-lemmas cont2cont_fst [cont2cont] = cont_compose [OF cont_fst]
+lemmas cont2cont_fst [simp, cont2cont] = cont_compose [OF cont_fst]
-lemmas cont2cont_snd [cont2cont] = cont_compose [OF cont_snd]
+lemmas cont2cont_snd [simp, cont2cont] = cont_compose [OF cont_snd]
lemma cont2cont_split:
assumes f1: "\<And>a b. cont (\<lambda>x. f x a b)"
@@ -256,7 +256,7 @@
"cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
by (drule cont_compose [OF _ cont_pair2], simp)
-lemma cont2cont_split' [cont2cont]:
+lemma cont2cont_split' [simp, cont2cont]:
assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
assumes g: "cont (\<lambda>x. g x)"
shows "cont (\<lambda>x. split (f x) (g x))"
--- a/src/HOLCF/Sum_Cpo.thy Sat May 22 08:30:40 2010 -0700
+++ b/src/HOLCF/Sum_Cpo.thy Sat May 22 10:02:07 2010 -0700
@@ -136,8 +136,8 @@
lemma cont_Inr: "cont Inr"
by (intro contI is_lub_Inr cpo_lubI)
-lemmas cont2cont_Inl [cont2cont] = cont_compose [OF cont_Inl]
-lemmas cont2cont_Inr [cont2cont] = cont_compose [OF cont_Inr]
+lemmas cont2cont_Inl [simp, cont2cont] = cont_compose [OF cont_Inl]
+lemmas cont2cont_Inr [simp, cont2cont] = cont_compose [OF cont_Inr]
lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
@@ -168,7 +168,7 @@
apply (rule cont_sum_case1 [OF f1 g1])
done
-lemma cont2cont_sum_case' [cont2cont]:
+lemma cont2cont_sum_case' [simp, cont2cont]:
assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
assumes h: "cont (\<lambda>x. h x)"
--- a/src/HOLCF/Tools/fixrec.ML Sat May 22 08:30:40 2010 -0700
+++ b/src/HOLCF/Tools/fixrec.ML Sat May 22 10:02:07 2010 -0700
@@ -307,11 +307,7 @@
structure FixrecSimpData = Generic_Data
(
type T = simpset;
- val empty =
- HOL_basic_ss
- addsimps simp_thms
- addsimps [@{thm beta_cfun}]
- addsimprocs [@{simproc cont_proc}];
+ val empty = HOL_basic_ss addsimps simp_thms;
val extend = I;
val merge = merge_ss;
);