--- a/src/HOL/Library/Diagonal_Subsequence.thy Tue Aug 05 12:42:38 2014 +0200
+++ b/src/HOL/Library/Diagonal_Subsequence.thy Tue Aug 05 12:56:15 2014 +0200
@@ -27,8 +27,10 @@
lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)"
proof (induct n)
- case (Suc n) thus ?case by (subst seqseq.simps) (auto simp: subseq_reduce intro!: subseq_o)
-qed (simp add: subseq_def)
+ case 0 thus ?case by (simp add: subseq_def)
+next
+ case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: subseq_o)
+qed
lemma seqseq_holds:
"P n (seqseq (Suc n))"
--- a/src/HOL/Library/Float.thy Tue Aug 05 12:42:38 2014 +0200
+++ b/src/HOL/Library/Float.thy Tue Aug 05 12:56:15 2014 +0200
@@ -610,8 +610,7 @@
by (auto intro: exI[where x="m*2^nat (e+p)"]
simp add: ac_simps powr_add[symmetric] r powr_realpow)
with `\<not> p + e < 0` show ?thesis
- by transfer
- (auto simp add: round_down_def field_simps powr_add powr_minus inverse_eq_divide)
+ by transfer (auto simp add: round_down_def field_simps powr_add powr_minus)
qed
hide_fact (open) compute_float_down
@@ -682,8 +681,7 @@
by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow
intro: exI[where x="m*2^nat (e+p)"])
then show ?thesis using `\<not> p + e < 0`
- by transfer
- (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus inverse_eq_divide)
+ by transfer (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus)
qed
hide_fact (open) compute_float_up
@@ -840,7 +838,7 @@
have "(1::int) < 2" by simp
case False let ?S = "2^(nat (-e))"
have "inverse (2 ^ nat (- e)) = 2 powr e" using assms False powr_realpow[of 2 "nat (-e)"]
- by (auto simp: powr_minus field_simps inverse_eq_divide)
+ by (auto simp: powr_minus field_simps)
hence "1 \<le> real m * inverse ?S" using assms False powr_realpow[of 2 "nat (-e)"]
by (auto simp: powr_minus)
hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
@@ -940,7 +938,7 @@
have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
moreover have "real x * real (2::int) powr real l / real y = x / real y'"
using `\<not> 0 \<le> l`
- by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps inverse_eq_divide)
+ by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
ultimately show ?thesis
unfolding normfloat_def
using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
@@ -993,7 +991,7 @@
using rat_precision_pos[OF assms] by (rule power_aux)
finally show ?thesis
apply (transfer fixing: n x y)
- apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide powr1)
+ apply (simp add: round_up_def field_simps powr_minus powr1)
unfolding int_of_reals real_of_int_less_iff
apply (simp add: ceiling_less_eq)
done
@@ -1415,7 +1413,7 @@
by (simp add: powr_divide2[symmetric] powr_add powr_minus inverse_eq_divide)
also have "\<dots> = 2 powr (log 2 x - (real \<lfloor>log 2 x\<rfloor>) - 1)"
using `0 < x`
- by (auto simp: inverse_eq_divide field_simps powr_add powr_divide2[symmetric])
+ by (auto simp: field_simps powr_add powr_divide2[symmetric])
also have "\<dots> < 2 powr 0"
using real_of_int_floor_add_one_gt
unfolding neg_less_iff_less
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Aug 05 12:42:38 2014 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Aug 05 12:56:15 2014 +0200
@@ -808,7 +808,7 @@
then have tw: "cmod ?w \<le> cmod w"
using t(1) by (simp add: norm_mult)
from t inv0 have "t * (cmod w ^ (k + 1) * m) < 1"
- by (simp add: inverse_eq_divide field_simps)
+ by (simp add: field_simps)
with zero_less_power[OF t(1), of k] have th30: "t^k * (t* (cmod w ^ (k + 1) * m)) < t^k * 1"
by (metis comm_mult_strict_left_mono)
have "cmod (?w^k * ?w * poly s ?w) = t^k * (t* (cmod w ^ (k + 1) * cmod (poly s ?w)))"
--- a/src/HOL/Library/Lattice_Algebras.thy Tue Aug 05 12:42:38 2014 +0200
+++ b/src/HOL/Library/Lattice_Algebras.thy Tue Aug 05 12:56:15 2014 +0200
@@ -396,7 +396,7 @@
proof -
have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup (- a - b) (sup (- a + b) (a + (- b))))"
(is "_=sup ?m ?n")
- by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps)
+ by (simp add: abs_lattice add_sup_inf_distribs ac_simps)
have a: "a + b \<le> sup ?m ?n"
by simp
have b: "- a - b \<le> ?n"
@@ -410,7 +410,7 @@
from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n"
apply -
apply (drule abs_leI)
- apply (simp_all only: algebra_simps ac_simps minus_add)
+ apply (simp_all only: algebra_simps minus_add)
apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
done
with g[symmetric] show ?thesis by simp
--- a/src/HOL/Library/Polynomial.thy Tue Aug 05 12:42:38 2014 +0200
+++ b/src/HOL/Library/Polynomial.thy Tue Aug 05 12:56:15 2014 +0200
@@ -1315,8 +1315,7 @@
then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps)
then have "finite (insert a {x. poly k x = 0})" by simp
then show "finite {x. poly p x = 0}"
- by (simp add: k uminus_add_conv_diff Collect_disj_eq
- del: mult_pCons_left)
+ by (simp add: k Collect_disj_eq del: mult_pCons_left)
qed
qed