# HG changeset patch
# User wenzelm
# Date 1393103170 -3600
# Node ID ccbf1722ae32a8ef79a7e764818a0cfe35abb082
# Parent  8a213ab0e78a8165f453b091c82a0d5c1fb5b48c
tuned proofs;

diff -r 8a213ab0e78a -r ccbf1722ae32 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sat Feb 22 21:38:26 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sat Feb 22 22:06:10 2014 +0100
@@ -72,7 +72,10 @@
   {
     fix x
     assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
-    then guess w unfolding image_iff .. note w = this
+    then obtain w :: "real^2" where w:
+        "w \<in> {- 1..1}"
+        "x = (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w"
+      unfolding image_iff ..
     then have "x \<noteq> 0"
       using as[of "w$1" "w$2"]
       unfolding mem_interval_cart
@@ -114,7 +117,10 @@
     apply rule
   proof -
     case goal1
-    then guess y unfolding image_iff .. note y=this
+    then obtain y :: "real^2" where y:
+        "y \<in> {- 1..1}"
+        "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y"
+      unfolding image_iff ..
     have "?F y \<noteq> 0"
       apply (rule x0)
       using y(1)
@@ -140,12 +146,15 @@
         done
     qed
   qed
-  guess x
+  obtain x :: "real^2" where x:
+      "x \<in> {- 1..1}"
+      "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
     apply (rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"])
-    apply (rule compact_interval convex_interval)+ unfolding interior_closed_interval
+    apply (rule compact_interval convex_interval)+
+    unfolding interior_closed_interval
     apply (rule 1 2 3)+
+    apply blast
     done
-  note x=this
   have "?F x \<noteq> 0"
     apply (rule x0)
     using x(1)
@@ -312,10 +321,14 @@
       using assms
       by (auto simp add: *)
   qed
-  then guess s .. from this(2) guess t .. note st=this
+  then obtain s t where st:
+      "s \<in> {- 1..1}"
+      "t \<in> {- 1..1}"
+      "(f \<circ> iscale) s = (g \<circ> iscale) t"
+    by blast
   show thesis
     apply (rule_tac z = "f (iscale s)" in that)
-    using st `s \<in> {- 1..1}`
+    using st
     unfolding o_def path_image_def image_iff
     apply -
     apply (rule_tac x="iscale s" in bexI)
@@ -360,7 +373,7 @@
     unfolding pathstart_def
     apply (auto simp add: less_eq_vec_def)
     done
-  then guess z .. note z=this
+  then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" ..
   have "z \<in> {a..b}"
     using z(1) assms(4)
     unfolding path_image_def
@@ -392,7 +405,7 @@
     unfolding pathstart_def
     apply (auto simp add: less_eq_vec_def)
     done
-  then guess z .. note z=this
+  then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" ..
   have "z \<in> {a..b}"
     using z(1) assms(3)
     unfolding path_image_def
@@ -416,7 +429,9 @@
   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
+  obtain z :: "real^2" where z:
+      "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
+      "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
     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)
@@ -426,8 +441,10 @@
   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
+    then obtain y where y:
+        "y \<in> {0..1}"
+        "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
+      unfolding image_iff ..
     show "x \<in> {- 1..1}"
       unfolding y o_def
       apply (rule in_interval_interval_bij)
@@ -438,7 +455,10 @@
   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
+    then obtain y where y:
+        "y \<in> {0..1}"
+        "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
+      unfolding image_iff ..
     show "x \<in> {- 1..1}"
       unfolding y o_def
       apply (rule in_interval_interval_bij)
@@ -455,9 +475,14 @@
       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
-  from z(1) guess zf unfolding image_iff .. note zf=this
-  from z(2) guess zg unfolding image_iff .. note zg=this
+  from z(1) obtain zf where zf:
+      "zf \<in> {0..1}"
+      "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf"
+    unfolding image_iff ..
+  from z(2) obtain zg where zg:
+      "zg \<in> {0..1}"
+      "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
+    unfolding image_iff ..
   have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i"
     unfolding forall_2
     using as
@@ -493,7 +518,12 @@
   }
   {
     assume ?L
-    then guess u by (elim exE conjE) note u=this
+    then obtain u where u:
+        "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
+        "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
+        "0 \<le> u"
+        "u \<le> 1"
+      by blast
     { fix b a
       assume "b + u * a > a + u * b"
       then have "(1 - u) * b > (1 - u) * a"
@@ -568,7 +598,12 @@
   }
   {
     assume ?L
-    then guess u by (elim exE conjE) note u=this
+    then obtain u where u:
+        "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
+        "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
+        "0 \<le> u"
+        "u \<le> 1"
+      by blast
     {
       fix b a
       assume "b + u * a > a + u * b"
@@ -677,7 +712,19 @@
       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
+  obtain z where
+    "z \<in> path_image
+          (linepath (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) +++
+           linepath (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f) +++
+           f +++
+           linepath (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) +++
+           linepath (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]))"
+    "z \<in> path_image
+          (linepath (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g) +++
+           g +++
+           linepath (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1]) +++
+           linepath (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1]) +++
+           linepath (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]))"
     apply (rule fashoda[of ?P1 ?P2 ?a ?b])
     unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
   proof -