# HG changeset patch
# User huffman
# Date 1274547727 25200
# Node ID 0cd15d8c90a0e30cde98d87f14737fc22c15c7ba
# Parent  a1656804fcadf3f5bd11a0ff8396201b4e01925e
remove cont2cont simproc; instead declare cont2cont rules as simp rules

diff -r a1656804fcad -r 0cd15d8c90a0 src/HOLCF/Cfun.thy
--- 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)"
diff -r a1656804fcad -r 0cd15d8c90a0 src/HOLCF/Cont.thy
--- 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)
diff -r a1656804fcad -r 0cd15d8c90a0 src/HOLCF/Fixrec.thy
--- 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
diff -r a1656804fcad -r 0cd15d8c90a0 src/HOLCF/Product_Cpo.thy
--- 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))"
diff -r a1656804fcad -r 0cd15d8c90a0 src/HOLCF/Sum_Cpo.thy
--- 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)"
diff -r a1656804fcad -r 0cd15d8c90a0 src/HOLCF/Tools/fixrec.ML
--- 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;
 );