# HG changeset patch
# User wenzelm
# Date 1379103386 -7200
# Node ID f3fd9168911c82fa37ba5192261a55da5a7c538b
# Parent  da1c7b50fdfea3170c3383e6c5dcf99605a811fc
tuned proofs;

diff -r da1c7b50fdfe -r f3fd9168911c src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Fri Sep 13 21:14:08 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Fri Sep 13 22:16:26 2013 +0200
@@ -323,124 +323,327 @@
     done
 qed
 
-lemma fashoda: fixes b::"real^2"
-  assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
-  "(pathstart f)$1 = a$1" "(pathfinish f)$1 = b$1"
-  "(pathstart g)$2 = a$2" "(pathfinish g)$2 = b$2"
-  obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
-  fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto
-next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto
-  hence "a \<le> b" unfolding interval_eq_empty_cart less_eq_vec_def by(auto simp add: not_less)
-  thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding less_eq_vec_def forall_2 by auto
-next assume as:"a$1 = b$1" have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component_cart)
-    apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
+lemma fashoda:
+  fixes b :: "real^2"
+  assumes "path f"
+    and "path g"
+    and "path_image f \<subseteq> {a..b}"
+    and "path_image g \<subseteq> {a..b}"
+    and "(pathstart f)$1 = a$1"
+    and "(pathfinish f)$1 = b$1"
+    and "(pathstart g)$2 = a$2"
+    and "(pathfinish g)$2 = b$2"
+  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
+proof -
+  fix P Q S
+  presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis"
+  then show thesis
+    by auto
+next
+  have "{a..b} \<noteq> {}"
+    using assms(3) using path_image_nonempty by auto
+  then have "a \<le> b"
+    unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
+  then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)"
+    unfolding less_eq_vec_def forall_2 by auto
+next
+  assume as: "a$1 = b$1"
+  have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2"
+    apply (rule connected_ivt_component_cart)
+    apply (rule connected_path_image assms)+
+    apply (rule pathstart_in_path_image)
+    apply (rule pathfinish_in_path_image)
     unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
-    unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this
-  have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast 
-  hence "z = f 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def
+    unfolding pathstart_def
+    apply (auto simp add: less_eq_vec_def)
+    done
+  then guess z .. note z=this
+  have "z \<in> {a..b}"
+    using z(1) assms(4)
+    unfolding path_image_def
+    by blast 
+  then have "z = f 0"
+    unfolding vec_eq_iff forall_2
+    unfolding z(2) pathstart_def
     using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1]
-    unfolding mem_interval_cart apply(erule_tac x=1 in allE) using as by auto
-  thus thesis apply-apply(rule that[OF _ z(1)]) unfolding path_image_def by auto
-next assume as:"a$2 = b$2" have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component_cart)
-    apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
-    unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
-    unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this
-  have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast 
-  hence "z = g 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def
+    unfolding mem_interval_cart
+    apply (erule_tac x=1 in allE)
+    using as
+    apply auto
+    done
+  then show thesis
+    apply -
+    apply (rule that[OF _ z(1)])
+    unfolding path_image_def
+    apply auto
+    done
+next
+  assume as: "a$2 = b$2"
+  have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1"
+    apply (rule connected_ivt_component_cart)
+    apply (rule connected_path_image assms)+
+    apply (rule pathstart_in_path_image)
+    apply (rule pathfinish_in_path_image)
+    unfolding assms
+    using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
+    unfolding pathstart_def
+    apply (auto simp add: less_eq_vec_def)
+    done
+  then guess z .. note z=this
+  have "z \<in> {a..b}"
+    using z(1) assms(3)
+    unfolding path_image_def
+    by blast 
+  then have "z = g 0"
+    unfolding vec_eq_iff forall_2
+    unfolding z(2) pathstart_def
     using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2]
