src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

       and "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_field_derivative g' x) (at x within {a..b})"
     shows "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (integral {g a..g b} f)) {a..b}"
   by (intro has_integral_substitution_strong[of "{}" a b g c d] assms)
      (auto intro: DERIV_continuous_on assms)
 
+lemma integral_shift:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes cont: "continuous_on {a + c..b + c} f"
+  shows "integral {a..b} (f \<circ> (\<lambda>x. x + c)) = integral {a + c..b + c} f"
+proof (cases "a \<le> b")
+  case True
+  have "((\<lambda>x. 1 *\<^sub>R f (x + c)) has_integral integral {a+c..b+c} f) {a..b}"
+    using True cont
+    by (intro has_integral_substitution[where c = "a + c" and d = "b + c"])
+       (auto intro!: derivative_eq_intros)
+  thus ?thesis by (simp add: has_integral_iff o_def)
+qed auto
+
 
 subsection \<open>Compute a double integral using iterated integrals and switching the order of integration\<close>
 
 lemma continuous_on_imp_integrable_on_Pair1:
   fixes f :: "_ \<Rightarrow> 'b::banach"