# HG changeset patch
# User wenzelm
# Date 1348868715 -7200
# Node ID 366d8b41ca17d379510704efc9b900f4b9bc537a
# Parent  03bc7afe88140db43fd2f2cbfc7c776760db4517
tuned proofs;

diff -r 03bc7afe8814 -r 366d8b41ca17 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Sep 28 23:40:48 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Sep 28 23:45:15 2012 +0200
@@ -137,17 +137,17 @@
   proof -
     fix x
     assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real..1}"
-    hence "x \<le> 1 / 2" unfolding image_iff by auto
-    thus "(g1 +++ g2) x = g1 (2 *\<^sub>R x)" unfolding joinpaths_def by auto
+    then have "x \<le> 1 / 2" unfolding image_iff by auto
+    then show "(g1 +++ g2) x = g1 (2 *\<^sub>R x)" unfolding joinpaths_def by auto
   next
     fix x
     assume "x \<in> (\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real..1}"
-    hence "x \<ge> 1 / 2" unfolding image_iff by auto
-    thus "(g1 +++ g2) x = g2 (2 *\<^sub>R x - 1)"
+    then have "x \<ge> 1 / 2" unfolding image_iff by auto
+    then show "(g1 +++ g2) x = g2 (2 *\<^sub>R x - 1)"
     proof (cases "x = 1 / 2")
       case True
-      hence "x = (1/2) *\<^sub>R 1" by auto
-      thus ?thesis
+      then have "x = (1/2) *\<^sub>R 1" by auto
+      then show ?thesis
         unfolding joinpaths_def
         using assms[unfolded pathstart_def pathfinish_def]
         by (auto simp add: mult_ac)
@@ -202,7 +202,7 @@
   assume "x \<in> path_image (g1 +++ g2)"
   then obtain y where y:"y\<in>{0..1}" "x = (if y \<le> 1 / 2 then g1 (2 *\<^sub>R y) else g2 (2 *\<^sub>R y - 1))"
     unfolding path_image_def image_iff joinpaths_def by auto
-  thus "x \<in> path_image g1 \<union> path_image g2"
+  then show "x \<in> path_image g1 \<union> path_image g2"
     apply (cases "y \<le> 1/2")
     apply (rule_tac UnI1) defer
     apply (rule_tac UnI2)
@@ -227,7 +227,7 @@
   assume "x \<in> path_image g1"
   then obtain y where y: "y\<in>{0..1}" "x = g1 y"
     unfolding path_image_def image_iff by auto
-  thus "x \<in> path_image (g1 +++ g2)"
+  then show "x \<in> path_image (g1 +++ g2)"
     unfolding joinpaths_def path_image_def image_iff
     apply (rule_tac x="(1/2) *\<^sub>R y" in bexI)
     apply auto
@@ -274,7 +274,7 @@
   show "x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
   proof (case_tac "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le)
     assume as: "x \<le> 1 / 2" "y \<le> 1 / 2"
-    hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)"
+    then have "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)"
       using xy(3) unfolding joinpaths_def by auto
     moreover
     have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" using xy(1,2) as
@@ -283,7 +283,7 @@
     show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto
   next
     assume as:"x > 1 / 2" "y > 1 / 2"
-    hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)"
+    then have "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)"
       using xy(3) unfolding joinpaths_def by auto
     moreover
     have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}"
@@ -292,7 +292,7 @@
     show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto
   next
     assume as:"x \<le> 1 / 2" "y > 1 / 2"
-    hence "?g x \<in> path_image g1" "?g y \<in> path_image g2"
+    then have "?g x \<in> path_image g1" "?g y \<in> path_image g2"
       unfolding path_image_def joinpaths_def
       using xy(1,2) by auto
     moreover
@@ -301,7 +301,7 @@
       by (auto simp add: field_simps)
     ultimately
     have *:"?g x = pathstart g1" using assms(4) unfolding xy(3) by auto
-    hence "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1)
+    then have "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1)
       using inj(1)[of "2 *\<^sub>R x" 0] by auto
     moreover
     have "y = 1" using * unfolding xy(3) assms(3)[THEN sym]
@@ -310,7 +310,7 @@
     ultimately show ?thesis by auto
   next
     assume as: "x > 1 / 2" "y \<le> 1 / 2"
-    hence "?g x \<in> path_image g2" "?g y \<in> path_image g1"
+    then have "?g x \<in> path_image g2" "?g y \<in> path_image g1"
       unfolding path_image_def joinpaths_def
       using xy(1,2) by auto
     moreover
@@ -319,7 +319,7 @@
       by (auto simp add: field_simps)
     ultimately
     have *: "?g y = pathstart g1" using assms(4) unfolding xy(3) by auto
-    hence "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2)
+    then have "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2)
       using inj(1)[of "2 *\<^sub>R y" 0] by auto
     moreover
     have "x = 1" using * unfolding xy(3)[THEN sym] assms(3)[THEN sym]
