author wenzelm Tue Aug 05 16:58:19 2014 +0200 (2014-08-05) changeset 57865 dcfb33c26f50 parent 57864 7cf01ece66e4 child 57866 1dbc506289bb
tuned proofs -- fewer warnings;
```     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Tue Aug 05 16:21:27 2014 +0200
1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Tue Aug 05 16:58:19 2014 +0200
1.3 @@ -74,7 +74,7 @@
1.4    have c: "inv (a \<otimes> b) \<otimes> a \<in> carrier G" by simp
1.5
1.6    have "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = inv (a \<otimes> b) \<otimes> (a \<otimes> b)" by (simp add: m_assoc)
1.7 -  also have "\<dots> = \<one>" by (simp add: Units_l_inv)
1.8 +  also have "\<dots> = \<one>" by simp
1.9    finally have li: "(inv (a \<otimes> b) \<otimes> a) \<otimes> b = \<one>" .
1.10
1.11    have "\<one> = inv a \<otimes> a" by (simp add: Units_l_inv[symmetric])
1.12 @@ -83,7 +83,7 @@
1.13         by (simp add: Units_r_inv[OF abunit, symmetric] del: Units_r_inv)
1.14    also have "\<dots> = ((inv a \<otimes> a) \<otimes> b) \<otimes> inv (a \<otimes> b) \<otimes> a"
1.15      by (simp add: m_assoc del: Units_l_inv)
1.16 -  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by (simp add: Units_l_inv)
1.17 +  also have "\<dots> = b \<otimes> inv (a \<otimes> b) \<otimes> a" by simp
1.18    also have "\<dots> = b \<otimes> (inv (a \<otimes> b) \<otimes> a)" by (simp add: m_assoc)
1.19    finally have ri: "b \<otimes> (inv (a \<otimes> b) \<otimes> a) = \<one> " by simp
1.20
1.21 @@ -327,7 +327,7 @@
1.22  unfolding a
1.23  apply (intro associatedI)
1.24   apply (rule dividesI[of "inv u"], simp)
1.25 - apply (simp add: m_assoc Units_closed Units_r_inv)
1.26 + apply (simp add: m_assoc Units_closed)
1.27  apply fast
1.28  done
1.29
1.30 @@ -1764,7 +1764,7 @@
1.31    note [simp] = acarr Units_closed[OF uunit] Units_inv_closed[OF uunit]
1.32
1.33    have "a = a \<otimes> \<one>" by simp
1.34 -  also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: Units_r_inv uunit)
1.35 +  also have "\<dots> = a \<otimes> (u \<otimes> inv u)" by (simp add: uunit)
1.36    also have "\<dots> = a' \<otimes> inv u" by (simp add: m_assoc[symmetric] a'[symmetric])
1.37    finally
1.38         have a: "a = a' \<otimes> inv u" .
1.39 @@ -2646,7 +2646,7 @@
1.40      hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+
1.41
1.42      from ya yb csmset
1.43 -    have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def multiset_inter_count)
1.44 +    have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def)
1.45      thus "y divides c" by (rule fmsubset_divides) fact+
1.46    qed
1.47
1.48 @@ -3208,7 +3208,7 @@
1.49            and nyx: "\<not> y \<sim> x"
1.50            by - (fast elim: properfactorE2)+
1.51        hence "\<exists>z. z \<in> carrier G \<and> x = y \<otimes> z"
1.52 -          by (fast elim: dividesE)
1.53 +          by fast
1.54
1.55        from this obtain z
1.56            where zcarr: "z \<in> carrier G"
1.57 @@ -3327,7 +3327,7 @@
1.58        and afs': "wfactors G as' a"
1.59      hence ahdvda: "ah divides a"
1.60        by (intro wfactors_dividesI[of "ah#as" "a"], simp+)
1.61 -    hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE)
1.62 +    hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by fast
1.63      from this obtain a'
1.64        where a'carr: "a' \<in> carrier G"
1.65        and a: "a = ah \<otimes> a'"
1.66 @@ -3360,7 +3360,7 @@
1.67        have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force)
1.68      note carr = carr asicarr
1.69
1.70 -    from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE)
1.71 +    from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by fast
1.72      from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto
1.73
1.74      with carr irrasi[simplified asi]
1.75 @@ -3454,7 +3454,7 @@
1.76      next
1.77        show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
1.79 -      apply (simp add: asiah[symmetric] ahcarr asicarr)
1.80 +      apply (simp add: asiah[symmetric])
1.81        done
1.82      qed
1.83
1.84 @@ -3463,12 +3463,12 @@
1.85      also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
1.86        (take i as' @ as' ! i # drop (Suc i) as')"
1.87        apply (intro essentially_equalI)
1.88 -      apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
1.89 +       apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
1.90          take i as' @ as' ! i # drop (Suc i) as'")
1.91 -  apply simp
1.92 +        apply simp
1.93         apply (rule perm_append_Cons)
1.94        apply simp
1.95 -    done
1.96 +      done
1.97      finally
1.98        have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" by simp
1.99      then show "essentially_equal G (ah # as) as'" by (subst as', assumption)
1.100 @@ -3617,7 +3617,7 @@
1.101      also from ccarr acarr cunit
1.102          have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc)
1.103      also from ccarr cunit
1.104 -        have "\<dots> = a \<otimes> \<one>" by (simp add: Units_r_inv)
1.105 +        have "\<dots> = a \<otimes> \<one>" by simp
1.106      also from acarr
1.107          have "\<dots> = a" by simp
1.108      finally have "a = b \<otimes> inv c" by simp
1.109 @@ -3706,7 +3706,7 @@
1.110    shows "(divisor_chain_condition_monoid G \<and> gcd_condition_monoid G) = factorial_monoid G"
1.111  apply rule
1.112  proof clarify
1.113 -    assume dcc: "divisor_chain_condition_monoid G"
1.114 +  assume dcc: "divisor_chain_condition_monoid G"
1.115       and gc: "gcd_condition_monoid G"
1.116    interpret divisor_chain_condition_monoid "G" by (rule dcc)
1.117    interpret gcd_condition_monoid "G" by (rule gc)
```
```     2.1 --- a/src/HOL/Algebra/Exponent.thy	Tue Aug 05 16:21:27 2014 +0200
2.2 +++ b/src/HOL/Algebra/Exponent.thy	Tue Aug 05 16:58:19 2014 +0200
2.3 @@ -249,7 +249,7 @@
2.4  apply (simp (no_asm))
2.5  (*induction step*)
2.6  apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0")
2.7 - prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
2.8 + prefer 2 apply (simp, clarify)
2.9  apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) =
2.10                      exponent p (Suc k)")
2.11   txt{*First, use the assumed equation.  We simplify the LHS to
2.12 @@ -260,7 +260,7 @@
2.13     @{text Suc_times_binomial_eq} ...*}
2.15  txt{*...then @{text exponent_mult_add} and the quantified premise.*}
2.18  done
2.19
2.20  (*The lemma above, with two changes of variables*)
```
```     3.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Aug 05 16:21:27 2014 +0200
3.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Tue Aug 05 16:58:19 2014 +0200
3.3 @@ -528,7 +528,7 @@
3.4      case 0 with R show ?thesis by simp
3.5    next
3.6      case Suc with R show ?thesis
3.7 -      using R.finsum_Suc2 by (simp del: R.finsum_Suc add: R.r_null Pi_def)
3.8 +      using R.finsum_Suc2 by (simp del: R.finsum_Suc add: Pi_def)
3.9    qed
3.11
```
```     4.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 05 16:21:27 2014 +0200
4.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 05 16:58:19 2014 +0200
4.3 @@ -137,17 +137,17 @@
4.4  end
4.5  *} "lift trivial vector statements to real arith statements"
4.6
4.7 -lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def)
4.8 -lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def)
4.9 +lemma vec_0[simp]: "vec 0 = 0" by vector
4.10 +lemma vec_1[simp]: "vec 1 = 1" by vector
4.11
4.12  lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector
4.13
4.14  lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
4.15
4.16 -lemma vec_add: "vec(x + y) = vec x + vec y"  by (vector vec_def)
4.17 -lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def)
4.18 -lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def)
4.19 -lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
4.20 +lemma vec_add: "vec(x + y) = vec x + vec y"  by vector
4.21 +lemma vec_sub: "vec(x - y) = vec x - vec y" by vector
4.22 +lemma vec_cmul: "vec(c * x) = c *s vec x " by vector
4.23 +lemma vec_neg: "vec(- x) = - vec x " by vector
4.24
4.25  lemma vec_setsum:
4.26    assumes "finite S"
4.27 @@ -164,7 +164,7 @@
4.28  text{* Obvious "component-pushing". *}
4.29
4.30  lemma vec_component [simp]: "vec x \$ i = x"
4.31 -  by (vector vec_def)
4.32 +  by vector
4.33
4.34  lemma vector_mult_component [simp]: "(x * y)\$i = x\$i * y\$i"
4.35    by vector
4.36 @@ -330,7 +330,7 @@
4.37    assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
4.38    shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) *  e"
4.39    using setsum_norm_allsubsets_bound[OF assms]
4.40 -  by (simp add: DIM_cart Basis_real_def)
4.41 +  by simp
4.42
4.43  subsection {* Matrix operations *}
4.44
```
```     5.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 05 16:21:27 2014 +0200
5.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Aug 05 16:58:19 2014 +0200
5.3 @@ -1502,7 +1502,7 @@
5.4        by (intro convex_linear_vimage convex_translation convex_convex_hull,
5.6      also have "?S = {y. (x, y) \<in> convex hull (s \<times> t)}"
5.8 +      by (auto simp add: image_def Bex_def)
5.9      finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
5.10    next
5.11      show "convex {x. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)}"
5.12 @@ -1512,7 +1512,7 @@
5.13        by (intro convex_linear_vimage convex_translation convex_convex_hull,
5.15        also have "?S = {x. (x, y) \<in> convex hull (s \<times> t)}"
5.17 +        by (auto simp add: image_def Bex_def)
5.18        finally show "convex {x. (x, y) \<in> convex hull (s \<times> t)}" .
5.19      qed
5.20    qed
5.21 @@ -5504,12 +5504,12 @@
5.22      using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *\<^sub>R -a + ?d *\<^sub>R x) ` s",
5.23        OF convex_affinity compact_affinity]
5.24      using assms(1,2)
5.26 +    by (auto simp add: scaleR_right_diff_distrib)
5.27    then show ?thesis
5.28      apply (rule_tac homeomorphic_trans[OF _ homeomorphic_balls(2)[of 1 _ ?n]])
5.29      apply (rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
5.30      using `d>0` `e>0`
5.32 +    apply (auto simp add: scaleR_right_diff_distrib)
5.33      done
5.34  qed
5.35
5.36 @@ -5808,7 +5808,7 @@
5.37    apply (rule_tac f="\<lambda>x. a + x" in arg_cong)
5.38    apply (rule setsum.cong [OF refl])
5.39    apply clarsimp
5.40 -  apply (fast intro: set_plus_intro)
5.41 +  apply fast
5.42    done
5.43
5.44  lemma box_eq_set_setsum_Basis:
5.45 @@ -5895,7 +5895,7 @@
5.46      apply (rule image_eqI[where x="{i. i\<in>Basis \<and> x\<bullet>i = 1}"])
5.47      using as
5.48      apply (subst euclidean_eq_iff)
5.49 -    apply (auto simp: inner_setsum_left_Basis)
5.50 +    apply auto
5.51      done
5.52  qed auto
5.53
5.54 @@ -6430,7 +6430,7 @@
5.55          apply (subst (asm) euclidean_eq_iff)
5.56          using i
5.57          apply (erule_tac x=i in ballE)
5.58 -        apply (auto simp add:field_simps inner_simps)
5.59 +        apply (auto simp add: field_simps inner_simps)
5.60          done
5.61        finally show "x \<bullet> i =
5.62          ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) \<bullet> i"
5.63 @@ -8138,8 +8138,7 @@
5.64      and "convex S"
5.65      and "rel_open S"
5.66    shows "convex (f ` S) \<and> rel_open (f ` S)"
5.67 -  by (metis assms convex_linear_image rel_interior_convex_linear_image
5.68 -    linear_conv_bounded_linear rel_open_def)
5.69 +  by (metis assms convex_linear_image rel_interior_convex_linear_image rel_open_def)
5.70
5.71  lemma convex_rel_open_linear_preimage:
5.72    fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
```
```     6.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Aug 05 16:21:27 2014 +0200
6.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Aug 05 16:58:19 2014 +0200
6.3 @@ -69,7 +69,7 @@
6.4  lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
6.5      bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x within s)"
6.6    unfolding has_derivative_def Lim
6.7 -  by (auto simp add: netlimit_within inverse_eq_divide field_simps)
6.8 +  by (auto simp add: netlimit_within field_simps)
6.9
6.10  lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
6.11      bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) ---> 0) (at x)"
6.12 @@ -1773,9 +1773,9 @@
6.13          apply (rule lem3[rule_format])+
6.14          done
6.15        obtain N where N: "\<forall>h. norm (f' N x h - g' x h) \<le> 1 * norm h"
6.16 -        using assms(3) `x \<in> s` by (fast intro: zero_less_one order_refl)
6.17 +        using assms(3) `x \<in> s` by (fast intro: zero_less_one)
6.18        have "bounded_linear (f' N x)"
6.19 -        using assms(2) `x \<in> s` by (fast dest: has_derivative_bounded_linear)
6.20 +        using assms(2) `x \<in> s` by fast
6.21        from bounded_linear.bounded [OF this]
6.22        obtain K where K: "\<forall>h. norm (f' N x h) \<le> norm h * K" ..
6.23        {
```
```     7.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Aug 05 16:21:27 2014 +0200
7.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Aug 05 16:58:19 2014 +0200
7.3 @@ -1125,7 +1125,7 @@
7.4    note fin = this
7.5    have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
7.6      using f
7.7 -    by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)
7.8 +    by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
7.9    also have "\<dots> = ereal r"
7.10      using fin r by (auto simp: ereal_real)
7.11    finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
7.12 @@ -1252,7 +1252,8 @@
7.13    apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
7.14    apply (drule sym)
7.15    apply auto
7.16 -  by (metis INF_absorb centre_in_ball)
7.17 +  apply (metis INF_absorb centre_in_ball)
7.18 +  done
7.19
7.20
7.21  lemma suminf_ereal_offset_le:
```
```     8.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Aug 05 16:21:27 2014 +0200
8.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Aug 05 16:58:19 2014 +0200
8.3 @@ -343,7 +343,7 @@
8.4                  using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
8.5                then have "y\<bullet>k < a\<bullet>k"
8.6                  using e[THEN conjunct1] k
8.7 -                by (auto simp add: field_simps abs_less_iff as inner_Basis inner_simps)
8.8 +                by (auto simp add: field_simps abs_less_iff as inner_simps)
8.9                then have "y \<notin> i"
8.10                  unfolding ab mem_box by (auto intro!: bexI[OF _ k])
8.11                then show False using yi by auto
8.12 @@ -12092,7 +12092,7 @@
8.13      by (induct I) (auto intro!: bounded_linear_add bounded_linear_zero)
8.14  next
8.15    case False
8.16 -  then show ?thesis by (simp add: bounded_linear_zero)
8.17 +  then show ?thesis by simp
8.18  qed
8.19
8.20  lemma absolutely_integrable_vector_abs:
```
```     9.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 05 16:21:27 2014 +0200
9.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 05 16:58:19 2014 +0200
9.3 @@ -7307,27 +7307,27 @@
9.4
9.5  lemma real_affinity_le:
9.6   "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c \<le> y \<longleftrightarrow> x \<le> inverse(m) * y + -(c / m))"
9.7 -  by (simp add: field_simps inverse_eq_divide)
9.8 +  by (simp add: field_simps)
9.9
9.10  lemma real_le_affinity:
9.11   "0 < (m::'a::linordered_field) \<Longrightarrow> (y \<le> m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) \<le> x)"
9.12 -  by (simp add: field_simps inverse_eq_divide)
9.13 +  by (simp add: field_simps)
9.14
9.15  lemma real_affinity_lt:
9.16   "0 < (m::'a::linordered_field) \<Longrightarrow> (m * x + c < y \<longleftrightarrow> x < inverse(m) * y + -(c / m))"
9.17 -  by (simp add: field_simps inverse_eq_divide)
9.18 +  by (simp add: field_simps)
9.19
9.20  lemma real_lt_affinity:
9.21   "0 < (m::'a::linordered_field) \<Longrightarrow> (y < m * x + c \<longleftrightarrow> inverse(m) * y + -(c / m) < x)"
9.22 -  by (simp add: field_simps inverse_eq_divide)
9.23 +  by (simp add: field_simps)
9.24
9.25  lemma real_affinity_eq:
9.26   "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (m * x + c = y \<longleftrightarrow> x = inverse(m) * y + -(c / m))"
9.27 -  by (simp add: field_simps inverse_eq_divide)
9.28 +  by (simp add: field_simps)
9.29
9.30  lemma real_eq_affinity:
9.31   "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (y = m * x + c  \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
9.32 -  by (simp add: field_simps inverse_eq_divide)
9.33 +  by (simp add: field_simps)
9.34
9.35
9.36  subsection {* Banach fixed point theorem (not really topological...) *}
```