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.8 -qed (simp add: subseq_def)
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.5 simp add: ac_simps powr_add[symmetric] r powr_realpow)
2.6 with `\<not> p + e < 0` show ?thesis
2.7 - by transfer
2.8 - (auto simp add: round_down_def field_simps powr_add powr_minus inverse_eq_divide)
2.9 + by transfer (auto simp add: round_down_def field_simps powr_add powr_minus)
2.10 qed
2.11 hide_fact (open) compute_float_down
2.12
2.13 @@ -682,8 +681,7 @@
2.14 by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow
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.18 - (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus inverse_eq_divide)
2.19 + by transfer (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus)
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.48 apply (simp add: ceiling_less_eq)
2.49 done
2.50 @@ -1415,7 +1413,7 @@
2.51 by (simp add: powr_divide2[symmetric] powr_add powr_minus inverse_eq_divide)
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.57 using real_of_int_floor_add_one_gt
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.7 - by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps)
4.8 + by (simp add: abs_lattice add_sup_inf_distribs ac_simps)
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.18 apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
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}"
5.7 - by (simp add: k uminus_add_conv_diff Collect_disj_eq
5.8 - del: mult_pCons_left)
5.9 + by (simp add: k Collect_disj_eq del: mult_pCons_left)
5.10 qed
5.11 qed
5.12