src/HOLCF/Cfun.thy

 
 
 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])
 
 instance cfun :: (finite_po, chfin) chfin

 
 subsection {* Continuity simplification procedure *}
 
 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))"
 proof -
   have "cont (\<lambda>x. Rep_CFun (f x))"

 text {*
   This version does work as a cont2cont rule, since it
   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)"
 proof (rule cont2cont_LAM)
   fix x :: 'a show "cont (\<lambda>y. f x y)"

 next
   fix y :: 'b show "cont (\<lambda>x. f x y)"
     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)
 
 lemmas cont_lemmas1 =
   cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM

   assumes g1: "\<And>y. cont (\<lambda>x. g x y)"
   assumes g2: "\<And>x. cont (\<lambda>y. g x y)"
   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)"
 using f
 proof (rule cont2cont_Let)