# HG changeset patch
# User wenzelm
# Date 1407236175 -7200
# Node ID 8f074e6e22fc7da4fabca74f10ae2f045aab9599
# Parent  287e3b1298b375f7cdbd004bf2234bd569d4cf5d
tuned proofs;

diff -r 287e3b1298b3 -r 8f074e6e22fc src/HOL/Library/Diagonal_Subsequence.thy
--- 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))"
diff -r 287e3b1298b3 -r 8f074e6e22fc src/HOL/Library/Float.thy
--- 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
diff -r 287e3b1298b3 -r 8f074e6e22fc src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- 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)))"
diff -r 287e3b1298b3 -r 8f074e6e22fc src/HOL/Library/Lattice_Algebras.thy
--- 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
diff -r 287e3b1298b3 -r 8f074e6e22fc src/HOL/Library/Polynomial.thy
--- 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