--- 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> \\
--- 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>
--- 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)}"