-    unfolding mem_interval_cart apply(erule_tac x=2 in allE) using as by auto
-  thus thesis apply-apply(rule that[OF z(1)]) unfolding path_image_def by auto
-next assume as:"a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
-  have int_nem:"{- 1..1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto
-  guess z apply(rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"]) 
+    unfolding mem_interval_cart
+    apply (erule_tac x=2 in allE)
+    using as
+    apply auto
+    done
+  then show thesis
+    apply -
+    apply (rule that[OF z(1)])
+    unfolding path_image_def
+    apply auto
+    done
+next
+  assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
+  have int_nem: "{- 1..1::real^2} \<noteq> {}"
+    unfolding interval_eq_empty_cart by auto
+  guess z
+    apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"]) 
     unfolding path_def path_image_def pathstart_def pathfinish_def
-    apply(rule_tac[1-2] continuous_on_compose) apply(rule assms[unfolded path_def] continuous_on_interval_bij)+
-    unfolding subset_eq apply(rule_tac[1-2] ballI)
-  proof- fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
+    apply (rule_tac[1-2] continuous_on_compose)
+    apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
+    unfolding subset_eq
+    apply(rule_tac[1-2] ballI)
+  proof -
+    fix x
+    assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
+    then guess y
+      unfolding image_iff .. note y=this
+    show "x \<in> {- 1..1}"
+      unfolding y o_def
+      apply (rule in_interval_interval_bij)
+      using y(1)
+      using assms(3)[unfolded path_image_def subset_eq] int_nem
+      apply auto
+      done
+  next
+    fix x
+    assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
     then guess y unfolding image_iff .. note y=this
-    show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
-      using y(1) using assms(3)[unfolded path_image_def subset_eq] int_nem by auto
-  next fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
-    then guess y unfolding image_iff .. note y=this
-    show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
-      using y(1) using assms(4)[unfolded path_image_def subset_eq] int_nem by auto
-  next show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
-      "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
-      "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
-      "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
+    show "x \<in> {- 1..1}"
+      unfolding y o_def
+      apply (rule in_interval_interval_bij)
+      using y(1)
+      using assms(4)[unfolded path_image_def subset_eq] int_nem
+      apply auto
+      done
+  next
+    show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
+      and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
+      and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
+      and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
       using assms as 
       by (simp_all add: axis_in_Basis cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
          (simp_all add: inner_axis)
-  qed note z=this
+  qed
+  note z=this
   from z(1) guess zf unfolding image_iff .. note zf=this
   from z(2) guess zg unfolding image_iff .. note zg=this
-  have *:"\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" unfolding forall_2 using as by auto
-  show thesis apply(rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
-    apply(subst zf) defer apply(subst zg) unfolding o_def interval_bij_bij_cart[OF *] path_image_def
-    using zf(1) zg(1) by auto qed
+  have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i"
+    unfolding forall_2
+    using as
+    by auto
+  show thesis
+    apply (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
+    apply (subst zf)
+    defer
+    apply (subst zg)
+    unfolding o_def interval_bij_bij_cart[OF *] path_image_def
+    using zf(1) zg(1)
+    apply auto
+    done
+qed
 
-subsection {*Some slightly ad hoc lemmas I use below*}
+
+subsection {* Some slightly ad hoc lemmas I use below *}
 
-lemma segment_vertical: fixes a::"real^2" assumes "a$1 = b$1"
-  shows "x \<in> closed_segment a b \<longleftrightarrow> (x$1 = a$1 \<and> x$1 = b$1 \<and>
-           (a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2))" (is "_ = ?R")
-proof- 
+lemma segment_vertical:
+  fixes a :: "real^2"
+  assumes "a$1 = b$1"
+  shows "x \<in> closed_segment a b \<longleftrightarrow>
+    x$1 = a$1 \<and> x$1 = b$1 \<and> (a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2)"
+  (is "_ = ?R")
+proof -
   let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1"
-  { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
-      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[THEN sym] vector_component_simps by blast }
-  { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
-    { fix b a assume "b + u * a > a + u * b"
-      hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
-      hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
-      hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)]) 
-        using u(3-4) by(auto simp add:field_simps) } note * = this
-    { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
-        apply(drule mult_less_imp_less_left) using u by auto
-      hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
-    thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
-  { assume ?R thus ?L proof(cases "x$2 = b$2")
-      case True thus ?L apply(rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) unfolding assms True
-        using `?R` by(auto simp add:field_simps)
-    next case False thus ?L apply(rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) unfolding assms using `?R`
-        by(auto simp add:field_simps)
-    qed } qed
+  {
+    presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
+    then show ?thesis
+      unfolding closed_segment_def mem_Collect_eq
+      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[THEN sym] vector_component_simps
+      by blast
+  }
+  {
+    assume ?L
+    then guess u by (elim exE conjE) note u=this
+    { fix b a
+      assume "b + u * a > a + u * b"
+      then have "(1 - u) * b > (1 - u) * a"
+        by (auto simp add:field_simps)
+      then have "b \<ge> a"
+        apply (drule_tac mult_less_imp_less_left)
+        using u
+        apply auto
+        done
+      then have "u * a \<le> u * b"
+        apply -
+        apply (rule mult_left_mono[OF _ u(3)]) 
+        using u(3-4)
+        apply (auto simp add: field_simps)
+        done
+    } note * = this
+    {
+      fix a b
+      assume "u * b > u * a"
+      then have "(1 - u) * a \<le> (1 - u) * b"
+        apply -
+        apply (rule mult_left_mono)
+        apply (drule mult_less_imp_less_left)
+        using u
+        apply auto
+        done
+      then have "a + u * b \<le> b + u * a"
+        by (auto simp add: field_simps)
+    } note ** = this
+    then show ?R
+      unfolding u assms
+      using u
+      by (auto simp add:field_simps not_le intro: * **)
+  }
+  {
+    assume ?R
+    then show ?L
+    proof (cases "x$2 = b$2")
+      case True
+      then show ?L
+        apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI)
+        unfolding assms True
+        using `?R`
+        apply (auto simp add: field_simps)
+        done
+    next
+      case False
+      then show ?L
+        apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI)
+        unfolding assms
+        using `?R`
+        apply (auto simp add: field_simps)
+        done
+    qed
+  }
+qed
 
