diff -r e58ca0311c0f -r e7b77b217491 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Wed Sep 11 20:16:28 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Wed Sep 11 20:34:45 2013 +0200
@@ -1,7 +1,8 @@
-(* Author:                     John Harrison
-   Translation from HOL light: Robert Himmelmann, TU Muenchen *)
+(*  Author:     John Harrison
+    Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
+*)
 
-header {* Fashoda meet theorem. *}
+header {* Fashoda meet theorem *}
 
 theory Fashoda
 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
@@ -15,131 +16,312 @@
 lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
   by (auto simp add: Basis_vec_def axis_eq_axis)
 
-subsection {*Fashoda meet theorem. *}
+
+subsection {* Fashoda meet theorem *}
 
-lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))"
-  unfolding infnorm_cart UNIV_2 apply(rule cSup_eq) by auto
+lemma infnorm_2:
+  fixes x :: "real^2"
+  shows "infnorm x = max (abs (x$1)) (abs (x$2))"
+  unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto
 
-lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow>
-        (abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1))"
+lemma infnorm_eq_1_2:
+  fixes x :: "real^2"
+  shows "infnorm x = 1 \<longleftrightarrow>
+    abs (x$1) \<le> 1 \<and> abs (x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)"
   unfolding infnorm_2 by auto
 
-lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1"
+lemma infnorm_eq_1_imp:
+  fixes x :: "real^2"
+  assumes "infnorm x = 1"
+  shows "abs (x$1) \<le> 1" and "abs (x$2) \<le> 1"
   using assms unfolding infnorm_eq_1_2 by auto
 
-lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2"
-  assumes "f ` {- 1..1} \<subseteq> {- 1..1}" "g ` {- 1..1} \<subseteq> {- 1..1}"
-  "continuous_on {- 1..1} f"  "continuous_on {- 1..1} g"
-  "f (- 1)$1 = - 1" "f 1$1 = 1" "g (- 1) $2 = -1" "g 1 $2 = 1"
-  shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t" proof(rule ccontr)
-  case goal1 note as = this[unfolded bex_simps,rule_format]
+lemma fashoda_unit:
+  fixes f g :: "real \<Rightarrow> real^2"
+  assumes "f ` {- 1..1} \<subseteq> {- 1..1}"
+    and "g ` {- 1..1} \<subseteq> {- 1..1}"
+    and "continuous_on {- 1..1} f"
+    and "continuous_on {- 1..1} g"
+    and "f (- 1)$1 = - 1"
+    and "f 1$1 = 1" "g (- 1) $2 = -1"
+    and "g 1 $2 = 1"
+  shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t"
+proof (rule ccontr)
+  assume "\<not> ?thesis"
+  note as = this[unfolded bex_simps,rule_format]
   def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z" 
-  def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2" 
-  have lem1:"\<forall>z::real^2. infnorm(negatex z) = infnorm z"
+  def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2"
+  have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z"
     unfolding negatex_def infnorm_2 vector_2 by auto
