# HG changeset patch
# User wenzelm
# Date 1300051450 -3600
# Node ID 5abc60a017e08c1c50fd88806b2e6099e8ec49c0
# Parent  d488ae70366d6fd9ea3855b3bcc88a0931e25b93
eliminated hard tabs;

diff -r d488ae70366d -r 5abc60a017e0 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Mar 13 21:41:44 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Mar 13 22:24:10 2011 +0100
@@ -145,7 +145,7 @@
     have inj:"inj_on f (s - {z})" apply(rule eq_card_imp_inj_on) unfolding as using as(1) and assms by auto
     show "z = a \<or> z = c" proof(rule ccontr)
       assume "\<not> (z = a \<or> z = c)" thus False using inj[unfolded inj_on_def,THEN bspec[where x=a],THEN bspec[where x=c]]
-	using `a\<in>s` `c\<in>s` `f a = f c` `a\<noteq>c` by auto qed qed qed
+        using `a\<in>s` `c\<in>s` `f a = f c` `a\<noteq>c` by auto qed qed qed
 
 subsection {* Combine this with the basic counting lemma. *}
 
@@ -195,12 +195,12 @@
       using as(5)[rule_format,OF a(1) insertI1] apply- proof(erule disjE)
       assume "\<forall>j. a j \<le> x j" thus ?thesis apply(rule_tac x=a in bexI) using a by auto next
       assume "\<forall>j. x j \<le> a j" thus ?thesis apply(rule_tac x=x in bexI) apply(rule,rule) using a apply -
-	apply(erule_tac x=xa in ballE) apply(erule_tac x=j in allE)+ by auto qed moreover
+        apply(erule_tac x=xa in ballE) apply(erule_tac x=j in allE)+ by auto qed moreover
     have "\<exists>b\<in>insert x F. \<forall>x\<in>insert x F. \<forall>j. x j \<le> b j"
       using as(5)[rule_format,OF b(1) insertI1] apply- proof(erule disjE)
       assume "\<forall>j. x j \<le> b j" thus ?thesis apply(rule_tac x=b in bexI) using b by auto next
       assume "\<forall>j. b j \<le> x j" thus ?thesis apply(rule_tac x=x in bexI) apply(rule,rule) using b apply -
-	apply(erule_tac x=xa in ballE) apply(erule_tac x=j in allE)+ by auto qed
+        apply(erule_tac x=xa in ballE) apply(erule_tac x=j in allE)+ by auto qed
     ultimately show  ?thesis by auto qed qed(auto)
 
 lemma kle_imp_pointwise: "kle n x y \<Longrightarrow> (\<forall>j. x j \<le> y j)" unfolding kle_def by auto
@@ -231,7 +231,7 @@
   then guess a .. note a=this show ?thesis apply(rule_tac x=a in bexI) proof fix x assume "x\<in>s"
     show "kle n a x" using assms(3)[rule_format,OF a(1) `x\<in>s`] apply- proof(erule disjE)
       assume "kle n x a" hence "x = a" apply- unfolding pointwise_antisym[THEN sym]
-	apply(drule kle_imp_pointwise) using a(2)[rule_format,OF `x\<in>s`] by auto
+        apply(drule kle_imp_pointwise) using a(2)[rule_format,OF `x\<in>s`] by auto
       thus ?thesis using kle_refl by auto  qed qed(insert a, auto) qed
 
 lemma kle_maximal: assumes "finite s" "s \<noteq> {}" "\<forall>x\<in>s. \<forall>y\<in>s. kle n x y \<or> kle n y x"
@@ -241,7 +241,7 @@
   then guess a .. note a=this show ?thesis apply(rule_tac x=a in bexI) proof fix x assume "x\<in>s"
     show "kle n x a" using assms(3)[rule_format,OF a(1) `x\<in>s`] apply- proof(erule disjE)
       assume "kle n a x" hence "x = a" apply- unfolding pointwise_antisym[THEN sym]
-	apply(drule kle_imp_pointwise) using a(2)[rule_format,OF `x\<in>s`] by auto
+        apply(drule kle_imp_pointwise) using a(2)[rule_format,OF `x\<in>s`] by auto
       thus ?thesis using kle_refl by auto  qed qed(insert a, auto) qed
 
 lemma kle_strict_set: assumes "kle n x y" "x \<noteq> y"
@@ -315,7 +315,7 @@
   show ?thesis unfolding kle_def apply(rule_tac x="kk1 \<union> kk2" in exI) apply(rule) defer proof
     fix i show "c i = a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)" proof(cases "i\<in>kk1 \<union> kk2")
       case True hence "c i \<ge> a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)"
-	unfolding kk1[THEN conjunct2,rule_format,of i] kk2[THEN conjunct2,rule_format,of i] by auto
+        unfolding kk1[THEN conjunct2,rule_format,of i] kk2[THEN conjunct2,rule_format,of i] by auto
       moreover have "c i \<le> a i + (if i \<in> kk1 \<union> kk2 then 1 else 0)" using True assms(3) by auto  
       ultimately show ?thesis by auto next
       case False thus ?thesis using kk1 kk2 by auto qed qed(insert kk1 kk2, auto) qed
@@ -508,8 +508,8 @@
     case goal1 note as = this(1,4-)[unfolded goal1 split_conv]
     have "xa = xb" using as(1)[THEN cong[of _ _ a]] by auto
     moreover have "ya = yb" proof(rule ext) fix x show "ya x = yb x" proof(cases "x = a") 
-	case False thus ?thesis using as(1)[THEN cong[of _ _ x x]] by auto next
-	case True thus ?thesis using as(5,7) using as0(2) by auto qed qed 
+        case False thus ?thesis using as(1)[THEN cong[of _ _ x x]] by auto next
+        case True thus ?thesis using as(5,7) using as0(2) by auto qed qed 
     ultimately show ?case unfolding goal1 by auto qed
   have "finite s0" using `finite s` unfolding as0 by simp
   show ?case unfolding as0 * card_image[OF inj] using assms
@@ -549,19 +549,19 @@
   assume ?ls then guess s .. then guess a apply-apply(erule exE,(erule conjE)+) . note sa=this
   show ?rs unfolding ksimplex_def sa(3) apply(rule) defer apply rule defer apply(rule,rule,rule,rule) defer apply(rule,rule) proof-
     fix x y assume as:"x \<in>s - {a}" "y \<in>s - {a}" have xyp:"x (n + 1) = y (n + 1)"
-	using as(1)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]]
-	using as(2)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]] by auto
+        using as(1)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]]
+        using as(2)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]] by auto
     show "kle n x y \<or> kle n y x" proof(cases "kle (n + 1) x y")
       case True then guess k unfolding kle_def .. note k=this hence *:"n+1 \<notin> k" using xyp by auto
       have "\<not> (\<exists>x\<in>k. x\<notin>{1..n})" apply(rule ccontr) unfolding not_not apply(erule bexE) proof-
-	fix x assume as:"x \<in> k" "x \<notin> {1..n}" have "x \<noteq> n+1" using as and * by auto
-	thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed
+        fix x assume as:"x \<in> k" "x \<notin> {1..n}" have "x \<noteq> n+1" using as and * by auto
+        thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed
       thus ?thesis apply-apply(rule disjI1) unfolding kle_def using k apply(rule_tac x=k in exI) by auto next
       case False hence "kle (n + 1) y x" using ksimplexD(6)[OF sa(1),rule_format, of x y] using as by auto
       then guess k unfolding kle_def .. note k=this hence *:"n+1 \<notin> k" using xyp by auto
       hence "\<not> (\<exists>x\<in>k. x\<notin>{1..n})" apply-apply(rule ccontr) unfolding not_not apply(erule bexE) proof-
-	fix x assume as:"x \<in> k" "x \<notin> {1..n}" have "x \<noteq> n+1" using as and * by auto
-	thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed
+        fix x assume as:"x \<in> k" "x \<notin> {1..n}" have "x \<noteq> n+1" using as and * by auto
+        thus False using as and k[THEN conjunct1,unfolded subset_eq] by auto qed
       thus ?thesis apply-apply(rule disjI2) unfolding kle_def using k apply(rule_tac x=k in exI) by auto qed next
     fix x j assume as:"x\<in>s - {a}" "j\<notin>{1..n}"
     thus "x j = p" using as(1)[unfolded sa(3)[THEN sym], THEN assms(2)[rule_format]]
@@ -577,10 +577,10 @@
     qed(insert x rs(4), auto simp add:c_def)
     show "j \<notin> {1..n + 1} \<longrightarrow> x j = p" apply(cases "x=c") using x ab(1) rs(5) unfolding c_def by auto
     { fix z assume z:"z \<in> insert c f" hence "kle (n + 1) c z" apply(cases "z = c") (*defer apply(rule kle_Suc)*) proof-
-	case False hence "z\<in>f" using z by auto
-	then guess k apply(drule_tac ab(3)[THEN bspec[where x=z], THEN conjunct1]) unfolding kle_def apply(erule exE) .
-	thus "kle (n + 1) c z" unfolding kle_def apply(rule_tac x="insert (n + 1) k" in exI) unfolding c_def
-	  using ab using rs(5)[rule_format,OF ab(1),of "n + 1"] assms(1) by auto qed auto } note * = this
+        case False hence "z\<in>f" using z by auto
+        then guess k apply(drule_tac ab(3)[THEN bspec[where x=z], THEN conjunct1]) unfolding kle_def apply(erule exE) .
+        thus "kle (n + 1) c z" unfolding kle_def apply(rule_tac x="insert (n + 1) k" in exI) unfolding c_def
+          using ab using rs(5)[rule_format,OF ab(1),of "n + 1"] assms(1) by auto qed auto } note * = this
     fix y assume y:"y \<in> insert c f" show "kle (n + 1) x y \<or> kle (n + 1) y x" proof(cases "x = c \<or> y = c")
       case False hence **:"x\<in>f" "y\<in>f" using x y by auto
       show ?thesis using rs(6)[rule_format,OF **] by(auto dest: kle_Suc) qed(insert * x y, auto)
