src/HOL/Deriv.thy

 lemmas has_derivative_mult_right [derivative_intros] =
   bounded_linear.has_derivative [OF bounded_linear_mult_right]
 
 lemmas has_derivative_mult_left [derivative_intros] =
   bounded_linear.has_derivative [OF bounded_linear_mult_left]
+
+lemmas has_derivative_of_real[derivative_intros, simp] = 
+  bounded_linear.has_derivative[OF bounded_linear_of_real] 
 
 lemma has_derivative_add[simp, derivative_intros]:
   assumes f: "(f has_derivative f') F"
     and g: "(g has_derivative g') F"
   shows "((\<lambda>x. f x + g x) has_derivative (\<lambda>x. f' x + g' x)) F"

 lemma has_vector_derivative_of_real[derivative_intros]:
   "(f has_field_derivative D) F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_vector_derivative (of_real D)) F"
   by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real])
     (simp add: has_field_derivative_iff_has_vector_derivative)
 
+lemma has_vector_derivative_real_field:
+  "(f has_field_derivative f') (at (of_real a)) \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
+  using has_derivative_compose[of of_real of_real a _ f "(*) f'"] 
+  by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
+
 lemma has_vector_derivative_continuous:
   "(f has_vector_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
   by (auto intro: has_derivative_continuous simp: has_vector_derivative_def)
 
 lemma continuous_on_vector_derivative:

     by eventually_elim auto
 qed
 
 lemmas has_derivative_floor[derivative_intros] =
   floor_has_real_derivative[THEN DERIV_compose_FDERIV]
+
+lemma continuous_floor:
+  fixes x::real
+  shows "x \<notin> \<int> \<Longrightarrow> continuous (at x) (real_of_int \<circ> floor)"
+  using floor_has_real_derivative [where f=id]
+  by (auto simp: o_def has_field_derivative_def intro: has_derivative_continuous)
+
+lemma continuous_frac:
+  fixes x::real
+  assumes "x \<notin> \<int>"
+  shows "continuous (at x) frac"
+proof -
+  have "isCont (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x"
+    using continuous_floor [OF assms] by (simp add: o_def)
+  then have *: "continuous (at x) (\<lambda>x. x - real_of_int \<lfloor>x\<rfloor>)"
+    by (intro continuous_intros)
+  moreover have "\<forall>\<^sub>F x in nhds x. frac x = x - real_of_int \<lfloor>x\<rfloor>"
+    by (simp add: frac_def)
+  ultimately show ?thesis
+    by (simp add: LIM_imp_LIM frac_def isCont_def)
+qed
 
 text \<open>Caratheodory formulation of derivative at a point\<close>
 
 lemma CARAT_DERIV:
   "(DERIV f x :> l) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> g x = l)"