# HG changeset patch
# User wenzelm
# Date 1380037065 -7200
# Node ID 2e4b435e17bc001e5a28e2ee5a5995d43ca489db
# Parent  08721d7b22628e9688328b1863d383d3b52c7fa2
tuned proofs;

diff -r 08721d7b2262 -r 2e4b435e17bc src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Sep 24 17:13:12 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Sep 24 17:37:45 2013 +0200
@@ -24,9 +24,10 @@
 
 (** move this **)
 lemma divide_nonneg_nonneg:
+  fixes a b :: real
   assumes "a \<ge> 0"
     and "b \<ge> 0"
-  shows "0 \<le> a / (b::real)"
+  shows "0 \<le> a / b"
 proof (cases "b = 0")
   case True
   then show ?thesis by auto
@@ -1390,7 +1391,8 @@
     fix x xa xb xc y
     assume as:
       "x = (\<lambda>(b, g) x. if x = a then b else g x) xa"
-      "xb \<in> UNIV - insert a s0" "xa = (xc, y)"
+      "xb \<in> UNIV - insert a s0"
+      "xa = (xc, y)"
       "xc \<in> t"
       "\<forall>x\<in>s0. y x \<in> t"
       "\<forall>x\<in>UNIV - s0. y x = d"
@@ -2220,7 +2222,7 @@
     ultimately have *: "?A = {s, insert a3 (s - {a0})}"
       by blast
     have "s \<noteq> insert a3 (s - {a0})"
-      using `a3\<notin>s` by auto
+      using `a3 \<notin> s` by auto
     then have ?thesis
       unfolding * by auto
   }
@@ -3344,7 +3346,9 @@
     moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] ..
     then guess a ..
     ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and>
-      a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<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))" (is ?ex)
+        a \<in> s \<and> f = s - {a} \<and>
+        reduced lab (n + 1) ` f = {0..n} \<and>
+        ((\<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))"
       apply (rule_tac x = s in exI)
       apply (rule_tac x = a in exI)
       unfolding complete_face_top[OF *]
@@ -3354,7 +3358,8 @@
   next
     fix f
     assume as: "\<exists>s a. ksimplex p (n + 1) s \<and>
-      a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<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))" (is ?ex)
+      a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and>
+      ((\<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))"
     then guess s ..
     then guess a by (elim exE conjE) note sa = this
     {
@@ -3447,7 +3452,7 @@
     and "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
     and "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
     and "odd (card {f. ksimplex p n f \<and> reduced lab n ` f = {0..n}})"
-  shows "odd (card {s. ksimplex p (Suc n) s \<and> reduced lab (Suc n) `  s = {0..Suc n}})"
+  shows "odd (card {s. ksimplex p (Suc n) s \<and> reduced lab (Suc n) ` s = {0..Suc n}})"
   using assms
   unfolding Suc_eq_plus1
   by (rule kuhn_induction)
@@ -4255,7 +4260,7 @@
 
 lemma interval_bij_bij:
   "\<forall>(i::'a::ordered_euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow>
-    interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
+    interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x"
   by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])
 
 end