tuned proofs;
authorwenzelm
Tue Mar 26 19:43:31 2013 +0100 (2013-03-26)
changeset 51541e7b6b61b7be2
parent 51539 625d2ec0bbff
child 51542 738598beeb26
tuned proofs;
src/HOL/Library/Fundamental_Theorem_Algebra.thy
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Mar 26 15:10:28 2013 +0100
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Mar 26 19:43:31 2013 +0100
     1.3 @@ -191,7 +191,7 @@
     1.4      hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
     1.5        by - (rule power_mono, simp, simp)+
     1.6      hence th0: "4*x^2 \<le> 1" "4*y^2 \<le> 1"
     1.7 -      by (simp_all  add: power2_abs power_mult_distrib)
     1.8 +      by (simp_all add: power_mult_distrib)
     1.9      from add_mono[OF th0] xy have False by simp }
    1.10    thus ?thesis unfolding linorder_not_le[symmetric] by blast
    1.11  qed
    1.12 @@ -490,7 +490,7 @@
    1.13          unfolding norm_mult by (simp add: algebra_simps)
    1.14        from complex_mod_triangle_sub[of "z * poly (pCons c cs) z" a]
    1.15        have th2: "cmod(z * poly (pCons c cs) z) - cmod a \<le> cmod (poly (pCons a (pCons c cs)) z)"
    1.16 -        by (simp add: diff_le_eq algebra_simps)
    1.17 +        by (simp add: algebra_simps)
    1.18        from th1 th2 have "d \<le> cmod (poly (pCons a (pCons c cs)) z)"  by arith}
    1.19      hence ?case by blast}
    1.20    moreover
    1.21 @@ -601,7 +601,6 @@
    1.22      apply (rule_tac x="a" in exI)
    1.23      apply simp
    1.24      apply (rule_tac x="q" in exI)
    1.25 -    apply (auto simp add: power_Suc)
    1.26      apply (auto simp add: psize_def split: if_splits)
    1.27      done
    1.28  qed
    1.29 @@ -718,7 +717,7 @@
    1.30        have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
    1.31          apply - apply (rule mult_strict_left_mono) by simp_all
    1.32        have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k+1) * cmod (poly s ?w)))"  using w0 t(1)
    1.33 -        by (simp add: algebra_simps power_mult_distrib norm_of_real norm_power norm_mult)
    1.34 +        by (simp add: algebra_simps power_mult_distrib norm_power norm_mult)
    1.35        then have "cmod (?w^k * ?w * poly s ?w) \<le> t^k * (t* (cmod w ^ (k + 1) * m))"
    1.36          using t(1,2) m(2)[rule_format, OF tw] w0
    1.37          apply (simp only: )
    1.38 @@ -819,9 +818,8 @@
    1.39          have sne: "s \<noteq> 0"
    1.40            using s pne by auto
    1.41          {assume ds0: "degree s = 0"
    1.42 -          from ds0 have "\<exists>k. s = [:k:]"
    1.43 -            by (cases s, simp split: if_splits)
    1.44 -          then obtain k where kpn: "s = [:k:]" by blast
    1.45 +          from ds0 obtain k where kpn: "s = [:k:]"
    1.46 +            by (cases s) (auto split: if_splits)
    1.47            from sne kpn have k: "k \<noteq> 0" by simp
    1.48            let ?w = "([:1/k:] * ([:-a,1:] ^ (n - ?op))) * (r ^ n)"
    1.49            from k oop [of a] have "q ^ n = p * ?w"
    1.50 @@ -878,9 +876,7 @@
    1.51  
    1.52      then have pp: "\<And>x. poly p x =  c" by simp
    1.53      let ?w = "[:1/c:] * (q ^ n)"
    1.54 -    from ccs
    1.55 -    have "(q ^ n) = (p * ?w) "
    1.56 -      by (simp add: smult_smult)
    1.57 +    from ccs have "(q ^ n) = (p * ?w)" by simp
    1.58      hence ?ths unfolding dvd_def by blast}
    1.59    ultimately show ?ths by blast
    1.60  qed
    1.61 @@ -902,7 +898,7 @@
    1.62    {assume pe: "p \<noteq> 0"
    1.63      {assume dp: "degree p = 0"
    1.64        then obtain k where k: "p = [:k:]" "k\<noteq>0" using pe
    1.65 -        by (cases p, simp split: if_splits)
    1.66 +        by (cases p) (simp split: if_splits)
    1.67        hence th1: "\<forall>x. poly p x \<noteq> 0" by simp
    1.68        from k dp have "q ^ (degree p) = p * [:1/k:]"
    1.69          by (simp add: one_poly_def)
    1.70 @@ -937,7 +933,7 @@
    1.71  next
    1.72    assume r: ?rhs
    1.73    then obtain k where "p = [:k:]"
    1.74 -    by (cases p, simp split: if_splits)
    1.75 +    by (cases p) (simp split: if_splits)
    1.76    then show ?lhs unfolding constant_def by auto
    1.77  qed
    1.78  
    1.79 @@ -1019,14 +1015,13 @@
    1.80    {assume l: ?lhs
    1.81      then obtain u where u: "q = p * u" ..
    1.82       have "r = p * (smult a u - t)"
    1.83 -       using u qrp' [symmetric] t by (simp add: algebra_simps mult_smult_right)
    1.84 +       using u qrp' [symmetric] t by (simp add: algebra_simps)
    1.85       then have ?rhs ..}
    1.86    moreover
    1.87    {assume r: ?rhs
    1.88      then obtain u where u: "r = p * u" ..
    1.89      from u [symmetric] t qrp' [symmetric] a0
    1.90 -    have "q = p * smult (1/a) (u + t)"
    1.91 -      by (simp add: algebra_simps mult_smult_right smult_smult)
    1.92 +    have "q = p * smult (1/a) (u + t)" by (simp add: algebra_simps)
    1.93      hence ?lhs ..}
    1.94    ultimately have "?lhs = ?rhs" by blast }
    1.95  thus "?lhs \<equiv> ?rhs"  by - (atomize(full), blast)
    1.96 @@ -1056,7 +1051,7 @@
    1.97  proof-
    1.98    have "p = 0 \<longleftrightarrow> poly p = poly 0"
    1.99      by (simp add: poly_zero)
   1.100 -  also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by (auto intro: ext)
   1.101 +  also have "\<dots> \<longleftrightarrow> (\<not> (\<exists>x. poly p x \<noteq> 0))" by auto
   1.102    finally show "(\<exists>x. poly p x \<noteq> (0::complex)) \<equiv> p \<noteq> 0"
   1.103      by - (atomize (full), blast)
   1.104  qed
   1.105 @@ -1078,7 +1073,7 @@
   1.106    assumes h: "\<And>x. poly (q ^ n) x \<equiv> poly r x"
   1.107    shows "p dvd (q ^ n) \<equiv> p dvd r"
   1.108  proof-
   1.109 -  from h have "poly (q ^ n) = poly r" by (auto intro: ext)
   1.110 +  from h have "poly (q ^ n) = poly r" by auto
   1.111    then have "(q ^ n) = r" by (simp add: poly_eq_iff)
   1.112    thus "p dvd (q ^ n) \<equiv> p dvd r" by simp
   1.113  qed