diff -r 3793c3a11378 -r ef949192e5d6 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -831,16 +831,7 @@
 
 lemma lemma_MVT:
      "f a - (f b - f a)/(b-a) * a = f b - (f b - f a)/(b-a) * (b::real)"
-proof cases
-  assume "a=b" thus ?thesis by simp
-next
-  assume "a\<noteq>b"
-  hence ba: "b-a \<noteq> 0" by arith
-  show ?thesis
-    by (rule real_mult_left_cancel [OF ba, THEN iffD1],
-        simp add: right_diff_distrib,
-        simp add: left_diff_distrib)
-qed
+  by (cases "a = b") (simp_all add: field_simps)
 
 theorem MVT:
   assumes lt:  "a < b"
@@ -1090,152 +1081,47 @@
     by simp
 qed
 
-subsection {* Continuous injective functions *}
-
-text{*Dull lemma: an continuous injection on an interval must have a
-strict maximum at an end point, not in the middle.*}
-
-lemma lemma_isCont_inj:
-  fixes f :: "real \<Rightarrow> real"
-  assumes d: "0 < d"
-      and inj [rule_format]: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
-      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
-  shows "\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z"
-proof (rule ccontr)
-  assume  "~ (\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z)"
-  hence all [rule_format]: "\<forall>z. \<bar>z - x\<bar> \<le> d --> f z \<le> f x" by auto
-  show False
-  proof (cases rule: linorder_le_cases [of "f(x-d)" "f(x+d)"])
-    case le
-    from d cont all [of "x+d"]
-    have flef: "f(x+d) \<le> f x"
-     and xlex: "x - d \<le> x"
-     and cont': "\<forall>z. x - d \<le> z \<and> z \<le> x \<longrightarrow> isCont f z"
-       by (auto simp add: abs_if)
-    from IVT [OF le flef xlex cont']
-    obtain x' where "x-d \<le> x'" "x' \<le> x" "f x' = f(x+d)" by blast
-    moreover
-    hence "g(f x') = g (f(x+d))" by simp
-    ultimately show False using d inj [of x'] inj [of "x+d"]
-      by (simp add: abs_le_iff)
-  next
-    case ge
-    from d cont all [of "x-d"]
-    have flef: "f(x-d) \<le> f x"
-     and xlex: "x \<le> x+d"
-     and cont': "\<forall>z. x \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z"
-       by (auto simp add: abs_if)
-    from IVT2 [OF ge flef xlex cont']
-    obtain x' where "x \<le> x'" "x' \<le> x+d" "f x' = f(x-d)" by blast
-    moreover
-    hence "g(f x') = g (f(x-d))" by simp
-    ultimately show False using d inj [of x'] inj [of "x-d"]
-      by (simp add: abs_le_iff)
-  qed
-qed
-
-
-text{*Similar version for lower bound.*}
-
-lemma lemma_isCont_inj2:
-  fixes f g :: "real \<Rightarrow> real"
-  shows "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
-        \<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z |]
-      ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
-apply (insert lemma_isCont_inj
-          [where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
-apply (simp add: linorder_not_le)
-done
-
-text{*Show there's an interval surrounding @{term "f(x)"} in
-@{text "f[[x - d, x + d]]"} .*}
-
-lemma isCont_inj_range:
-  fixes f :: "real \<Rightarrow> real"
-  assumes d: "0 < d"
-      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
-      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
-  shows "\<exists>e>0. \<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y)"
-proof -
-  have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
-    by (auto simp add: abs_le_iff)
-  from isCont_Lb_Ub [OF this]
-  obtain L M
-  where all1 [rule_format]: "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> L \<le> f z \<and> f z \<le> M"
-    and all2 [rule_format]:
-           "\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>z. x-d \<le> z \<and> z \<le> x+d \<and> f z = y)"
-    by auto
-  with d have "L \<le> f x & f x \<le> M" by simp
-  moreover have "L \<noteq> f x"
-  proof -
-    from lemma_isCont_inj2 [OF d inj cont]
-    obtain u where "\<bar>u - x\<bar> \<le> d" "f u < f x"  by auto
-    thus ?thesis using all1 [of u] by arith
-  qed
-  moreover have "f x \<noteq> M"
-  proof -
-    from lemma_isCont_inj [OF d inj cont]
-    obtain u where "\<bar>u - x\<bar> \<le> d" "f x < f u"  by auto
-    thus ?thesis using all1 [of u] by arith
-  qed
-  ultimately have "L < f x & f x < M" by arith
-  hence "0 < f x - L" "0 < M - f x" by arith+
-  from real_lbound_gt_zero [OF this]
-  obtain e where e: "0 < e" "e < f x - L" "e < M - f x" by auto
-  thus ?thesis
-  proof (intro exI conjI)
-    show "0<e" using e(1) .
-    show "\<forall>y. \<bar>y - f x\<bar> \<le> e \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y)"
-    proof (intro strip)
-      fix y::real
-      assume "\<bar>y - f x\<bar> \<le> e"
-      with e have "L \<le> y \<and> y \<le> M" by arith
-      from all2 [OF this]
-      obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
-      thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y" 
-        by (force simp add: abs_le_iff)
-    qed
-  qed
-qed
-
-
 text{*Continuity of inverse function*}
 
 lemma isCont_inverse_function:
   fixes f g :: "real \<Rightarrow> real"
   assumes d: "0 < d"
-      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
-      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
+      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> g (f z) = z"
+      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> isCont f z"
   shows "isCont g (f x)"
-proof (simp add: isCont_iff LIM_eq)
-  show "\<forall>r. 0 < r \<longrightarrow>
-         (\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
-  proof (intro strip)
-    fix r::real
-    assume r: "0<r"
-    from real_lbound_gt_zero [OF r d]
-    obtain e where e: "0 < e" and e_lt: "e < r \<and> e < d" by blast
-    with inj cont
-    have e_simps: "\<forall>z. \<bar>z-x\<bar> \<le> e --> g (f z) = z"
-                  "\<forall>z. \<bar>z-x\<bar> \<le> e --> isCont f z"   by auto
-    from isCont_inj_range [OF e this]
-    obtain e' where e': "0 < e'"
-        and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
-          by blast
-    show "\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r"
-    proof (intro exI conjI)
-      show "0<e'" using e' .
-      show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
-      proof (intro strip)
-        fix z::real
-        assume z: "z \<noteq> 0 \<and> \<bar>z\<bar> < e'"
-        with e e_lt e_simps all [rule_format, of "f x + z"]
-        show "\<bar>g (f x + z) - g (f x)\<bar> < r" by force
-      qed
-    qed
-  qed
+proof -
+  let ?A = "f (x - d)" and ?B = "f (x + d)" and ?D = "{x - d..x + d}"
+
+  have f: "continuous_on ?D f"
+    using cont by (intro continuous_at_imp_continuous_on ballI) auto
+  then have g: "continuous_on (f`?D) g"
+    using inj by (intro continuous_on_inv) auto
+
+  from d f have "{min ?A ?B <..< max ?A ?B} \<subseteq> f ` ?D"
+    by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max)
+  with g have "continuous_on {min ?A ?B <..< max ?A ?B} g"
+    by (rule continuous_on_subset)
+  moreover
+  have "(?A < f x \<and> f x < ?B) \<or> (?B < f x \<and> f x < ?A)"
+    using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto
+  then have "f x \<in> {min ?A ?B <..< max ?A ?B}"
+    by auto
+  ultimately
+  show ?thesis
+    by (simp add: continuous_on_eq_continuous_at)
 qed
 
+lemma isCont_inverse_function2:
+  fixes f g :: "real \<Rightarrow> real" shows
+  "\<lbrakk>a < x; x < b;
+    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
+    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
+   \<Longrightarrow> isCont g (f x)"
+apply (rule isCont_inverse_function
+       [where f=f and d="min (x - a) (b - x)"])
+apply (simp_all add: abs_le_iff)
+done
+
 text {* Derivative of inverse function *}
 
 lemma DERIV_inverse_function:
@@ -1285,7 +1171,6 @@
     using neq by (rule tendsto_inverse)
 qed
 
-
 subsection {* Generalized Mean Value Theorem *}
 
 theorem GMVT:
@@ -1355,21 +1240,6 @@
       ==> isCont g (f x)"
 by (rule isCont_inverse_function)
 
-lemma isCont_inv_fun_inv:
-  fixes f g :: "real \<Rightarrow> real"
-  shows "[| 0 < d;  
-         \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
-         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
-       ==> \<exists>e. 0 < e &  
-             (\<forall>y. 0 < \<bar>y - f(x)\<bar> & \<bar>y - f(x)\<bar> < e --> f(g(y)) = y)"
-apply (drule isCont_inj_range)
-prefer 2 apply (assumption, assumption, auto)
-apply (rule_tac x = e in exI, auto)
-apply (rotate_tac 2)
-apply (drule_tac x = y in spec, auto)
-done
-
-
 text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
 lemma LIM_fun_gt_zero:
      "[| f -- c --> (l::real); 0 < l |]