@@ -635,7 +635,7 @@
     have a':"a' = b0" apply(rule ksimplex_fix_plane_p[OF goal1(1-2) assms(4), of _ b1]) unfolding goal1 extb using extb(1,2) assms(5) by auto
     moreover have *:"b1 = a1" unfolding kle_antisym[THEN sym, of b1 a1 n] using exta extb using goal1(3) unfolding a a' by blast moreover
     have "a0 = b0" apply(rule ext) proof- case goal1 show "a0 x = b0 x"
-	using *[THEN cong, of x x] unfolding exta extb apply-apply(cases "x\<in>{1..n}") by auto qed
+        using *[THEN cong, of x x] unfolding exta extb apply-apply(cases "x\<in>{1..n}") by auto qed
     ultimately show "s' = s" apply-apply(rule lem[OF goal1(3) _ goal1(2) assms(2)]) by auto qed 
   show ?thesis unfolding card_1_exists apply(rule ex1I[of _ s]) unfolding mem_Collect_eq apply(rule,rule assms(1))
     apply(rule_tac x=a in bexI) prefer 3 apply(erule conjE bexE)+ apply(rule_tac a'=b in lem) using assms(1-2) by auto qed
@@ -672,38 +672,38 @@
         using `a3\<noteq>a0` `a3\<notin>s` `a0\<in>s` by(auto simp add:card_insert_if)
       fix x assume x:"x \<in> insert a3 (s - {a0})"
       show "\<forall>j. x j \<le> p" proof(rule,cases "x = a3")
-	fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
-	fix j case True show "x j\<le>p" unfolding True proof(cases "j=k") 
-	  case False thus "a3 j \<le>p" unfolding True a3_def using `a1\<in>s` ksimplexD(4)[OF assms(1)] by auto next
-	  guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. note a4=this
-	  have "a2 k \<le> a4 k" using lem3[OF a4(1)[unfolded `a=a0`],THEN kle_imp_pointwise] by auto
-	  also have "\<dots> < p" using ksimplexD(4)[OF assms(1),rule_format,of a4 k] using a4 by auto
-	  finally have *:"a0 k + 1 < p" unfolding k(2)[rule_format] by auto
-	  case True thus "a3 j \<le>p" unfolding a3_def unfolding a0a1(5)[rule_format]
-	    using k(1) k(2)assms(5) using * by simp qed qed
+        fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
+        fix j case True show "x j\<le>p" unfolding True proof(cases "j=k") 
+          case False thus "a3 j \<le>p" unfolding True a3_def using `a1\<in>s` ksimplexD(4)[OF assms(1)] by auto next
+          guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. note a4=this
+          have "a2 k \<le> a4 k" using lem3[OF a4(1)[unfolded `a=a0`],THEN kle_imp_pointwise] by auto
+          also have "\<dots> < p" using ksimplexD(4)[OF assms(1),rule_format,of a4 k] using a4 by auto
+          finally have *:"a0 k + 1 < p" unfolding k(2)[rule_format] by auto
+          case True thus "a3 j \<le>p" unfolding a3_def unfolding a0a1(5)[rule_format]
+            using k(1) k(2)assms(5) using * by simp qed qed
       show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a3") fix j::nat assume j:"j\<notin>{1..n}"
-	{ case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }
-	case True show "x j = p" unfolding True a3_def using j k(1) 
-	  using ksimplexD(5)[OF assms(1),rule_format,OF `a1\<in>s` j] by auto qed
+        { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }
+        case True show "x j = p" unfolding True a3_def using j k(1) 
+          using ksimplexD(5)[OF assms(1),rule_format,OF `a1\<in>s` j] by auto qed
       fix y assume y:"y\<in>insert a3 (s - {a0})"
       have lem4:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a0 \<Longrightarrow> kle n x a3" proof- case goal1
-	guess kk using a0a1(4)[rule_format,OF `x\<in>s`,THEN conjunct2,unfolded kle_def] 
+        guess kk using a0a1(4)[rule_format,OF `x\<in>s`,THEN conjunct2,unfolded kle_def] 
           apply-apply(erule exE,erule conjE) . note kk=this
-	have "k\<notin>kk" proof assume "k\<in>kk"
-	  hence "a1 k = x k + 1" using kk by auto
-	  hence "a0 k = x k" unfolding a0a1(5)[rule_format] using k(1) by auto
-	  hence "a2 k = x k + 1" unfolding k(2)[rule_format] by auto moreover
-	  have "a2 k \<le> x k" using lem3[of x,THEN kle_imp_pointwise] goal1 by auto 
-	  ultimately show False by auto qed
-	thus ?case unfolding kle_def apply(rule_tac x="insert k kk" in exI) using kk(1)
-	  unfolding a3_def kle_def kk(2)[rule_format] using k(1) by auto qed
+        have "k\<notin>kk" proof assume "k\<in>kk"
+          hence "a1 k = x k + 1" using kk by auto
+          hence "a0 k = x k" unfolding a0a1(5)[rule_format] using k(1) by auto
+          hence "a2 k = x k + 1" unfolding k(2)[rule_format] by auto moreover
+          have "a2 k \<le> x k" using lem3[of x,THEN kle_imp_pointwise] goal1 by auto 
+          ultimately show False by auto qed
+        thus ?case unfolding kle_def apply(rule_tac x="insert k kk" in exI) using kk(1)
+          unfolding a3_def kle_def kk(2)[rule_format] using k(1) by auto qed
       show "kle n x y \<or> kle n y x" proof(cases "y=a3")
-	case True show ?thesis unfolding True apply(cases "x=a3") defer apply(rule disjI1,rule lem4)
-	  using x by auto next
-	case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True
-	    apply(rule disjI2,rule lem4) using y False by auto next
-	  case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 
-	    using x y `y\<noteq>a3` by auto qed qed qed
+        case True show ?thesis unfolding True apply(cases "x=a3") defer apply(rule disjI1,rule lem4)
+          using x by auto next
+        case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True
+            apply(rule disjI2,rule lem4) using y False by auto next
+          case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 
+            using x y `y\<noteq>a3` by auto qed qed qed
     hence "insert a3 (s - {a0}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)
       apply(rule_tac x="a3" in bexI) unfolding `a=a0` using `a3\<notin>s` by auto moreover
     have "s \<in> ?A" using assms(1,2) by auto ultimately have  "?A \<supseteq> {s, insert a3 (s - {a0})}" by auto
@@ -712,40 +712,40 @@
       from this(2) guess a' .. note a'=this
       guess a_min a_max apply(rule ksimplex_extrema_strong[OF as assms(3)]) . note min_max=this
       have *:"\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\<in>s-{a}"
-	hence "kle n a2 x" apply-apply(rule lem3) using `a=a0` by auto
-	hence "a2 k \<le> x k" apply(drule_tac kle_imp_pointwise) by auto moreover
-	have "x k \<le> a2 k" unfolding k(2)[rule_format] using a0a1(4)[rule_format,of x,THEN conjunct1] 
-	  unfolding kle_def using x by auto ultimately show "x k = a2 k" by auto qed
+        hence "kle n a2 x" apply-apply(rule lem3) using `a=a0` by auto
+        hence "a2 k \<le> x k" apply(drule_tac kle_imp_pointwise) by auto moreover
+        have "x k \<le> a2 k" unfolding k(2)[rule_format] using a0a1(4)[rule_format,of x,THEN conjunct1] 
+          unfolding kle_def using x by auto ultimately show "x k = a2 k" by auto qed
       have **:"a'=a_min \<or> a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto
       show "s' \<in> {s, insert a3 (s - {a0})}" proof(cases "a'=a_min")
-	case True have "a_max = a1" unfolding kle_antisym[THEN sym,of a_max a1 n] apply(rule)
-	  apply(rule a0a1(4)[rule_format,THEN conjunct2]) defer  proof(rule min_max(4)[rule_format,THEN conjunct2])
-	  show "a1\<in>s'" using a' unfolding `a=a0` using a0a1 by auto
-	  show "a_max \<in> s" proof(rule ccontr) assume "a_max\<notin>s"
-	    hence "a_max = a'" using a' min_max by auto
-	    thus False unfolding True using min_max by auto qed qed
-	hence "\<forall>i. a_max i = a1 i" by auto
-	hence "a' = a" unfolding True `a=a0` apply-apply(subst fun_eq_iff,rule)
-	  apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
-	proof- case goal1 thus ?case apply(cases "x\<in>{1..n}") by auto qed
-	hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` by auto
-	thus ?thesis by auto next
-	case False hence as:"a' = a_max" using ** by auto
-	have "a_min = a2" unfolding kle_antisym[THEN sym, of _ _ n] apply rule
-	  apply(rule min_max(4)[rule_format,THEN conjunct1]) defer proof(rule lem3)
-	  show "a_min \<in> s - {a0}" unfolding a'(2)[THEN sym,unfolded `a=a0`] 
-	    unfolding as using min_max(1-3) by auto
-	  have "a2 \<noteq> a" unfolding `a=a0` using k(2)[rule_format,of k] by auto
-	  hence "a2 \<in> s - {a}" using a2 by auto thus "a2 \<in> s'" unfolding a'(2)[THEN sym] by auto qed
-	hence "\<forall>i. a_min i = a2 i" by auto
-	hence "a' = a3" unfolding as `a=a0` apply-apply(subst fun_eq_iff,rule)
-	  apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
-	  unfolding a3_def k(2)[rule_format] unfolding a0a1(5)[rule_format] proof- case goal1
-	  show ?case unfolding goal1 apply(cases "x\<in>{1..n}") defer apply(cases "x=k")
-	    using `k\<in>{1..n}` by auto qed
-	hence "s' = insert a3 (s - {a0})" apply-apply(rule lem1) defer apply assumption
-	  apply(rule a'(1)) unfolding a' `a=a0` using `a3\<notin>s` by auto
-	thus ?thesis by auto qed qed
+        case True have "a_max = a1" unfolding kle_antisym[THEN sym,of a_max a1 n] apply(rule)
+          apply(rule a0a1(4)[rule_format,THEN conjunct2]) defer  proof(rule min_max(4)[rule_format,THEN conjunct2])
+          show "a1\<in>s'" using a' unfolding `a=a0` using a0a1 by auto
+          show "a_max \<in> s" proof(rule ccontr) assume "a_max\<notin>s"
+            hence "a_max = a'" using a' min_max by auto
+            thus False unfolding True using min_max by auto qed qed
+        hence "\<forall>i. a_max i = a1 i" by auto
+        hence "a' = a" unfolding True `a=a0` apply-apply(subst fun_eq_iff,rule)
+          apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
+        proof- case goal1 thus ?case apply(cases "x\<in>{1..n}") by auto qed
+        hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` by auto
+        thus ?thesis by auto next
+        case False hence as:"a' = a_max" using ** by auto
+        have "a_min = a2" unfolding kle_antisym[THEN sym, of _ _ n] apply rule
+          apply(rule min_max(4)[rule_format,THEN conjunct1]) defer proof(rule lem3)
+          show "a_min \<in> s - {a0}" unfolding a'(2)[THEN sym,unfolded `a=a0`] 
+            unfolding as using min_max(1-3) by auto
+          have "a2 \<noteq> a" unfolding `a=a0` using k(2)[rule_format,of k] by auto
+          hence "a2 \<in> s - {a}" using a2 by auto thus "a2 \<in> s'" unfolding a'(2)[THEN sym] by auto qed
+        hence "\<forall>i. a_min i = a2 i" by auto
+        hence "a' = a3" unfolding as `a=a0` apply-apply(subst fun_eq_iff,rule)
+          apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
+          unfolding a3_def k(2)[rule_format] unfolding a0a1(5)[rule_format] proof- case goal1
+          show ?case unfolding goal1 apply(cases "x\<in>{1..n}") defer apply(cases "x=k")
+            using `k\<in>{1..n}` by auto qed
+        hence "s' = insert a3 (s - {a0})" apply-apply(rule lem1) defer apply assumption
+          apply(rule a'(1)) unfolding a' `a=a0` using `a3\<notin>s` by auto
+        thus ?thesis by auto qed qed
     ultimately have *:"?A = {s, insert a3 (s - {a0})}" by blast
     have "s \<noteq> insert a3 (s - {a0})" using `a3\<notin>s` by auto
     hence ?thesis unfolding * by auto } moreover
@@ -780,17 +780,17 @@
         using `a3\<noteq>a0` `a3\<notin>s` `a1\<in>s` by(auto simp add:card_insert_if)
       fix x assume x:"x \<in> insert a3 (s - {a1})"
       show "\<forall>j. x j \<le> p" proof(rule,cases "x = a3")
-	fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
-	fix j case True show "x j\<le>p" unfolding True proof(cases "j=k") 
-	  case False thus "a3 j \<le>p" unfolding True a3_def using `a0\<in>s` ksimplexD(4)[OF assms(1)] by auto next
-	  guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. note a4=this
+        fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
+        fix j case True show "x j\<le>p" unfolding True proof(cases "j=k") 
+          case False thus "a3 j \<le>p" unfolding True a3_def using `a0\<in>s` ksimplexD(4)[OF assms(1)] by auto next
+          guess a4 using assms(5)[unfolded bex_simps ball_simps,rule_format,OF k(1)] .. note a4=this
           case True have "a3 k \<le> a0 k" unfolding lem4[rule_format] by auto
           also have "\<dots> \<le> p" using ksimplexD(4)[OF assms(1),rule_format,of a0 k] a0a1 by auto
           finally show "a3 j \<le> p" unfolding True by auto qed qed
       show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a3") fix j::nat assume j:"j\<notin>{1..n}"
-	{ case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }
-	case True show "x j = p" unfolding True a3_def using j k(1) 
-	  using ksimplexD(5)[OF assms(1),rule_format,OF `a0\<in>s` j] by auto qed
+        { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }
+        case True show "x j = p" unfolding True a3_def using j k(1) 
+          using ksimplexD(5)[OF assms(1),rule_format,OF `a0\<in>s` j] by auto qed
       fix y assume y:"y\<in>insert a3 (s - {a1})"
       have lem4:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a1 \<Longrightarrow> kle n a3 x" proof- case goal1 hence *:"x\<in>s - {a1}" by auto
         have "kle n a3 a2" proof- have "kle n a0 a1" using a0a1 by auto then guess kk unfolding kle_def ..
@@ -801,12 +801,12 @@
         ultimately show ?case apply-apply(rule kle_between_l[of _ a0 _ a2]) using lem3[OF *]
           using a0a1(4)[rule_format,OF goal1(1)] by auto qed
       show "kle n x y \<or> kle n y x" proof(cases "y=a3")
-	case True show ?thesis unfolding True apply(cases "x=a3") defer apply(rule disjI2,rule lem4)
-	  using x by auto next
-	case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True
-	    apply(rule disjI1,rule lem4) using y False by auto next
-	  case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 
-	    using x y `y\<noteq>a3` by auto qed qed qed
+        case True show ?thesis unfolding True apply(cases "x=a3") defer apply(rule disjI2,rule lem4)
+          using x by auto next
+        case False show ?thesis proof(cases "x=a3") case True show ?thesis unfolding True
+            apply(rule disjI1,rule lem4) using y False by auto next
+          case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 
+            using x y `y\<noteq>a3` by auto qed qed qed
     hence "insert a3 (s - {a1}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)
       apply(rule_tac x="a3" in bexI) unfolding `a=a1` using `a3\<notin>s` by auto moreover
     have "s \<in> ?A" using assms(1,2) by auto ultimately have  "?A \<supseteq> {s, insert a3 (s - {a1})}" by auto
@@ -815,61 +815,61 @@
       from this(2) guess a' .. note a'=this
       guess a_min a_max apply(rule ksimplex_extrema_strong[OF as assms(3)]) . note min_max=this
       have *:"\<forall>x\<in>s' - {a'}. x k = a2 k" unfolding a' proof fix x assume x:"x\<in>s-{a}"
-	hence "kle n x a2" apply-apply(rule lem3) using `a=a1` by auto
-	hence "x k \<le> a2 k" apply(drule_tac kle_imp_pointwise) by auto moreover
-	{ have "a2 k \<le> a0 k" using k(2)[rule_format,of k] unfolding a0a1(5)[rule_format] using k(1) by simp
-	  also have "\<dots> \<le> x k" using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x by auto
-	  finally have "a2 k \<le> x k" . } ultimately show "x k = a2 k" by auto qed
+        hence "kle n x a2" apply-apply(rule lem3) using `a=a1` by auto
+        hence "x k \<le> a2 k" apply(drule_tac kle_imp_pointwise) by auto moreover
+        { have "a2 k \<le> a0 k" using k(2)[rule_format,of k] unfolding a0a1(5)[rule_format] using k(1) by simp
+          also have "\<dots> \<le> x k" using a0a1(4)[rule_format,of x,THEN conjunct1,THEN kle_imp_pointwise] x by auto
+          finally have "a2 k \<le> x k" . } ultimately show "x k = a2 k" by auto qed
       have **:"a'=a_min \<or> a'=a_max" apply(rule ksimplex_fix_plane[OF a'(1) k(1) *]) using min_max by auto
       have "a2 \<noteq> a1" proof assume as:"a2 = a1"
-	show False using k(2) unfolding as apply(erule_tac x=k in allE) by auto qed
+        show False using k(2) unfolding as apply(erule_tac x=k in allE) by auto qed
       hence a2':"a2 \<in> s' - {a'}" unfolding a' using a2 unfolding `a=a1` by auto
       show "s' \<in> {s, insert a3 (s - {a1})}" proof(cases "a'=a_min")
-	case True have "a_max \<in> s - {a1}" using min_max unfolding a'(2)[unfolded `a=a1`,THEN sym] True by auto
-	hence "a_max = a2" unfolding kle_antisym[THEN sym,of a_max a2 n] apply-apply(rule)
-	  apply(rule lem3,assumption) apply(rule min_max(4)[rule_format,THEN conjunct2]) using a2' by auto
-	hence a_max:"\<forall>i. a_max i = a2 i" by auto
-	have *:"\<forall>j. a2 j = (if j\<in>{1..n} then a3 j + 1 else a3 j)" 
-	  using k(2) unfolding lem4[rule_format] a0a1(5)[rule_format] apply-apply(rule,erule_tac x=j in allE)
-	proof- case goal1 thus ?case apply(cases "j\<in>{1..n}",case_tac[!] "j=k") by auto qed
-	have "\<forall>i. a_min i = a3 i" using a_max apply-apply(rule,erule_tac x=i in allE)
-	  unfolding min_max(5)[rule_format] *[rule_format] proof- case goal1
-	  thus ?case apply(cases "i\<in>{1..n}") by auto qed hence "a_min = a3" unfolding fun_eq_iff .
-	hence "s' = insert a3 (s - {a1})" using a' unfolding `a=a1` True by auto thus ?thesis by auto next
-	case False hence as:"a'=a_max" using ** by auto
-	have "a_min = a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule)
-	  apply(rule min_max(4)[rule_format,THEN conjunct1]) defer apply(rule a0a1(4)[rule_format,THEN conjunct1]) proof-
-	  have "a_min \<in> s - {a1}" using min_max(1,3) unfolding a'(2)[THEN sym,unfolded `a=a1`] as by auto
-	  thus "a_min \<in> s" by auto have "a0 \<in> s - {a1}" using a0a1(1-3) by auto thus "a0 \<in> s'"
-	    unfolding a'(2)[THEN sym,unfolded `a=a1`] by auto qed
-	hence "\<forall>i. a_max i = a1 i" unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto
-	hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` unfolding as `a=a1` unfolding fun_eq_iff by auto
-	thus ?thesis by auto qed qed 
+        case True have "a_max \<in> s - {a1}" using min_max unfolding a'(2)[unfolded `a=a1`,THEN sym] True by auto
+        hence "a_max = a2" unfolding kle_antisym[THEN sym,of a_max a2 n] apply-apply(rule)
+          apply(rule lem3,assumption) apply(rule min_max(4)[rule_format,THEN conjunct2]) using a2' by auto
+        hence a_max:"\<forall>i. a_max i = a2 i" by auto
+        have *:"\<forall>j. a2 j = (if j\<in>{1..n} then a3 j + 1 else a3 j)" 
+          using k(2) unfolding lem4[rule_format] a0a1(5)[rule_format] apply-apply(rule,erule_tac x=j in allE)
+        proof- case goal1 thus ?case apply(cases "j\<in>{1..n}",case_tac[!] "j=k") by auto qed
+        have "\<forall>i. a_min i = a3 i" using a_max apply-apply(rule,erule_tac x=i in allE)
+          unfolding min_max(5)[rule_format] *[rule_format] proof- case goal1
+          thus ?case apply(cases "i\<in>{1..n}") by auto qed hence "a_min = a3" unfolding fun_eq_iff .
+        hence "s' = insert a3 (s - {a1})" using a' unfolding `a=a1` True by auto thus ?thesis by auto next
+        case False hence as:"a'=a_max" using ** by auto
+        have "a_min = a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule)
+          apply(rule min_max(4)[rule_format,THEN conjunct1]) defer apply(rule a0a1(4)[rule_format,THEN conjunct1]) proof-
+          have "a_min \<in> s - {a1}" using min_max(1,3) unfolding a'(2)[THEN sym,unfolded `a=a1`] as by auto
+          thus "a_min \<in> s" by auto have "a0 \<in> s - {a1}" using a0a1(1-3) by auto thus "a0 \<in> s'"
+            unfolding a'(2)[THEN sym,unfolded `a=a1`] by auto qed
+        hence "\<forall>i. a_max i = a1 i" unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto
+        hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` unfolding as `a=a1` unfolding fun_eq_iff by auto
+        thus ?thesis by auto qed qed 
     ultimately have *:"?A = {s, insert a3 (s - {a1})}" by blast
     have "s \<noteq> insert a3 (s - {a1})" using `a3\<notin>s` by auto
     hence ?thesis unfolding * by auto } moreover
   { assume as:"a\<noteq>a0" "a\<noteq>a1" have "\<not> (\<forall>x\<in>s. kle n a x)" proof case goal1
       have "a=a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule)
-	using goal1 a0a1 assms(2) by auto thus False using as by auto qed
+        using goal1 a0a1 assms(2) by auto thus False using as by auto qed
     hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. a j = (if j = k then y j + 1 else y j)" using  ksimplex_predecessor[OF assms(1-2)] by blast
     then guess u .. from this(2) guess k .. note k = this[rule_format] note u = `u\<in>s`
     have "\<not> (\<forall>x\<in>s. kle n x a)" proof case goal1
       have "a=a1" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule)
-	using goal1 a0a1 assms(2) by auto thus False using as by auto qed
+        using goal1 a0a1 assms(2) by auto thus False using as by auto qed
     hence "\<exists>y\<in>s. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then a j + 1 else a j)" using  ksimplex_successor[OF assms(1-2)] by blast
     then guess v .. from this(2) guess l .. note l = this[rule_format] note v = `v\<in>s`
     def a' \<equiv> "\<lambda>j. if j = l then u j + 1 else u j"
     have kl:"k \<noteq> l" proof assume "k=l" have *:"\<And>P. (if P then (1::nat) else 0) \<noteq> 2" by auto
       thus False using ksimplexD(6)[OF assms(1),rule_format,OF u v] unfolding kle_def
-	unfolding l(2) k(2) `k=l` apply-apply(erule disjE)apply(erule_tac[!] exE conjE)+
-	apply(erule_tac[!] x=l in allE)+ by(auto simp add: *) qed
+        unfolding l(2) k(2) `k=l` apply-apply(erule disjE)apply(erule_tac[!] exE conjE)+
+        apply(erule_tac[!] x=l in allE)+ by(auto simp add: *) qed
     hence aa':"a'\<noteq>a" apply-apply rule unfolding fun_eq_iff unfolding a'_def k(2)
       apply(erule_tac x=l in allE) by auto
     have "a' \<notin> s" apply(rule) apply(drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`]) proof(cases "kle n a a'")
       case goal2 hence "kle n a' a" by auto thus False apply(drule_tac kle_imp_pointwise)
-	apply(erule_tac x=l in allE) unfolding a'_def k(2) using kl by auto next
+        apply(erule_tac x=l in allE) unfolding a'_def k(2) using kl by auto next
       case True thus False apply(drule_tac kle_imp_pointwise)
-	apply(erule_tac x=k in allE) unfolding a'_def k(2) using kl by auto qed
+        apply(erule_tac x=k in allE) unfolding a'_def k(2) using kl by auto qed
     have kle_uv:"kle n u a" "kle n u a'" "kle n a v" "kle n a' v" unfolding kle_def apply-
       apply(rule_tac[1] x="{k}" in exI,rule_tac[2] x="{l}" in exI)
       apply(rule_tac[3] x="{l}" in exI,rule_tac[4] x="{k}" in exI)
@@ -878,24 +878,24 @@
     proof- case goal1 thus ?case proof(cases "x k = u k", case_tac[!] "x l = u l")
       assume as:"x l = u l" "x k = u k"
       have "x = u" unfolding fun_eq_iff
-	using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)] unfolding k(2) apply-
-	using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
-	thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
+        using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)] unfolding k(2) apply-
+        using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
+        thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
       assume as:"x l \<noteq> u l" "x k = u k"
       have "x = a'" unfolding fun_eq_iff unfolding a'_def
-	using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
-	using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
-	thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
+        using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
+        using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
+        thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
       assume as:"x l = u l" "x k \<noteq> u k"
       have "x = a" unfolding fun_eq_iff
-	using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
-	using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
-	thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
+        using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
+        using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
+        thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
       assume as:"x l \<noteq> u l" "x k \<noteq> u k"
       have "x = v" unfolding fun_eq_iff
-	using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
-	using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
-	thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as `k\<noteq>l` by auto qed thus ?case by auto qed qed
+        using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
+        using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
+        thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as `k\<noteq>l` by auto qed thus ?case by auto qed qed
     have uv:"kle n u v" apply(rule kle_trans[OF kle_uv(1,3)]) using ksimplexD(6)[OF assms(1)] using u v by auto
     have lem3:"\<And>x. x\<in>s \<Longrightarrow> kle n v x \<Longrightarrow> kle n a' x" apply(rule kle_between_r[of _ u _ v])
       prefer 3 apply(rule kle_trans[OF uv]) defer apply(rule ksimplexD(6)[OF assms(1),rule_format])
@@ -905,30 +905,30 @@
       using kle_uv `v\<in>s` by auto
     have lem5:"\<And>x. x\<in>s \<Longrightarrow> x\<noteq>a \<Longrightarrow> kle n x a' \<or> kle n a' x" proof- case goal1 thus ?case
       proof(cases "kle n v x \<or> kle n x u") case True thus ?thesis using goal1 by(auto intro:lem3 lem4) next
-	case False hence *:"kle n u x" "kle n x v" using ksimplexD(6)[OF assms(1)] using goal1 `u\<in>s` `v\<in>s` by auto
-	show ?thesis using uxv[OF *] using kle_uv using goal1 by auto qed qed
+        case False hence *:"kle n u x" "kle n x v" using ksimplexD(6)[OF assms(1)] using goal1 `u\<in>s` `v\<in>s` by auto
+        show ?thesis using uxv[OF *] using kle_uv using goal1 by auto qed qed
     have "ksimplex p n (insert a' (s - {a}))" apply(rule ksimplexI) proof(rule_tac[2-] ballI,rule_tac[4] ballI)
       show "card (insert a' (s - {a})) = n + 1" using ksimplexD(2-3)[OF assms(1)]
         using `a'\<noteq>a` `a'\<notin>s` `a\<in>s` by(auto simp add:card_insert_if)
       fix x assume x:"x \<in> insert a' (s - {a})"
       show "\<forall>j. x j \<le> p" proof(rule,cases "x = a'")
-	fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
-	fix j case True show "x j\<le>p" unfolding True proof(cases "j=l") 
-	  case False thus "a' j \<le>p" unfolding True a'_def using `u\<in>s` ksimplexD(4)[OF assms(1)] by auto next
-	  case True have *:"a l = u l" "v l = a l + 1" using k(2)[of l] l(2)[of l] `k\<noteq>l` by auto
-	  have "u l + 1 \<le> p" unfolding *[THEN sym] using ksimplexD(4)[OF assms(1)] using `v\<in>s` by auto
-	  thus "a' j \<le>p" unfolding a'_def True by auto qed qed
+        fix j case False thus "x j\<le>p" using x ksimplexD(4)[OF assms(1)] by auto next
+        fix j case True show "x j\<le>p" unfolding True proof(cases "j=l") 
+          case False thus "a' j \<le>p" unfolding True a'_def using `u\<in>s` ksimplexD(4)[OF assms(1)] by auto next
+          case True have *:"a l = u l" "v l = a l + 1" using k(2)[of l] l(2)[of l] `k\<noteq>l` by auto
+          have "u l + 1 \<le> p" unfolding *[THEN sym] using ksimplexD(4)[OF assms(1)] using `v\<in>s` by auto
+          thus "a' j \<le>p" unfolding a'_def True by auto qed qed
       show "\<forall>j. j \<notin> {1..n} \<longrightarrow> x j = p" proof(rule,rule,cases "x=a'") fix j::nat assume j:"j\<notin>{1..n}"
-	{ case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }
-	case True show "x j = p" unfolding True a'_def using j l(1) 
-	  using ksimplexD(5)[OF assms(1),rule_format,OF `u\<in>s` j] by auto qed
+        { case False thus "x j = p" using j x ksimplexD(5)[OF assms(1)] by auto }
+        case True show "x j = p" unfolding True a'_def using j l(1) 
+          using ksimplexD(5)[OF assms(1),rule_format,OF `u\<in>s` j] by auto qed
       fix y assume y:"y\<in>insert a' (s - {a})"
       show "kle n x y \<or> kle n y x" proof(cases "y=a'")
-	case True show ?thesis unfolding True apply(cases "x=a'") defer apply(rule lem5) using x by auto next
-	case False show ?thesis proof(cases "x=a'") case True show ?thesis unfolding True
-	    using lem5[of y] using y by auto next
-	  case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 
-	    using x y `y\<noteq>a'` by auto qed qed qed
+        case True show ?thesis unfolding True apply(cases "x=a'") defer apply(rule lem5) using x by auto next
+        case False show ?thesis proof(cases "x=a'") case True show ?thesis unfolding True
+            using lem5[of y] using y by auto next
+          case False thus ?thesis apply(rule_tac ksimplexD(6)[OF assms(1),rule_format]) 
+            using x y `y\<noteq>a'` by auto qed qed qed
     hence "insert a' (s - {a}) \<in> ?A" unfolding mem_Collect_eq apply-apply(rule,assumption)
       apply(rule_tac x="a'" in bexI) using aa' `a'\<notin>s` by auto moreover
     have "s \<in> ?A" using assms(1,2) by auto ultimately have  "?A \<supseteq> {s, insert a' (s - {a})}" by auto
@@ -940,27 +940,27 @@
       have "u\<noteq>a" "v\<noteq>a" unfolding fun_eq_iff k(2) l(2) by auto 
       hence uvs':"u\<in>s'" "v\<in>s'" using `u\<in>s` `v\<in>s` using a'' by auto
       have lem6:"a \<in> s' \<or> a' \<in> s'" proof(cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")
-	case False then guess w unfolding ball_simps .. note w=this
-	hence "kle n u w" "kle n w v" using ksimplexD(6)[OF as] uvs' by auto
-	hence "w = a' \<or> w = a" using uxv[of w] uvs' w by auto thus ?thesis using w by auto next
-	case True have "\<not> (\<forall>x\<in>s'. kle n x u)" unfolding ball_simps apply(rule_tac x=v in bexI)
-	  using uv `u\<noteq>v` unfolding kle_antisym[of n u v,THEN sym] using `v\<in>s'` by auto
-	hence "\<exists>y\<in>s'. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then u j + 1 else u j)" using ksimplex_successor[OF as `u\<in>s'`] by blast
-	then guess w .. note w=this from this(2) guess kk .. note kk=this[rule_format]
-	have "\<not> kle n w u" apply-apply(rule,drule kle_imp_pointwise) 
-	  apply(erule_tac x=kk in allE) unfolding kk by auto 
-	hence *:"kle n v w" using True[rule_format,OF w(1)] by auto
-	hence False proof(cases "kk\<noteq>l") case True thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
-	    apply(erule_tac x=l in allE) using `k\<noteq>l` by auto  next
-	  case False hence "kk\<noteq>k" using `k\<noteq>l` by auto thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
-	    apply(erule_tac x=k in allE) using `k\<noteq>l` by auto qed
-	thus ?thesis by auto qed
+        case False then guess w unfolding ball_simps .. note w=this
+        hence "kle n u w" "kle n w v" using ksimplexD(6)[OF as] uvs' by auto
+        hence "w = a' \<or> w = a" using uxv[of w] uvs' w by auto thus ?thesis using w by auto next
+        case True have "\<not> (\<forall>x\<in>s'. kle n x u)" unfolding ball_simps apply(rule_tac x=v in bexI)
+          using uv `u\<noteq>v` unfolding kle_antisym[of n u v,THEN sym] using `v\<in>s'` by auto
+        hence "\<exists>y\<in>s'. \<exists>k\<in>{1..n}. \<forall>j. y j = (if j = k then u j + 1 else u j)" using ksimplex_successor[OF as `u\<in>s'`] by blast
+        then guess w .. note w=this from this(2) guess kk .. note kk=this[rule_format]
+        have "\<not> kle n w u" apply-apply(rule,drule kle_imp_pointwise) 
+          apply(erule_tac x=kk in allE) unfolding kk by auto 
+        hence *:"kle n v w" using True[rule_format,OF w(1)] by auto
+        hence False proof(cases "kk\<noteq>l") case True thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
+            apply(erule_tac x=l in allE) using `k\<noteq>l` by auto  next
+          case False hence "kk\<noteq>k" using `k\<noteq>l` by auto thus False using *[THEN kle_imp_pointwise, unfolded l(2) kk k(2)]
+            apply(erule_tac x=k in allE) using `k\<noteq>l` by auto qed
+        thus ?thesis by auto qed
       thus "s' \<in> {s, insert a' (s - {a})}" proof(cases "a\<in>s'")
-	case True hence "s' = s" apply-apply(rule lem1[OF a''(2)]) using a'' `a\<in>s` by auto
-	thus ?thesis by auto next case False hence "a'\<in>s'" using lem6 by auto
-	hence "s' = insert a' (s - {a})" apply-apply(rule lem1[of _ a'' _ a'])
-	  unfolding a''(2)[THEN sym] using a'' using `a'\<notin>s` by auto
-	thus ?thesis by auto qed qed 
+        case True hence "s' = s" apply-apply(rule lem1[OF a''(2)]) using a'' `a\<in>s` by auto
+        thus ?thesis by auto next case False hence "a'\<in>s'" using lem6 by auto
+        hence "s' = insert a' (s - {a})" apply-apply(rule lem1[of _ a'' _ a'])
+          unfolding a''(2)[THEN sym] using a'' using `a'\<notin>s` by auto
+        thus ?thesis by auto qed qed 
     ultimately have *:"?A = {s, insert a' (s - {a})}" by blast
     have "s \<noteq> insert a' (s - {a})" using `a'\<notin>s` by auto
     hence ?thesis unfolding * by auto } 
@@ -986,9 +986,9 @@
     let ?S = "{s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})}"
     have S:"?S = {s'. ksimplex p (n + 1) s' \<and> (\<exists>b\<in>s'. s' - {b} = s - {a})}" unfolding as by blast
     { fix j assume j:"j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = 0" thus "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})} = 1" unfolding S
-	apply-apply(rule ksimplex_replace_0) apply(rule as)+ unfolding as by auto }
+        apply-apply(rule ksimplex_replace_0) apply(rule as)+ unfolding as by auto }
     { fix j assume j:"j \<in> {1..n + 1}" "\<forall>x\<in>f. x j = p" thus "card {s. ksimplex p (n + 1) s \<and> (\<exists>a\<in>s. f = s - {a})} = 1" unfolding S
-	apply-apply(rule ksimplex_replace_1) apply(rule as)+ unfolding as by auto }
+        apply-apply(rule ksimplex_replace_1) apply(rule as)+ unfolding as by auto }
     show "\<not> ((\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n+1}. \<forall>x\<in>f. x j = p)) \<Longrightarrow> card ?S = 2"
       unfolding S apply(rule ksimplex_replace_2) apply(rule as)+ unfolding as by auto qed auto qed
 
@@ -1058,7 +1058,7 @@
       using assms(2-3) using as(1)[unfolded ksimplex_def] by auto
     have allp:"\<forall>x\<in>f. x (n + 1) = p" using assms(2) using as(1)[unfolded ksimplex_def] by auto
     { fix x assume "x\<in>f" hence "reduced lab (n + 1) x < n + 1" apply-apply(rule reduced_labelling_1)
-	defer using assms(3) using as(1)[unfolded ksimplex_def] by auto
+        defer using assms(3) using as(1)[unfolded ksimplex_def] by auto
       hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) using reduced_labelling(1) by auto }
     hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[THEN sym] apply- apply(rule set_eqI) unfolding image_iff by auto
     moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,THEN sym]] .. then guess a ..
@@ -1071,21 +1071,21 @@
     { fix x assume "x\<in>f" hence "reduced lab (n + 1) x \<in> reduced lab (n + 1) ` f" by auto
       hence "reduced lab (n + 1) x < n + 1" using sa(4) by auto 
       hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc)
-	using reduced_labelling(1) by auto }
+        using reduced_labelling(1) by auto }
     thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[THEN sym] apply-apply(rule set_eqI) unfolding image_iff by auto
     have *:"\<forall>x\<in>f. x (n + 1) = p" proof(cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
       case True then guess j .. hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1" apply-apply(rule reduced_labelling_0) apply assumption
-	apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover
+        apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover
       have "j - 1 \<in> {0..n}" using `j\<in>{1..n+1}` by auto
       ultimately have False unfolding sa(4)[THEN sym] unfolding image_iff by fastsimp thus ?thesis by auto next
       case False hence "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p" using sa(5) by fastsimp then guess j .. note j=this
       thus ?thesis proof(cases "j = n+1")
-	case False hence *:"j\<in>{1..n}" using j by auto
-	hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab n x < j" apply(rule reduced_labelling_1) proof- fix x assume "x\<in>f"
-	  hence "lab x j = 1" apply-apply(rule assms(3)[rule_format,OF j(1)]) 
-	    using sa(1)[unfolded ksimplex_def] using j unfolding sa by auto thus "lab x j \<noteq> 0" by auto qed
-	moreover have "j\<in>{0..n}" using * by auto
-	ultimately have False unfolding part1[THEN sym] using * unfolding image_iff by auto thus ?thesis by auto qed auto qed 
+        case False hence *:"j\<in>{1..n}" using j by auto
+        hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab n x < j" apply(rule reduced_labelling_1) proof- fix x assume "x\<in>f"
+          hence "lab x j = 1" apply-apply(rule assms(3)[rule_format,OF j(1)]) 
+            using sa(1)[unfolded ksimplex_def] using j unfolding sa by auto thus "lab x j \<noteq> 0" by auto qed
+        moreover have "j\<in>{0..n}" using * by auto
+        ultimately have False unfolding part1[THEN sym] using * unfolding image_iff by auto thus ?thesis by auto qed auto qed 
     thus "ksimplex p n f" using as unfolding simplex_top_face[OF assms(1) *,THEN sym] by auto qed qed
 
 lemma kuhn_induction_Suc:
diff -r d488ae70366d -r 5abc60a017e0 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Mar 13 21:41:44 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Mar 13 22:24:10 2011 +0100
@@ -374,9 +374,9 @@
     show "norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)" proof(cases "y=x")
       case True thus ?thesis using `bounded_linear f'` by(auto simp add: zero) next
       case False hence "norm (f y - (f x + f' (y - x))) < e * norm (y - x)" using as(4)[rule_format, OF `y\<in>s`]
-	unfolding dist_norm diff_0_right using as(3)
-	using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded dist_norm]
-	by (auto simp add: linear_0 linear_sub)
+        unfolding dist_norm diff_0_right using as(3)
+        using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded dist_norm]
+        by (auto simp add: linear_0 linear_sub)
       thus ?thesis by(auto simp add:algebra_simps) qed qed next
   assume ?rhs thus ?lhs unfolding has_derivative_within Lim_within apply-apply(erule conjE,rule,assumption)
     apply(rule,erule_tac x="e/2" in allE,rule,erule impE) defer apply(erule exE,rule_tac x=d in exI)
