author huffman Mon Apr 26 09:21:25 2010 -0700 (2010-04-26) changeset 36362 06475a1547cb parent 36361 1debc8e29f6a child 36363 ebaa558fc698
fix lots of looping simp calls and other warnings
```     1.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Apr 25 23:22:29 2010 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 26 09:21:25 2010 -0700
1.3 @@ -22,8 +22,6 @@
1.4    imports Convex_Euclidean_Space
1.5  begin
1.6
1.7 -declare norm_scaleR[simp]
1.8 -
1.9  lemma brouwer_compactness_lemma:
1.10    assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = (0::real^'n)))"
1.11    obtains d where "0 < d" "\<forall>x\<in>s. d \<le> norm(f x)" proof(cases "s={}") case False
1.12 @@ -131,7 +129,7 @@
1.13  lemma image_lemma_2: assumes "finite s" "finite t" "card s = card t" "f ` s \<subseteq> t" "f ` s \<noteq> t" "b \<in> t"
1.14    shows "(card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0) \<or>
1.15           (card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 2)" proof(cases "{a\<in>s. f ` (s - {a}) = t - {b}} = {}")
1.16 -  case True thus ?thesis apply-apply(rule disjI1, rule image_lemma_0) using assms(1) by(auto simp add:card_0_eq)
1.17 +  case True thus ?thesis apply-apply(rule disjI1, rule image_lemma_0) using assms(1) by auto
1.18  next let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}"
1.19    case False then obtain a where "a\<in>?M" by auto hence a:"a\<in>s" "f ` (s - {a}) = t - {b}" by auto
1.20    have "f a \<in> t - {b}" using a and assms by auto
1.21 @@ -1691,11 +1689,11 @@
1.22        path_image(linepath(pathfinish g)(vector[(pathfinish g)\$1,a\$2 - 1])) \<union>
1.23        path_image(linepath(vector[(pathfinish g)\$1,a\$2 - 1])(vector[b\$1 + 1,a\$2 - 1])) \<union>
1.24        path_image(linepath(vector[b\$1 + 1,a\$2 - 1])(vector[b\$1 + 1,b\$2 + 3]))" using assms(1-2)
1.25 -      by(auto simp add: pathstart_join pathfinish_join path_image_join path_image_linepath path_join path_linepath)
1.26 +      by(auto simp add: path_image_join path_linepath)
1.27    have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_le_def forall_2 vector_2)
1.28    guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
1.29      unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
1.30 -    show "path ?P1" "path ?P2" using assms by(auto simp add: pathstart_join pathfinish_join path_join)
1.31 +    show "path ?P1" "path ?P2" using assms by auto
1.32      have "path_image ?P1 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 3
1.33        apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
1.34        unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(3)
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun Apr 25 23:22:29 2010 -0700
2.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Apr 26 09:21:25 2010 -0700
2.3 @@ -24,7 +24,7 @@
2.4  lemma dest_vec1_simps[simp]: fixes a::"real^1"
2.5    shows "a\$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
2.6    "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
2.7 -  by(auto simp add:vector_component_simps forall_1 Cart_eq)
2.8 +  by(auto simp add: vector_le_def Cart_eq)
2.9
2.10  lemma norm_not_0:"(x::real^'n)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
2.11
2.12 @@ -50,7 +50,7 @@
2.13  lemma mem_interval_1: fixes x :: "real^1" shows
2.14   "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
2.15   "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
2.16 -by(simp_all add: Cart_eq vector_less_def vector_le_def forall_1)
2.17 +by(simp_all add: Cart_eq vector_less_def vector_le_def)
2.18
2.19  lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n)) ` {a..b} =
2.20    (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
2.21 @@ -66,8 +66,7 @@
2.22    apply(rule_tac [!] allI)apply(rule_tac [!] impI)
2.23    apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
2.24    apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
2.25 -  by (auto simp add: vector_less_def vector_le_def forall_1
2.26 -    vec1_dest_vec1[unfolded One_nat_def])
2.27 +  by (auto simp add: vector_less_def vector_le_def)
2.28
2.29  lemma dest_vec1_setsum: assumes "finite S"
2.30    shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
2.31 @@ -90,7 +89,7 @@
2.32    using one_le_card_finite by auto
2.33
2.34  lemma real_dimindex_ge_1:"real (CARD('n::finite)) \<ge> 1"
2.35 -  by(metis dimindex_ge_1 linorder_not_less real_eq_of_nat real_le_trans real_of_nat_1 real_of_nat_le_iff)
2.36 +  by(metis dimindex_ge_1 real_eq_of_nat real_of_nat_1 real_of_nat_le_iff)
2.37
2.38  lemma real_dimindex_gt_0:"real (CARD('n::finite)) > 0" apply(rule less_le_trans[OF _ real_dimindex_ge_1]) by auto
2.39
2.40 @@ -480,8 +479,8 @@
2.41  next
2.42    fix t u assume asm:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s" "finite (t::'a set)"
2.43    (*"finite t" "t \<subseteq> s" "\<forall>x\<in>t. (0::real) \<le> u x" "setsum u t = 1"*)
2.44 -  from this(2) have "\<forall>u. t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" apply(induct_tac t rule:finite_induct)
2.45 -    prefer 3 apply (rule,rule) apply(erule conjE)+ proof-
2.46 +  from this(2) have "\<forall>u. t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" apply(induct t rule:finite_induct)
2.47 +    prefer 2 apply (rule,rule) apply(erule conjE)+ proof-
2.48      fix x f u assume ind:"\<forall>u. f \<subseteq> s \<and> (\<forall>x\<in>f. 0 \<le> u x) \<and> setsum u f = 1 \<longrightarrow> (\<Sum>x\<in>f. u x *\<^sub>R x) \<in> s"
2.49      assume as:"finite f" "x \<notin> f" "insert x f \<subseteq> s" "\<forall>x\<in>insert x f. 0 \<le> u x" "setsum u (insert x f) = (1::real)"
2.50      show "(\<Sum>x\<in>insert x f. u x *\<^sub>R x) \<in> s" proof(cases "u x = 1")
2.51 @@ -776,7 +775,7 @@
2.52  lemma convex_cball:
2.53    fixes x :: "'a::real_normed_vector"
2.54    shows "convex(cball x e)"
2.55 -proof(auto simp add: convex_def Ball_def mem_cball)
2.56 +proof(auto simp add: convex_def Ball_def)
2.57    fix y z assume yz:"dist x y \<le> e" "dist x z \<le> e"
2.58    fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1"
2.59    have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz
2.60 @@ -1144,7 +1143,7 @@
2.61      hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1]
2.62        apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE)
2.63        apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto  }
2.64 -  thus ?thesis unfolding convex_def cone_def by auto
2.65 +  thus ?thesis unfolding convex_def cone_def by blast
2.66  qed
2.67
2.68  lemma affine_dependent_biggerset: fixes s::"(real^'n) set"
2.69 @@ -1259,7 +1258,7 @@
2.70    fixes s :: "'a::real_normed_vector set"
2.71    assumes "open s"
2.72    shows "open(convex hull s)"
2.73 -  unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10)
2.74 +  unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10)
2.75  proof(rule, rule) fix a
2.76    assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a"
2.77    then obtain t u where obt:"finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a" by auto
2.78 @@ -1279,7 +1278,7 @@
2.79        hence "Min i \<le> b x" unfolding i_def apply(rule_tac Min_le) using obt(1) by auto
2.80        hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_norm by auto
2.81        moreover from `x\<in>t` have "x\<in>s" using obt(2) by auto
2.82 -      ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by auto }
2.83 +      ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by fast }
2.84      moreover
2.85      have *:"inj_on (\<lambda>v. v + (y - a)) t" unfolding inj_on_def by auto
2.86      have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a))) = 1"
2.87 @@ -1349,7 +1348,7 @@
2.88    show ?thesis unfolding caratheodory[of s]
2.89    proof(induct ("CARD('n) + 1"))
2.90      have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}"
2.91 -      using compact_empty by (auto simp add: convex_hull_empty)
2.92 +      using compact_empty by auto
2.93      case 0 thus ?case unfolding * by simp
2.94    next
2.95      case (Suc n)
2.96 @@ -1359,11 +1358,11 @@
2.97          fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
2.98          then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto
2.99          show "x\<in>s" proof(cases "card t = 0")
2.100 -          case True thus ?thesis using t(4) unfolding card_0_eq[OF t(1)] by(simp add: convex_hull_empty)
2.101 +          case True thus ?thesis using t(4) unfolding card_0_eq[OF t(1)] by simp
2.102          next
2.103            case False hence "card t = Suc 0" using t(3) `n=0` by auto
2.104            then obtain a where "t = {a}" unfolding card_Suc_eq by auto
2.105 -          thus ?thesis using t(2,4) by (simp add: convex_hull_singleton)
2.106 +          thus ?thesis using t(2,4) by simp
2.107          qed
2.108        next
2.109          fix x assume "x\<in>s"
2.110 @@ -1398,7 +1397,7 @@
2.111            show ?P proof(cases "u={}")
2.112              case True hence "x=a" using t(4)[unfolded au] by auto
2.113              show ?P unfolding `x=a` apply(rule_tac x=a in exI, rule_tac x=a in exI, rule_tac x=1 in exI)
2.114 -              using t and `n\<noteq>0` unfolding au by(auto intro!: exI[where x="{a}"] simp add: convex_hull_singleton)
2.115 +              using t and `n\<noteq>0` unfolding au by(auto intro!: exI[where x="{a}"])
2.116            next
2.117              case False obtain ux vx b where obt:"ux\<ge>0" "vx\<ge>0" "ux + vx = 1" "b \<in> convex hull u" "x = ux *\<^sub>R a + vx *\<^sub>R b"
2.118                using t(4)[unfolded au convex_hull_insert[OF False]] by auto
2.119 @@ -1411,7 +1410,7 @@
2.120        qed
2.121        thus ?thesis using compact_convex_combinations[OF assms Suc] by simp
2.122      qed
2.123 -  qed
2.124 +  qed
2.125  qed
2.126
2.127  lemma finite_imp_compact_convex_hull:
2.128 @@ -1851,7 +1850,7 @@
2.129  lemma convex_hull_scaling:
2.130    "convex hull ((\<lambda>x. c *\<^sub>R x) ` s) = (\<lambda>x. c *\<^sub>R x) ` (convex hull s)"
2.131    apply(cases "c=0") defer apply(rule convex_hull_bilemma[rule_format, of _ _ inverse]) apply(rule convex_hull_scaling_lemma)
2.132 -  unfolding image_image scaleR_scaleR by(auto simp add:image_constant_conv convex_hull_eq_empty)
2.133 +  unfolding image_image scaleR_scaleR by(auto simp add:image_constant_conv)
2.134
2.135  lemma convex_hull_affinity:
2.136    "convex hull ((\<lambda>x. a + c *\<^sub>R x) ` s) = (\<lambda>x. a + c *\<^sub>R x) ` (convex hull s)"
2.137 @@ -2313,7 +2312,7 @@
2.138      hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: ring_simps)
2.139      hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) }
2.140    ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
2.141 -    using as(3-) dimindex_ge_1 apply- by(auto simp add: vector_component) qed
2.142 +    using as(3-) dimindex_ge_1 by auto qed
2.143
2.144  lemma is_interval_connected:
2.145    fixes s :: "(real ^ _) set"
2.146 @@ -2336,7 +2335,7 @@
2.147    hence *:"dest_vec1 a < dest_vec1 x" "dest_vec1 x < dest_vec1 b" apply(rule_tac [!] ccontr) unfolding not_less by auto
2.148    let ?halfl = "{z. inner (basis 1) z < dest_vec1 x} " and ?halfr = "{z. inner (basis 1) z > dest_vec1 x} "
2.149    { fix y assume "y \<in> s" have "y \<in> ?halfr \<union> ?halfl" apply(rule ccontr)
2.150 -    using as(6) `y\<in>s` by (auto simp add: inner_vector_def dest_vec1_eq) }
2.151 +    using as(6) `y\<in>s` by (auto simp add: inner_vector_def) }
2.152    moreover have "a\<in>?halfl" "b\<in>?halfr" using * by (auto simp add: inner_vector_def)
2.153    hence "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}"  using as(2-3) by auto
2.154    ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]])
2.155 @@ -2374,7 +2373,7 @@
2.156    shows "\<exists>x\<in>{a..b}. (f x)\$k = y"
2.157    apply(subst neg_equal_iff_equal[THEN sym]) unfolding vector_uminus_component[THEN sym]
2.158    apply(rule ivt_increasing_component_on_1) using assms using continuous_on_neg
2.160 +  by auto
2.161
2.162  lemma ivt_decreasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
2.163    shows "dest_vec1 a \<le> dest_vec1 b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
2.164 @@ -2415,7 +2414,7 @@
2.165          unfolding i'(1) xi_def apply(rule_tac Min_le) unfolding image_iff
2.166          defer apply(rule_tac x=j in bexI) using i' by auto
2.167        have i01:"x\$i \<le> 1" "x\$i > 0" using Suc(2)[unfolded mem_interval,rule_format,of i] using i'(2) `x\$i \<noteq> 0`
2.168 -        by(auto simp add: Cart_lambda_beta)
2.169 +        by auto
2.170        show ?thesis proof(cases "x\$i=1")
2.171          case True have "\<forall>j\<in>{i. x\$i \<noteq> 0}. x\$j = 1" apply(rule, rule ccontr) unfolding mem_Collect_eq proof-
2.172            fix j assume "x \$ j \<noteq> 0" "x \$ j \<noteq> 1"
2.173 @@ -2424,21 +2423,21 @@
2.174            hence "x\$j \<ge> x\$i" unfolding i'(1) xi_def apply(rule_tac Min_le) by auto
2.175            thus False using True Suc(2) j by(auto simp add: vector_le_def elim!:ballE[where x=j]) qed
2.176          thus "x\<in>convex hull ?points" apply(rule_tac hull_subset[unfolded subset_eq, rule_format])
2.177 -          by(auto simp add: Cart_lambda_beta)
2.178 +          by auto
2.179        next let ?y = "\<lambda>j. if x\$j = 0 then 0 else (x\$j - x\$i) / (1 - x\$i)"
2.180          case False hence *:"x = x\$i *\<^sub>R (\<chi> j. if x\$j = 0 then 0 else 1) + (1 - x\$i) *\<^sub>R (\<chi> j. ?y j)" unfolding Cart_eq
2.182 +          by(auto simp add: field_simps)
2.183          { fix j have "x\$j \<noteq> 0 \<Longrightarrow> 0 \<le> (x \$ j - x \$ i) / (1 - x \$ i)" "(x \$ j - x \$ i) / (1 - x \$ i) \<le> 1"
2.184              apply(rule_tac divide_nonneg_pos) using i(1)[of j] using False i01
2.185 -            using Suc(2)[unfolded mem_interval, rule_format, of j] by(auto simp add:field_simps Cart_lambda_beta)
2.186 +            using Suc(2)[unfolded mem_interval, rule_format, of j] by(auto simp add:field_simps)
2.187            hence "0 \<le> ?y j \<and> ?y j \<le> 1" by auto }
2.188 -        moreover have "i\<in>{j. x\$j \<noteq> 0} - {j. ((\<chi> j. ?y j)::real^'n) \$ j \<noteq> 0}" using i01 by(auto simp add: Cart_lambda_beta)
2.189 +        moreover have "i\<in>{j. x\$j \<noteq> 0} - {j. ((\<chi> j. ?y j)::real^'n) \$ j \<noteq> 0}" using i01 by auto
2.190          hence "{j. x\$j \<noteq> 0} \<noteq> {j. ((\<chi> j. ?y j)::real^'n) \$ j \<noteq> 0}" by auto
2.191 -        hence **:"{j. ((\<chi> j. ?y j)::real^'n) \$ j \<noteq> 0} \<subset> {j. x\$j \<noteq> 0}" apply - apply rule by(auto simp add: Cart_lambda_beta)
2.192 +        hence **:"{j. ((\<chi> j. ?y j)::real^'n) \$ j \<noteq> 0} \<subset> {j. x\$j \<noteq> 0}" apply - apply rule by auto
2.193          have "card {j. ((\<chi> j. ?y j)::real^'n) \$ j \<noteq> 0} \<le> n" using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto
2.194          ultimately show ?thesis apply(subst *) apply(rule convex_convex_hull[unfolded convex_def, rule_format])
2.195            apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) defer apply(rule Suc(1))
2.196 -          unfolding mem_interval using i01 Suc(3) by (auto simp add: Cart_lambda_beta)
2.197 +          unfolding mem_interval using i01 Suc(3) by auto
2.198        qed qed qed } note * = this
2.199    show ?thesis apply rule defer apply(rule hull_minimal) unfolding subset_eq prefer 3 apply rule
2.200      apply(rule_tac n2="CARD('n)" in *) prefer 3 apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule
2.201 @@ -2453,7 +2452,7 @@
2.202    prefer 3 apply(rule unit_interval_convex_hull) apply rule unfolding mem_Collect_eq proof-
2.203    fix x::"real^'n" assume as:"\<forall>i. x \$ i = 0 \<or> x \$ i = 1"
2.204    show "x \<in> (\<lambda>s. \<chi> i. if i \<in> s then 1 else 0) ` UNIV" apply(rule image_eqI[where x="{i. x\$i = 1}"])
2.205 -    unfolding Cart_eq using as by(auto simp add:Cart_lambda_beta) qed auto
2.206 +    unfolding Cart_eq using as by auto qed auto
2.207
2.208  subsection {* Hence any cube (could do any nonempty interval). *}
2.209
2.210 @@ -2464,23 +2463,23 @@
2.211      unfolding image_iff defer apply(erule bexE) proof-
2.212      fix y assume as:"y\<in>{x - ?d .. x + ?d}"
2.213      { fix i::'n have "x \$ i \<le> d + y \$ i" "y \$ i \<le> d + x \$ i" using as[unfolded mem_interval, THEN spec[where x=i]]
2.214 -        by(auto simp add: vector_component)
2.215 +        by auto
2.216        hence "1 \<ge> inverse d * (x \$ i - y \$ i)" "1 \<ge> inverse d * (y \$ i - x \$ i)"
2.217          apply(rule_tac[!] mult_left_le_imp_le[OF _ assms]) unfolding mult_assoc[THEN sym]
2.218 -        using assms by(auto simp add: field_simps right_inverse)
2.219 +        using assms by(auto simp add: field_simps)
2.220        hence "inverse d * (x \$ i * 2) \<le> 2 + inverse d * (y \$ i * 2)"
2.221              "inverse d * (y \$ i * 2) \<le> 2 + inverse d * (x \$ i * 2)" by(auto simp add:field_simps) }
2.222      hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..1}" unfolding mem_interval using assms
2.223 -      by(auto simp add: Cart_eq vector_component_simps field_simps)
2.224 +      by(auto simp add: Cart_eq field_simps)
2.225      thus "\<exists>z\<in>{0..1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
2.226 -      using assms by(auto simp add: Cart_eq vector_le_def Cart_lambda_beta)
2.227 +      using assms by(auto simp add: Cart_eq vector_le_def)
2.228    next
2.229      fix y z assume as:"z\<in>{0..1}" "y = x - ?d + (2*d) *\<^sub>R z"
2.230      have "\<And>i. 0 \<le> d * z \$ i \<and> d * z \$ i \<le> d" using assms as(1)[unfolded mem_interval] apply(erule_tac x=i in allE)
2.231        apply rule apply(rule mult_nonneg_nonneg) prefer 3 apply(rule mult_right_le_one_le)
2.232 -      using assms by(auto simp add: vector_component_simps Cart_eq)
2.233 +      using assms by(auto simp add: Cart_eq)
2.234      thus "y \<in> {x - ?d..x + ?d}" unfolding as(2) mem_interval apply- apply rule using as(1)[unfolded mem_interval]
2.235 -      apply(erule_tac x=i in allE) using assms by(auto simp add:  vector_component_simps Cart_eq) qed
2.236 +      apply(erule_tac x=i in allE) using assms by(auto simp add: Cart_eq) qed
2.237    obtain s where "finite s" "{0..1::real^'n} = convex hull s" using unit_cube_convex_hull by auto
2.238    thus ?thesis apply(rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"]) unfolding * and convex_hull_affinity by auto qed
2.239
2.240 @@ -2570,8 +2569,8 @@
2.241    have "0 < d" unfolding d_def using `e>0` dimge1 by(rule_tac divide_pos_pos, auto)
2.242    let ?d = "(\<chi> i. d)::real^'n"
2.243    obtain c where c:"finite c" "{x - ?d..x + ?d} = convex hull c" using cube_convex_hull[OF `d>0`, of x] by auto
2.244 -  have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by(auto simp add:vector_component_simps)
2.245 -  hence "c\<noteq>{}" using c by(auto simp add:convex_hull_empty)
2.246 +  have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by auto
2.247 +  hence "c\<noteq>{}" using c by auto
2.248    def k \<equiv> "Max (f ` c)"
2.249    have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)])
2.250      apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof
2.251 @@ -2579,7 +2578,7 @@
2.252      have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1
2.253        by (metis eq_divide_imp mult_frac_num real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute)
2.254      show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
2.255 -      using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:field_simps vector_component_simps) qed
2.256 +      using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed
2.257    hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
2.258      unfolding k_def apply(rule, rule Max_ge) using c(1) by auto
2.259    have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 using real_dimindex_ge_1 by auto
2.260 @@ -2588,9 +2587,9 @@
2.261    hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof
2.262      fix y assume y:"y\<in>cball x d"
2.263      { fix i::'n have "x \$ i - d \<le> y \$ i"  "y \$ i \<le> x \$ i + d"
2.264 -        using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by(auto simp add: vector_component)  }
2.265 +        using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by auto  }
2.266      thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm
2.267 -      by(auto simp add: vector_component_simps) qed
2.268 +      by auto qed
2.269    hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
2.270      apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
2.271      apply force
2.272 @@ -2716,17 +2715,17 @@
2.273          unfolding as(1) by(auto simp add:algebra_simps)
2.274        show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)"
2.275          unfolding norm_minus_commute[of x a] * Cart_eq using as(2,3)
2.276 -        by(auto simp add: vector_component_simps field_simps)
2.277 +        by(auto simp add: field_simps)
2.278      next assume as:"dist a b = dist a x + dist x b"
2.279        have "norm (a - x) / norm (a - b) \<le> 1" unfolding divide_le_eq_1_pos[OF Fal2] unfolding as[unfolded dist_norm] norm_ge_zero by auto
2.280        thus "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" apply(rule_tac x="dist a x / dist a b" in exI)
2.281          unfolding dist_norm Cart_eq apply- apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4 proof rule
2.282            fix i::'n have "((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \$ i =
2.283              ((norm (a - b) - norm (a - x)) * (a \$ i) + norm (a - x) * (b \$ i)) / norm (a - b)"
2.284 -            using Fal by(auto simp add:vector_component_simps field_simps)
2.285 +            using Fal by(auto simp add: field_simps)
2.286            also have "\<dots> = x\$i" apply(rule divide_eq_imp[OF Fal])
2.287              unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i]
2.288 -            by(auto simp add:field_simps vector_component_simps)
2.290            finally show "x \$ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \$ i" by auto
2.291          qed(insert Fal2, auto) qed qed
2.292
2.293 @@ -2735,7 +2734,7 @@
2.294    "between (b,a) (midpoint a b)" (is ?t2)
2.295  proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by auto
2.296    show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
2.297 -    by(auto simp add:field_simps Cart_eq vector_component_simps) qed
2.298 +    by(auto simp add:field_simps Cart_eq) qed
2.299
2.300  lemma between_mem_convex_hull:
2.301    "between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
2.302 @@ -2754,7 +2753,7 @@
2.303      have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
2.304      have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
2.305        unfolding dist_norm unfolding norm_scaleR[THEN sym] apply(rule norm_eqI) using `e>0`
2.306 -      by(auto simp add:vector_component_simps Cart_eq field_simps)
2.307 +      by(auto simp add: Cart_eq field_simps)
2.308      also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:norm_eqI simp add: algebra_simps)
2.309      also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
2.310        by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute)
2.311 @@ -2826,11 +2825,11 @@
2.312    fix x::"real^'n" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x. 0 \<le> xa \$ x) \<and> setsum (op \$ xa) UNIV \<le> 1"
2.313    show "(\<forall>xa. 0 < x \$ xa) \<and> setsum (op \$ x) UNIV < 1" apply(rule,rule) proof-
2.314      fix i::'n show "0 < x \$ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
2.315 -      unfolding dist_norm by(auto simp add: norm_basis vector_component_simps basis_component elim:allE[where x=i])
2.316 +      unfolding dist_norm by(auto simp add: norm_basis elim:allE[where x=i])
2.317    next guess a using UNIV_witness[where 'a='n] ..
2.318      have **:"dist x (x + (e / 2) *\<^sub>R basis a) < e" using  `e>0` and norm_basis[of a]
2.319 -      unfolding dist_norm by(auto simp add: vector_component_simps basis_component intro!: mult_strict_left_mono_comm)
2.320 -    have "\<And>i. (x + (e / 2) *\<^sub>R basis a) \$ i = x\$i + (if i = a then e/2 else 0)" by(auto simp add:vector_component_simps)
2.321 +      unfolding dist_norm by(auto intro!: mult_strict_left_mono_comm)
2.322 +    have "\<And>i. (x + (e / 2) *\<^sub>R basis a) \$ i = x\$i + (if i = a then e/2 else 0)" by auto
2.323      hence *:"setsum (op \$ (x + (e / 2) *\<^sub>R basis a)) UNIV = setsum (\<lambda>i. x\$i + (if a = i then e/2 else 0)) UNIV" by(rule_tac setsum_cong, auto)
2.324      have "setsum (op \$ x) UNIV < setsum (op \$ (x + (e / 2) *\<^sub>R basis a)) UNIV" unfolding * setsum_addf
2.325        using `0<e` dimindex_ge_1 by(auto simp add: setsum_delta')
2.326 @@ -2847,13 +2846,13 @@
2.327      fix y assume y:"dist x y < min (Min (op \$ x ` UNIV)) ?d"
2.328      have "setsum (op \$ y) UNIV \<le> setsum (\<lambda>i. x\$i + ?d) UNIV" proof(rule setsum_mono)
2.329        fix i::'n have "abs (y\$i - x\$i) < ?d" apply(rule le_less_trans) using component_le_norm[of "y - x" i]
2.330 -        using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add:vector_component_simps norm_minus_commute)
2.331 +        using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add: norm_minus_commute)
2.332        thus "y \$ i \<le> x \$ i + ?d" by auto qed
2.333      also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat using dimindex_ge_1 by(auto simp add: Suc_le_eq)
2.334      finally show "(\<forall>i. 0 \<le> y \$ i) \<and> setsum (op \$ y) UNIV \<le> 1" apply- proof(rule,rule)
2.335        fix i::'n have "norm (x - y) < x\$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
2.336 -        using Min_gr_iff[of "op \$ x ` dimset x"] dimindex_ge_1 by auto
2.337 -      thus "0 \<le> y\$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by(auto simp add: vector_component_simps)
2.338 +        by auto
2.339 +      thus "0 \<le> y\$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by auto
2.340      qed auto qed auto qed
2.341
2.342  lemma interior_std_simplex_nonempty: obtains a::"real^'n" where
2.343 @@ -3040,9 +3039,6 @@
2.344    apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE)
2.345    unfolding mem_interval_1 by auto
2.346
2.347 -(** move this **)
2.348 -declare vector_scaleR_component[simp]
2.349 -
2.350  lemma simple_path_join_loop:
2.351    assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1"
2.352    "(path_image g1 \<inter> path_image g2) \<subseteq> {pathstart g1,pathstart g2}"
2.353 @@ -3390,7 +3386,7 @@
2.354          hence "\<psi> k \<noteq> \<psi> (Suc k)" using \<psi>[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=k]] by auto
2.355          hence **:"?basis k + ?basis (Suc k) \<in> {x. 0 < inner (?basis (Suc k)) x} \<inter> (?A k)"
2.356            "?basis k - ?basis (Suc k) \<in> {x. 0 > inner (?basis (Suc k)) x} \<inter> ({x. 0 < inner (?basis (Suc k)) x} \<union> (?A k))" using d
2.357 -          by(auto simp add: inner_basis vector_component_simps intro!:bexI[where x=k])
2.358 +          by(auto simp add: inner_basis intro!:bexI[where x=k])
2.359          show ?thesis unfolding * Un_assoc apply(rule path_connected_Un) defer apply(rule path_connected_Un)
2.360            prefer 5 apply(rule_tac[1-2] convex_imp_path_connected, rule convex_halfspace_lt, rule convex_halfspace_gt)
2.361            apply(rule Suc(1)) using d ** False by auto
2.362 @@ -3404,7 +3400,7 @@
2.363            apply(rule_tac[5] x=" ?basis 1 + ?basis 2" in nequals0I)
2.364            apply(rule_tac[6] x="-?basis 1 + ?basis 2" in nequals0I)
2.365            apply(rule_tac[7] x="-?basis 1 - ?basis 2" in nequals0I)
2.366 -          using d unfolding *** by(auto intro!: convex_halfspace_gt convex_halfspace_lt, auto simp add:vector_component_simps inner_basis)
2.367 +          using d unfolding *** by(auto intro!: convex_halfspace_gt convex_halfspace_lt, auto simp add: inner_basis)
2.368    qed qed auto qed note lem = this
2.369
2.370    have ***:"\<And>x::real^'n. (\<exists>i\<in>{1..CARD('n)}. inner (basis (\<psi> i)) x \<noteq> 0) \<longleftrightarrow> (\<exists>i. inner (basis i) x \<noteq> 0)"
2.371 @@ -3432,7 +3428,7 @@
2.372      apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
2.373      apply(rule continuous_at_norm[unfolded o_def]) by auto
2.374    thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
2.375 -    by(auto intro!: path_connected_continuous_image continuous_on_intros continuous_on_mul) qed
2.376 +    by(auto intro!: path_connected_continuous_image continuous_on_intros) qed
2.377
2.378  lemma connected_sphere: "2 \<le> CARD('n) \<Longrightarrow> connected {x::real^'n. norm(x - a) = r}"
2.379    using path_connected_sphere path_connected_imp_connected by auto
```
```     3.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Apr 25 23:22:29 2010 -0700
3.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Apr 26 09:21:25 2010 -0700
3.3 @@ -93,7 +93,7 @@
3.4
3.5  subsection {* Derivatives on real = Derivatives on @{typ "real^1"} *}
3.6
3.7 -lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by(auto simp add:vec1_dest_vec1_simps)
3.8 +lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by auto
3.9
3.10  lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
3.11    shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
3.12 @@ -281,6 +281,8 @@
3.13
3.14  subsection {* differentiability. *}
3.15
3.16 +no_notation Deriv.differentiable (infixl "differentiable" 60)
3.17 +
3.18  definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "differentiable" 30) where
3.19    "f differentiable net \<equiv> (\<exists>f'. (f has_derivative f') net)"
3.20
3.21 @@ -754,11 +756,11 @@
3.22  lemma onorm_vec1: fixes f::"real \<Rightarrow> real"
3.23    shows "onorm (\<lambda>x. vec1 (f (dest_vec1 x))) = onorm f" proof-
3.24    have "\<forall>x::real^1. norm x = 1 \<longleftrightarrow> x\<in>{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:Cart_eq)
3.25 -  hence 1:"{x. norm x = 1} = {vec1 -1, vec1 (1::real)}" by(auto simp add:norm_vec1)
3.26 +  hence 1:"{x. norm x = 1} = {vec1 -1, vec1 (1::real)}" by auto
3.27    have 2:"{norm (vec1 (f (dest_vec1 x))) |x. norm x = 1} = (\<lambda>x. norm (vec1 (f (dest_vec1 x)))) ` {x. norm x=1}" by auto
3.28    have "\<forall>x::real. norm x = 1 \<longleftrightarrow> x\<in>{-1, 1}" by auto hence 3:"{x. norm x = 1} = {-1, (1::real)}" by auto
3.29    have 4:"{norm (f x) |x. norm x = 1} = (\<lambda>x. norm (f x)) ` {x. norm x=1}" by auto
3.30 -  show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max norm_vec1) qed
3.31 +  show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max) qed
3.32
3.33  lemma differentiable_bound_real: fixes f::"real \<Rightarrow> real"
3.34    assumes "convex s" "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)" "\<forall>x\<in>s. onorm(f' x) \<le> B" and x:"x\<in>s" and y:"y\<in>s"
3.35 @@ -1013,7 +1015,7 @@
3.36  	  unfolding ph' * apply(rule diff_chain_within) defer apply(rule bounded_linear.has_derivative[OF assms(3)])
3.37  	  apply(rule has_derivative_intros) defer apply(rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
3.38  	  apply(rule has_derivative_at_within) using assms(5) and `u\<in>s` `a\<in>s`
3.39 -	  by(auto intro!: has_derivative_intros derivative_linear)
3.40 +          by(auto intro!: has_derivative_intros derivative_linear)
3.41  	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)
3.42  	  apply(rule_tac[!] derivative_linear) using assms(5) `u\<in>s` `a\<in>s` by auto
3.43  	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)
```
```     4.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Apr 25 23:22:29 2010 -0700
4.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Mon Apr 26 09:21:25 2010 -0700
4.3 @@ -813,7 +813,7 @@
4.4  lemma cramer:
4.5    fixes A ::"real^'n^'n"
4.6    assumes d0: "det A \<noteq> 0"
4.7 -  shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b\$i else A\$i\$j :: real^'n^'n) / det A)"
4.8 +  shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b\$i else A\$i\$j) / det A)"
4.9  proof-
4.10    from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1"
4.11      unfolding invertible_det_nz[symmetric] invertible_def by blast
4.12 @@ -821,7 +821,7 @@
4.13    hence "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc)
4.14    then have xe: "\<exists>x. A*v x = b" by blast
4.15    {fix x assume x: "A *v x = b"
4.16 -  have "x = (\<chi> k. det(\<chi> i j. if j=k then b\$i else A\$i\$j :: real^'n^'n) / det A)"
4.17 +  have "x = (\<chi> k. det(\<chi> i j. if j=k then b\$i else A\$i\$j) / det A)"
4.18      unfolding x[symmetric]
4.19      using d0 by (simp add: Cart_eq cramer_lemma field_simps)}
4.20    with xe show ?thesis by auto
4.21 @@ -993,15 +993,15 @@
4.22      moreover
4.23      {assume "x = 0" "y \<noteq> 0"
4.24        then have "dist (?g x) (?g y) = dist x y"
4.25 -        apply (simp add: dist_norm norm_mul)
4.26 +        apply (simp add: dist_norm)
4.27          apply (rule f1[rule_format])
4.28 -        by(simp add: norm_mul field_simps)}
4.30      moreover
4.31      {assume "x \<noteq> 0" "y = 0"
4.32        then have "dist (?g x) (?g y) = dist x y"
4.33 -        apply (simp add: dist_norm norm_mul)
4.34 +        apply (simp add: dist_norm)
4.35          apply (rule f1[rule_format])
4.36 -        by(simp add: norm_mul field_simps)}
4.38      moreover
4.39      {assume z: "x \<noteq> 0" "y \<noteq> 0"
4.40        have th00: "x = norm x *s (inverse (norm x) *s x)" "y = norm y *s (inverse (norm y) *s y)" "norm x *s f ((inverse (norm x) *s x)) = norm x *s f (inverse (norm x) *s x)"
4.41 @@ -1013,7 +1013,7 @@
4.42          "norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) =
4.43          norm (inverse (norm x) *s x - inverse (norm y) *s y)"
4.44          using z
4.45 -        by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
4.46 +        by (auto simp add: vector_smult_assoc field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
4.47        from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
4.49      ultimately have "dist (?g x) (?g y) = dist x y" by blast}
4.50 @@ -1047,7 +1047,7 @@
4.51    by (simp add: nat_number setprod_numseg mult_commute)
4.52
4.53  lemma det_1: "det (A::'a::comm_ring_1^1^1) = A\$1\$1"
4.54 -  by (simp add: det_def permutes_sing sign_id UNIV_1)
4.55 +  by (simp add: det_def sign_id UNIV_1)
4.56
4.57  lemma det_2: "det (A::'a::comm_ring_1^2^2) = A\$1\$1 * A\$2\$2 - A\$1\$2 * A\$2\$1"
4.58  proof-
4.59 @@ -1057,7 +1057,7 @@
4.60    unfolding setsum_over_permutations_insert[OF f12]
4.61    unfolding permutes_sing
4.62    apply (simp add: sign_swap_id sign_id swap_id_eq)
4.63 -  by (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31))
4.64 +  by (simp add: arith_simps(31)[symmetric] del: arith_simps(31))
4.65  qed
4.66
4.67  lemma det_3: "det (A::'a::comm_ring_1^3^3) =
4.68 @@ -1078,7 +1078,7 @@
4.69
4.70    unfolding permutes_sing
4.71    apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
4.72 -  apply (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31))
4.73 +  apply (simp add: arith_simps(31)[symmetric] del: arith_simps(31))
4.75  qed
4.76
```
```     5.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Apr 25 23:22:29 2010 -0700
5.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Apr 26 09:21:25 2010 -0700
5.3 @@ -670,7 +670,7 @@
5.4  subsection{* The collapse of the general concepts to dimension one. *}
5.5
5.6  lemma vector_one: "(x::'a ^1) = (\<chi> i. (x\$1))"
5.7 -  by (simp add: Cart_eq forall_1)
5.8 +  by (simp add: Cart_eq)
5.9
5.10  lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
5.11    apply auto
5.12 @@ -775,8 +775,7 @@
5.13  lemma sqrt_even_pow2: assumes n: "even n"
5.14    shows "sqrt(2 ^ n) = 2 ^ (n div 2)"
5.15  proof-
5.16 -  from n obtain m where m: "n = 2*m" unfolding even_nat_equiv_def2
5.17 -    by (auto simp add: nat_number)
5.18 +  from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex ..
5.19    from m  have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)"
5.20      by (simp only: power_mult[symmetric] mult_commute)
5.21    then show ?thesis  using m by simp
5.22 @@ -785,7 +784,7 @@
5.23  lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)"
5.24    apply (cases "x = 0", simp_all)
5.25    using sqrt_divide_self_eq[of x]
5.26 -  apply (simp add: inverse_eq_divide real_sqrt_ge_0_iff field_simps)
5.27 +  apply (simp add: inverse_eq_divide field_simps)
5.28    done
5.29
5.30  text{* Hence derive more interesting properties of the norm. *}
5.31 @@ -798,8 +797,8 @@
5.32    by (rule norm_zero)
5.33
5.34  lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x"
5.35 -  by (simp add: norm_vector_def vector_component setL2_right_distrib
5.36 -           abs_mult cong: strong_setL2_cong)
5.37 +  by (simp add: norm_vector_def setL2_right_distrib abs_mult)
5.38 +
5.39  lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
5.40    by (simp add: norm_vector_def setL2_def power2_eq_square)
5.41  lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
5.42 @@ -866,10 +865,14 @@
5.43    by (auto simp add: norm_eq_sqrt_inner)
5.44
5.45  lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
5.46 -proof-
5.47 -  have "x^2 \<le> y^2 \<longleftrightarrow> (x -y) * (y + x) \<le> 0" by (simp add: ring_simps power2_eq_square)
5.48 -  also have "\<dots> \<longleftrightarrow> \<bar>x\<bar> \<le> \<bar>y\<bar>" apply (simp add: zero_compare_simps real_abs_def not_less) by arith
5.49 -finally show ?thesis ..
5.50 +proof
5.51 +  assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
5.52 +  then have "\<bar>x\<bar>\<twosuperior> \<le> \<bar>y\<bar>\<twosuperior>" by (rule power_mono, simp)
5.53 +  then show "x\<twosuperior> \<le> y\<twosuperior>" by simp
5.54 +next
5.55 +  assume "x\<twosuperior> \<le> y\<twosuperior>"
5.56 +  then have "sqrt (x\<twosuperior>) \<le> sqrt (y\<twosuperior>)" by (rule real_sqrt_le_mono)
5.57 +  then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" by simp
5.58  qed
5.59
5.60  lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
5.61 @@ -1179,7 +1182,7 @@
5.62    assumes fS: "finite S"
5.63    shows "setsum f S *s v = setsum (\<lambda>x. f x *s v) S"
5.64  proof(induct rule: finite_induct[OF fS])
5.65 -  case 1 then show ?case by (simp add: vector_smult_lzero)
5.66 +  case 1 then show ?case by simp
5.67  next
5.68    case (2 x F)
5.69    from "2.hyps" have "setsum f (insert x F) *s v = (f x + setsum f F) *s v"
5.70 @@ -1398,7 +1401,7 @@
5.71    apply (subgoal_tac "vector [v\$1] = v")
5.72    apply simp
5.73    apply (vector vector_def)
5.74 -  apply (simp add: forall_1)
5.75 +  apply simp
5.76    done
5.77
5.78  lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
5.79 @@ -1536,7 +1539,7 @@
5.80        unfolding norm_mul
5.81        apply (simp only: mult_commute)
5.82        apply (rule mult_mono)
5.83 -      by (auto simp add: ring_simps norm_ge_zero) }
5.84 +      by (auto simp add: ring_simps) }
5.85      then have th: "\<forall>i\<in> ?S. norm ((x\$i) *s f (basis i :: real ^'m)) \<le> norm (f (basis i)) * norm x" by metis
5.86      from real_setsum_norm_le[OF fS, of "\<lambda>i. (x\$i) *s (f (basis i))", OF th]
5.87      have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}
5.88 @@ -1553,9 +1556,9 @@
5.89    let ?K = "\<bar>B\<bar> + 1"
5.90    have Kp: "?K > 0" by arith
5.91      {assume C: "B < 0"
5.92 -      have "norm (1::real ^ 'n) > 0" by (simp add: zero_less_norm_iff)
5.93 +      have "norm (1::real ^ 'n) > 0" by simp
5.94        with C have "B * norm (1:: real ^ 'n) < 0"
5.95 -        by (simp add: zero_compare_simps)
5.96 +        by (simp add: mult_less_0_iff)
5.97        with B[rule_format, of 1] norm_ge_zero[of "f 1"] have False by simp
5.98      }
5.99      then have Bp: "B \<ge> 0" by ferrack
5.100 @@ -1677,11 +1680,11 @@
5.101        apply (rule real_setsum_norm_le)
5.102        using fN fM
5.103        apply simp
5.104 -      apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] norm_mul ring_simps)
5.105 +      apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] ring_simps)
5.106        apply (rule mult_mono)
5.107 -      apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
5.108 +      apply (auto simp add: zero_le_mult_iff component_le_norm)
5.109        apply (rule mult_mono)
5.110 -      apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
5.111 +      apply (auto simp add: zero_le_mult_iff component_le_norm)
5.112        done}
5.113    then show ?thesis by metis
5.114  qed
5.115 @@ -1701,7 +1704,7 @@
5.116      have "B * norm x * norm y \<le> ?K * norm x * norm y"
5.117        apply -
5.118        apply (rule mult_right_mono, rule mult_right_mono)
5.119 -      by (auto simp add: norm_ge_zero)
5.120 +      by auto
5.121      then have "norm (h x y) \<le> ?K * norm x * norm y"
5.122        using B[rule_format, of x y] by simp}
5.123    with Kp show ?thesis by blast
5.124 @@ -2006,8 +2009,8 @@
5.125    have uv': "u = 0 \<longrightarrow> v \<noteq> 0" using u v uv by arith
5.126    have "a = a * (u + v)" unfolding uv  by simp
5.127    hence th: "u * a + v * a = a" by (simp add: ring_simps)
5.128 -  from xa u have "u \<noteq> 0 \<Longrightarrow> u*x < u*a" by (simp add: mult_compare_simps)
5.129 -  from ya v have "v \<noteq> 0 \<Longrightarrow> v * y < v * a" by (simp add: mult_compare_simps)
5.130 +  from xa u have "u \<noteq> 0 \<Longrightarrow> u*x < u*a" by (simp add: mult_strict_left_mono)
5.131 +  from ya v have "v \<noteq> 0 \<Longrightarrow> v * y < v * a" by (simp add: mult_strict_left_mono)
5.132    from xa ya u v have "u * x + v * y < u * a + v * a"
5.133      apply (cases "u = 0", simp_all add: uv')
5.134      apply(rule mult_strict_left_mono)
5.135 @@ -2048,7 +2051,7 @@
5.136    assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2"
5.137    shows "x <= y + z"
5.138  proof-
5.139 -  have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y  by (simp add: zero_compare_simps)
5.140 +  have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg)
5.141    with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square ring_simps)
5.142    from y z have yz: "y + z \<ge> 0" by arith
5.143    from power2_le_imp_le[OF th yz] show ?thesis .
5.144 @@ -2100,10 +2103,10 @@
5.145        {assume x0: "x \<noteq> 0"
5.146          hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
5.147          let ?c = "1/ norm x"
5.148 -        have "norm (?c*s x) = 1" using x0 by (simp add: n0 norm_mul)
5.149 +        have "norm (?c*s x) = 1" using x0 by (simp add: n0)
5.150          with H have "norm (f(?c*s x)) \<le> b" by blast
5.151          hence "?c * norm (f x) \<le> b"
5.152 -          by (simp add: linear_cmul[OF lf] norm_mul)
5.153 +          by (simp add: linear_cmul[OF lf])
5.154          hence "norm (f x) \<le> b * norm x"
5.155            using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}
5.156        ultimately have "norm (f x) \<le> b * norm x" by blast}
5.157 @@ -2221,18 +2224,24 @@
5.158    where "dest_vec1 x \<equiv> (x\$1)"
5.159
5.160  lemma vec1_component[simp]: "(vec1 x)\$1 = x"
5.161 -  by (simp add: )
5.162 -
5.163 -lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
5.164 -  by (simp_all add:  Cart_eq forall_1)
5.165 -
5.166 -lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))" by (metis vec1_dest_vec1)
5.167 -
5.168 -lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))" by (metis vec1_dest_vec1)
5.169 -
5.170 -lemma vec1_eq[simp]:  "vec1 x = vec1 y \<longleftrightarrow> x = y" by (metis vec1_dest_vec1)
5.171 -
5.172 -lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y" by (metis vec1_dest_vec1)
5.173 +  by simp
5.174 +
5.175 +lemma vec1_dest_vec1: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
5.176 +  by (simp_all add:  Cart_eq)
5.177 +
5.178 +declare vec1_dest_vec1(1) [simp]
5.179 +
5.180 +lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
5.181 +  by (metis vec1_dest_vec1(1))
5.182 +
5.183 +lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
5.184 +  by (metis vec1_dest_vec1(1))
5.185 +
5.186 +lemma vec1_eq[simp]:  "vec1 x = vec1 y \<longleftrightarrow> x = y"
5.187 +  by (metis vec1_dest_vec1(2))
5.188 +
5.189 +lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
5.190 +  by (metis vec1_dest_vec1(1))
5.191
5.192  lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
5.193
5.194 @@ -2260,8 +2269,8 @@
5.195  lemma dest_vec1_sum: assumes fS: "finite S"
5.196    shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
5.197    apply (induct rule: finite_induct[OF fS])
5.198 -  apply (simp add: dest_vec1_vec)
5.199 -  apply (auto simp add:vector_minus_component)
5.200 +  apply simp
5.201 +  apply auto
5.202    done
5.203
5.204  lemma norm_vec1: "norm(vec1 x) = abs(x)"
5.205 @@ -2270,7 +2279,7 @@
5.206  lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
5.207    by (simp only: dist_real vec1_component)
5.208  lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
5.209 -  by (metis vec1_dest_vec1 norm_vec1)
5.210 +  by (metis vec1_dest_vec1(1) norm_vec1)
5.211
5.212  lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
5.213     vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
5.214 @@ -2298,7 +2307,7 @@
5.215    shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
5.216    apply (rule ext)
5.217    apply (subst matrix_works[OF lf, symmetric])
5.218 -  apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute forall_1)
5.219 +  apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute)
5.220    done
5.221
5.222  lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
5.223 @@ -2366,13 +2375,13 @@
5.224    by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0)
5.225
5.226  lemma pastecart_vec[simp]: "pastecart (vec x) (vec x) = vec x"
5.227 -  by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart)
5.228 +  by (simp add: pastecart_eq)
5.229
5.230  lemma pastecart_add[simp]:"pastecart (x1::'a::{plus,times}^_) y1 + pastecart x2 y2 = pastecart (x1 + x2) (y1 + y2)"
5.231 -  by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart)
5.232 +  by (simp add: pastecart_eq)
5.233
5.234  lemma pastecart_cmul[simp]: "pastecart (c *s (x1::'a::{plus,times}^_)) (c *s y1) = c *s pastecart x1 y1"
5.235 -  by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart)
5.236 +  by (simp add: pastecart_eq)
5.237
5.238  lemma pastecart_neg[simp]: "pastecart (- (x::'a::ring_1^_)) (- y) = - pastecart x y"
5.239    unfolding vector_sneg_minus1 pastecart_cmul ..
5.240 @@ -2384,7 +2393,7 @@
5.241    fixes f:: "'d \<Rightarrow> 'a::semiring_1^_"
5.242    assumes fS: "finite S"
5.243    shows "pastecart (setsum f S) (setsum g S) = setsum (\<lambda>i. pastecart (f i) (g i)) S"
5.244 -  by (simp  add: pastecart_eq fstcart_setsum[OF fS] sndcart_setsum[OF fS] fstcart_pastecart sndcart_pastecart)
5.245 +  by (simp  add: pastecart_eq fstcart_setsum[OF fS] sndcart_setsum[OF fS])
5.246
5.247  lemma setsum_Plus:
5.248    "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow>
5.249 @@ -2402,7 +2411,7 @@
5.250  lemma norm_fstcart: "norm(fstcart x) <= norm (x::real ^('n::finite + 'm::finite))"
5.251  proof-
5.252    have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"
5.253 -    by (simp add: pastecart_fst_snd)
5.254 +    by simp
5.255    have th1: "fstcart x \<bullet> fstcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"
5.256      by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg)
5.257    then show ?thesis
5.258 @@ -2417,7 +2426,7 @@
5.259  lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))"
5.260  proof-
5.261    have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"
5.262 -    by (simp add: pastecart_fst_snd)
5.263 +    by simp
5.264    have th1: "sndcart x \<bullet> sndcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"
5.265      by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg)
5.266    then show ?thesis
5.267 @@ -2519,7 +2528,7 @@
5.268
5.269  lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
5.270    using reals_Archimedean
5.271 -  apply (auto simp add: field_simps inverse_positive_iff_positive)
5.272 +  apply (auto simp add: field_simps)
5.273    apply (subgoal_tac "inverse (real n) > 0")
5.274    apply arith
5.275    apply simp
5.276 @@ -2732,7 +2741,8 @@
5.277    "0 \<in> span S"
5.278    "x\<in> span S \<Longrightarrow> y \<in> span S ==> x + y \<in> span S"
5.279    "x \<in> span S \<Longrightarrow> c *s x \<in> span S"
5.280 -  by (metis span_def hull_subset subset_eq subspace_span subspace_def)+
5.281 +  by (metis span_def hull_subset subset_eq)
5.282 +     (metis subspace_span subspace_def)+
5.283
5.284  lemma span_induct: assumes SP: "\<And>x. x \<in> S ==> P x"
5.285    and P: "subspace P" and x: "x \<in> span S" shows "P x"
5.286 @@ -2830,7 +2840,7 @@
5.287
5.288  (* Individual closure properties. *)
5.289
5.290 -lemma span_superset: "x \<in> S ==> x \<in> span S" by (metis span_clauses)
5.291 +lemma span_superset: "x \<in> S ==> x \<in> span S" by (metis span_clauses(1))
5.292
5.293  lemma span_0: "0 \<in> span S" by (metis subspace_span subspace_0)
5.294
5.295 @@ -2847,8 +2857,7 @@
5.296    by (metis subspace_span subspace_sub)
5.297
5.298  lemma span_setsum: "finite A \<Longrightarrow> \<forall>x \<in> A. f x \<in> span S ==> setsum f A \<in> span S"
5.299 -  apply (rule subspace_setsum)
5.300 -  by (metis subspace_span subspace_setsum)+
5.301 +  by (rule subspace_setsum, rule subspace_span)
5.302
5.303  lemma span_add_eq: "(x::'a::ring_1^_) \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
5.304    apply (auto simp only: span_add span_sub)
5.305 @@ -3110,7 +3119,7 @@
5.306      from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0" by auto
5.307      have s0: "setsum (\<lambda>v. ?u v *s v) ?S = 0"
5.308        using fS aS
5.309 -      apply (simp add: vector_smult_lneg vector_smult_lid setsum_clauses ring_simps )
5.310 +      apply (simp add: vector_smult_lneg setsum_clauses ring_simps)
5.311        apply (subst (2) ua[symmetric])
5.312        apply (rule setsum_cong2)
5.313        by auto
5.314 @@ -3479,7 +3488,7 @@
5.315
5.316  lemma basis_card_eq_dim:
5.317    "B \<subseteq> (V:: (real ^'n) set) \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B = dim V"
5.318 -  by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_mono independent_bound)
5.319 +  by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_bound)
5.320
5.321  lemma dim_unique: "(B::(real ^'n) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = n \<Longrightarrow> dim V = n"
5.322    by (metis basis_card_eq_dim)
5.323 @@ -3669,7 +3678,7 @@
5.324          apply (subst Cy)
5.325          using C(1) fth
5.326          apply (simp only: setsum_clauses) unfolding smult_conv_scaleR
5.327 -        apply (auto simp add: inner_simps inner_eq_zero_iff inner_commute[of y a] dot_lsum[OF fth])
5.328 +        apply (auto simp add: inner_simps inner_commute[of y a] dot_lsum[OF fth])
5.329          apply (rule setsum_0')
5.330          apply clarsimp
5.331          apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
5.332 @@ -3686,7 +3695,7 @@
5.333          using C(1) fth
5.334          apply (simp only: setsum_clauses) unfolding smult_conv_scaleR
5.335          apply (subst inner_commute[of x])
5.336 -        apply (auto simp add: inner_simps inner_eq_zero_iff inner_commute[of x a] dot_rsum[OF fth])
5.337 +        apply (auto simp add: inner_simps inner_commute[of x a] dot_rsum[OF fth])
5.338          apply (rule setsum_0')
5.339          apply clarsimp
5.340          apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
5.341 @@ -3759,10 +3768,10 @@
5.342          apply (subst B') using fB fth
5.343          unfolding setsum_clauses(2)[OF fth]
5.344          apply simp unfolding inner_simps smult_conv_scaleR
5.345 -        apply (clarsimp simp add: inner_simps inner_eq_zero_iff smult_conv_scaleR dot_lsum)
5.346 +        apply (clarsimp simp add: inner_simps smult_conv_scaleR dot_lsum)
5.347          apply (rule setsum_0', rule ballI)
5.348          unfolding inner_commute
5.349 -        by (auto simp add: x field_simps inner_eq_zero_iff intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
5.350 +        by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
5.351      then show "\<forall>x \<in> B. ?a \<bullet> x = 0" by blast
5.352    qed
5.353    with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"])
5.354 @@ -3915,7 +3924,7 @@
5.355      {assume xb: "x \<in> b"
5.356        have h0: "0 = ?h x"
5.357          apply (rule conjunct2[OF h, rule_format])
5.358 -        apply (metis  span_superset insertI1 xb x)
5.359 +        apply (metis  span_superset x)
5.360          apply simp
5.361          apply (metis span_superset xb)
5.362          done
5.363 @@ -4262,8 +4271,7 @@
5.364      {fix y have "?P y"
5.365        proof(rule span_induct_alt[of ?P "columns A"])
5.366          show "\<exists>x\<Colon>real ^ 'm. setsum (\<lambda>i. (x\$i) *s column i A) ?U = 0"
5.367 -          apply (rule exI[where x=0])
5.368 -          by (simp add: zero_index vector_smult_lzero)
5.369 +          by (rule exI[where x=0], simp)
5.370        next
5.371          fix c y1 y2 assume y1: "y1 \<in> columns A" and y2: "?P y2"
5.372          from y1 obtain i where i: "i \<in> ?U" "y1 = column i A"
5.373 @@ -4687,7 +4695,7 @@
5.374    hence d2: "(sqrt (real ?d))^2 = real ?d"
5.375      by (auto intro: real_sqrt_pow2)
5.376    have th: "sqrt (real ?d) * infnorm x \<ge> 0"
5.377 -    by (simp add: zero_le_mult_iff real_sqrt_ge_0_iff infnorm_pos_le)
5.378 +    by (simp add: zero_le_mult_iff infnorm_pos_le)
5.379    have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)^2"
5.380      unfolding power_mult_distrib d2
5.381      unfolding real_of_nat_def inner_vector_def
5.382 @@ -4861,4 +4869,3 @@
5.383  done
5.384
5.385  end
5.386 -
5.387 \ No newline at end of file
```
```     6.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Apr 25 23:22:29 2010 -0700
6.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Apr 26 09:21:25 2010 -0700
6.3 @@ -933,7 +933,7 @@
6.4  lemma has_integral_vec1: assumes "(f has_integral k) {a..b}"
6.5    shows "((\<lambda>x. vec1 (f x)) has_integral (vec1 k)) {a..b}"
6.6  proof- have *:"\<And>p. (\<Sum>(x, k)\<in>p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k)"
6.7 -    unfolding vec_sub Cart_eq by(auto simp add:vec1_dest_vec1_simps split_beta)
6.8 +    unfolding vec_sub Cart_eq by(auto simp add: split_beta)
6.9    show ?thesis using assms unfolding has_integral apply safe
6.10      apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
6.11      apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
6.12 @@ -1356,7 +1356,7 @@
6.13
6.14  lemma has_integral_eq_eq:
6.15    shows "\<forall>x\<in>s. f x = g x \<Longrightarrow> ((f has_integral k) s \<longleftrightarrow> (g has_integral k) s)"
6.16 -  using has_integral_eq[of s f g] has_integral_eq[of s g f] by auto
6.17 +  using has_integral_eq[of s f g] has_integral_eq[of s g f] by rule auto
6.18
6.19  lemma has_integral_null[dest]:
6.20    assumes "content({a..b}) = 0" shows  "(f has_integral 0) ({a..b})"
6.21 @@ -1653,7 +1653,7 @@
6.22  proof- have *:"{a..b} = ({a..b} \<inter> {x. x\$k \<le> c}) \<union> ({a..b} \<inter> {x. x\$k \<ge> c})" by auto
6.23    show ?thesis apply(subst *) apply(rule tagged_division_union[OF assms])
6.24      unfolding interval_split interior_closed_interval
6.25 -    by(auto simp add: vector_less_def Cart_lambda_beta elim!:allE[where x=k]) qed
6.26 +    by(auto simp add: vector_less_def elim!:allE[where x=k]) qed
6.27
6.28  lemma has_integral_separate_sides: fixes f::"real^'m \<Rightarrow> 'a::real_normed_vector"
6.29    assumes "(f has_integral i) ({a..b})" "e>0"
6.30 @@ -1743,11 +1743,11 @@
6.31  subsection {* Using additivity of lifted function to encode definedness. *}
6.32
6.33  lemma forall_option: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P(Some x))"
6.34 -  by (metis map_of.simps option.nchotomy)
6.35 +  by (metis option.nchotomy)
6.36
6.37  lemma exists_option:
6.38   "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))"
6.39 -  by (metis map_of.simps option.nchotomy)
6.40 +  by (metis option.nchotomy)
6.41
6.42  fun lifted where
6.43    "lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some(opp x y)" |
6.44 @@ -1842,9 +1842,8 @@
6.45  lemma operative_content[intro]: "operative (op +) content"
6.46    unfolding operative_def content_split[THEN sym] neutral_add by auto
6.47
6.48 -lemma neutral_monoid[simp]: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
6.49 -  unfolding neutral_def apply(rule some_equality) defer
6.50 -  apply(erule_tac x=0 in allE) by auto
6.51 +lemma neutral_monoid: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
6.52 +  by (rule neutral_add) (* FIXME: duplicate *)
6.53
6.54  lemma monoidal_monoid[intro]:
6.55    shows "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
6.56 @@ -1941,7 +1940,7 @@
6.57      apply(rule_tac x="(k,(interval_lowerbound l)\$k)" in exI) defer
6.58      apply(rule_tac x="(k,(interval_upperbound l)\$k)" in exI)
6.59      unfolding division_points_def unfolding interval_bounds[OF ab]
6.60 -    apply (auto simp add:interval_bounds) unfolding * by auto
6.61 +    apply auto unfolding * by auto
6.62    thus "?D1 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4)]) by auto
6.63
6.64    have *:"interval_lowerbound ({a..b} \<inter> {x. x \$ k \<ge> interval_lowerbound l \$ k}) \$ k = interval_lowerbound l \$ k"
6.65 @@ -1952,7 +1951,7 @@
6.66      apply(rule_tac x="(k,(interval_lowerbound l)\$k)" in exI) defer
6.67      apply(rule_tac x="(k,(interval_upperbound l)\$k)" in exI)
6.68      unfolding division_points_def unfolding interval_bounds[OF ab]
6.69 -    apply (auto simp add:interval_bounds) unfolding * by auto
6.70 +    apply auto unfolding * by auto
6.71    thus "?D2 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4)]) by auto qed
6.72
6.73  subsection {* Preservation by divisions and tagged divisions. *}
6.74 @@ -2254,7 +2253,7 @@
6.75    assumes "p tagged_division_of {a..b}"  "\<forall>x\<in>{a..b}. (f x)\$i \<le> (g x)\$i"
6.76    shows "(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p)\$i \<le> (setsum (\<lambda>(x,k). content k *\<^sub>R g x) p)\$i"
6.77    unfolding setsum_component apply(rule setsum_mono)
6.78 -  apply(rule mp) defer apply assumption apply(induct_tac x,rule) unfolding split_conv
6.79 +  apply(rule mp) defer apply assumption unfolding split_paired_all apply rule unfolding split_conv
6.80  proof- fix a b assume ab:"(a,b) \<in> p" note assm = tagged_division_ofD(2-4)[OF assms(1) ab]
6.81    from this(3) guess u v apply-by(erule exE)+ note b=this
6.82    show "(content b *\<^sub>R f a) \$ i \<le> (content b *\<^sub>R g a) \$ i" unfolding b
6.83 @@ -2903,7 +2902,7 @@
6.84    shows "setsum (\<lambda>(x,k). f(interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a"
6.85  proof- let ?f = "(\<lambda>k::(real^1) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
6.86    have *:"operative op + ?f" unfolding operative_1_lt[OF monoidal_monoid] interval_eq_empty_1
6.87 -    by(auto simp add:not_less interval_bound_1 vector_less_def)
6.88 +    by(auto simp add:not_less vector_less_def)
6.89    have **:"{a..b} \<noteq> {}" using assms(1) by auto note operative_tagged_division[OF monoidal_monoid * assms(2)]
6.90    note * = this[unfolded if_not_P[OF **] interval_bound_1[OF assms(1)],THEN sym ]
6.91    show ?thesis unfolding * apply(subst setsum_iterate[THEN sym]) defer
6.92 @@ -3340,7 +3339,7 @@
6.93  proof- { presume *:"a < b \<Longrightarrow> ?thesis"
6.94      show ?thesis proof(cases,rule *,assumption)
6.95        assume "\<not> a < b" hence "a = b" using assms(1) by auto
6.96 -      hence *:"{vec a .. vec b} = {vec b}" "f b - f a = 0" apply(auto simp add: Cart_simps) by smt
6.97 +      hence *:"{vec a .. vec b} = {vec b}" "f b - f a = 0" by(auto simp add: Cart_eq vector_le_def order_antisym)
6.98        show ?thesis unfolding *(2) apply(rule has_integral_null) unfolding content_eq_0_1 using * `a=b` by auto
6.99      qed } assume ab:"a < b"
6.100    let ?P = "\<lambda>e. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {vec1 a..vec1 b} \<and> d fine p \<longrightarrow>
6.101 @@ -3422,7 +3421,7 @@
6.102          hence "\<forall>i. u\$i \<le> v\$i" and uv:"{u,v}\<subseteq>{u..v}" using p(2)[OF as(1)] by auto note this(1) this(1)[unfolded forall_1]
6.103          note result = as(2)[unfolded k interval_bounds[OF this(1)] content_1[OF this(2)]]
6.104
6.105 -        assume as':"x \<noteq> vec1 a" "x \<noteq> vec1 b" hence "x\$1 \<in> {a<..<b}" using p(2-3)[OF as(1)] by(auto simp add:Cart_simps) note  * = d(2)[OF this]
6.106 +        assume as':"x \<noteq> vec1 a" "x \<noteq> vec1 b" hence "x\$1 \<in> {a<..<b}" using p(2-3)[OF as(1)] by(auto simp add: Cart_eq) note  * = d(2)[OF this]
6.107          have "norm ((v\$1 - u\$1) *\<^sub>R f' (x\$1) - (f (v\$1) - f (u\$1))) =
6.108            norm ((f (u\$1) - f (x\$1) - (u\$1 - x\$1) *\<^sub>R f' (x\$1)) - (f (v\$1) - f (x\$1) - (v\$1 - x\$1) *\<^sub>R f' (x\$1)))"
6.109            apply(rule arg_cong[of _ _ norm]) unfolding scaleR_left.diff by auto
6.110 @@ -3669,7 +3668,7 @@
6.111      from indefinite_integral_continuous_left[OF assms(1) `a<b` this `e>0`] guess d . note d=this
6.112      show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
6.113        unfolding `x=b` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
6.114 -  next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add:Cart_simps)
6.115 +  next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add: vector_less_def)
6.116      from indefinite_integral_continuous_left [OF assms(1) xl `e>0`] guess d1 . note d1=this
6.117      from indefinite_integral_continuous_right[OF assms(1) xr `e>0`] guess d2 . note d2=this
6.118      show ?thesis apply(rule_tac x="min d1 d2" in exI)
6.119 @@ -3726,7 +3725,7 @@
6.120      unfolding o_def using assms(5) defer apply-apply(rule)
6.121    proof- fix t assume as:"t\<in>{0..1} - {t. (1 - t) *\<^sub>R c + t *\<^sub>R x \<in> k}"
6.122      have *:"c - t *\<^sub>R c + t *\<^sub>R x \<in> s - k" apply safe apply(rule conv[unfolded scaleR_simps])
6.123 -      using `x\<in>s` `c\<in>s` as by(auto simp add:scaleR_simps)
6.124 +      using `x\<in>s` `c\<in>s` as by(auto simp add: algebra_simps)
6.125      have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
6.127        unfolding scaleR_simps apply(rule has_derivative_sub) apply(rule has_derivative_const)
6.128 @@ -3949,7 +3948,7 @@
6.129
6.130  lemma has_integral_spike_set_eq: fixes f::"real^'n \<Rightarrow> 'a::banach"
6.131    assumes "negligible((s - t) \<union> (t - s))" shows "((f has_integral y) s \<longleftrightarrow> (f has_integral y) t)"
6.132 -  unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by auto
6.133 +  unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by (safe, auto split: split_if_asm)
6.134
6.135  lemma has_integral_spike_set[dest]: fixes f::"real^'n \<Rightarrow> 'a::banach"
6.136    assumes "negligible((s - t) \<union> (t - s))" "(f has_integral y) s"
```
```     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Apr 25 23:22:29 2010 -0700
7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 26 09:21:25 2010 -0700
7.3 @@ -48,16 +48,17 @@
7.4    "\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
7.5    "\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
7.6    using openin[of U] unfolding istopology_def Collect_def mem_def
7.7 -  by (metis mem_def subset_eq)+
7.8 +  unfolding subset_eq Ball_def mem_def by auto
7.9
7.10  lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
7.11    unfolding topspace_def by blast
7.12  lemma openin_empty[simp]: "openin U {}" by (simp add: openin_clauses)
7.13
7.14  lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
7.15 -  by (simp add: openin_clauses)
7.16 -
7.17 -lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)" by (simp add: openin_clauses)
7.18 +  using openin_clauses by simp
7.19 +
7.20 +lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)"
7.21 +  using openin_clauses by simp
7.22
7.23  lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
7.24    using openin_Union[of "{S,T}" U] by auto
7.25 @@ -946,7 +947,7 @@
7.26    by (metis frontier_def closure_closed Diff_subset)
7.27
7.28  lemma frontier_empty[simp]: "frontier {} = {}"
7.29 -  by (simp add: frontier_def closure_empty)
7.30 +  by (simp add: frontier_def)
7.31
7.32  lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
7.33  proof-
7.34 @@ -954,7 +955,7 @@
7.35      hence "closure S \<subseteq> S" using interior_subset unfolding frontier_def by auto
7.36      hence "closed S" using closure_subset_eq by auto
7.37    }
7.38 -  thus ?thesis using frontier_subset_closed[of S] by auto
7.39 +  thus ?thesis using frontier_subset_closed[of S] ..
7.40  qed
7.41
7.42  lemma frontier_complement: "frontier(- S) = frontier S"
7.43 @@ -1588,7 +1589,7 @@
7.44
7.45  (* FIXME: Only one congruence rule for tendsto can be used at a time! *)
7.46
7.49    fixes a :: "'a::metric_space"
7.50    fixes l :: "'b::metric_space" (* TODO: generalize *)
7.51    shows "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
7.52 @@ -1667,7 +1668,7 @@
7.53    { fix e::real assume "e>0"
7.54      hence "\<exists>N::nat. \<forall>n::nat\<ge>N. inverse (real n) < e"
7.55        using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI)
7.56 -      by (metis not_le le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
7.57 +      by (metis le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
7.58    }
7.59    thus ?thesis unfolding Lim_sequentially dist_norm by simp
7.60  qed
7.61 @@ -1702,7 +1703,7 @@
7.62    apply (simp add: interior_def, safe)
7.63    apply (force simp add: open_contains_cball)
7.64    apply (rule_tac x="ball x e" in exI)
7.65 -  apply (simp add: open_ball centre_in_ball subset_trans [OF ball_subset_cball])
7.66 +  apply (simp add: subset_trans [OF ball_subset_cball])
7.67    done
7.68
7.69  lemma islimpt_ball:
7.70 @@ -1877,14 +1878,14 @@
7.71  lemma frontier_ball:
7.72    fixes a :: "'a::real_normed_vector"
7.73    shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}"
7.74 -  apply (simp add: frontier_def closure_ball interior_open open_ball order_less_imp_le)
7.75 +  apply (simp add: frontier_def closure_ball interior_open order_less_imp_le)
7.77    by arith
7.78
7.79  lemma frontier_cball:
7.80    fixes a :: "'a::{real_normed_vector, perfect_space}"
7.81    shows "frontier(cball a e) = {x. dist a x = e}"
7.82 -  apply (simp add: frontier_def interior_cball closed_cball closure_closed order_less_imp_le)
7.83 +  apply (simp add: frontier_def interior_cball closed_cball order_less_imp_le)
7.85    by arith
7.86
7.87 @@ -2004,9 +2005,10 @@
7.88  lemma bounded_ball[simp,intro]: "bounded(ball x e)"
7.89    by (metis ball_subset_cball bounded_cball bounded_subset)
7.90
7.91 -lemma finite_imp_bounded[intro]: assumes "finite S" shows "bounded S"
7.92 +lemma finite_imp_bounded[intro]:
7.93 +  fixes S :: "'a::metric_space set" assumes "finite S" shows "bounded S"
7.94  proof-
7.95 -  { fix a F assume as:"bounded F"
7.96 +  { fix a and F :: "'a set" assume as:"bounded F"
7.97      then obtain x e where "\<forall>y\<in>F. dist x y \<le> e" unfolding bounded_def by auto
7.98      hence "\<forall>y\<in>(insert a F). dist x y \<le> max e (dist x a)" by auto
7.99      hence "bounded (insert a F)" unfolding bounded_def by (intro exI)
7.100 @@ -2216,7 +2218,7 @@
7.101  apply (rule allI, rule impI, rule ext)
7.102  apply (erule conjE)
7.103  apply (induct_tac x)
7.105 +apply simp
7.106  apply (erule_tac x="n" in allE)
7.107  apply (simp)
7.108  done
7.109 @@ -2648,7 +2650,8 @@
7.110    { fix x y assume "x\<in>t" "y\<in>t" "f x = f y"
7.111      hence "x \<in> f x"  "y \<in> f x \<longrightarrow> y = x" using f[THEN bspec[where x=x]] and `t\<subseteq>s` by auto
7.112      hence "x = y" using `f x = f y` and f[THEN bspec[where x=y]] and `y\<in>t` and `t\<subseteq>s` by auto  }
7.113 -  hence "infinite (f ` t)" using assms(2) using finite_imageD[unfolded inj_on_def, of f t] by auto
7.114 +  hence "inj_on f t" unfolding inj_on_def by simp
7.115 +  hence "infinite (f ` t)" using assms(2) using finite_imageD by auto
7.116    moreover
7.117    { fix x assume "x\<in>t" "f x \<notin> g"
7.118      from g(3) assms(3) `x\<in>t` obtain h where "h\<in>g" and "x\<in>h" by auto
7.119 @@ -3143,7 +3146,7 @@
7.120        using `?lhs`[unfolded continuous_within Lim_within] by auto
7.121      { fix y assume "y\<in>f ` (ball x d \<inter> s)"
7.122        hence "y \<in> ball (f x) e" using d(2) unfolding dist_nz[THEN sym]
7.123 -        apply (auto simp add: dist_commute mem_ball) apply(erule_tac x=xa in ballE) apply auto using `e>0` by auto
7.124 +        apply (auto simp add: dist_commute) apply(erule_tac x=xa in ballE) apply auto using `e>0` by auto
7.125      }
7.126      hence "\<exists>d>0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e" using `d>0` unfolding subset_eq ball_def by (auto simp add: dist_commute)  }
7.127    thus ?rhs by auto
7.128 @@ -3875,7 +3878,7 @@
7.129    fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
7.130    assumes "connected s"  "continuous_on s f"  "open {x \<in> s. f x = a}"  "\<exists>x \<in> s.  f x = a"
7.131    shows "\<forall>x \<in> s. f x = a"
7.132 -using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open] using assms (3,4) by auto
7.133 +using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open] using assms (3,4) by fast
7.134
7.135  text{* Some arithmetical combinations (more to prove).                           *}
7.136
7.137 @@ -4387,7 +4390,7 @@
7.138        using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. sndcart (x n)"], THEN spec[where x="sndcart l"]]
7.139        unfolding Lim_sequentially by auto
7.140      hence "l \<in> {pastecart x y |x y. x \<in> s \<and> y \<in> t}" apply- unfolding mem_Collect_eq apply(rule_tac x="fstcart l" in exI,rule_tac x="sndcart l" in exI) by auto }
7.141 -  thus ?thesis unfolding closed_sequential_limits by auto
7.142 +  thus ?thesis unfolding closed_sequential_limits by blast
7.143  qed
7.144
7.145  lemma compact_pastecart:
7.146 @@ -4478,7 +4481,7 @@
7.147    have "{x - y | x y . x\<in>s \<and> y\<in>s} \<noteq> {}" using `s \<noteq> {}` by auto
7.148    then obtain x where x:"x\<in>{x - y |x y. x \<in> s \<and> y \<in> s}"  "\<forall>y\<in>{x - y |x y. x \<in> s \<and> y \<in> s}. norm y \<le> norm x"
7.149      using compact_differences[OF assms(1) assms(1)]
7.150 -    using distance_attains_sup[where 'a="'a", unfolded dist_norm, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by(auto simp add: norm_minus_cancel)
7.151 +    using distance_attains_sup[where 'a="'a", unfolded dist_norm, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by auto
7.152    from x(1) obtain a b where "a\<in>s" "b\<in>s" "x = a - b" by auto
7.153    thus ?thesis using x(2)[unfolded `x = a - b`] by blast
7.154  qed
7.155 @@ -4499,7 +4502,7 @@
7.156      hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: ring_simps)  }
7.157    note * = this
7.158    { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
7.159 -    have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s`
7.160 +    have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s`
7.161        by simp (blast intro!: Sup_upper *) }
7.162    moreover
7.163    { fix d::real assume "d>0" "d < diameter s"
7.164 @@ -4530,10 +4533,10 @@
7.165  proof-
7.166    have b:"bounded s" using assms(1) by (rule compact_imp_bounded)
7.167    then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. norm (u - v) \<le> norm (x - y)" using compact_sup_maxdistance[OF assms] by auto
7.168 -  hence "diameter s \<le> norm (x - y)"
7.169 -    by (force simp add: diameter_def intro!: Sup_least)
7.170 +  hence "diameter s \<le> norm (x - y)"
7.171 +    unfolding diameter_def by clarsimp (rule Sup_least, fast+)
7.172    thus ?thesis
7.173 -    by (metis b diameter_bounded_bound order_antisym xys)
7.174 +    by (metis b diameter_bounded_bound order_antisym xys)
7.175  qed
7.176
7.177  text{* Related results with closure as the conclusion.                           *}
7.178 @@ -4722,7 +4725,7 @@
7.179  lemma mem_interval_1: fixes x :: "real^1" shows
7.180   "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
7.181   "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
7.182 -by(simp_all add: Cart_eq vector_less_def vector_le_def forall_1)
7.183 +by(simp_all add: Cart_eq vector_less_def vector_le_def)
7.184
7.185  lemma vec1_interval:fixes a::"real" shows
7.186    "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
7.187 @@ -4748,7 +4751,7 @@
7.188        have "a\$i < b\$i" using as[THEN spec[where x=i]] by auto
7.189        hence "a\$i < ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i < b\$i"
7.191 -        by (auto simp add: less_divide_eq_number_of1)  }
7.192 +        by auto  }
7.193      hence "{a <..< b} \<noteq> {}" using mem_interval(1)[of "?x" a b] by auto  }
7.194    ultimately show ?th1 by blast
7.195
7.196 @@ -4763,7 +4766,7 @@
7.197        have "a\$i \<le> b\$i" using as[THEN spec[where x=i]] by auto
7.198        hence "a\$i \<le> ((1/2) *\<^sub>R (a+b)) \$ i" "((1/2) *\<^sub>R (a+b)) \$ i \<le> b\$i"
7.200 -        by (auto simp add: less_divide_eq_number_of1)  }
7.201 +        by auto  }
7.202      hence "{a .. b} \<noteq> {}" using mem_interval(2)[of "?x" a b] by auto  }
7.203    ultimately show ?th2 by blast
7.204  qed
7.205 @@ -4826,13 +4829,13 @@
7.206        { fix j
7.207          have "c \$ j < ?x \$ j \<and> ?x \$ j < d \$ j" unfolding Cart_lambda_beta
7.208            apply(cases "j=i") using as(2)[THEN spec[where x=j]]
7.209 -          by (auto simp add: less_divide_eq_number_of1 as2)  }
7.210 +          by (auto simp add: as2)  }
7.211        hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
7.212        moreover
7.213        have "?x\<notin>{a .. b}"
7.214          unfolding mem_interval apply auto apply(rule_tac x=i in exI)
7.215          using as(2)[THEN spec[where x=i]] and as2
7.216 -        by (auto simp add: less_divide_eq_number_of1)
7.217 +        by auto
7.218        ultimately have False using as by auto  }
7.219      hence "a\$i \<le> c\$i" by(rule ccontr)auto
7.220      moreover
7.221 @@ -4841,13 +4844,13 @@
7.222        { fix j
7.223          have "d \$ j > ?x \$ j \<and> ?x \$ j > c \$ j" unfolding Cart_lambda_beta
7.224            apply(cases "j=i") using as(2)[THEN spec[where x=j]]
7.225 -          by (auto simp add: less_divide_eq_number_of1 as2)  }
7.226 +          by (auto simp add: as2)  }
7.227        hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
7.228        moreover
7.229        have "?x\<notin>{a .. b}"
7.230          unfolding mem_interval apply auto apply(rule_tac x=i in exI)
7.231          using as(2)[THEN spec[where x=i]] and as2
7.232 -        by (auto simp add: less_divide_eq_number_of1)
7.233 +        by auto
7.234        ultimately have False using as by auto  }
7.235      hence "b\$i \<ge> d\$i" by(rule ccontr)auto
7.236      ultimately
7.237 @@ -4878,7 +4881,7 @@
7.238  lemma inter_interval: fixes a :: "'a::linorder^'n" shows
7.239   "{a .. b} \<inter> {c .. d} =  {(\<chi> i. max (a\$i) (c\$i)) .. (\<chi> i. min (b\$i) (d\$i))}"
7.240    unfolding expand_set_eq and Int_iff and mem_interval
7.241 -  by (auto simp add: less_divide_eq_number_of1 intro!: bexI)
7.242 +  by auto
7.243
7.244  (* Moved interval_open_subset_closed a bit upwards *)
7.245
7.246 @@ -4918,7 +4921,7 @@
7.247    using open_interval[of "vec1 a" "vec1 b"] unfolding open_contains_ball
7.248    apply-apply(rule,erule_tac x="vec1 x" in ballE) apply(erule exE,rule_tac x=e in exI)
7.249    unfolding subset_eq mem_ball apply(rule) defer apply(rule,erule conjE,erule_tac x="vec1 xa" in ballE)
7.250 -  by(auto simp add: vec1_dest_vec1_simps vector_less_def forall_1)
7.251 +  by(auto simp add: dist_vec1 dist_real_def vector_less_def)
7.252
7.253  lemma closed_interval[intro]: fixes a :: "real^'n" shows "closed {a .. b}"
7.254  proof-
7.255 @@ -4999,7 +5002,7 @@
7.256      have "a \$ i < ((1 / 2) *\<^sub>R (a + b)) \$ i \<and> ((1 / 2) *\<^sub>R (a + b)) \$ i < b \$ i"
7.257        using assms[unfolded interval_ne_empty, THEN spec[where x=i]]
7.259 -      by(auto simp add: less_divide_eq_number_of1)  }
7.260 +      by auto  }
7.261    thus ?thesis unfolding mem_interval by auto
7.262  qed
7.263
7.264 @@ -5041,7 +5044,7 @@
7.265          x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
7.266          by (auto simp add: algebra_simps)
7.267        hence "f n < b" and "a < f n" using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *] unfolding f_def by auto
7.268 -      hence False using fn unfolding f_def using xc by(auto simp add: vector_mul_lcancel vector_ssub_ldistrib)  }
7.269 +      hence False using fn unfolding f_def using xc by(auto simp add: vector_ssub_ldistrib)  }
7.270      moreover
7.271      { assume "\<not> (f ---> x) sequentially"
7.272        { fix e::real assume "e>0"
7.273 @@ -5457,7 +5460,7 @@
7.274        then obtain y where y:"y\<in>t" "g y = x" by auto
7.275        then obtain x' where x':"x'\<in>s" "f x' = y" using assms(3) by auto
7.276        hence "x \<in> s" unfolding g_def using someI2[of "\<lambda>b. b\<in>s \<and> f b = y" x' "\<lambda>x. x\<in>s"] unfolding y(2)[THEN sym] and g_def by auto }
7.277 -    ultimately have "x\<in>s \<longleftrightarrow> x \<in> g ` t" by auto  }
7.278 +    ultimately have "x\<in>s \<longleftrightarrow> x \<in> g ` t" ..  }
7.279    hence "g ` t = s" by auto
7.280    ultimately
7.281    show ?thesis unfolding homeomorphism_def homeomorphic_def
7.282 @@ -5599,7 +5602,7 @@
7.283    let ?S' = "{x::real^'m. x\<in>s \<and> norm x = norm a}"
7.284    let ?S'' = "{x::real^'m. norm x = norm a}"
7.285
7.286 -  have "?S'' = frontier(cball 0 (norm a))" unfolding frontier_cball and dist_norm by (auto simp add: norm_minus_cancel)
7.287 +  have "?S'' = frontier(cball 0 (norm a))" unfolding frontier_cball and dist_norm by auto
7.288    hence "compact ?S''" using compact_frontier[OF compact_cball, of 0 "norm a"] by auto
7.289    moreover have "?S' = s \<inter> ?S''" by auto
7.290    ultimately have "compact ?S'" using closed_inter_compact[of s ?S''] using s(1) by auto
7.291 @@ -5646,7 +5649,7 @@
7.292
7.293  lemma subspace_substandard:
7.294   "subspace {x::real^_. (\<forall>i. P i \<longrightarrow> x\$i = 0)}"
7.296 +  unfolding subspace_def by auto
7.297
7.298  lemma closed_substandard:
7.299   "closed {x::real^'n. \<forall>i. P i --> x\$i = 0}" (is "closed ?A")
7.300 @@ -5663,7 +5666,7 @@
7.301          then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::real^'n. inner (basis i) x = 0}" by auto
7.302          hence "x \$ i = 0" unfolding B using x unfolding inner_basis by auto  }
7.303        hence "x\<in>?A" by auto }
7.304 -    ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" by auto }
7.305 +    ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" .. }
7.306    hence "?A = \<Inter> ?Bs" by auto
7.307    thus ?thesis by(auto simp add: closed_Inter closed_hyperplane)
7.308  qed
7.309 @@ -5839,23 +5842,23 @@
7.310    case False
7.311    { fix y assume "a \<le> y" "y \<le> b" "m > 0"
7.312      hence "m *\<^sub>R a + c \<le> m *\<^sub>R y + c"  "m *\<^sub>R y + c \<le> m *\<^sub>R b + c"
7.314 +      unfolding vector_le_def by auto
7.315    } moreover
7.316    { fix y assume "a \<le> y" "y \<le> b" "m < 0"
7.317      hence "m *\<^sub>R b + c \<le> m *\<^sub>R y + c"  "m *\<^sub>R y + c \<le> m *\<^sub>R a + c"
7.319 +      unfolding vector_le_def by(auto simp add: mult_left_mono_neg)
7.320    } moreover
7.321    { fix y assume "m > 0"  "m *\<^sub>R a + c \<le> y"  "y \<le> m *\<^sub>R b + c"
7.322      hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
7.323        unfolding image_iff Bex_def mem_interval vector_le_def