@@ -342,31 +342,31 @@
   show "x = y"
   proof (cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le)
     assume "x \<le> 1 / 2" "y \<le> 1 / 2"
-    thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy
+    then show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy
       unfolding joinpaths_def by auto
   next
     assume "x > 1 / 2" "y > 1 / 2"
-    thus ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy
+    then show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy
       unfolding joinpaths_def by auto
   next
     assume as: "x \<le> 1 / 2" "y > 1 / 2"
-    hence "?g x \<in> path_image g1" "?g y \<in> path_image g2"
+    then have "?g x \<in> path_image g1" "?g y \<in> path_image g2"
       unfolding path_image_def joinpaths_def
       using xy(1,2) by auto
-    hence "?g x = pathfinish g1" "?g y = pathstart g2"
+    then have "?g x = pathfinish g1" "?g y = pathstart g2"
       using assms(4) unfolding assms(3) xy(3) by auto
-    thus ?thesis
+    then show ?thesis
       using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2)
       unfolding pathstart_def pathfinish_def joinpaths_def
       by auto
   next
     assume as:"x > 1 / 2" "y \<le> 1 / 2" 
-    hence "?g x \<in> path_image g2" "?g y \<in> path_image g1"
+    then have "?g x \<in> path_image g2" "?g y \<in> path_image g1"
       unfolding path_image_def joinpaths_def
       using xy(1,2) by auto
-    hence "?g x = pathstart g2" "?g y = pathfinish g1"
+    then have "?g x = pathstart g2" "?g y = pathfinish g1"
       using assms(4) unfolding assms(3) xy(3) by auto
-    thus ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2)
+    then show ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2)
       unfolding pathstart_def pathfinish_def joinpaths_def
       by auto
   qed
@@ -431,21 +431,21 @@
 proof -
   { fix x
     assume as:"g 1 = g 0" "x \<in> {0..1::real}" " \<forall>y\<in>{0..1} \<inter> {x. \<not> a + x \<le> 1}. g x \<noteq> g (a + y - 1)" 
-    hence "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)"
+    then have "\<exists>y\<in>{0..1} \<inter> {x. a + x \<le> 1}. g x = g (a + y)"
     proof (cases "a \<le> x")
       case False
-      thus ?thesis
+      then show ?thesis
         apply (rule_tac x="1 + x - a" in bexI)
         using as(1,2) and as(3)[THEN bspec[where x="1 + x - a"]] and assms(1)
         apply (auto simp add: field_simps atomize_not)
         done
     next
       case True
-      thus ?thesis using as(1-2) and assms(1) apply(rule_tac x="x - a" in bexI)
+      then show ?thesis using as(1-2) and assms(1) apply(rule_tac x="x - a" in bexI)
         by(auto simp add: field_simps)
     qed
   }
-  thus ?thesis
+  then show ?thesis
     using assms unfolding shiftpath_def path_image_def pathfinish_def pathstart_def
     by(auto simp add: image_iff)
 qed
@@ -490,9 +490,9 @@
 proof -
   { fix x y :: "real"
     assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b"
-    hence "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b" by (simp add: algebra_simps)
+    then have "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b" by (simp add: algebra_simps)
     with assms have "x = y" by simp }
-  thus ?thesis
+  then show ?thesis
     unfolding injective_path_def linepath_def
     by (auto simp add: algebra_simps)
 qed
@@ -511,7 +511,7 @@
   obtain a where "a \<in> path_image g" "\<forall>y \<in> path_image g. dist z a \<le> dist z y"
     using distance_attains_inf[OF _ path_image_nonempty, of g z]
     using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto
-  thus ?thesis
+  then show ?thesis
     apply (rule_tac x="dist z a" in exI)
     using assms(2)
     apply (auto intro!: dist_pos_lt)
@@ -667,7 +667,7 @@
 proof
   fix y
   assume as: "y \<in> {y. path_component s x y}"
-  hence "y \<in> s"
+  then have "y \<in> s"
     apply -
     apply (rule path_component_mem(2))
     unfolding mem_Collect_eq
@@ -682,7 +682,7 @@
   proof -
     fix z
     assume "dist y z < e"
-    thus "path_component s x z"
+    then show "path_component s x z"
       apply (rule_tac path_component_trans[of _ _ y]) defer
       apply (rule path_component_of_subset[OF e(2)])
       apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format])
@@ -708,7 +708,7 @@
   proof (rule ccontr)
     fix z
     assume "z \<in> ball y e" "\<not> z \<notin> {y. path_component s x y}"
-    hence "y \<in> {y. path_component s x y}"
+    then have "y \<in> {y. path_component s x y}"
       unfolding not_not mem_Collect_eq using `e>0`
       apply -
       apply (rule path_component_trans, assumption)
@@ -716,7 +716,7 @@
       apply (rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format])
       apply auto
       done
-    thus False using as by auto
+    then show False using as by auto
   qed (insert e(2), auto)
 qed
 