-lemma segment_horizontal: fixes a::"real^2" assumes "a$2 = b$2"
-  shows "x \<in> closed_segment a b \<longleftrightarrow> (x$2 = a$2 \<and> x$2 = b$2 \<and>
-           (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1))" (is "_ = ?R")
-proof- 
+lemma segment_horizontal:
+  fixes a :: "real^2"
+  assumes "a$2 = b$2"
+  shows "x \<in> closed_segment a b \<longleftrightarrow>
+    x$2 = a$2 \<and> x$2 = b$2 \<and> (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1)"
+  (is "_ = ?R")
+proof -
   let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1"
-  { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
-      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[THEN sym] vector_component_simps by blast }
-  { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
-    { fix b a assume "b + u * a > a + u * b"
-      hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
-      hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
-      hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)]) 
-        using u(3-4) by(auto simp add:field_simps) } note * = this
-    { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
-        apply(drule mult_less_imp_less_left) using u by auto
-      hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
-    thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
-  { assume ?R thus ?L proof(cases "x$1 = b$1")
-      case True thus ?L apply(rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) unfolding assms True
-        using `?R` by(auto simp add:field_simps)
-    next case False thus ?L apply(rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) unfolding assms using `?R`
-        by(auto simp add:field_simps)
-    qed } qed
+  {
+    presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
+    then show ?thesis
+      unfolding closed_segment_def mem_Collect_eq
+      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[THEN sym] vector_component_simps
+      by blast
+  }
+  {
+    assume ?L
+    then guess u by (elim exE conjE) note u=this
+    {
+      fix b a
+      assume "b + u * a > a + u * b"
+      then have "(1 - u) * b > (1 - u) * a"
+        by (auto simp add:field_simps)
+      then have "b \<ge> a"
+        apply (drule_tac mult_less_imp_less_left)
+        using u
+        apply auto
+        done
+      then have "u * a \<le> u * b"
+        apply -
+        apply (rule mult_left_mono[OF _ u(3)])
+        using u(3-4)
+        apply (auto simp add: field_simps)
+        done
+    } note * = this
+    {
+      fix a b
+      assume "u * b > u * a"
+      then have "(1 - u) * a \<le> (1 - u) * b"
+        apply -
+        apply (rule mult_left_mono)
+        apply (drule mult_less_imp_less_left)
+        using u
+        apply auto
+        done
+      then have "a + u * b \<le> b + u * a"
+        by (auto simp add: field_simps)
+    } note ** = this
+    then show ?R
+      unfolding u assms
+      using u
+      by (auto simp add: field_simps not_le intro: * **)
+  }
+  {
+    assume ?R
+    then show ?L
+    proof (cases "x$1 = b$1")
+      case True
+      then show ?L
+        apply (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI)
+        unfolding assms True
+        using `?R`
+        apply (auto simp add: field_simps)
+        done
+    next
+      case False
+      then show ?L
+        apply (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI)
+        unfolding assms
+        using `?R`
+        apply (auto simp add: field_simps)
+        done
+    qed
+  }
+qed
 
-subsection {*useful Fashoda corollary pointed out to me by Tom Hales. *}
+
+subsection {* Useful Fashoda corollary pointed out to me by Tom Hales *}
 
-lemma fashoda_interlace: fixes a::"real^2"
-  assumes "path f" "path g"
-  "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
-  "(pathstart f)$2 = a$2" "(pathfinish f)$2 = a$2"
-  "(pathstart g)$2 = a$2" "(pathfinish g)$2 = a$2"
-  "(pathstart f)$1 < (pathstart g)$1" "(pathstart g)$1 < (pathfinish f)$1"
-  "(pathfinish f)$1 < (pathfinish g)$1"
-  obtains z where "z \<in> path_image f" "z \<in> path_image g"
-proof-
-  have "{a..b} \<noteq> {}" using path_image_nonempty using assms(3) by auto
+lemma fashoda_interlace:
+  fixes a :: "real^2"
+  assumes "path f"
+    and "path g"
+    and "path_image f \<subseteq> {a..b}"
+    and "path_image g \<subseteq> {a..b}"
+    and "(pathstart f)$2 = a$2"
+    and "(pathfinish f)$2 = a$2"
+    and "(pathstart g)$2 = a$2"
+    and "(pathfinish g)$2 = a$2"
+    and "(pathstart f)$1 < (pathstart g)$1"
+    and "(pathstart g)$1 < (pathfinish f)$1"
+    and "(pathfinish f)$1 < (pathfinish g)$1"
+  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
+proof -
+  have "{a..b} \<noteq> {}"
+    using path_image_nonempty using assms(3) by auto
   note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
   have "pathstart f \<in> {a..b}" "pathfinish f \<in> {a..b}" "pathstart g \<in> {a..b}" "pathfinish g \<in> {a..b}"
     using pathstart_in_path_image pathfinish_in_path_image using assms(3-4) by auto
@@ -455,7 +658,7 @@
      linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])"
   let ?a = "vector[a$1 - 2, a$2 - 3]"
   let ?b = "vector[b$1 + 2, b$2 + 3]"