@@ -678,7 +678,7 @@
     guess c using continuous_attains_inf[OF compact_interval * assms(3)] .. note c=this
     show ?thesis proof(cases "d\<in>{a<..<b} \<or> c\<in>{a<..<b}")
       case True thus ?thesis apply(erule_tac disjE) apply(rule_tac x=d in bexI)
-	apply(rule_tac[3] x=c in bexI) using d c by auto next def e \<equiv> "(a + b) /2"
+        apply(rule_tac[3] x=c in bexI) using d c by auto next def e \<equiv> "(a + b) /2"
       case False hence "f d = f c" using d c assms(2) by auto
       hence "\<And>x. x\<in>{a..b} \<Longrightarrow> f x = f d" using c d apply- apply(erule_tac x=x in ballE)+ by auto
       thus ?thesis apply(rule_tac x=e in bexI) unfolding e_def using assms(1) by auto qed qed
@@ -813,11 +813,11 @@
       fix z assume as:"norm (z - y) < d" hence "z\<in>t" using d2 d unfolding dist_norm by auto
       have "norm (g z - g y - g' (z - y)) \<le> norm (g' (f (g z) - y - f' (g z - g y)))"
         unfolding g'.diff f'.diff unfolding assms(3)[unfolded o_def id_def, THEN fun_cong] 
