1.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Sep 24 17:13:12 2013 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Sep 24 17:37:45 2013 +0200
     1.3 @@ -24,9 +24,10 @@
     1.4  
     1.5  (** move this **)
     1.6  lemma divide_nonneg_nonneg:
     1.7 +  fixes a b :: real
     1.8    assumes "a \<ge> 0"
     1.9      and "b \<ge> 0"
    1.10 -  shows "0 \<le> a / (b::real)"
    1.11 +  shows "0 \<le> a / b"
    1.12  proof (cases "b = 0")
    1.13    case True
    1.14    then show ?thesis by auto
    1.15 @@ -1390,7 +1391,8 @@
    1.16      fix x xa xb xc y
    1.17      assume as:
    1.18        "x = (\<lambda>(b, g) x. if x = a then b else g x) xa"
    1.19 -      "xb \<in> UNIV - insert a s0" "xa = (xc, y)"
    1.20 +      "xb \<in> UNIV - insert a s0"
    1.21 +      "xa = (xc, y)"
    1.22        "xc \<in> t"
    1.23        "\<forall>x\<in>s0. y x \<in> t"
    1.24        "\<forall>x\<in>UNIV - s0. y x = d"
    1.25 @@ -2220,7 +2222,7 @@
    1.26      ultimately have *: "?A = {s, insert a3 (s - {a0})}"
    1.27        by blast
    1.28      have "s \<noteq> insert a3 (s - {a0})"
    1.29 -      using `a3\<notin>s` by auto
    1.30 +      using `a3 \<notin> s` by auto
    1.31      then have ?thesis
    1.32        unfolding * by auto
    1.33    }
    1.34 @@ -3344,7 +3346,9 @@
    1.35      moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,symmetric]] ..
    1.36      then guess a ..
    1.37      ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and>
    1.38 -      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)
    1.39 +        a \<in> s \<and> f = s - {a} \<and>
    1.40 +        reduced lab (n + 1) ` f = {0..n} \<and>
    1.41 +        ((\<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))"
    1.42        apply (rule_tac x = s in exI)
    1.43        apply (rule_tac x = a in exI)
    1.44        unfolding complete_face_top[OF *]
    1.45 @@ -3354,7 +3358,8 @@
    1.46    next
    1.47      fix f
    1.48      assume as: "\<exists>s a. ksimplex p (n + 1) s \<and>
    1.49 -      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)
    1.50 +      a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and>
    1.51 +      ((\<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))"
    1.52      then guess s ..
    1.53      then guess a by (elim exE conjE) note sa = this
    1.54      {
    1.55 @@ -3447,7 +3452,7 @@
    1.56      and "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> x j = 0 \<longrightarrow> lab x j = 0"
    1.57      and "\<forall>x. \<forall>j\<in>{1..Suc n}. (\<forall>j. x j \<le> p) \<and> x j = p \<longrightarrow> lab x j = 1"
    1.58      and "odd (card {f. ksimplex p n f \<and> reduced lab n ` f = {0..n}})"
    1.59 -  shows "odd (card {s. ksimplex p (Suc n) s \<and> reduced lab (Suc n) `  s = {0..Suc n}})"
    1.60 +  shows "odd (card {s. ksimplex p (Suc n) s \<and> reduced lab (Suc n) ` s = {0..Suc n}})"
    1.61    using assms
    1.62    unfolding Suc_eq_plus1
    1.63    by (rule kuhn_induction)
    1.64 @@ -4255,7 +4260,7 @@
    1.65  
    1.66  lemma interval_bij_bij:
    1.67    "\<forall>(i::'a::ordered_euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow>
    1.68 -    interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
    1.69 +    interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x"
    1.70    by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])
    1.71  
    1.72  end