-  have P1P2:"path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
+  have P1P2: "path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
       path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union>
       path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union>
       path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))"
@@ -464,58 +667,111 @@
       path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
       path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
       by(auto simp add: path_image_join path_linepath)
-  have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:less_eq_vec_def forall_2 vector_2)
-  guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
-    unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
-    show "path ?P1" "path ?P2" using assms by auto
-    have "path_image ?P1 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 3
-      apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
-      unfolding mem_interval_cart forall_2 vector_2 using ab startfin abab assms(3)
-      using assms(9-) unfolding assms by(auto simp add:field_simps)
-    thus "path_image ?P1  \<subseteq> {?a .. ?b}" .
-    have "path_image ?P2 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 2
-      apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
-      unfolding mem_interval_cart forall_2 vector_2 using ab startfin abab assms(4)
-      using assms(9-) unfolding assms  by(auto simp add:field_simps)
-    thus "path_image ?P2  \<subseteq> {?a .. ?b}" . 
-    show "a $ 1 - 2 = a $ 1 - 2"  "b $ 1 + 2 = b $ 1 + 2" "pathstart g $ 2 - 3 = a $ 2 - 3"  "b $ 2 + 3 = b $ 2 + 3"
-      by(auto simp add: assms)
+  have abab: "{a..b} \<subseteq> {?a..?b}"
+    by (auto simp add:less_eq_vec_def forall_2 vector_2)
+  guess z
+    apply (rule fashoda[of ?P1 ?P2 ?a ?b])
+    unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
+  proof -
+    show "path ?P1" "path ?P2"
+      using assms by auto
+    have "path_image ?P1 \<subseteq> {?a .. ?b}"
+      unfolding P1P2 path_image_linepath
+      apply (rule Un_least)+
+      defer 3
+      apply (rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
+      unfolding mem_interval_cart forall_2 vector_2
+      using ab startfin abab assms(3)
+      using assms(9-)
+      unfolding assms
+      apply (auto simp add: field_simps)
+      done
+    then show "path_image ?P1  \<subseteq> {?a .. ?b}" .
+    have "path_image ?P2 \<subseteq> {?a .. ?b}"
+      unfolding P1P2 path_image_linepath
+      apply (rule Un_least)+
+      defer 2
+      apply (rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
+      unfolding mem_interval_cart forall_2 vector_2
+      using ab startfin abab assms(4)
+      using assms(9-)
+      unfolding assms
+      apply (auto simp add: field_simps)
+      done
+    then show "path_image ?P2  \<subseteq> {?a .. ?b}" .
+    show "a $ 1 - 2 = a $ 1 - 2"
+      and "b $ 1 + 2 = b $ 1 + 2"
+      and "pathstart g $ 2 - 3 = a $ 2 - 3"
+      and "b $ 2 + 3 = b $ 2 + 3"
+      by (auto simp add: assms)
   qed note z=this[unfolded P1P2 path_image_linepath]
-  show thesis apply(rule that[of z]) proof-
+  show thesis
+    apply (rule that[of z])
+  proof -
     have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
-     z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
-   z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
-  z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
-  (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
-    z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
-   z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
-  z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
-      apply(simp only: segment_vertical segment_horizontal vector_2) proof- case goal1 note as=this
-      have "pathfinish f \<in> {a..b}" using assms(3) pathfinish_in_path_image[of f] by auto 
-      hence "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" unfolding mem_interval_cart forall_2 by auto
-      hence "z$1 \<noteq> pathfinish f$1" using as(2) using assms ab by(auto simp add:field_simps)
-      moreover have "pathstart f \<in> {a..b}" using assms(3) pathstart_in_path_image[of f] by auto 
-      hence "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False" unfolding mem_interval_cart forall_2 by auto
-      hence "z$1 \<noteq> pathstart f$1" using as(2) using assms ab by(auto simp add:field_simps)
-      ultimately have *:"z$2 = a$2 - 2" using goal1(1) by auto
-      have "z$1 \<noteq> pathfinish g$1" using as(2) using assms ab by(auto simp add:field_simps *)
-      moreover have "pathstart g \<in> {a..b}" using assms(4) pathstart_in_path_image[of g] by auto 
+      z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
+      z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
+      z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
+    (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
+      z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
+      z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
+      z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
+      apply (simp only: segment_vertical segment_horizontal vector_2)
+    proof -
+      case goal1 note as=this
+      have "pathfinish f \<in> {a..b}"
+        using assms(3) pathfinish_in_path_image[of f] by auto 
+      hence "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
+        unfolding mem_interval_cart forall_2 by auto
+      then have "z$1 \<noteq> pathfinish f$1"
+        using as(2) using assms ab by (auto simp add: field_simps)
+      moreover have "pathstart f \<in> {a..b}"
+        using assms(3) pathstart_in_path_image[of f] by auto 
+      then have "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False"
+        unfolding mem_interval_cart forall_2 by auto
+      then have "z$1 \<noteq> pathstart f$1"
+        using as(2) using assms ab by (auto simp add: field_simps)
+      ultimately have *: "z$2 = a$2 - 2"
+        using goal1(1) by auto
+      have "z$1 \<noteq> pathfinish g$1"
+        using as(2) using assms ab by (auto simp add: field_simps *)
+      moreover have "pathstart g \<in> {a..b}"
+        using assms(4) pathstart_in_path_image[of g] by auto 
       note this[unfolded mem_interval_cart forall_2]
-      hence "z$1 \<noteq> pathstart g$1" using as(1) using assms ab by(auto simp add:field_simps *)
+      then have "z$1 \<noteq> pathstart g$1"
+        using as(1) using assms ab by (auto simp add: field_simps *)
       ultimately have "a $ 2 - 1 \<le> z $ 2 \<and> z $ 2 \<le> b $ 2 + 3 \<or> b $ 2 + 3 \<le> z $ 2 \<and> z $ 2 \<le> a $ 2 - 1"
-        using as(2) unfolding * assms by(auto simp add:field_simps)
-      thus False unfolding * using ab by auto
-    qed hence "z \<in> path_image f \<or> z \<in> path_image g" using z unfolding Un_iff by blast
-    hence z':"z\<in>{a..b}" using assms(3-4) by auto
-    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow> (z = pathstart f \<or> z = pathfinish f)"
+        using as(2) unfolding * assms by (auto simp add: field_simps)
+      then show False
+        unfolding * using ab by auto
+    qed
+    then have "z \<in> path_image f \<or> z \<in> path_image g"
+      using z unfolding Un_iff by blast
+    then have z': "z \<in> {a..b}"
+      using assms(3-4) by auto
+    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow>
+      z = pathstart f \<or> z = pathfinish f"
       unfolding vec_eq_iff forall_2 assms by auto
-    with z' show "z\<in>path_image f" using z(1) unfolding Un_iff mem_interval_cart forall_2 apply-
-      apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
-    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow> (z = pathstart g \<or> z = pathfinish g)"
+    with z' show "z \<in> path_image f"
+      using z(1)
+      unfolding Un_iff mem_interval_cart forall_2
+      apply -
+      apply (simp only: segment_vertical segment_horizontal vector_2)
+      unfolding assms
+      apply auto
+      done
+    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow>
+      z = pathstart g \<or> z = pathfinish g"
       unfolding vec_eq_iff forall_2 assms by auto
-    with z' show "z\<in>path_image g" using z(2) unfolding Un_iff mem_interval_cart forall_2 apply-
-      apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
-  qed qed
+    with z' show "z \<in> path_image g"
+      using z(2)
+      unfolding Un_iff mem_interval_cart forall_2
+      apply (simp only: segment_vertical segment_horizontal vector_2)
+      unfolding assms
+      apply auto
+      done
+  qed
+qed
 
 (** The Following still needs to be translated. Maybe I will do that later.