# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1465916068 -3600
# Node ID d15dde801536f6c2003a8dc79d5cb5b3f34a8e90
# Parent  d3c87eb0bad2c38482f14ff523cdd8bc75d49da6# Parent  e7920a0abf4a271ea2a46ce83e636c42ec19a44b
Merge

diff -r d3c87eb0bad2 -r d15dde801536 src/Doc/Isar_Ref/Quick_Reference.thy
--- a/src/Doc/Isar_Ref/Quick_Reference.thy	Tue Jun 14 15:34:21 2016 +0100
+++ b/src/Doc/Isar_Ref/Quick_Reference.thy	Tue Jun 14 15:54:28 2016 +0100
@@ -22,13 +22,13 @@
     & & \quad\<^theory_text>\<open>fixes vars\<close> \\
     & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
     & & \quad\<^theory_text>\<open>obtains (name) vars where props | \<dots> "proof"\<close> \\
-    \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" main_proof\<close> \\
+    \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" proper_proof\<close> \\
     \<open>refinement\<close> & = &  \<^theory_text>\<open>apply method\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>supply name = thms\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>using thms\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>unfolding thms\<close> \\
-    \<open>main_proof\<close> & = & \<^theory_text>\<open>proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
+    \<open>proper_proof\<close> & = & \<^theory_text>\<open>proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>done\<close> \\
     \<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>next\<close> \\
diff -r d3c87eb0bad2 -r d15dde801536 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Jun 14 15:34:21 2016 +0100
+++ b/src/HOL/Deriv.thy	Tue Jun 14 15:54:28 2016 +0100
@@ -756,8 +756,9 @@
   by (rule DERIV_continuous)
 
 lemma DERIV_continuous_on:
-  "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative (D x)) (at x)) \<Longrightarrow> continuous_on s f"
-  by (metis DERIV_continuous continuous_at_imp_continuous_on)
+  "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative (D x)) (at x within s)) \<Longrightarrow> continuous_on s f"
+  unfolding continuous_on_eq_continuous_within
+  by (intro continuous_at_imp_continuous_on ballI DERIV_continuous) 
 
 lemma DERIV_mult':
   "(f has_field_derivative D) (at x within s) \<Longrightarrow> (g has_field_derivative E) (at x within s) \<Longrightarrow>
diff -r d3c87eb0bad2 -r d15dde801536 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jun 14 15:34:21 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jun 14 15:54:28 2016 +0100
@@ -12487,6 +12487,61 @@
   by (rule integrable_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)
 
 
+subsection \<open>Integration by substitution\<close>
+
+
+lemma has_integral_substitution_strong:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
+  assumes s: "finite s" and le: "a \<le> b" "c \<le> d" "g a \<le> g b"
+      and subset: "g ` {a..b} \<subseteq> {c..d}"
+      and f [continuous_intros]: "continuous_on {c..d} f"
+      and g [continuous_intros]: "continuous_on {a..b} g"
+      and deriv [derivative_intros]:
+              "\<And>x. x \<in> {a..b} - s \<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}"
+proof -
+  let ?F = "\<lambda>x. integral {c..g x} f"
+  have cont_int: "continuous_on {a..b} ?F"
+    by (rule continuous_on_compose2[OF _ g subset] indefinite_integral_continuous
+          f integrable_continuous_real)+
+  have deriv: "(((\<lambda>x. integral {c..x} f) \<circ> g) has_vector_derivative g' x *\<^sub>R f (g x))
+                 (at x within {a..b})" if "x \<in> {a..b} - s" for x
+    apply (rule has_vector_derivative_eq_rhs)
+    apply (rule vector_diff_chain_within)
+    apply (subst has_field_derivative_iff_has_vector_derivative [symmetric])
+    apply (rule deriv that)+
+    apply (rule has_vector_derivative_within_subset)
+    apply (rule integral_has_vector_derivative f)+
+    using that le subset
+    apply blast+
+    done
+  have deriv: "(?F has_vector_derivative g' x *\<^sub>R f (g x))
+                  (at x)" if "x \<in> {a..b} - (s \<union> {a,b})" for x
+    using deriv[of x] that by (simp add: at_within_closed_interval o_def)
+
+
+  have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
+    using le cont_int s deriv cont_int
+    by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all
+  also from subset have "g x \<in> {c..d}" if "x \<in> {a..b}" for x using that by blast
+  from this[of a] this[of b] le have "c \<le> g a" "g b \<le> d" by auto
+  hence "integral {c..g a} f + integral {g a..g b} f = integral {c..g b} f"
+    by (intro integral_combine integrable_continuous_real continuous_on_subset[OF f] le) simp_all
+  hence "integral {c..g b} f - integral {c..g a} f = integral {g a..g b} f"
+    by (simp add: algebra_simps)
+  finally show ?thesis .
+qed
+
+lemma has_integral_substitution:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
+  assumes "a \<le> b" "c \<le> d" "g a \<le> g b" "g ` {a..b} \<subseteq> {c..d}"
+      and "continuous_on {c..d} f"
+      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 c d] assms)
+     (auto intro: DERIV_continuous_on assms)
+
+
 subsection \<open>Compute a double integral using iterated integrals and switching the order of integration\<close>
 
 lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"