author wenzelm Tue, 24 Sep 2013 17:37:45 +0200 changeset 53846 2e4b435e17bc parent 53845 08721d7b2262 child 53847 104a08c2be9f
tuned proofs;
```--- 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```