@@ -751,7 +751,7 @@
   assume "x' \<in> f ` s" "y' \<in> f ` s"
   then obtain x y where xy: "x\<in>s" "y\<in>s" "x' = f x" "y' = f y" by auto
   guess g using assms(2)[unfolded path_connected_def, rule_format, OF xy(1,2)] ..
-  thus "\<exists>g. path g \<and> path_image g \<subseteq> f ` s \<and> pathstart g = x' \<and> pathfinish g = y'"
+  then show "\<exists>g. path g \<and> path_image g \<subseteq> f ` s \<and> pathstart g = x' \<and> pathfinish g = y'"
     unfolding xy
     apply (rule_tac x="f \<circ> g" in exI)
     unfolding path_defs
@@ -787,7 +787,7 @@
   fix x y
   assume as: "x \<in> s \<union> t" "y \<in> s \<union> t"
   from assms(3) obtain z where "z \<in> s \<inter> t" by auto
-  thus "path_component (s \<union> t) x y"
+  then show "path_component (s \<union> t) x y"
     using as and assms(1-2)[unfolded path_connected_component]
     apply - 
     apply (erule_tac[!] UnE)+
@@ -804,11 +804,11 @@
 proof clarify
   fix x i y j
   assume *: "i \<in> A" "x \<in> S i" "j \<in> A" "y \<in> S j"
-  hence "path_component (S i) x z" and "path_component (S j) z y"
+  then have "path_component (S i) x z" and "path_component (S j) z y"
     using assms by (simp_all add: path_connected_component)
-  hence "path_component (\<Union>i\<in>A. S i) x z" and "path_component (\<Union>i\<in>A. S i) z y"
+  then have "path_component (\<Union>i\<in>A. S i) x z" and "path_component (\<Union>i\<in>A. S i) z y"
     using *(1,3) by (auto elim!: path_component_of_subset [rotated])
-  thus "path_component (\<Union>i\<in>A. S i) x y"
+  then show "path_component (\<Union>i\<in>A. S i) x y"
     by (rule path_component_trans)
 qed
 
@@ -827,7 +827,7 @@
   proof (rule path_connected_UNION)
     fix i
     assume "i \<in> {..<DIM('a)}"
-    thus "(\<chi>\<chi> i. a $$ i - 1) \<in> {x::'a. x $$ i < a $$ i}" by simp
+    then show "(\<chi>\<chi> i. a $$ i - 1) \<in> {x::'a. x $$ i < a $$ i}" by simp
     show "path_connected {x. x $$ i < a $$ i}" unfolding euclidean_component_def
       by (rule convex_imp_path_connected [OF convex_halfspace_lt])
   qed
@@ -835,13 +835,13 @@
   proof (rule path_connected_UNION)
     fix i
     assume "i \<in> {..<DIM('a)}"
-    thus "(\<chi>\<chi> i. a $$ i + 1) \<in> {x::'a. a $$ i < x $$ i}" by simp
+    then show "(\<chi>\<chi> i. a $$ i + 1) \<in> {x::'a. a $$ i < x $$ i}" by simp
     show "path_connected {x. a $$ i < x $$ i}" unfolding euclidean_component_def
       by (rule convex_imp_path_connected [OF convex_halfspace_gt])
   qed
   from assms have "1 < DIM('a)" by auto
-  hence "a + basis 0 - basis 1 \<in> ?A \<inter> ?B" by auto
-  hence "?A \<inter> ?B \<noteq> {}" by fast
+  then have "a + basis 0 - basis 1 \<in> ?A \<inter> ?B" by auto
+  then have "?A \<inter> ?B \<noteq> {}" by fast
   with A B have "path_connected (?A \<union> ?B)"
     by (rule path_connected_Un)
   also have "?A \<union> ?B = {x. \<exists>i\<in>{..<DIM('a)}. x $$ i \<noteq> a $$ i}"
@@ -857,14 +857,14 @@
   shows "path_connected {x::'a::euclidean_space. norm(x - a) = r}"
 proof (rule linorder_cases [of r 0])
   assume "r < 0"
-  hence "{x::'a. norm(x - a) = r} = {}" by auto
-  thus ?thesis using path_connected_empty by simp
+  then have "{x::'a. norm(x - a) = r} = {}" by auto
+  then show ?thesis using path_connected_empty by simp
 next
   assume "r = 0"
-  thus ?thesis using path_connected_singleton by simp
+  then show ?thesis using path_connected_singleton by simp
 next
   assume r: "0 < r"
-  hence *: "{x::'a. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}"
+  then have *: "{x::'a. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}"
     apply -
     apply (rule set_eqI, rule)
     unfolding image_iff
@@ -881,7 +881,7 @@
     done
   have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)"
     unfolding field_divide_inverse by (simp add: continuous_on_intros)
-  thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
+  then show ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
     by (auto intro!: path_connected_continuous_image continuous_on_intros)
 qed