author wenzelm Tue, 24 Sep 2013 16:03:00 +0200 changeset 53842 b98c6cd90230 parent 53841 73536e119310 child 53843 88c6e630c15f
tuned proofs;
```--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Sep 24 14:14:49 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Sep 24 16:03:00 2013 +0200
@@ -2479,7 +2479,7 @@
and "(f has_integral k2) i"
shows "k1 = k2"
proof (rule ccontr)
-  let ?e = "norm(k1 - k2) / 2"
+  let ?e = "norm (k1 - k2) / 2"
assume as:"k1 \<noteq> k2"
then have e: "?e > 0"
by auto
@@ -5082,7 +5082,7 @@
and "\<forall>x\<in>s. (f x)\<bullet>k \<le> (g x)\<bullet>k"
shows "i\<bullet>k \<le> j\<bullet>k"
proof -
-  have lem:"\<And>a b i (j::'b). \<And>g f::'a \<Rightarrow> 'b. (f has_integral i) ({a..b}) \<Longrightarrow>
+  have lem: "\<And>a b i j::'b. \<And>g f::'a \<Rightarrow> 'b. (f has_integral i) {a..b} \<Longrightarrow>
(g has_integral j) ({a..b}) \<Longrightarrow> \<forall>x\<in>{a..b}. (f x)\<bullet>k \<le> (g x)\<bullet>k \<Longrightarrow> i\<bullet>k \<le> j\<bullet>k"
proof (rule ccontr)
case goal1
@@ -7345,7 +7345,8 @@
by auto
have same: "(x, k) = (x', k')"
apply -
-          apply (rule ccontr,drule p(5)[OF xk xk'])
+          apply (rule ccontr)
+          apply (drule p(5)[OF xk xk'])
proof -
assume as: "interior k \<inter> interior k' = {}"
from nonempty_witness[OF *] guess z .
@@ -8037,7 +8038,7 @@
using p(2-3)[OF goal1(1)] unfolding uv by auto
have "u \<ge> a"
using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto
-                moreover assume "u \<noteq> a"
+                moreover assume "\<not> ?thesis"
ultimately have "u > a" by auto
then show False
using p(2)[OF goal1(1)] unfolding uv by (auto simp add:)
@@ -8061,7 +8062,7 @@
using p(2-3)[OF goal1(1)] unfolding uv by auto
have "v \<le> b"
using p(2-3)[OF goal1(1)] unfolding uv subset_eq by auto
-                moreover assume "v \<noteq> b"
+                moreover assume "\<not> ?thesis"
ultimately have "v < b" by auto
then show False
using p(2)[OF goal1(1)] unfolding uv by (auto simp add:)
@@ -8098,7 +8099,7 @@
apply auto
done
{ assume "x \<in> k" then show "x \<in> k'" unfolding * . }
-              { assume "x \<in> k'" then show "x\<in>k" unfolding * . }
+              { assume "x \<in> k'" then show "x \<in> k" unfolding * . }
qed
show "\<forall>x y. x \<in> ?B b \<and> y \<in> ?B b \<longrightarrow> x = y"
apply rule
@@ -8473,7 +8474,7 @@
unfolding subset_eq
apply (erule_tac x="c + ((k + w)/2)" in ballE)
unfolding d_def
-        using `k>0` `w>0`
+        using `k > 0` `w > 0`
apply (auto simp add: field_simps not_le not_less dist_real_def)
done
ultimately show ?thesis using `t < c`
@@ -11788,7 +11789,7 @@
case goal2
have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> i - e"
proof (rule ccontr)
-      case goal1
+      assume "\<not> ?thesis"
then have "i \<le> i - e"
apply -
apply (rule isLub_le_isUb[OF i])
@@ -12451,7 +12452,7 @@

have "\<exists>y\<in>?S. \<not> y \<ge> i + r"
proof(rule ccontr)
-        case goal1
+        assume "\<not> ?thesis"
then have "i \<ge> i + r"
apply -
apply (rule isGlb_le_isLb[OF i])
@@ -12554,7 +12555,7 @@

have "\<exists>y\<in>?S. \<not> y \<le> i - r"
proof (rule ccontr)
-        case goal1
+        assume "\<not> ?thesis"
then have "i \<le> i - r"
apply -
apply (rule isLub_le_isUb[OF i])```
```--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 24 14:14:49 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 24 16:03:00 2013 +0200
@@ -165,7 +165,7 @@

lemma norm_triangle_half_l:
assumes "norm (x - y) < e / 2"
-    and "norm (x' - (y)) < e / 2"
+    and "norm (x' - y) < e / 2"
shows "norm (x - x') < e"
using dist_triangle_half_l[OF assms[unfolded dist_norm[symmetric]]]
unfolding dist_norm[symmetric] .
@@ -227,17 +227,17 @@
context real_inner
begin

-definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)"
+definition "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"

lemma orthogonal_clauses:
"orthogonal a 0"
"orthogonal a x \<Longrightarrow> orthogonal a (c *\<^sub>R x)"
-  "orthogonal a x \<Longrightarrow> orthogonal a (-x)"
+  "orthogonal a x \<Longrightarrow> orthogonal a (- x)"
"orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x + y)"
"orthogonal a x \<Longrightarrow> orthogonal a y \<Longrightarrow> orthogonal a (x - y)"
"orthogonal 0 a"
"orthogonal x a \<Longrightarrow> orthogonal (c *\<^sub>R x) a"
-  "orthogonal x a \<Longrightarrow> orthogonal (-x) a"
+  "orthogonal x a \<Longrightarrow> orthogonal (- x) a"
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x + y) a"
"orthogonal x a \<Longrightarrow> orthogonal y a \<Longrightarrow> orthogonal (x - y) a"
unfolding orthogonal_def inner_add inner_diff by auto```