-	unfolding assms(7)[rule_format,OF `z\<in>t`] apply(subst norm_minus_cancel[THEN sym]) by auto
+        unfolding assms(7)[rule_format,OF `z\<in>t`] apply(subst norm_minus_cancel[THEN sym]) by auto
       also have "\<dots> \<le> norm(f (g z) - y - f' (g z - g y)) * C" by(rule C[THEN conjunct2,rule_format]) 
       also have "\<dots> \<le> (e / C) * norm (g z - g y) * C" apply(rule mult_right_mono)
-	apply(rule d0[THEN conjunct2,rule_format,unfolded assms(7)[rule_format,OF `y\<in>t`]]) apply(cases "z=y") defer
-	apply(rule d1[THEN conjunct2, unfolded dist_norm,rule_format]) using as d C d0 by auto
+        apply(rule d0[THEN conjunct2,rule_format,unfolded assms(7)[rule_format,OF `y\<in>t`]]) apply(cases "z=y") defer
+        apply(rule d1[THEN conjunct2, unfolded dist_norm,rule_format]) using as d C d0 by auto
       also have "\<dots> \<le> e * norm (g z - g y)" using C by(auto simp add:field_simps)
       finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)" by simp qed auto qed
   have *:"(0::real) < 1 / 2" by auto guess d using lem1[rule_format,OF *] .. note d=this def B\<equiv>"C*2"