-  have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def
-    unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR] unfolding abs_inverse real_abs_infnorm
-    apply(subst infnorm_eq_0[THEN sym]) by auto
-  let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)"
-  have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
-    apply(rule set_eqI) unfolding image_iff Bex_def mem_interval_cart apply rule defer 
-    apply(rule_tac x="vec x" in exI) by auto
-  { 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}"
+  have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1"
+    unfolding sqprojection_def
+    unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR]
+    unfolding abs_inverse real_abs_infnorm
+    apply (subst infnorm_eq_0[THEN sym])
+    apply auto
+    done
+  let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
+  have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
+    apply (rule set_eqI)
+    unfolding image_iff Bex_def mem_interval_cart
+    apply rule
+    defer
+    apply (rule_tac x="vec x" in exI)
+    apply auto
+    done
+  {
+    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
-    hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval_cart by auto} note x0=this
-  have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto
-  have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto
-  have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
-    apply(intro continuous_on_intros continuous_on_component)
-    unfolding * apply(rule assms)+
-    apply(subst sqprojection_def)
-    apply(intro continuous_on_intros)
-    apply(simp add: infnorm_eq_0 x0)
-    apply(rule linear_continuous_on)
-  proof-
-    show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
-      show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
-        apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21) 
-        unfolding negatex_def by(auto simp add:vector_2 ) qed
+    then have "x \<noteq> 0"
+      using as[of "w$1" "w$2"]
+      unfolding mem_interval_cart
+      by auto
+  } note x0 = this
+  have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
+    using UNIV_2 by auto
+  have 1: "{- 1<..<1::real^2} \<noteq> {}"
+    unfolding interval_eq_empty_cart by auto
+  have 2: "continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
+    apply (intro continuous_on_intros continuous_on_component)
+    unfolding *
+    apply (rule assms)+
+    apply (subst sqprojection_def)
+    apply (intro continuous_on_intros)
+    apply (simp add: infnorm_eq_0 x0)
+    apply (rule linear_continuous_on)
+  proof -
+    show "bounded_linear negatex"
+      apply (rule bounded_linearI')
+      unfolding vec_eq_iff
+    proof (rule_tac[!] allI)
+      fix i :: 2
+      fix x y :: "real^2"
+      fix c :: real
+      show "negatex (x + y) $ i =
+        (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
+        apply -
+        apply (case_tac[!] "i\<noteq>1")
+        prefer 3
+        apply (drule_tac[1-2] 21) 
+        unfolding negatex_def
+        apply (auto simp add:vector_2)
+        done
+    qed
   qed
-  have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof-
-    case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto
-    hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format])
-    have "infnorm x = 1" unfolding *[THEN sym] y o_def by(rule lem1[rule_format])
-    thus "x\<in>{- 1..1}" unfolding mem_interval_cart infnorm_2 apply- apply rule
-    proof-case goal1 thus ?case apply(cases "i=1") defer apply(drule 21) by auto qed qed
-  guess 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 1 2 3)+ . note x=this
-  have "?F x \<noteq> 0" apply(rule x0) using x(1) by auto
-  hence *:"infnorm (sqprojection (?F x)) = 1" unfolding o_def by(rule lem2[rule_format])
-  have nx:"infnorm x = 1" apply(subst x(2)[THEN sym]) unfolding *[THEN sym] o_def by(rule lem1[rule_format])
-  have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"    "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
-    apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
-    have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
-    thus "(0 < sqprojection x $ i) = (0 < x $ i)"   "(sqprojection x $ i < 0) = (x $ i < 0)"
+  have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}"
+    unfolding subset_eq
+    apply rule
+  proof -
+    case goal1
+    then guess y unfolding image_iff .. note y=this
+    have "?F y \<noteq> 0"
+      apply (rule x0)
+      using y(1)
+      apply auto
+      done
+    then have *: "infnorm (sqprojection (?F y)) = 1"
+      unfolding y o_def by - (rule lem2[rule_format])
+    have "infnorm x = 1"
+      unfolding *[THEN sym] y o_def by (rule lem1[rule_format])
+    then show "x \<in> {- 1..1}"
+      unfolding mem_interval_cart infnorm_2
+      apply -
+      apply rule
+    proof -
+      case goal1
+      then show ?case
+        apply (cases "i = 1")
+        defer
+        apply (drule 21)
+        apply auto
+        done
+    qed
+  qed
+  guess 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 1 2 3)+
+    done
+  note x=this
+  have "?F x \<noteq> 0"
+    apply (rule x0)
+    using x(1)
+    apply auto
+    done
+  then have *: "infnorm (sqprojection (?F x)) = 1"
+    unfolding o_def by (rule lem2[rule_format])
+  have nx: "infnorm x = 1"
+    apply (subst x(2)[THEN sym])
+    unfolding *[THEN sym] o_def
+    apply (rule lem1[rule_format])
+    done
+  have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"
+    and "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
+    apply -
+    apply (rule_tac[!] allI impI)+
+  proof -
+    fix x :: "real^2"
+    fix i :: 2
+    assume x: "x \<noteq> 0"
+    have "inverse (infnorm x) > 0"
+      using x[unfolded infnorm_pos_lt[THEN sym]] by auto
+    then show "(0 < sqprojection x $ i) = (0 < x $ i)"
+      and "(sqprojection x $ i < 0) = (x $ i < 0)"
       unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
-      unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
+      unfolding zero_less_mult_iff mult_less_0_iff
+      by (auto simp add: field_simps)
+  qed
   note lem3 = this[rule_format]
-  have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto
-  hence nz:"f (x $ 1) - g (x $ 2) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto
-  have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto 
-  thus False proof- fix P Q R S 
-    presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto
-  next assume as:"x$1 = 1"
-    hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto
+  have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
+    using x(1) unfolding mem_interval_cart by auto
+  then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0"
+    unfolding right_minus_eq
+    apply -
+    apply (rule as)
+    apply auto
+    done
+  have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1"
+    using nx unfolding infnorm_eq_1_2 by auto 
+  then show False
+  proof -
+    fix P Q R S 
+    presume "P \<or> Q \<or> R \<or> S"
+      and "P \<Longrightarrow> False"
+      and "Q \<Longrightarrow> False"
+      and "R \<Longrightarrow> False"
+      and "S \<Longrightarrow> False"
+    then show False by auto
+  next
+    assume as: "x$1 = 1"
+    then have *: "f (x $ 1) $ 1 = 1"
+      using assms(6) by auto
     have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
-      apply(erule_tac x=1 in allE) by auto 
-  next assume as:"x$1 = -1"
-    hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto
+      unfolding as negatex_def vector_2
+      by auto
+    moreover
+    from x1 have "g (x $ 2) \<in> {- 1..1}"
+      apply -
+      apply (rule assms(2)[unfolded subset_eq,rule_format])
+      apply auto
+      done
+    ultimately show False
+      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
+      apply (erule_tac x=1 in allE)
+      apply auto
+      done
+  next
+    assume as: "x$1 = -1"
+    then have *: "f (x $ 1) $ 1 = - 1"
+      using assms(5) by auto
     have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
