author wenzelm Tue Aug 05 12:56:15 2014 +0200 (2014-08-05) changeset 57862 8f074e6e22fc parent 57861 287e3b1298b3 child 57863 0c104888f1ca
tuned proofs;
 src/HOL/Library/Diagonal_Subsequence.thy file | annotate | diff | revisions src/HOL/Library/Float.thy file | annotate | diff | revisions src/HOL/Library/Fundamental_Theorem_Algebra.thy file | annotate | diff | revisions src/HOL/Library/Lattice_Algebras.thy file | annotate | diff | revisions src/HOL/Library/Polynomial.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Library/Diagonal_Subsequence.thy	Tue Aug 05 12:42:38 2014 +0200
1.2 +++ b/src/HOL/Library/Diagonal_Subsequence.thy	Tue Aug 05 12:56:15 2014 +0200
1.3 @@ -27,8 +27,10 @@
1.4
1.5  lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)"
1.6  proof (induct n)
1.7 -  case (Suc n) thus ?case by (subst seqseq.simps) (auto simp: subseq_reduce intro!: subseq_o)
1.9 +  case 0 thus ?case by (simp add: subseq_def)
1.10 +next
1.11 +  case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: subseq_o)
1.12 +qed
1.13
1.14  lemma seqseq_holds:
1.15    "P n (seqseq (Suc n))"
```
```     2.1 --- a/src/HOL/Library/Float.thy	Tue Aug 05 12:42:38 2014 +0200
2.2 +++ b/src/HOL/Library/Float.thy	Tue Aug 05 12:56:15 2014 +0200
2.3 @@ -610,8 +610,7 @@
2.4      by (auto intro: exI[where x="m*2^nat (e+p)"]
2.6    with `\<not> p + e < 0` show ?thesis
2.7 -    by transfer
2.10  qed
2.11  hide_fact (open) compute_float_down
2.12
2.13 @@ -682,8 +681,7 @@
2.15        intro: exI[where x="m*2^nat (e+p)"])
2.16    then show ?thesis using `\<not> p + e < 0`
2.17 -    by transfer
2.20  qed
2.21  hide_fact (open) compute_float_up
2.22
2.23 @@ -840,7 +838,7 @@
2.24      have "(1::int) < 2" by simp
2.25      case False let ?S = "2^(nat (-e))"
2.26      have "inverse (2 ^ nat (- e)) = 2 powr e" using assms False powr_realpow[of 2 "nat (-e)"]
2.27 -      by (auto simp: powr_minus field_simps inverse_eq_divide)
2.28 +      by (auto simp: powr_minus field_simps)
2.29      hence "1 \<le> real m * inverse ?S" using assms False powr_realpow[of 2 "nat (-e)"]
2.30        by (auto simp: powr_minus)
2.31      hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
2.32 @@ -940,7 +938,7 @@
2.33      have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
2.34      moreover have "real x * real (2::int) powr real l / real y = x / real y'"
2.35        using `\<not> 0 \<le> l`
2.36 -      by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps inverse_eq_divide)
2.37 +      by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
2.38      ultimately show ?thesis
2.39        unfolding normfloat_def
2.40        using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
2.41 @@ -993,7 +991,7 @@
2.42      using rat_precision_pos[OF assms] by (rule power_aux)
2.43    finally show ?thesis
2.44      apply (transfer fixing: n x y)
2.45 -    apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide powr1)
2.46 +    apply (simp add: round_up_def field_simps powr_minus powr1)
2.47      unfolding int_of_reals real_of_int_less_iff
2.49      done
2.50 @@ -1415,7 +1413,7 @@
2.52    also have "\<dots> = 2 powr (log 2 x - (real \<lfloor>log 2 x\<rfloor>) - 1)"
2.53      using `0 < x`
2.54 -    by (auto simp: inverse_eq_divide field_simps powr_add powr_divide2[symmetric])
2.55 +    by (auto simp: field_simps powr_add powr_divide2[symmetric])
2.56    also have "\<dots> < 2 powr 0"
2.58      unfolding neg_less_iff_less
```
```     3.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Aug 05 12:42:38 2014 +0200
3.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Aug 05 12:56:15 2014 +0200
3.3 @@ -808,7 +808,7 @@
3.4        then have tw: "cmod ?w \<le> cmod w"
3.5          using t(1) by (simp add: norm_mult)
3.6        from t inv0 have "t * (cmod w ^ (k + 1) * m) < 1"
3.7 -        by (simp add: inverse_eq_divide field_simps)
3.8 +        by (simp add: field_simps)
3.9        with zero_less_power[OF t(1), of k] have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
3.10          by (metis comm_mult_strict_left_mono)
3.11        have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k + 1) * cmod (poly s ?w)))"
```
```     4.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Tue Aug 05 12:42:38 2014 +0200
4.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Tue Aug 05 12:56:15 2014 +0200
4.3 @@ -396,7 +396,7 @@
4.4    proof -
4.5      have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup (- a - b) (sup (- a + b) (a + (- b))))"
4.6        (is "_=sup ?m ?n")
4.9      have a: "a + b \<le> sup ?m ?n"
4.10        by simp
4.11      have b: "- a - b \<le> ?n"
4.12 @@ -410,7 +410,7 @@
4.13      from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n"
4.14        apply -
4.15        apply (drule abs_leI)
4.16 -      apply (simp_all only: algebra_simps ac_simps minus_add)
4.17 +      apply (simp_all only: algebra_simps minus_add)
4.19        done
4.20      with g[symmetric] show ?thesis by simp
```
```     5.1 --- a/src/HOL/Library/Polynomial.thy	Tue Aug 05 12:42:38 2014 +0200
5.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Aug 05 12:56:15 2014 +0200
5.3 @@ -1315,8 +1315,7 @@
5.4      then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
5.5      then have "finite (insert a {x. poly k x = 0})" by simp
5.6      then show "finite {x. poly p x = 0}"