@@ -834,7 +834,7 @@
     show ?case apply(rule_tac x=k in exI,rule) defer proof(rule,rule) fix z assume as:"norm(z - y) < k"
       hence "norm (g z - g y - g' (z - y)) \<le> e / B * norm(g z - g y)" using d' k by auto
       also have "\<dots> \<le> e * norm(z - y)" unfolding times_divide_eq_left pos_divide_le_eq[OF `B>0`]
-	using lem2[THEN spec[where x=z]] using k as using `e>0` by(auto simp add:field_simps)
+        using lem2[THEN spec[where x=z]] using k as using `e>0` by(auto simp add:field_simps)
       finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (z - y)" by simp qed(insert k, auto) qed qed
 
 subsection {* Simply rewrite that based on the domain point x. *}
@@ -976,7 +976,7 @@
     show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
       apply(rule_tac x=d in exI) apply(rule,rule d[THEN conjunct1]) proof(rule,rule) case goal1
       hence "g y \<in> g ` f ` (ball x e \<inter> s)" using d[THEN conjunct2,unfolded subset_eq,THEN bspec[where x=y]]
-	by(auto simp add:dist_commute)
+        by(auto simp add:dist_commute)
       hence "g y \<in> ball x e \<inter> s" using assms(4) by auto
       thus "dist (g y) (g (f x)) < e" using assms(4)[rule_format,OF `x\<in>s`] by(auto simp add:dist_commute) qed qed
   moreover have "f x \<in> interior (f ` s)" apply(rule sussmann_open_mapping)