-      apply(erule_tac x=1 in allE) by auto
-  next assume as:"x$2 = 1"
-    hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto
+      unfolding as negatex_def vector_2
+      by auto
+    moreover
+    from x1 have "g (x $ 2) \<in> {- 1..1}"
+      apply -
+      apply (rule assms(2)[unfolded subset_eq,rule_format])
+      apply auto
+      done
+    ultimately show False
+      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
+      apply (erule_tac x=1 in allE)
+      apply auto
+      done
+  next
+    assume as: "x$2 = 1"
+    then have *: "g (x $ 2) $ 2 = 1"
+      using assms(8) by auto
     have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
-     apply(erule_tac x=2 in allE) by auto
- next assume as:"x$2 = -1"
-    hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto
+      unfolding as negatex_def vector_2
+      by auto
+    moreover
+    from x1 have "f (x $ 1) \<in> {- 1..1}"
+      apply -
+      apply (rule assms(1)[unfolded subset_eq,rule_format])
+      apply auto
+      done
+    ultimately show False
+      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+      apply (erule_tac x=2 in allE)
+      apply auto
+      done
+  next
+    assume as: "x$2 = -1"
+    then have *: "g (x $ 2) $ 2 = - 1"
+      using assms(7) by auto
     have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
-      apply(erule_tac x=2 in allE) by auto qed(auto) qed
+      unfolding as negatex_def vector_2
+      by auto
+    moreover
+    from x1 have "f (x $ 1) \<in> {- 1..1}"
+      apply -
+      apply (rule assms(1)[unfolded subset_eq,rule_format])
+      apply auto
+      done
+    ultimately show False
+      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+      apply (erule_tac x=2 in allE)
+      apply auto
+      done
+  qed auto
+qed
 
-lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2"
-  assumes "path f" "path g" "path_image f \<subseteq> {- 1..1}" "path_image g \<subseteq> {- 1..1}"
-  "(pathstart f)$1 = -1" "(pathfinish f)$1 = 1"  "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1"
-  obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
+lemma fashoda_unit_path:
+  fixes f g :: "real \<Rightarrow> real^2"
+  assumes "path f"
+    and "path g"
+    and "path_image f \<subseteq> {- 1..1}"
+    and "path_image g \<subseteq> {- 1..1}"
+    and "(pathstart f)$1 = -1"
+    and "(pathfinish f)$1 = 1"
+    and "(pathstart g)$2 = -1"
+    and "(pathfinish g)$2 = 1"
+  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
+proof -
   note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
   def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)"
-  have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto)
-  have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit) 
+  have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
+    unfolding iscale_def by auto
+  have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
+  proof (rule fashoda_unit)
     show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
       using isc and assms(3-4) unfolding image_compose by auto
-    have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+
+    have *: "continuous_on {- 1..1} iscale"
+      unfolding iscale_def by (rule continuous_on_intros)+
     show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
-      apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc])
-      by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding vec_eq_iff by auto
-    show "(f \<circ> iscale) (- 1) $ 1 = - 1" "(f \<circ> iscale) 1 $ 1 = 1" "(g \<circ> iscale) (- 1) $ 2 = -1" "(g \<circ> iscale) 1 $ 2 = 1"
-      unfolding o_def iscale_def using assms by(auto simp add:*) qed
+      apply -
+      apply (rule_tac[!] continuous_on_compose[OF *])
+      apply (rule_tac[!] continuous_on_subset[OF _ isc])
+      apply (rule assms)+
+      done
+    have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
+      unfolding vec_eq_iff by auto
+    show "(f \<circ> iscale) (- 1) $ 1 = - 1"
+      and "(f \<circ> iscale) 1 $ 1 = 1"
+      and "(g \<circ> iscale) (- 1) $ 2 = -1"
+      and "(g \<circ> iscale) 1 $ 2 = 1"
+      unfolding o_def iscale_def
+      using assms
+      by (auto simp add: *)
+  qed
   then guess s .. from this(2) guess t .. note st=this
-  show thesis apply(rule_tac z="f (iscale s)" in that)
-    using st `s\<in>{- 1..1}` unfolding o_def path_image_def image_iff apply-
-    apply(rule_tac x="iscale s" in bexI) prefer 3 apply(rule_tac x="iscale t" in bexI)
-    using isc[unfolded subset_eq, rule_format] by auto qed
+  show thesis
+    apply (rule_tac z="f (iscale s)" in that)
+    using st `s\<in>{- 1..1}`
+    unfolding o_def path_image_def image_iff
+    apply -
+    apply (rule_tac x="iscale s" in bexI)
+    prefer 3
+    apply (rule_tac x="iscale t" in bexI)
+    using isc[unfolded subset_eq, rule_format]
+    apply auto
+    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}"