@@ -1031,27 +1031,27 @@
     show "\<forall>x\<in>ball a d. \<forall>x'\<in>ball a d. f x' = f x \<longrightarrow> x' = x" proof(intro strip)
       fix x y assume as:"x\<in>ball a d" "y\<in>ball a d" "f x = f y"
       def ph \<equiv> "\<lambda>w. w - g'(f w - f x)" have ph':"ph = g' \<circ> (\<lambda>w. f' a w - (f w - f x))"
-	unfolding ph_def o_def unfolding diff using f'g' by(auto simp add:algebra_simps)
+        unfolding ph_def o_def unfolding diff using f'g' by(auto simp add:algebra_simps)
       have "norm (ph x - ph y) \<le> (1/2) * norm (x - y)"
-	apply(rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"])
-	apply(rule_tac[!] ballI) proof- fix u assume u:"u \<in> ball a d" hence "u\<in>s" using d d2 by auto
-	have *:"(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)" unfolding o_def and diff using f'g' by auto
-	show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
-	  unfolding ph' * apply(rule diff_chain_within) defer apply(rule bounded_linear.has_derivative[OF assms(3)])
-	  apply(rule has_derivative_intros) defer apply(rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
-	  apply(rule has_derivative_at_within) using assms(5) and `u\<in>s` `a\<in>s`
+        apply(rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\<lambda>x v. v - g'(f' x v)"])
+        apply(rule_tac[!] ballI) proof- fix u assume u:"u \<in> ball a d" hence "u\<in>s" using d d2 by auto
+        have *:"(\<lambda>v. v - g' (f' u v)) = g' \<circ> (\<lambda>w. f' a w - f' u w)" unfolding o_def and diff using f'g' by auto
+        show "(ph has_derivative (\<lambda>v. v - g' (f' u v))) (at u within ball a d)"
+          unfolding ph' * apply(rule diff_chain_within) defer apply(rule bounded_linear.has_derivative[OF assms(3)])
+          apply(rule has_derivative_intros) defer apply(rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
+          apply(rule has_derivative_at_within) using assms(5) and `u\<in>s` `a\<in>s`
           by(auto intro!: has_derivative_intros derivative_linear)
-	have **:"bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)" apply(rule_tac[!] bounded_linear_sub)
-	  apply(rule_tac[!] derivative_linear) using assms(5) `u\<in>s` `a\<in>s` by auto
-	have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)" unfolding * apply(rule onorm_compose)
-	  unfolding linear_conv_bounded_linear by(rule assms(3) **)+ 
-	also have "\<dots> \<le> onorm g' * k" apply(rule mult_left_mono) 
-	  using d1[THEN conjunct2,rule_format,of u] using onorm_neg[OF **(1)[unfolded linear_linear]]
-	  using d and u and onorm_pos_le[OF assms(3)[unfolded linear_linear]] by(auto simp add:algebra_simps) 
-	also have "\<dots> \<le> 1/2" unfolding k_def by auto
-	finally show "onorm (\<lambda>v. v - g' (f' u v)) \<le> 1 / 2" by assumption qed
+        have **:"bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)" apply(rule_tac[!] bounded_linear_sub)
+          apply(rule_tac[!] derivative_linear) using assms(5) `u\<in>s` `a\<in>s` by auto
+        have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)" unfolding * apply(rule onorm_compose)
+          unfolding linear_conv_bounded_linear by(rule assms(3) **)+ 
+        also have "\<dots> \<le> onorm g' * k" apply(rule mult_left_mono) 
+          using d1[THEN conjunct2,rule_format,of u] using onorm_neg[OF **(1)[unfolded linear_linear]]
+          using d and u and onorm_pos_le[OF assms(3)[unfolded linear_linear]] by(auto simp add:algebra_simps) 
+        also have "\<dots> \<le> 1/2" unfolding k_def by auto
+        finally show "onorm (\<lambda>v. v - g' (f' u v)) \<le> 1 / 2" by assumption qed
       moreover have "norm (ph y - ph x) = norm (y - x)" apply(rule arg_cong[where f=norm])
-	unfolding ph_def using diff unfolding as by auto
+        unfolding ph_def using diff unfolding as by auto
       ultimately show "x = y" unfolding norm_minus_commute by auto qed qed auto qed
 
 subsection {* Uniformly convergent sequence of derivatives. *}
@@ -1066,9 +1066,9 @@
     fix x assume "x\<in>s" show "((\<lambda>a. f m a - f n a) has_derivative (\<lambda>h. f' m x h - f' n x h)) (at x within s)"
       by(rule has_derivative_intros assms(2)[rule_format] `x\<in>s`)+
     { fix h have "norm (f' m x h - f' n x h) \<le> norm (f' m x h - g' x h) + norm (f' n x h - g' x h)"
-	using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"] unfolding norm_minus_commute by(auto simp add:algebra_simps) 
+        using norm_triangle_ineq[of "f' m x h - g' x h" "- f' n x h + g' x h"] unfolding norm_minus_commute by(auto simp add:algebra_simps) 
       also have "\<dots> \<le> e * norm h+ e * norm h"  using assms(3)[rule_format,OF `N\<le>m` `x\<in>s`, of h] assms(3)[rule_format,OF `N\<le>n` `x\<in>s`, of h]
-	by(auto simp add:field_simps)
+        by(auto simp add:field_simps)
       finally have "norm (f' m x h - f' n x h) \<le> 2 * e * norm h" by auto }
     thus "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e" apply-apply(rule onorm(2)) apply(rule linear_compose_sub)
       unfolding linear_conv_bounded_linear using assms(2)[rule_format,OF `x\<in>s`, THEN derivative_linear] by auto qed qed
@@ -1092,66 +1092,66 @@
     fix x assume "x\<in>s" show "Cauchy (\<lambda>n. f n x)" proof(cases "x=x0")
       case True thus ?thesis using convergent_imp_cauchy[OF assms(5)] by auto next
       case False show ?thesis unfolding Cauchy_def proof(rule,rule)
-	fix e::real assume "e>0" hence *:"e/2>0" "e/2/norm(x-x0)>0" using False by(auto intro!:divide_pos_pos)
-	guess M using convergent_imp_cauchy[OF assms(5), unfolded Cauchy_def, rule_format,OF *(1)] .. note M=this
-	guess N using lem1[rule_format,OF *(2)] .. note N = this
-	show " \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" apply(rule_tac x="max M N" in exI) proof(default+)
-	  fix m n assume as:"max M N \<le>m" "max M N\<le>n"
-	  have "dist (f m x) (f n x) \<le> norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))"
-	    unfolding dist_norm by(rule norm_triangle_sub)
-	  also have "\<dots> \<le> norm (f m x0 - f n x0) + e / 2" using N[rule_format,OF _ _ `x\<in>s` `x0\<in>s`, of m n] and as and False by auto
-	  also have "\<dots> < e / 2 + e / 2" apply(rule add_strict_right_mono) using as and M[rule_format] unfolding dist_norm by auto 
-	  finally show "dist (f m x) (f n x) < e" by auto qed qed qed qed
+        fix e::real assume "e>0" hence *:"e/2>0" "e/2/norm(x-x0)>0" using False by(auto intro!:divide_pos_pos)
+        guess M using convergent_imp_cauchy[OF assms(5), unfolded Cauchy_def, rule_format,OF *(1)] .. note M=this
+        guess N using lem1[rule_format,OF *(2)] .. note N = this
+        show " \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" apply(rule_tac x="max M N" in exI) proof(default+)
+          fix m n assume as:"max M N \<le>m" "max M N\<le>n"
+          have "dist (f m x) (f n x) \<le> norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))"
+            unfolding dist_norm by(rule norm_triangle_sub)
+          also have "\<dots> \<le> norm (f m x0 - f n x0) + e / 2" using N[rule_format,OF _ _ `x\<in>s` `x0\<in>s`, of m n] and as and False by auto
+          also have "\<dots> < e / 2 + e / 2" apply(rule add_strict_right_mono) using as and M[rule_format] unfolding dist_norm by auto 
+          finally show "dist (f m x) (f n x) < e" by auto qed qed qed qed
   then guess g .. note g = this
   have lem2:"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm((f n x - f n y) - (g x - g y)) \<le> e * norm(x - y)" proof(rule,rule)
     fix e::real assume *:"e>0" guess N using lem1[rule_format,OF *] .. note N=this
     show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)" apply(rule_tac x=N in exI) proof(default+)
       fix n x y assume as:"N \<le> n" "x \<in> s" "y \<in> s"
       have "eventually (\<lambda>xa. norm (f n x - f n y - (f xa x - f xa y)) \<le> e * norm (x - y)) sequentially" 
-	unfolding eventually_sequentially apply(rule_tac x=N in exI) proof(rule,rule)
-	fix m assume "N\<le>m" thus "norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)"
-	  using N[rule_format, of n m x y] and as by(auto simp add:algebra_simps) qed
+        unfolding eventually_sequentially apply(rule_tac x=N in exI) proof(rule,rule)
+        fix m assume "N\<le>m" thus "norm (f n x - f n y - (f m x - f m y)) \<le> e * norm (x - y)"
+          using N[rule_format, of n m x y] and as by(auto simp add:algebra_simps) qed
       thus "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)" apply-
-	apply(rule Lim_norm_ubound[OF trivial_limit_sequentially, where f="\<lambda>m. (f n x - f n y) - (f m x - f m y)"])
-	apply(rule Lim_sub Lim_const g[rule_format] as)+ by assumption qed qed
+        apply(rule Lim_norm_ubound[OF trivial_limit_sequentially, where f="\<lambda>m. (f n x - f n y) - (f m x - f m y)"])
+        apply(rule Lim_sub Lim_const g[rule_format] as)+ by assumption qed qed
   show ?thesis unfolding has_derivative_within_alt apply(rule_tac x=g in exI)
     apply(rule,rule,rule g[rule_format],assumption) proof fix x assume "x\<in>s"
     have lem3:"\<forall>u. ((\<lambda>n. f' n x u) ---> g' x u) sequentially" unfolding Lim_sequentially proof(rule,rule,rule)
       fix u and e::real assume "e>0" show "\<exists>N. \<forall>n\<ge>N. dist (f' n x u) (g' x u) < e" proof(cases "u=0")
-	case True guess N using assms(3)[rule_format,OF `e>0`] .. note N=this
-	show ?thesis apply(rule_tac x=N in exI) unfolding True 
-	  using N[rule_format,OF _ `x\<in>s`,of _ 0] and `e>0` by auto next
-	case False hence *:"e / 2 / norm u > 0" using `e>0` by(auto intro!: divide_pos_pos)
-	guess N using assms(3)[rule_format,OF *] .. note N=this
-	show ?thesis apply(rule_tac x=N in exI) proof(rule,rule) case goal1
-	  show ?case unfolding dist_norm using N[rule_format,OF goal1 `x\<in>s`, of u] False `e>0`
-	    by (auto simp add:field_simps) qed qed qed
+        case True guess N using assms(3)[rule_format,OF `e>0`] .. note N=this
+        show ?thesis apply(rule_tac x=N in exI) unfolding True 
+          using N[rule_format,OF _ `x\<in>s`,of _ 0] and `e>0` by auto next
+        case False hence *:"e / 2 / norm u > 0" using `e>0` by(auto intro!: divide_pos_pos)
+        guess N using assms(3)[rule_format,OF *] .. note N=this
+        show ?thesis apply(rule_tac x=N in exI) proof(rule,rule) case goal1
+          show ?case unfolding dist_norm using N[rule_format,OF goal1 `x\<in>s`, of u] False `e>0`
+            by (auto simp add:field_simps) qed qed qed
     show "bounded_linear (g' x)" unfolding linear_linear linear_def apply(rule,rule,rule) defer proof(rule,rule)
       fix x' y z::"'m" and c::real
       note lin = assms(2)[rule_format,OF `x\<in>s`,THEN derivative_linear]
       show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'" apply(rule Lim_unique[OF trivial_limit_sequentially])
-	apply(rule lem3[rule_format])
+        apply(rule lem3[rule_format])
         unfolding lin[unfolded bounded_linear_def bounded_linear_axioms_def,THEN conjunct2,THEN conjunct1,rule_format]
-	apply(rule Lim_cmul) by(rule lem3[rule_format])
+        apply(rule Lim_cmul) by(rule lem3[rule_format])
       show "g' x (y + z) = g' x y + g' x z" apply(rule Lim_unique[OF trivial_limit_sequentially])
-	apply(rule lem3[rule_format]) unfolding lin[unfolded bounded_linear_def additive_def,THEN conjunct1,rule_format]
+        apply(rule lem3[rule_format]) unfolding lin[unfolded bounded_linear_def additive_def,THEN conjunct1,rule_format]
         apply(rule Lim_add) by(rule lem3[rule_format])+ qed 
     show "\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm (y - x) < d \<longrightarrow> norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)" proof(rule,rule) case goal1
       have *:"e/3>0" using goal1 by auto guess N1 using assms(3)[rule_format,OF *] .. note N1=this
       guess N2 using lem2[rule_format,OF *] .. note N2=this
       guess d1 using assms(2)[unfolded has_derivative_within_alt, rule_format,OF `x\<in>s`, of "max N1 N2",THEN conjunct2,rule_format,OF *] .. note d1=this
       show ?case apply(rule_tac x=d1 in exI) apply(rule,rule d1[THEN conjunct1]) proof(rule,rule)
-	fix y assume as:"y \<in> s" "norm (y - x) < d1" let ?N ="max N1 N2"
-	have "norm (g y - g x - (f ?N y - f ?N x)) \<le> e /3 * norm (y - x)" apply(subst norm_minus_cancel[THEN sym])
-	  using N2[rule_format, OF _ `y\<in>s` `x\<in>s`, of ?N] by auto moreover
-	have "norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)" using d1 and as by auto ultimately
-	have "norm (g y - g x - f' ?N x (y - x)) \<le> 2 * e / 3 * norm (y - x)" 
-	  using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"] 
-	  by (auto simp add:algebra_simps) moreover
-	have " norm (f' ?N x (y - x) - g' x (y - x)) \<le> e / 3 * norm (y - x)" using N1 `x\<in>s` by auto
-	ultimately show "norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
-	  using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"] by(auto simp add:algebra_simps)
-	qed qed qed qed
+        fix y assume as:"y \<in> s" "norm (y - x) < d1" let ?N ="max N1 N2"
+        have "norm (g y - g x - (f ?N y - f ?N x)) \<le> e /3 * norm (y - x)" apply(subst norm_minus_cancel[THEN sym])
+          using N2[rule_format, OF _ `y\<in>s` `x\<in>s`, of ?N] by auto moreover
+        have "norm (f ?N y - f ?N x - f' ?N x (y - x)) \<le> e / 3 * norm (y - x)" using d1 and as by auto ultimately
+        have "norm (g y - g x - f' ?N x (y - x)) \<le> 2 * e / 3 * norm (y - x)" 
+          using norm_triangle_le[of "g y - g x - (f ?N y - f ?N x)" "f ?N y - f ?N x - f' ?N x (y - x)" "2 * e / 3 * norm (y - x)"] 
+          by (auto simp add:algebra_simps) moreover
+        have " norm (f' ?N x (y - x) - g' x (y - x)) \<le> e / 3 * norm (y - x)" using N1 `x\<in>s` by auto
+        ultimately show "norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
+          using norm_triangle_le[of "g y - g x - f' (max N1 N2) x (y - x)" "f' (max N1 N2) x (y - x) - g' x (y - x)"] by(auto simp add:algebra_simps)
+        qed qed qed qed
 
 subsection {* Can choose to line up antiderivatives if we want. *}
 
@@ -1174,9 +1174,9 @@
     fix e::real assume "0<e" guess  N using reals_Archimedean[OF `e>0`] .. note N=this 
     show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"  apply(rule_tac x=N in exI) proof(default+) case goal1
       have *:"inverse (real (Suc n)) \<le> e" apply(rule order_trans[OF _ N[THEN less_imp_le]])
-	using goal1(1) by(auto simp add:field_simps) 
+        using goal1(1) by(auto simp add:field_simps) 
       show ?case using f[rule_format,THEN conjunct2,OF goal1(2), of n, THEN spec[where x=h]] 
-	apply(rule order_trans) using N * apply(cases "h=0") by auto qed qed(insert f,auto) qed
+        apply(rule order_trans) using N * apply(cases "h=0") by auto qed qed(insert f,auto) qed
 
 subsection {* Differentiation of a series. *}
 
@@ -1220,12 +1220,12 @@
       fix y assume as:"y \<in> s" "0 < dist y x" "dist y x < e / (B * C * D)"
       have "norm (h (f' (y - x)) (g' (y - x))) \<le> norm (f' (y - x)) * norm (g' (y - x)) * B" using B by auto
       also have "\<dots> \<le> (norm (y - x) * C) * (D * norm (y - x)) * B" apply(rule mult_right_mono)
-	apply(rule mult_mono) using B C D by (auto simp add: field_simps intro!:mult_nonneg_nonneg)
+        apply(rule mult_mono) using B C D by (auto simp add: field_simps intro!:mult_nonneg_nonneg)
       also have "\<dots> = (B * C * D * norm (y - x)) * norm (y - x)" by(auto simp add:field_simps)
       also have "\<dots> < e * norm (y - x)" apply(rule mult_strict_right_mono)
-	using as(3)[unfolded dist_norm] and as(2) unfolding pos_less_divide_eq[OF bcd] by (auto simp add:field_simps)
+        using as(3)[unfolded dist_norm] and as(2) unfolding pos_less_divide_eq[OF bcd] by (auto simp add:field_simps)
       finally show "dist ((1 / norm (y - x)) *\<^sub>R h (f' (y - x)) (g' (y - x))) 0 < e"
-	unfolding dist_norm apply-apply(cases "y = x") by(auto simp add:field_simps) qed qed
+        unfolding dist_norm apply-apply(cases "y = x") by(auto simp add:field_simps) qed qed
   have "bounded_linear (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))"
     apply (rule bounded_linear_add)
     apply (rule bounded_linear_compose [OF h.bounded_linear_right `bounded_linear g'`])
diff -r d488ae70366d -r 5abc60a017e0 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Mar 13 21:41:44 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Mar 13 22:24:10 2011 +0100
@@ -48,8 +48,8 @@
     apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
     show "bounded_linear negatex" apply(rule bounded_linearI') unfolding Cart_eq 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 qed(insert x0, auto)
+        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 qed(insert x0, auto)
   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])
diff -r d488ae70366d -r 5abc60a017e0 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Mar 13 21:41:44 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Mar 13 22:24:10 2011 +0100
@@ -136,33 +136,33 @@
     case True show ?thesis proof(cases "x\<in>{a<..<b}")
       case True then guess d unfolding open_contains_ball_eq[OF open_interval,rule_format] ..
       thus ?thesis apply(rule_tac x=i in bexI,rule_tac x=x in exI,rule_tac x="min d e" in exI)
-	unfolding ab using interval_open_subset_closed[of a b] and e by fastsimp+ next
+        unfolding ab using interval_open_subset_closed[of a b] and e by fastsimp+ next
     case False then obtain k where "x$$k \<le> a$$k \<or> x$$k \<ge> b$$k" and k:"k<DIM('a)" unfolding mem_interval by(auto simp add:not_less) 
     hence "x$$k = a$$k \<or> x$$k = b$$k" using True unfolding ab and mem_interval apply(erule_tac x=k in allE) by auto
     hence "\<exists>x. ball x (e/2) \<subseteq> s \<inter> (\<Union>f)" proof(erule_tac disjE)
       let ?z = "x - (e/2) *\<^sub>R basis k" assume as:"x$$k = a$$k" have "ball ?z (e / 2) \<inter> i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE)
-	fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
-	hence "\<bar>(?z - y) $$ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
-	hence "y$$k < a$$k" using e[THEN conjunct1] k by(auto simp add:field_simps basis_component as)
-	hence "y \<notin> i" unfolding ab mem_interval not_all apply(rule_tac x=k in exI) using k by auto thus False using yi by auto qed
+        fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
+        hence "\<bar>(?z - y) $$ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
+        hence "y$$k < a$$k" using e[THEN conjunct1] k by(auto simp add:field_simps basis_component as)
+        hence "y \<notin> i" unfolding ab mem_interval not_all apply(rule_tac x=k in exI) using k by auto thus False using yi by auto qed
       moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof
-	fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R basis k)"
-	   apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R basis k"])
-	  unfolding norm_scaleR norm_basis by auto
-	also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps)
-	finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed
+        fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R basis k)"
+           apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R basis k"])
+          unfolding norm_scaleR norm_basis by auto
+        also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps)
+        finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed
       ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto
     next let ?z = "x + (e/2) *\<^sub>R basis k" assume as:"x$$k = b$$k" have "ball ?z (e / 2) \<inter> i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE)
-	fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
-	hence "\<bar>(?z - y) $$ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
-	hence "y$$k > b$$k" using e[THEN conjunct1] k by(auto simp add:field_simps as)
-	hence "y \<notin> i" unfolding ab mem_interval not_all using k by(rule_tac x=k in exI,auto) thus False using yi by auto qed
+        fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
+        hence "\<bar>(?z - y) $$ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
+        hence "y$$k > b$$k" using e[THEN conjunct1] k by(auto simp add:field_simps as)
+        hence "y \<notin> i" unfolding ab mem_interval not_all using k by(rule_tac x=k in exI,auto) thus False using yi by auto qed
       moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof
-	fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y + (e / 2) *\<^sub>R basis k)"
-	   apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R basis k"])
-	  unfolding norm_scaleR by auto
-	also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps)
-	finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed
+        fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y + (e / 2) *\<^sub>R basis k)"
+           apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R basis k"])
+          unfolding norm_scaleR by auto
+        also have "\<dots> < \<bar>e\<bar> / 2 + \<bar>e\<bar> / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps)
+        finally show "y\<in>ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed
       ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto qed 
     then guess x .. hence "x \<in> s \<inter> interior (\<Union>f)" unfolding lem1[where U="\<Union>f",THEN sym] using centre_in_ball e[THEN conjunct1] by auto
     thus ?thesis apply-apply(rule lem2,rule insert(3)) using insert(4) by auto qed qed qed qed note * = this
@@ -576,11 +576,11 @@
       apply(rule inter_interior_unions_intervals) apply(rule p open_interior ballI)+ proof(assumption,rule)
       fix k assume k:"k\<in>p" have *:"\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto
       show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<inter> interior k = {}" apply(rule *[of _ "interior (\<Union>(q k - {k}))"])
-	defer apply(subst Int_commute) apply(rule inter_interior_unions_intervals) proof- note qk=division_ofD[OF q(1)[OF k]]
-	show "finite (q k - {k})" "open (interior k)"  "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
-	show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" using qk(5) using q(2)[OF k] by auto
-	have *:"\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
-	  apply(rule subset_interior *)+ using k by auto qed qed qed auto qed
+        defer apply(subst Int_commute) apply(rule inter_interior_unions_intervals) proof- note qk=division_ofD[OF q(1)[OF k]]
+        show "finite (q k - {k})" "open (interior k)"  "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
+        show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" using qk(5) using q(2)[OF k] by auto
+        have *:"\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
+          apply(rule subset_interior *)+ using k by auto qed qed qed auto qed
 
 lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
   unfolding division_of_def by(metis bounded_Union bounded_interval)