Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
authorpaulson <lp15@cam.ac.uk>
Fri Nov 13 12:27:13 2015 +0000 (2015-11-13)
changeset 61649268d88ec9087
parent 61644 b1c24adc1581
child 61650 2be10c63a0ab
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
src/HOL/Archimedean_Field.thy
src/HOL/Binomial.thy
src/HOL/Complex.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Divides.thy
src/HOL/GCD.thy
src/HOL/Inequalities.thy
src/HOL/Int.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/NSA/NSA.thy
src/HOL/Nat.thy
src/HOL/Nat_Transfer.thy
src/HOL/NthRoot.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Old_Number_Theory/Euler.thy
src/HOL/Old_Number_Theory/EvenOdd.thy
src/HOL/Old_Number_Theory/WilsonRuss.thy
src/HOL/Power.thy
src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Rings.thy
src/HOL/Transcendental.thy
src/HOL/Word/Word.thy
src/HOL/ex/Sqrt.thy
src/HOL/ex/Sum_of_Powers.thy
src/HOL/ex/Transfer_Int_Nat.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -152,7 +152,7 @@
     1.4    shows  "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
     1.5  using floor_correct floor_unique by auto
     1.6  
     1.7 -lemma of_int_floor_le: "of_int (floor x) \<le> x"
     1.8 +lemma of_int_floor_le [simp]: "of_int (floor x) \<le> x"
     1.9    using floor_correct ..
    1.10  
    1.11  lemma le_floor_iff: "z \<le> floor x \<longleftrightarrow> of_int z \<le> x"
    1.12 @@ -381,12 +381,12 @@
    1.13    ceiling  ("\<lceil>_\<rceil>")
    1.14  
    1.15  lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)"
    1.16 -  unfolding ceiling_def using floor_correct [of "- x"] by simp
    1.17 +  unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff) 
    1.18  
    1.19  lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> ceiling x = z"
    1.20    unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
    1.21  
    1.22 -lemma le_of_int_ceiling: "x \<le> of_int (ceiling x)"
    1.23 +lemma le_of_int_ceiling [simp]: "x \<le> of_int (ceiling x)"
    1.24    using ceiling_correct ..
    1.25  
    1.26  lemma ceiling_le_iff: "ceiling x \<le> z \<longleftrightarrow> x \<le> of_int z"
    1.27 @@ -494,7 +494,7 @@
    1.28  text \<open>Addition and subtraction of integers\<close>
    1.29  
    1.30  lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z"
    1.31 -  using ceiling_correct [of x] by (simp add: ceiling_unique)
    1.32 +  using ceiling_correct [of x] by (simp add: ceiling_def)
    1.33  
    1.34  lemma ceiling_add_numeral [simp]:
    1.35      "ceiling (x + numeral v) = ceiling x + numeral v"
     2.1 --- a/src/HOL/Binomial.thy	Thu Nov 12 11:22:26 2015 +0100
     2.2 +++ b/src/HOL/Binomial.thy	Fri Nov 13 12:27:13 2015 +0000
     2.3 @@ -67,11 +67,11 @@
     2.4    proof (induct n)
     2.5      case (Suc n)
     2.6      then have *: "fact n \<le> (of_nat (Suc n ^ n) ::'a)"
     2.7 -      by (rule order_trans) (simp add: power_mono)
     2.8 +      by (rule order_trans) (simp add: power_mono del: of_nat_power)
     2.9      have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)"
    2.10        by (simp add: algebra_simps)
    2.11      also have "... \<le> (of_nat (Suc n) * of_nat (Suc n ^ n) ::'a)"
    2.12 -      by (simp add: "*" ordered_comm_semiring_class.comm_mult_left_mono)
    2.13 +      by (simp add: "*" ordered_comm_semiring_class.comm_mult_left_mono del: of_nat_power)
    2.14      also have "... \<le> (of_nat (Suc n ^ Suc n) ::'a)"
    2.15        by (metis of_nat_mult order_refl power_Suc)
    2.16      finally show ?case .
     3.1 --- a/src/HOL/Complex.thy	Thu Nov 12 11:22:26 2015 +0100
     3.2 +++ b/src/HOL/Complex.thy	Fri Nov 13 12:27:13 2015 +0000
     3.3 @@ -842,7 +842,7 @@
     3.4      by (simp add: cis_divide [symmetric] cis_2pi_int)
     3.5    moreover have "- pi < c \<and> c \<le> pi"
     3.6      using ceiling_correct [of "(b - pi) / (2*pi)"]
     3.7 -    by (simp add: c_def less_divide_eq divide_le_eq algebra_simps)
     3.8 +    by (simp add: c_def less_divide_eq divide_le_eq algebra_simps del: le_of_int_ceiling)
     3.9    ultimately show "\<exists>a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi" by fast
    3.10  qed
    3.11  
     4.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Nov 12 11:22:26 2015 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Nov 13 12:27:13 2015 +0000
     4.3 @@ -808,7 +808,7 @@
     4.4          also note float_round_up
     4.5          finally have "pi / 2 - float_round_up prec (?ub_horner ?invx) \<le> arctan x"
     4.6            using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>]
     4.7 -          unfolding real_sgn_pos[OF \<open>0 < 1 / real_of_float x\<close>] le_diff_eq by auto
     4.8 +          unfolding sgn_pos[OF \<open>0 < 1 / real_of_float x\<close>] le_diff_eq by auto
     4.9          moreover
    4.10          have "lb_pi prec * Float 1 (- 1) \<le> pi / 2"
    4.11            unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp
    4.12 @@ -935,7 +935,7 @@
    4.13          unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone') (rule float_divl)
    4.14        finally have "arctan x \<le> pi / 2 - (?lb_horner ?invx)"
    4.15          using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>]
    4.16 -        unfolding real_sgn_pos[OF \<open>0 < 1 / x\<close>] le_diff_eq by auto
    4.17 +        unfolding sgn_pos[OF \<open>0 < 1 / x\<close>] le_diff_eq by auto
    4.18        moreover
    4.19        have "pi / 2 \<le> ub_pi prec * Float 1 (- 1)"
    4.20          unfolding Float_num times_divide_eq_right mult_1_right
     5.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Nov 12 11:22:26 2015 +0100
     5.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Nov 13 12:27:13 2015 +0000
     5.3 @@ -35,12 +35,12 @@
     5.4    hence th: "\<exists> k. x=real_of_int (i*k)" by (simp add: rdvd_def)
     5.5    hence th': "real_of_int (floor x) = x" by (auto simp del: of_int_mult)
     5.6    with th have "\<exists> k. real_of_int (floor x) = real_of_int (i*k)" by simp
     5.7 -  hence "\<exists> k. floor x = i*k" by blast
     5.8 +  hence "\<exists> k. floor x = i*k" by presburger
     5.9    thus ?r  using th' by (simp add: dvd_def) 
    5.10  next
    5.11    assume "?r" hence "(i::int) dvd \<lfloor>x::real\<rfloor>" ..
    5.12    hence "\<exists> k. real_of_int (floor x) = real_of_int (i*k)"
    5.13 -    using dvd_def by blast 
    5.14 +    by (metis (no_types) dvd_def)
    5.15    thus ?l using \<open>?r\<close> by (simp add: rdvd_def)
    5.16  qed
    5.17  
    5.18 @@ -123,7 +123,7 @@
    5.19    let ?fe = "floor ?e"
    5.20    assume be: "isint e bs" hence efe:"real_of_int ?fe = ?e" by (simp add: isint_iff)
    5.21    have "real_of_int ((floor (Inum bs (Mul c e)))) = real_of_int (floor (real_of_int (c * ?fe)))" using efe by simp
    5.22 -  also have "\<dots> = real_of_int (c* ?fe)" using floor_of_int by blast 
    5.23 +  also have "\<dots> = real_of_int (c* ?fe)"  by (metis floor_of_int)
    5.24    also have "\<dots> = real_of_int c * ?e" using efe by simp
    5.25    finally show ?thesis using isint_iff by simp
    5.26  qed
    5.27 @@ -1053,9 +1053,10 @@
    5.28    "iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else 
    5.29         if p=F then not q else if q=F then not p else if p=T then q else if q=T then p else 
    5.30    Iff p q)"
    5.31 +
    5.32  lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)"
    5.33 -  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp) 
    5.34 -(cases "not p= q", auto simp add:not)
    5.35 +  by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp)  (cases "not p= q", auto simp add:not)
    5.36 +
    5.37  lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
    5.38    by (unfold iff_def,cases "p=q", auto)
    5.39  
    5.40 @@ -2623,7 +2624,7 @@
    5.41        hence "x + floor ?e +1 \<ge> 1 \<and> x + floor ?e + 1 \<le> d"  by simp
    5.42        hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e + 1" by simp
    5.43        hence "\<exists> (j::int) \<in> {1 .. d}. x= - floor ?e - 1 + j" by (simp add: algebra_simps)
    5.44 -      hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= real_of_int (- floor ?e - 1 + j)" by blast
    5.45 +      hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= real_of_int (- floor ?e - 1 + j)" by presburger
    5.46        hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= - ?e - 1 + real_of_int j" 
    5.47          by (simp add: ie[simplified isint_iff])
    5.48        with nob have ?case by simp }
     6.1 --- a/src/HOL/Divides.thy	Thu Nov 12 11:22:26 2015 +0100
     6.2 +++ b/src/HOL/Divides.thy	Fri Nov 13 12:27:13 2015 +0000
     6.3 @@ -1696,17 +1696,14 @@
     6.4  
     6.5  lemma divmod_int_rel:
     6.6    "divmod_int_rel k l (k div l, k mod l)"
     6.7 +  unfolding divmod_int_rel_def divide_int_def mod_int_def
     6.8    apply (cases k rule: int_cases3)
     6.9 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
    6.10 +  apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
    6.11    apply (cases l rule: int_cases3)
    6.12 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
    6.13 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
    6.14 -  apply (simp add: of_nat_add [symmetric])
    6.15 -  apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
    6.16 -  apply (simp add: of_nat_add [symmetric])
    6.17 +  apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
    6.18 +  apply (simp_all del: of_nat_add of_nat_mult add: mod_greater_zero_iff_not_dvd not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
    6.19    apply (cases l rule: int_cases3)
    6.20 -  apply (simp_all add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
    6.21 -  apply (simp_all add: of_nat_add [symmetric])
    6.22 +  apply (simp_all del: of_nat_add of_nat_mult add: not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
    6.23    done
    6.24  
    6.25  instantiation int :: ring_div
     7.1 --- a/src/HOL/GCD.thy	Thu Nov 12 11:22:26 2015 +0100
     7.2 +++ b/src/HOL/GCD.thy	Fri Nov 13 12:27:13 2015 +0000
     7.3 @@ -1133,10 +1133,7 @@
     7.4    apply (erule subst)
     7.5    apply (rule iffI)
     7.6    apply force
     7.7 -  apply (drule_tac x = "abs e" for e in exI)
     7.8 -  apply (case_tac "e >= 0" for e :: int)
     7.9 -  apply force
    7.10 -  apply force
    7.11 +  using abs_dvd_iff abs_ge_zero apply blast
    7.12    done
    7.13  
    7.14  lemma gcd_coprime_nat:
     8.1 --- a/src/HOL/Inequalities.thy	Thu Nov 12 11:22:26 2015 +0100
     8.2 +++ b/src/HOL/Inequalities.thy	Fri Nov 13 12:27:13 2015 +0000
     8.3 @@ -34,7 +34,7 @@
     8.4      by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult simp del: of_nat_setsum
     8.5            split: zdiff_int_split)
     8.6    thus ?thesis
     8.7 -    by blast 
     8.8 +    using int_int_eq by blast
     8.9  qed
    8.10  
    8.11  lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n"
     9.1 --- a/src/HOL/Int.thy	Thu Nov 12 11:22:26 2015 +0100
     9.2 +++ b/src/HOL/Int.thy	Fri Nov 13 12:27:13 2015 +0000
     9.3 @@ -319,25 +319,25 @@
     9.4  text \<open>Comparisons involving @{term of_int}.\<close>
     9.5  
     9.6  lemma of_int_eq_numeral_iff [iff]:
     9.7 -   "of_int z = (numeral n :: 'a::ring_char_0) 
     9.8 +   "of_int z = (numeral n :: 'a::ring_char_0)
     9.9     \<longleftrightarrow> z = numeral n"
    9.10    using of_int_eq_iff by fastforce
    9.11  
    9.12 -lemma of_int_le_numeral_iff [simp]:           
    9.13 -   "of_int z \<le> (numeral n :: 'a::linordered_idom) 
    9.14 +lemma of_int_le_numeral_iff [simp]:
    9.15 +   "of_int z \<le> (numeral n :: 'a::linordered_idom)
    9.16     \<longleftrightarrow> z \<le> numeral n"
    9.17    using of_int_le_iff [of z "numeral n"] by simp
    9.18  
    9.19 -lemma of_int_numeral_le_iff [simp]:  
    9.20 +lemma of_int_numeral_le_iff [simp]:
    9.21     "(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z"
    9.22    using of_int_le_iff [of "numeral n"] by simp
    9.23  
    9.24 -lemma of_int_less_numeral_iff [simp]:           
    9.25 -   "of_int z < (numeral n :: 'a::linordered_idom) 
    9.26 +lemma of_int_less_numeral_iff [simp]:
    9.27 +   "of_int z < (numeral n :: 'a::linordered_idom)
    9.28     \<longleftrightarrow> z < numeral n"
    9.29    using of_int_less_iff [of z "numeral n"] by simp
    9.30  
    9.31 -lemma of_int_numeral_less_iff [simp]:           
    9.32 +lemma of_int_numeral_less_iff [simp]:
    9.33     "(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z"
    9.34    using of_int_less_iff [of "numeral n" z] by simp
    9.35  
    9.36 @@ -815,22 +815,22 @@
    9.37  
    9.38  subsection \<open>@{term setsum} and @{term setprod}\<close>
    9.39  
    9.40 -lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
    9.41 +lemma of_nat_setsum [simp]: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
    9.42    apply (cases "finite A")
    9.43    apply (erule finite_induct, auto)
    9.44    done
    9.45  
    9.46 -lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
    9.47 +lemma of_int_setsum [simp]: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
    9.48    apply (cases "finite A")
    9.49    apply (erule finite_induct, auto)
    9.50    done
    9.51  
    9.52 -lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
    9.53 +lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
    9.54    apply (cases "finite A")
    9.55    apply (erule finite_induct, auto simp add: of_nat_mult)
    9.56    done
    9.57  
    9.58 -lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
    9.59 +lemma of_int_setprod [simp]: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
    9.60    apply (cases "finite A")
    9.61    apply (erule finite_induct, auto)
    9.62    done
    9.63 @@ -1401,7 +1401,7 @@
    9.64      then show "x dvd y"
    9.65      proof (cases k)
    9.66        case (nonneg n)
    9.67 -      with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
    9.68 +      with A have "y = x * n" by (simp del: of_nat_mult add: of_nat_mult [symmetric])
    9.69        then show ?thesis ..
    9.70      next
    9.71        case (neg n)
    9.72 @@ -1695,16 +1695,6 @@
    9.73  lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
    9.74  lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
    9.75  
    9.76 -lemma zpower_zpower:
    9.77 -  "(x ^ y) ^ z = (x ^ (y * z)::int)"
    9.78 -  by (rule power_mult [symmetric])
    9.79 -
    9.80 -lemma int_power:
    9.81 -  "int (m ^ n) = int m ^ n"
    9.82 -  by (fact of_nat_power)
    9.83 -
    9.84 -lemmas zpower_int = int_power [symmetric]
    9.85 -
    9.86  text \<open>De-register @{text "int"} as a quotient type:\<close>
    9.87  
    9.88  lifting_update int.lifting
    10.1 --- a/src/HOL/Library/Float.thy	Thu Nov 12 11:22:26 2015 +0100
    10.2 +++ b/src/HOL/Library/Float.thy	Fri Nov 13 12:27:13 2015 +0000
    10.3 @@ -375,7 +375,7 @@
    10.4      also have "\<dots> = m2 * 2^nat (e2 - e1)"
    10.5        by (simp add: powr_realpow)
    10.6      finally have m1_eq: "m1 = m2 * 2^nat (e2 - e1)"
    10.7 -      by blast
    10.8 +      by linarith
    10.9      with m1 have "m1 = m2"
   10.10        by (cases "nat (e2 - e1)") (auto simp add: dvd_def)
   10.11      then show ?thesis
   10.12 @@ -526,8 +526,10 @@
   10.13    ultimately have "real_of_int m = mantissa f * 2^nat (exponent f - e)"
   10.14      by (simp add: powr_realpow[symmetric])
   10.15    with \<open>e \<le> exponent f\<close>
   10.16 -  show "m = mantissa f * 2 ^ nat (exponent f - e)" "e = exponent f - nat (exponent f - e)"
   10.17 -    by force+
   10.18 +  show "m = mantissa f * 2 ^ nat (exponent f - e)" 
   10.19 +    by linarith
   10.20 +  show "e = exponent f - nat (exponent f - e)"
   10.21 +    using `e \<le> exponent f` by auto
   10.22  qed
   10.23  
   10.24  context
   10.25 @@ -1258,7 +1260,7 @@
   10.26      case True
   10.27      def x' \<equiv> "x * 2 ^ nat l"
   10.28      have "int x * 2 ^ nat l = x'"
   10.29 -      by (simp add: x'_def int_mult int_power)
   10.30 +      by (simp add: x'_def int_mult of_nat_power)
   10.31      moreover have "real x * 2 powr l = real x'"
   10.32        by (simp add: powr_realpow[symmetric] \<open>0 \<le> l\<close> x'_def)
   10.33      ultimately show ?thesis
   10.34 @@ -1271,7 +1273,7 @@
   10.35      case False
   10.36      def y' \<equiv> "y * 2 ^ nat (- l)"
   10.37      from \<open>y \<noteq> 0\<close> have "y' \<noteq> 0" by (simp add: y'_def)
   10.38 -    have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
   10.39 +    have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult of_nat_power)
   10.40      moreover have "real x * real_of_int (2::int) powr real_of_int l / real y = x / real y'"
   10.41        using \<open>\<not> 0 \<le> l\<close>
   10.42        by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
   10.43 @@ -1554,7 +1556,7 @@
   10.44      using bitlen_bounds[of "\<bar>m2\<bar>"]
   10.45      by (auto simp: powr_add bitlen_nonneg)
   10.46    then show ?thesis
   10.47 -    by (metis bitlen_nonneg powr_int real_of_int_abs real_of_int_less_numeral_power_cancel_iff zero_less_numeral)
   10.48 +    by (metis bitlen_nonneg powr_int of_int_abs real_of_int_less_numeral_power_cancel_iff zero_less_numeral)
   10.49  qed
   10.50  
   10.51  lemma floor_sum_times_2_powr_sgn_eq:
   10.52 @@ -1984,7 +1986,7 @@
   10.53      by simp
   10.54    also have "\<dots> \<le> 2 powr (bitlen \<bar>mantissa x\<bar>)"
   10.55      using bitlen_bounds[of "\<bar>mantissa x\<bar>"] bitlen_nonneg \<open>mantissa x \<noteq> 0\<close>
   10.56 -    by (auto simp del: real_of_int_abs simp add: powr_int)
   10.57 +    by (auto simp del: of_int_abs simp add: powr_int)
   10.58    finally show ?thesis by (simp add: powr_add)
   10.59  qed
   10.60  
    11.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Nov 12 11:22:26 2015 +0100
    11.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Nov 13 12:27:13 2015 +0000
    11.3 @@ -3787,10 +3787,8 @@
    11.4  lemma binomial_Vandermonde:
    11.5    "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
    11.6    using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n]
    11.7 -  apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric]
    11.8 -                    of_nat_setsum[symmetric] of_nat_add[symmetric])
    11.9 -  apply blast
   11.10 -  done
   11.11 +  by (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric]
   11.12 +                 of_nat_setsum[symmetric] of_nat_add[symmetric] of_nat_eq_iff)
   11.13  
   11.14  lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)\<^sup>2) {0..n} = (2 * n) choose n"
   11.15    using binomial_Vandermonde[of n n n, symmetric]
    12.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Nov 12 11:22:26 2015 +0100
    12.2 +++ b/src/HOL/Library/Numeral_Type.thy	Fri Nov 13 12:27:13 2015 +0000
    12.3 @@ -376,7 +376,6 @@
    12.4  lemma Abs_bit0'_code [code abstract]:
    12.5    "Rep_bit0 (Abs_bit0' x :: 'a :: finite bit0) = x mod int (CARD('a bit0))"
    12.6  by(auto simp add: Abs_bit0'_def intro!: Abs_bit0_inverse)
    12.7 -  (metis bit0.Rep_Abs_mod bit0.Rep_less_n card_bit0 of_nat_numeral zmult_int)
    12.8  
    12.9  lemma inj_on_Abs_bit0:
   12.10    "inj_on (Abs_bit0 :: int \<Rightarrow> 'a bit0) {0..<2 * int CARD('a :: finite)}"
   12.11 @@ -389,8 +388,7 @@
   12.12  
   12.13  lemma Abs_bit1'_code [code abstract]:
   12.14    "Rep_bit1 (Abs_bit1' x :: 'a :: finite bit1) = x mod int (CARD('a bit1))"
   12.15 -by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse)
   12.16 -  (metis of_nat_0_less_iff of_nat_Suc of_nat_mult of_nat_numeral pos_mod_conj zero_less_Suc)
   12.17 +  by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse)
   12.18  
   12.19  lemma inj_on_Abs_bit1:
   12.20    "inj_on (Abs_bit1 :: int \<Rightarrow> 'a bit1) {0..<1 + 2 * int CARD('a :: finite)}"
   12.21 @@ -414,7 +412,7 @@
   12.22  instance
   12.23  proof(intro_classes)
   12.24    show "distinct (enum_class.enum :: 'a bit0 list)"
   12.25 -    by(auto intro!: inj_onI simp add: Abs_bit0'_def Abs_bit0_inject zmod_int[symmetric] enum_bit0_def distinct_map)
   12.26 +    by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject mod_pos_pos_trivial)
   12.27  
   12.28    show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
   12.29      unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
    13.1 --- a/src/HOL/Limits.thy	Thu Nov 12 11:22:26 2015 +0100
    13.2 +++ b/src/HOL/Limits.thy	Fri Nov 13 12:27:13 2015 +0000
    13.3 @@ -89,7 +89,7 @@
    13.4  lemma BfunE:
    13.5    assumes "Bfun f F"
    13.6    obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F"
    13.7 -using assms unfolding Bfun_def by fast
    13.8 +using assms unfolding Bfun_def by blast
    13.9  
   13.10  lemma Cauchy_Bseq: "Cauchy X \<Longrightarrow> Bseq X"
   13.11    unfolding Cauchy_def Bfun_metric_def eventually_sequentially
   13.12 @@ -175,7 +175,10 @@
   13.13    ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
   13.14      by (blast intro: order_trans)
   13.15    then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
   13.16 -qed (force simp add: of_nat_Suc)
   13.17 +next
   13.18 +  show "\<And>N. \<forall>n. norm (X n) \<le> real (Suc N) \<Longrightarrow> \<exists>K>0. \<forall>n. norm (X n) \<le> K"
   13.19 +    using of_nat_0_less_iff by blast
   13.20 +qed
   13.21  
   13.22  text\<open>alternative definition for Bseq\<close>
   13.23  lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
   13.24 @@ -367,7 +370,7 @@
   13.25      fix r::real assume "0 < r"
   13.26      hence "0 < r / K" using K by simp
   13.27      then have "eventually (\<lambda>x. norm (f x) < r / K) F"
   13.28 -      using ZfunD [OF f] by fast
   13.29 +      using ZfunD [OF f] by blast
   13.30      with g show "eventually (\<lambda>x. norm (g x) < r) F"
   13.31      proof eventually_elim
   13.32        case (elim x)
   13.33 @@ -433,7 +436,7 @@
   13.34    shows "Zfun (\<lambda>x. f (g x)) F"
   13.35  proof -
   13.36    obtain K where "\<And>x. norm (f x) \<le> norm x * K"
   13.37 -    using bounded by fast
   13.38 +    using bounded by blast
   13.39    then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) F"
   13.40      by simp
   13.41    with g show ?thesis
   13.42 @@ -448,7 +451,7 @@
   13.43    fix r::real assume r: "0 < r"
   13.44    obtain K where K: "0 < K"
   13.45      and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
   13.46 -    using pos_bounded by fast
   13.47 +    using pos_bounded by blast
   13.48    from K have K': "0 < inverse K"
   13.49      by (rule positive_imp_inverse_positive)
   13.50    have "eventually (\<lambda>x. norm (f x) < r) F"
   13.51 @@ -787,7 +790,7 @@
   13.52  proof -
   13.53    obtain K where K: "0 \<le> K"
   13.54      and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
   13.55 -    using nonneg_bounded by fast
   13.56 +    using nonneg_bounded by blast
   13.57    obtain B where B: "0 < B"
   13.58      and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) F"
   13.59      using g by (rule BfunE)
   13.60 @@ -816,7 +819,7 @@
   13.61    apply (rule scaleR_left)
   13.62    apply (subst mult.commute)
   13.63    using bounded
   13.64 -  apply fast
   13.65 +  apply blast
   13.66    done
   13.67  
   13.68  lemma (in bounded_bilinear) Bfun_prod_Zfun:
   13.69 @@ -840,9 +843,9 @@
   13.70  proof -
   13.71    from a have "0 < norm a" by simp
   13.72    hence "\<exists>r>0. r < norm a" by (rule dense)
   13.73 -  then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
   13.74 +  then obtain r where r1: "0 < r" and r2: "r < norm a" by blast
   13.75    have "eventually (\<lambda>x. dist (f x) a < r) F"
   13.76 -    using tendstoD [OF f r1] by fast
   13.77 +    using tendstoD [OF f r1] by blast
   13.78    hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) F"
   13.79    proof eventually_elim
   13.80      case (elim x)
   13.81 @@ -911,7 +914,7 @@
   13.82    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
   13.83    assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
   13.84    shows "continuous_on s (\<lambda>x. inverse (f x))"
   13.85 -  using assms unfolding continuous_on_def by (fast intro: tendsto_inverse)
   13.86 +  using assms unfolding continuous_on_def by (blast intro: tendsto_inverse)
   13.87  
   13.88  lemma tendsto_divide [tendsto_intros]:
   13.89    fixes a b :: "'a::real_normed_field"
   13.90 @@ -941,7 +944,7 @@
   13.91    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
   13.92    assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. g x \<noteq> 0"
   13.93    shows "continuous_on s (\<lambda>x. (f x) / (g x))"
   13.94 -  using assms unfolding continuous_on_def by (fast intro: tendsto_divide)
   13.95 +  using assms unfolding continuous_on_def by (blast intro: tendsto_divide)
   13.96  
   13.97  lemma tendsto_sgn [tendsto_intros]:
   13.98    fixes l :: "'a::real_normed_vector"
   13.99 @@ -970,7 +973,7 @@
  13.100    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
  13.101    assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
  13.102    shows "continuous_on s (\<lambda>x. sgn (f x))"
  13.103 -  using assms unfolding continuous_on_def by (fast intro: tendsto_sgn)
  13.104 +  using assms unfolding continuous_on_def by (blast intro: tendsto_sgn)
  13.105  
  13.106  lemma filterlim_at_infinity:
  13.107    fixes f :: "_ \<Rightarrow> 'a::real_normed_vector"
  13.108 @@ -1685,7 +1688,7 @@
  13.109    assumes "convergent (\<lambda>n. X n)"
  13.110    assumes "convergent (\<lambda>n. Y n)"
  13.111    shows "convergent (\<lambda>n. X n + Y n)"
  13.112 -  using assms unfolding convergent_def by (fast intro: tendsto_add)
  13.113 +  using assms unfolding convergent_def by (blast intro: tendsto_add)
  13.114  
  13.115  lemma convergent_setsum:
  13.116    fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
  13.117 @@ -1699,12 +1702,12 @@
  13.118  lemma (in bounded_linear) convergent:
  13.119    assumes "convergent (\<lambda>n. X n)"
  13.120    shows "convergent (\<lambda>n. f (X n))"
  13.121 -  using assms unfolding convergent_def by (fast intro: tendsto)
  13.122 +  using assms unfolding convergent_def by (blast intro: tendsto)
  13.123  
  13.124  lemma (in bounded_bilinear) convergent:
  13.125    assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
  13.126    shows "convergent (\<lambda>n. X n ** Y n)"
  13.127 -  using assms unfolding convergent_def by (fast intro: tendsto)
  13.128 +  using assms unfolding convergent_def by (blast intro: tendsto)
  13.129  
  13.130  lemma convergent_minus_iff:
  13.131    fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
  13.132 @@ -1719,7 +1722,7 @@
  13.133    assumes "convergent (\<lambda>n. X n)"
  13.134    assumes "convergent (\<lambda>n. Y n)"
  13.135    shows "convergent (\<lambda>n. X n - Y n)"
  13.136 -  using assms unfolding convergent_def by (fast intro: tendsto_diff)
  13.137 +  using assms unfolding convergent_def by (blast intro: tendsto_diff)
  13.138  
  13.139  lemma convergent_norm:
  13.140    assumes "convergent f"
  13.141 @@ -1757,7 +1760,7 @@
  13.142    assumes "convergent (\<lambda>n. X n)"
  13.143    assumes "convergent (\<lambda>n. Y n)"
  13.144    shows "convergent (\<lambda>n. X n * Y n)"
  13.145 -  using assms unfolding convergent_def by (fast intro: tendsto_mult)
  13.146 +  using assms unfolding convergent_def by (blast intro: tendsto_mult)
  13.147  
  13.148  lemma convergent_mult_const_iff:
  13.149    assumes "c \<noteq> 0"
  13.150 @@ -2122,7 +2125,7 @@
  13.151  proof (intro allI impI)
  13.152    fix r::real assume r: "0 < r"
  13.153    obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
  13.154 -    using pos_bounded by fast
  13.155 +    using pos_bounded by blast
  13.156    show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
  13.157    proof (rule exI, safe)
  13.158      from r K show "0 < r / K" by simp
    14.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Nov 12 11:22:26 2015 +0100
    14.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Fri Nov 13 12:27:13 2015 +0000
    14.3 @@ -2399,15 +2399,15 @@
    14.4    by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arccos_body_lemma)
    14.5  
    14.6  lemma Re_Arccos_bound: "abs(Re(Arccos z)) \<le> pi"
    14.7 -  using Re_Arccos_bounds abs_le_interval_iff less_eq_real_def by blast
    14.8 +  by (meson Re_Arccos_bounds abs_le_iff less_eq_real_def minus_less_iff)
    14.9  
   14.10  lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
   14.11    unfolding Re_Arcsin
   14.12    by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
   14.13  
   14.14  lemma Re_Arcsin_bound: "abs(Re(Arcsin z)) \<le> pi"
   14.15 -  using Re_Arcsin_bounds abs_le_interval_iff less_eq_real_def by blast
   14.16 -
   14.17 +  by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff)
   14.18 + 
   14.19  
   14.20  subsection\<open>Interrelations between Arcsin and Arccos\<close>
   14.21  
    15.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Nov 12 11:22:26 2015 +0100
    15.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Nov 13 12:27:13 2015 +0000
    15.3 @@ -2139,7 +2139,7 @@
    15.4    have *: "\<forall>n. \<exists>f f'. \<forall>x\<in>s.
    15.5      (f has_derivative (f' x)) (at x within s) \<and>
    15.6      (\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm h)"
    15.7 -    by (metis assms(2) inverse_positive_iff_positive real_of_nat_Suc_gt_zero)
    15.8 +    by (simp add: assms(2))
    15.9    obtain f where
   15.10      *: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. (f x has_derivative f' xa) (at xa within s) \<and>
   15.11        (\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
   15.12 @@ -2221,7 +2221,7 @@
   15.13        have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) = norm ((\<Sum>i<n. f' i x) - g' x) * norm h"
   15.14          by (simp add: norm_mult [symmetric] ring_distribs setsum_left_distrib)
   15.15        also from N[OF nx] have "norm ((\<Sum>i<n. f' i x) - g' x) \<le> e" by simp
   15.16 -      hence "norm ((\<Sum>i<n. f' i x) - g' x) * norm h \<le> e * norm h" 
   15.17 +      hence "norm ((\<Sum>i<n. f' i x) - g' x) * norm h \<le> e * norm h"
   15.18          by (intro mult_right_mono) simp_all
   15.19        finally have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" .
   15.20      }
   15.21 @@ -2245,9 +2245,9 @@
   15.22      "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
   15.23      "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
   15.24    from g(1)[OF \<open>x \<in> s\<close>] show "summable (\<lambda>n. f n x)" by (simp add: sums_iff)
   15.25 -  from g(2)[OF \<open>x \<in> s\<close>] \<open>x \<in> interior s\<close> have "(g has_field_derivative g' x) (at x)" 
   15.26 +  from g(2)[OF \<open>x \<in> s\<close>] \<open>x \<in> interior s\<close> have "(g has_field_derivative g' x) (at x)"
   15.27      by (simp add: at_within_interior[of x s])
   15.28 -  also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow> 
   15.29 +  also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow>
   15.30                  ((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)"
   15.31      using eventually_nhds_in_nhd[OF \<open>x \<in> interior s\<close>] interior_subset[of s] g(1)
   15.32      by (intro DERIV_cong_ev) (auto elim!: eventually_elim1 simp: sums_iff)
   15.33 @@ -2311,7 +2311,7 @@
   15.34      qed
   15.35    qed (insert f' f'', auto simp: has_vector_derivative_def)
   15.36    then show ?thesis
   15.37 -    unfolding fun_eq_iff by auto
   15.38 +    unfolding fun_eq_iff by (metis scaleR_one)
   15.39  qed
   15.40  
   15.41  lemma vector_derivative_unique_at:
   15.42 @@ -2350,7 +2350,7 @@
   15.43           intro: someI frechet_derivative_at [symmetric])
   15.44  
   15.45  lemma has_real_derivative:
   15.46 -  fixes f :: "real \<Rightarrow> real" 
   15.47 +  fixes f :: "real \<Rightarrow> real"
   15.48    assumes "(f has_derivative f') F"
   15.49    obtains c where "(f has_real_derivative c) F"
   15.50  proof -
   15.51 @@ -2361,7 +2361,7 @@
   15.52  qed
   15.53  
   15.54  lemma has_real_derivative_iff:
   15.55 -  fixes f :: "real \<Rightarrow> real" 
   15.56 +  fixes f :: "real \<Rightarrow> real"
   15.57    shows "(\<exists>c. (f has_real_derivative c) F) = (\<exists>D. (f has_derivative D) F)"
   15.58    by (metis has_field_derivative_def has_real_derivative)
   15.59  
   15.60 @@ -2390,7 +2390,7 @@
   15.61    assumes "open s" and t: "t = closure s" "x \<in> t"
   15.62    shows "x islimpt t"
   15.63  proof cases
   15.64 -  assume "x \<in> s" 
   15.65 +  assume "x \<in> s"
   15.66    { fix T assume "x \<in> T" "open T"
   15.67      then have "open (s \<inter> T)"
   15.68        using \<open>open s\<close> by auto
   15.69 @@ -2579,7 +2579,7 @@
   15.70        by (intro convex_onD_Icc'' convex_on_subset[OF convex] connected_contains_Icc) auto
   15.71      hence "f y - f c \<le> (f x - f c) * ((c - y) / (c - x))" by simp
   15.72      also have "(c - y) / (c - x) = (y - c) / (x - c)" using y xc by (simp add: field_simps)
   15.73 -    finally show "(f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)" using y xc 
   15.74 +    finally show "(f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)" using y xc
   15.75        by (simp add: divide_simps)
   15.76    qed
   15.77    hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at c within ?A')"
    16.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Nov 12 11:22:26 2015 +0100
    16.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 13 12:27:13 2015 +0000
    16.3 @@ -14,7 +14,8 @@
    16.4  lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *)
    16.5    fixes S :: "real set"
    16.6    shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
    16.7 -  by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2 bdd_aboveI)
    16.8 +  apply (auto simp add: abs_le_iff intro: cSup_least)
    16.9 +  by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans)
   16.10  
   16.11  lemma cInf_abs_ge:
   16.12    fixes S :: "real set"
    17.1 --- a/src/HOL/NSA/NSA.thy	Thu Nov 12 11:22:26 2015 +0100
    17.2 +++ b/src/HOL/NSA/NSA.thy	Fri Nov 13 12:27:13 2015 +0000
    17.3 @@ -1243,7 +1243,9 @@
    17.4  apply (frule lemma_st_part1a)
    17.5  apply (frule_tac [4] lemma_st_part2a, auto)
    17.6  apply (drule order_le_imp_less_or_eq)+
    17.7 -apply (auto dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff)
    17.8 +apply auto
    17.9 +using lemma_st_part_not_eq2 apply fastforce
   17.10 +using lemma_st_part_not_eq1 apply fastforce
   17.11  done
   17.12  
   17.13  lemma lemma_st_part_major2:
   17.14 @@ -1252,6 +1254,7 @@
   17.15  by (blast dest!: lemma_st_part_major)
   17.16  
   17.17  
   17.18 +
   17.19  text{*Existence of real and Standard Part Theorem*}
   17.20  lemma lemma_st_part_Ex:
   17.21       "(x::hypreal) \<in> HFinite
   17.22 @@ -1778,7 +1781,7 @@
   17.23  done
   17.24  
   17.25  lemma st_SReal_eq: "x \<in> \<real> ==> st x = x"
   17.26 -  by (metis approx_refl st_unique) 
   17.27 +  by (metis approx_refl st_unique)
   17.28  
   17.29  lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
   17.30  by (rule SReal_hypreal_of_real [THEN st_SReal_eq])
   17.31 @@ -2022,7 +2025,7 @@
   17.32  
   17.33  lemma lemma_Infinitesimal:
   17.34       "(\<forall>r. 0 < r --> x < r) = (\<forall>n. x < inverse(real (Suc n)))"
   17.35 -apply (auto simp add: real_of_nat_Suc_gt_zero simp del: of_nat_Suc)
   17.36 +apply (auto simp del: of_nat_Suc)
   17.37  apply (blast dest!: reals_Archimedean intro: order_less_trans)
   17.38  done
   17.39  
   17.40 @@ -2031,10 +2034,8 @@
   17.41        (\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
   17.42  apply safe
   17.43   apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec)
   17.44 -  apply (simp (no_asm_use))
   17.45 - apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN star_of_less [THEN iffD2], THEN [2] impE])
   17.46 -  prefer 2 apply assumption
   17.47 - apply simp
   17.48 +  apply simp_all
   17.49 +  using less_imp_of_nat_less apply fastforce
   17.50  apply (auto dest!: reals_Archimedean simp add: SReal_iff simp del: of_nat_Suc)
   17.51  apply (drule star_of_less [THEN iffD2])
   17.52  apply simp
   17.53 @@ -2077,7 +2078,7 @@
   17.54  by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real)
   17.55  
   17.56  lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) \<le> u}"
   17.57 -apply (simp (no_asm) add: real_of_nat_Suc_gt_zero finite_real_of_nat_le_real)
   17.58 +apply (simp (no_asm) add: finite_real_of_nat_le_real)
   17.59  done
   17.60  
   17.61  lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
   17.62 @@ -2133,7 +2134,7 @@
   17.63  apply (simp add: inverse_eq_divide)
   17.64  apply (subst pos_less_divide_eq, assumption)
   17.65  apply (subst pos_less_divide_eq)
   17.66 - apply (simp add: real_of_nat_Suc_gt_zero)
   17.67 + apply simp
   17.68  apply (simp add: mult.commute)
   17.69  done
   17.70  
   17.71 @@ -2153,7 +2154,7 @@
   17.72  
   17.73  lemma finite_inverse_real_of_posnat_ge_real:
   17.74       "0 < u ==> finite {n. u \<le> inverse(real(Suc n))}"
   17.75 -by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real 
   17.76 +by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real
   17.77              simp del: of_nat_Suc)
   17.78  
   17.79  lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
   17.80 @@ -2181,8 +2182,8 @@
   17.81  
   17.82  lemma SEQ_Infinitesimal:
   17.83        "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
   17.84 -by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff 
   17.85 -       real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc)
   17.86 +by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff
   17.87 +        FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc)
   17.88  
   17.89  text{* Example where we get a hyperreal from a real sequence
   17.90        for which a particular property holds. The theorem is
   17.91 @@ -2198,7 +2199,7 @@
   17.92       "\<forall>n. norm(X n - x) < inverse(real(Suc n))
   17.93       ==> star_n X - star_of x \<in> Infinitesimal"
   17.94  unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse
   17.95 -by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat  
   17.96 +by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
   17.97           intro: order_less_trans elim!: eventually_elim1)
   17.98  
   17.99  lemma real_seq_to_hypreal_approx:
    18.1 --- a/src/HOL/Nat.thy	Thu Nov 12 11:22:26 2015 +0100
    18.2 +++ b/src/HOL/Nat.thy	Fri Nov 13 12:27:13 2015 +0000
    18.3 @@ -1469,7 +1469,7 @@
    18.4  lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
    18.5    by (induct m) (simp_all add: ac_simps)
    18.6  
    18.7 -lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
    18.8 +lemma of_nat_mult [simp]: "of_nat (m * n) = of_nat m * of_nat n"
    18.9    by (induct m) (simp_all add: ac_simps distrib_right)
   18.10  
   18.11  lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
    19.1 --- a/src/HOL/Nat_Transfer.thy	Thu Nov 12 11:22:26 2015 +0100
    19.2 +++ b/src/HOL/Nat_Transfer.thy	Fri Nov 13 12:27:13 2015 +0000
    19.3 @@ -203,11 +203,9 @@
    19.4  lemma transfer_nat_int_sum_prod2:
    19.5      "setsum f A = nat(setsum (%x. int (f x)) A)"
    19.6      "setprod f A = nat(setprod (%x. int (f x)) A)"
    19.7 -  apply (subst int_setsum [symmetric])
    19.8 -  apply auto
    19.9 -  apply (subst int_setprod [symmetric])
   19.10 -  apply auto
   19.11 -done
   19.12 +  apply (simp only: int_setsum [symmetric] nat_int)
   19.13 +  apply (simp only: int_setprod [symmetric] nat_int)
   19.14 +  done
   19.15  
   19.16  lemma transfer_nat_int_sum_prod_closure:
   19.17      "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
   19.18 @@ -288,7 +286,7 @@
   19.19      "(int x) * (int y) = int (x * y)"
   19.20      "tsub (int x) (int y) = int (x - y)"
   19.21      "(int x)^n = int (x^n)"
   19.22 -  by (auto simp add: int_mult tsub_def int_power)
   19.23 +  by (auto simp add: int_mult tsub_def of_nat_power)
   19.24  
   19.25  lemma transfer_int_nat_function_closures:
   19.26      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
   19.27 @@ -411,9 +409,7 @@
   19.28      "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
   19.29        setprod f A = int(setprod (%x. nat (f x)) A)"
   19.30    unfolding is_nat_def
   19.31 -  apply (subst int_setsum, auto)
   19.32 -  apply (subst int_setprod, auto simp add: cong: setprod.cong)
   19.33 -done
   19.34 +  by (subst int_setsum) auto
   19.35  
   19.36  declare transfer_morphism_int_nat [transfer add
   19.37    return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
    20.1 --- a/src/HOL/NthRoot.thy	Thu Nov 12 11:22:26 2015 +0100
    20.2 +++ b/src/HOL/NthRoot.thy	Fri Nov 13 12:27:13 2015 +0000
    20.3 @@ -257,7 +257,7 @@
    20.4    have "continuous_on ({0..} \<union> {.. 0}) (\<lambda>x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)"
    20.5      using n by (intro continuous_on_If continuous_intros) auto
    20.6    then have "continuous_on UNIV ?f"
    20.7 -    by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less real_sgn_neg le_less n)
    20.8 +    by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less sgn_neg le_less n)
    20.9    then have [simp]: "\<And>x. isCont ?f x"
   20.10      by (simp add: continuous_on_eq_continuous_at)
   20.11  
   20.12 @@ -697,7 +697,7 @@
   20.13             (simp_all add: at_infinity_eq_at_top_bot)
   20.14        { fix n :: nat assume "1 < n"
   20.15          have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
   20.16 -          using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial by simp 
   20.17 +          using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial by simp
   20.18          also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
   20.19            by (simp add: x_def)
   20.20          also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
   20.21 @@ -741,8 +741,4 @@
   20.22  lemmas real_sqrt_mult_distrib2 = real_sqrt_mult
   20.23  lemmas real_sqrt_eq_zero_cancel_iff = real_sqrt_eq_0_iff
   20.24  
   20.25 -(* needed for CauchysMeanTheorem.het_base from AFP *)
   20.26 -lemma real_root_pos: "0 < x \<Longrightarrow> root (Suc n) (x ^ (Suc n)) = x"
   20.27 -by (rule real_root_power_cancel [OF zero_less_Suc order_less_imp_le])
   20.28 -
   20.29  end
    21.1 --- a/src/HOL/Number_Theory/Fib.thy	Thu Nov 12 11:22:26 2015 +0100
    21.2 +++ b/src/HOL/Number_Theory/Fib.thy	Fri Nov 13 12:27:13 2015 +0000
    21.3 @@ -51,7 +51,7 @@
    21.4  lemma fib_Cassini_nat:
    21.5    "fib (Suc (Suc n)) * fib n =
    21.6       (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
    21.7 -  using fib_Cassini_int [of n] by auto
    21.8 +  using fib_Cassini_int [of n]  by (auto simp del: of_nat_mult of_nat_power)
    21.9  
   21.10  
   21.11  subsection \<open>Law 6.111 of Concrete Mathematics\<close>
    22.1 --- a/src/HOL/Old_Number_Theory/Euler.thy	Thu Nov 12 11:22:26 2015 +0100
    22.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy	Fri Nov 13 12:27:13 2015 +0000
    22.3 @@ -284,7 +284,7 @@
    22.4     apply (metis zprime_zOdd_eq_grt_2)
    22.5    apply (frule aux__1, auto)
    22.6    apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)
    22.7 -  apply (auto simp add: zpower_zpower) 
    22.8 +  apply (auto simp add: power_mult [symmetric]) 
    22.9    apply (rule zcong_trans)
   22.10    apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
   22.11    apply (metis Little_Fermat even_div_2_prop2 odd_minus_one_even mult_1 aux__2)
    23.1 --- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Thu Nov 12 11:22:26 2015 +0100
    23.2 +++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Fri Nov 13 12:27:13 2015 +0000
    23.3 @@ -176,7 +176,7 @@
    23.4    finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
    23.5      by simp
    23.6    also have "... = (-1::int)\<^sup>2 ^ nat a"
    23.7 -    by (simp add: zpower_zpower [symmetric])
    23.8 +    by (simp add: power_mult)
    23.9    also have "(-1::int)\<^sup>2 = 1"
   23.10      by simp
   23.11    finally show ?thesis
    24.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Thu Nov 12 11:22:26 2015 +0100
    24.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri Nov 13 12:27:13 2015 +0000
    24.3 @@ -133,7 +133,7 @@
    24.4      5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
    24.5    apply (unfold inv_def)
    24.6    apply (subst power_mod)
    24.7 -  apply (subst zpower_zpower)
    24.8 +  apply (subst power_mult [symmetric])
    24.9    apply (rule zcong_zless_imp_eq)
   24.10        prefer 5
   24.11        apply (subst zcong_zmod)
    25.1 --- a/src/HOL/Power.thy	Thu Nov 12 11:22:26 2015 +0100
    25.2 +++ b/src/HOL/Power.thy	Fri Nov 13 12:27:13 2015 +0000
    25.3 @@ -175,7 +175,7 @@
    25.4  context semiring_1
    25.5  begin
    25.6  
    25.7 -lemma of_nat_power:
    25.8 +lemma of_nat_power [simp]:
    25.9    "of_nat (m ^ n) = of_nat m ^ n"
   25.10    by (induct n) (simp_all add: of_nat_mult)
   25.11  
   25.12 @@ -310,7 +310,7 @@
   25.13  lemma power_minus1_odd:
   25.14    "(- 1) ^ Suc (2*n) = -1"
   25.15    by simp
   25.16 -  
   25.17 +
   25.18  lemma power_minus_even [simp]:
   25.19    "(-a) ^ (2*n) = a ^ (2*n)"
   25.20    by (simp add: power_minus [of a])
   25.21 @@ -320,7 +320,7 @@
   25.22  context ring_1_no_zero_divisors
   25.23  begin
   25.24  
   25.25 -subclass semiring_1_no_zero_divisors .. 
   25.26 +subclass semiring_1_no_zero_divisors ..
   25.27  
   25.28  lemma power2_eq_1_iff:
   25.29    "a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
   25.30 @@ -377,7 +377,7 @@
   25.31    "(1 / a) ^ n = 1 / a ^ n"
   25.32    using power_inverse [of a] by (simp add: divide_inverse)
   25.33  
   25.34 -end  
   25.35 +end
   25.36  
   25.37  context field
   25.38  begin
   25.39 @@ -463,6 +463,10 @@
   25.40    qed
   25.41  qed
   25.42  
   25.43 +lemma of_nat_zero_less_power_iff [simp]:
   25.44 +  "of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
   25.45 +  by (induct n) auto
   25.46 +
   25.47  text\<open>Surely we can strengthen this? It holds for @{text "0<a<1"} too.\<close>
   25.48  lemma power_inject_exp [simp]:
   25.49    "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
   25.50 @@ -491,7 +495,7 @@
   25.51  proof (induct N)
   25.52    case 0 then show ?case by simp
   25.53  next
   25.54 -  case (Suc N) then show ?case 
   25.55 +  case (Suc N) then show ?case
   25.56    apply (auto simp add: power_Suc_less less_Suc_eq)
   25.57    apply (subgoal_tac "a * a^N < 1 * a^n")
   25.58    apply simp
   25.59 @@ -505,7 +509,7 @@
   25.60  proof (induct N)
   25.61    case 0 then show ?case by simp
   25.62  next
   25.63 -  case (Suc N) then show ?case 
   25.64 +  case (Suc N) then show ?case
   25.65    apply (auto simp add: le_Suc_eq)
   25.66    apply (subgoal_tac "a * a^N \<le> 1 * a^n", simp)
   25.67    apply (rule mult_mono) apply auto
   25.68 @@ -522,7 +526,7 @@
   25.69  proof (induct N)
   25.70    case 0 then show ?case by simp
   25.71  next
   25.72 -  case (Suc N) then show ?case 
   25.73 +  case (Suc N) then show ?case
   25.74    apply (auto simp add: le_Suc_eq)
   25.75    apply (subgoal_tac "1 * a^n \<le> a * a^N", simp)
   25.76    apply (rule mult_mono) apply (auto simp add: order_trans [OF zero_le_one])
   25.77 @@ -539,7 +543,7 @@
   25.78  proof (induct N)
   25.79    case 0 then show ?case by simp
   25.80  next
   25.81 -  case (Suc N) then show ?case 
   25.82 +  case (Suc N) then show ?case
   25.83    apply (auto simp add: power_less_power_Suc less_Suc_eq)
   25.84    apply (subgoal_tac "1 * a^n < a * a^N", simp)
   25.85    apply (rule mult_strict_mono) apply (auto simp add: less_trans [OF zero_less_one] less_imp_le)
   25.86 @@ -552,7 +556,7 @@
   25.87  
   25.88  lemma power_strict_increasing_iff [simp]:
   25.89    "1 < b \<Longrightarrow> b ^ x < b ^ y \<longleftrightarrow> x < y"
   25.90 -by (blast intro: power_less_imp_less_exp power_strict_increasing) 
   25.91 +by (blast intro: power_less_imp_less_exp power_strict_increasing)
   25.92  
   25.93  lemma power_le_imp_le_base:
   25.94    assumes le: "a ^ Suc n \<le> b ^ Suc n"
   25.95 @@ -680,7 +684,7 @@
   25.96  lemma odd_0_le_power_imp_0_le:
   25.97    "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
   25.98    using odd_power_less_zero [of a n]
   25.99 -    by (force simp add: linorder_not_less [symmetric]) 
  25.100 +    by (force simp add: linorder_not_less [symmetric])
  25.101  
  25.102  lemma zero_le_even_power'[simp]:
  25.103    "0 \<le> a ^ (2*n)"
  25.104 @@ -689,7 +693,7 @@
  25.105      show ?case by simp
  25.106  next
  25.107    case (Suc n)
  25.108 -    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
  25.109 +    have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
  25.110        by (simp add: ac_simps power_add power2_eq_square)
  25.111      thus ?case
  25.112        by (simp add: Suc zero_le_mult_iff)
  25.113 @@ -733,7 +737,7 @@
  25.114  
  25.115  lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> abs(x) = 1"
  25.116    by (auto simp add: abs_if power2_eq_1_iff)
  25.117 -  
  25.118 +
  25.119  lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> abs(x) < 1"
  25.120    using  abs_square_eq_1 [of x] abs_square_le_1 [of x]
  25.121    by (auto simp add: le_less)
  25.122 @@ -768,10 +772,10 @@
  25.123  
  25.124  lemmas zero_compare_simps =
  25.125      add_strict_increasing add_strict_increasing2 add_increasing
  25.126 -    zero_le_mult_iff zero_le_divide_iff 
  25.127 -    zero_less_mult_iff zero_less_divide_iff 
  25.128 -    mult_le_0_iff divide_le_0_iff 
  25.129 -    mult_less_0_iff divide_less_0_iff 
  25.130 +    zero_le_mult_iff zero_le_divide_iff
  25.131 +    zero_less_mult_iff zero_less_divide_iff
  25.132 +    mult_le_0_iff divide_le_0_iff
  25.133 +    mult_less_0_iff divide_less_0_iff
  25.134      zero_le_power2 power2_less_0
  25.135  
  25.136  
  25.137 @@ -785,7 +789,7 @@
  25.138    "x ^ n > 0 \<longleftrightarrow> x > (0::nat) \<or> n = 0"
  25.139    by (induct n) auto
  25.140  
  25.141 -lemma nat_power_eq_Suc_0_iff [simp]: 
  25.142 +lemma nat_power_eq_Suc_0_iff [simp]:
  25.143    "x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0"
  25.144    by (induct m) auto
  25.145  
  25.146 @@ -842,13 +846,13 @@
  25.147  
  25.148  lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
  25.149  proof (induct rule: finite_induct)
  25.150 -  case empty 
  25.151 +  case empty
  25.152      show ?case by auto
  25.153  next
  25.154    case (insert x A)
  25.155 -  then have "inj_on (insert x) (Pow A)" 
  25.156 +  then have "inj_on (insert x) (Pow A)"
  25.157      unfolding inj_on_def by (blast elim!: equalityE)
  25.158 -  then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A" 
  25.159 +  then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
  25.160      by (simp add: mult_2 card_image Pow_insert insert.hyps)
  25.161    then show ?case using insert
  25.162      apply (simp add: Pow_insert)
  25.163 @@ -882,11 +886,11 @@
  25.164  lemma setprod_power_distrib:
  25.165    fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
  25.166    shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
  25.167 -proof (cases "finite A") 
  25.168 -  case True then show ?thesis 
  25.169 +proof (cases "finite A")
  25.170 +  case True then show ?thesis
  25.171      by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
  25.172  next
  25.173 -  case False then show ?thesis 
  25.174 +  case False then show ?thesis
  25.175      by simp
  25.176  qed
  25.177  
  25.178 @@ -902,13 +906,13 @@
  25.179    {assume a: "a \<notin> S"
  25.180      hence "\<forall> k\<in> S. ?f k = c" by simp
  25.181      hence ?thesis  using a setprod_constant[OF fS, of c] by simp }
  25.182 -  moreover 
  25.183 +  moreover
  25.184    {assume a: "a \<in> S"
  25.185      let ?A = "S - {a}"
  25.186      let ?B = "{a}"
  25.187 -    have eq: "S = ?A \<union> ?B" using a by blast 
  25.188 +    have eq: "S = ?A \<union> ?B" using a by blast
  25.189      have dj: "?A \<inter> ?B = {}" by simp
  25.190 -    from fS have fAB: "finite ?A" "finite ?B" by auto  
  25.191 +    from fS have fAB: "finite ?A" "finite ?B" by auto
  25.192      have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
  25.193        apply (rule setprod.cong) by auto
  25.194      have cA: "card ?A = card S - 1" using fS a by auto
    26.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Thu Nov 12 11:22:26 2015 +0100
    26.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Fri Nov 13 12:27:13 2015 +0000
    26.3 @@ -471,7 +471,7 @@
    26.4      using entropy_le_card[of "t\<circ>OB", OF simple_distributedI[OF simple_function_finite refl]] by simp
    26.5    also have "\<dots> \<le> log b (real (n + 1)^card observations)"
    26.6      using card_T_bound not_empty
    26.7 -    by (auto intro!: log_le simp: card_gt_0_iff power_real_of_nat simp del: of_nat_power of_nat_Suc)
    26.8 +    by (auto intro!: log_le simp: card_gt_0_iff of_nat_power [symmetric] simp del: of_nat_power of_nat_Suc)
    26.9    also have "\<dots> = real (card observations) * log b (real n + 1)"
   26.10      by (simp add: log_nat_power add.commute)
   26.11    finally show ?thesis  .
    27.1 --- a/src/HOL/Real.thy	Thu Nov 12 11:22:26 2015 +0100
    27.2 +++ b/src/HOL/Real.thy	Fri Nov 13 12:27:13 2015 +0000
    27.3 @@ -114,7 +114,7 @@
    27.4  proof (rule vanishesI)
    27.5    fix r :: rat assume r: "0 < r"
    27.6    obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
    27.7 -    using X by fast
    27.8 +    using X by blast
    27.9    obtain b where b: "0 < b" "r = a * b"
   27.10    proof
   27.11      show "0 < r / a" using r a by simp
   27.12 @@ -217,9 +217,9 @@
   27.13    then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v"
   27.14      by (rule obtain_pos_sum)
   27.15    obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
   27.16 -    using cauchy_imp_bounded [OF X] by fast
   27.17 +    using cauchy_imp_bounded [OF X] by blast
   27.18    obtain b where b: "0 < b" "\<forall>n. \<bar>Y n\<bar> < b"
   27.19 -    using cauchy_imp_bounded [OF Y] by fast
   27.20 +    using cauchy_imp_bounded [OF Y] by blast
   27.21    obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b"
   27.22    proof
   27.23      show "0 < v/b" using v b(1) by simp
   27.24 @@ -259,7 +259,7 @@
   27.25    obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
   27.26      using cauchyD [OF X s] ..
   27.27    obtain k where "i \<le> k" and "r \<le> \<bar>X k\<bar>"
   27.28 -    using r by fast
   27.29 +    using r by blast
   27.30    have k: "\<forall>n\<ge>k. \<bar>X n - X k\<bar> < s"
   27.31      using i \<open>i \<le> k\<close> by auto
   27.32    have "X k \<le> - r \<or> r \<le> X k"
   27.33 @@ -285,7 +285,7 @@
   27.34  proof (rule cauchyI)
   27.35    fix r :: rat assume "0 < r"
   27.36    obtain b i where b: "0 < b" and i: "\<forall>n\<ge>i. b < \<bar>X n\<bar>"
   27.37 -    using cauchy_not_vanishes [OF X nz] by fast
   27.38 +    using cauchy_not_vanishes [OF X nz] by blast
   27.39    from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto
   27.40    obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b"
   27.41    proof
   27.42 @@ -317,9 +317,9 @@
   27.43  proof (rule vanishesI)
   27.44    fix r :: rat assume r: "0 < r"
   27.45    obtain a i where a: "0 < a" and i: "\<forall>n\<ge>i. a < \<bar>X n\<bar>"
   27.46 -    using cauchy_not_vanishes [OF X] by fast
   27.47 +    using cauchy_not_vanishes [OF X] by blast
   27.48    obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>"
   27.49 -    using cauchy_not_vanishes [OF Y] by fast
   27.50 +    using cauchy_not_vanishes [OF Y] by blast
   27.51    obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
   27.52    proof
   27.53      show "0 < a * r * b"
   27.54 @@ -372,7 +372,7 @@
   27.55    done
   27.56  
   27.57  lemma part_equivp_realrel: "part_equivp realrel"
   27.58 -  by (fast intro: part_equivpI symp_realrel transp_realrel
   27.59 +  by (blast intro: part_equivpI symp_realrel transp_realrel
   27.60      realrel_refl cauchy_const)
   27.61  
   27.62  subsection \<open>The field of real numbers\<close>
   27.63 @@ -527,7 +527,7 @@
   27.64        unfolding realrel_def by simp_all
   27.65      assume "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"
   27.66      then obtain r i where "0 < r" and i: "\<forall>n\<ge>i. r < X n"
   27.67 -      by fast
   27.68 +      by blast
   27.69      obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
   27.70        using \<open>0 < r\<close> by (rule obtain_pos_sum)
   27.71      obtain j where j: "\<forall>n\<ge>j. \<bar>X n - Y n\<bar> < s"
   27.72 @@ -539,7 +539,7 @@
   27.73          using i j n by simp_all
   27.74        thus "t < Y n" unfolding r by simp
   27.75      qed
   27.76 -    hence "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by fast
   27.77 +    hence "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by blast
   27.78    } note 1 = this
   27.79    fix X Y assume "realrel X Y"
   27.80    hence "realrel X Y" and "realrel Y X"
   27.81 @@ -579,7 +579,8 @@
   27.82    "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
   27.83  apply transfer
   27.84  apply (simp add: realrel_def)
   27.85 -apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast)
   27.86 +apply (drule (1) cauchy_not_vanishes_cases, safe)
   27.87 +apply blast+
   27.88  done
   27.89  
   27.90  instantiation real :: linordered_field
   27.91 @@ -781,7 +782,7 @@
   27.92      finally have "of_int (floor (x - 1)) < x" .
   27.93      hence "\<not> x \<le> of_int (floor (x - 1))" by (simp only: not_le)
   27.94      then show "\<not> P (of_int (floor (x - 1)))"
   27.95 -      unfolding P_def of_rat_of_int_eq using x by fast
   27.96 +      unfolding P_def of_rat_of_int_eq using x by blast
   27.97    qed
   27.98    obtain b where b: "P b"
   27.99    proof
  27.100 @@ -810,7 +811,7 @@
  27.101    have width: "\<And>n. B n - A n = (b - a) / 2^n"
  27.102      apply (simp add: eq_divide_eq)
  27.103      apply (induct_tac n, simp)
  27.104 -    apply (simp add: C_def avg_def power_Suc algebra_simps)
  27.105 +    apply (simp add: C_def avg_def algebra_simps)
  27.106      done
  27.107  
  27.108    have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r"
  27.109 @@ -902,7 +903,7 @@
  27.110    proof (rule vanishesI)
  27.111      fix r :: rat assume "0 < r"
  27.112      then obtain k where k: "\<bar>b - a\<bar> / 2 ^ k < r"
  27.113 -      using twos by fast
  27.114 +      using twos by blast
  27.115      have "\<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r"
  27.116      proof (clarify)
  27.117        fix n assume n: "k \<le> n"
  27.118 @@ -1022,17 +1023,20 @@
  27.119  declare [[coercion_map "\<lambda>f g (x,y). (f x, g y)"]]
  27.120  
  27.121  declare of_int_eq_0_iff [algebra, presburger]
  27.122 -declare of_int_eq_iff [iff, algebra, presburger] (*FIXME*)
  27.123 -declare of_int_eq_iff [iff, algebra, presburger] (*FIXME*)
  27.124 -declare of_int_less_iff [iff, algebra, presburger] (*FIXME*)
  27.125 -declare of_int_le_iff [iff, algebra, presburger] (*FIXME*)
  27.126 +declare of_int_eq_1_iff [algebra, presburger]
  27.127 +declare of_int_eq_iff [algebra, presburger]
  27.128 +declare of_int_less_0_iff [algebra, presburger]
  27.129 +declare of_int_less_1_iff [algebra, presburger]
  27.130 +declare of_int_less_iff [algebra, presburger]
  27.131 +declare of_int_le_0_iff [algebra, presburger]
  27.132 +declare of_int_le_1_iff [algebra, presburger]
  27.133 +declare of_int_le_iff [algebra, presburger]
  27.134 +declare of_int_0_less_iff [algebra, presburger]
  27.135 +declare of_int_0_le_iff [algebra, presburger]
  27.136 +declare of_int_1_less_iff [algebra, presburger]
  27.137 +declare of_int_1_le_iff [algebra, presburger]
  27.138  
  27.139 -declare of_int_0_less_iff [presburger]
  27.140 -declare of_int_0_le_iff [presburger]
  27.141 -declare of_int_less_0_iff [presburger]
  27.142 -declare of_int_le_0_iff [presburger]
  27.143 -
  27.144 -lemma real_of_int_abs [simp]: "real_of_int (abs x) = abs(real_of_int x)"
  27.145 +lemma of_int_abs [simp]: "of_int (abs x) = (abs(of_int x) :: 'a::linordered_idom)"
  27.146    by (auto simp add: abs_if)
  27.147  
  27.148  lemma int_less_real_le: "(n < m) = (real_of_int n + 1 <= real_of_int m)"
  27.149 @@ -1086,29 +1090,9 @@
  27.150  
  27.151  subsection\<open>Embedding the Naturals into the Reals\<close>
  27.152  
  27.153 -declare of_nat_less_iff [iff] (*FIXME*)
  27.154 -declare of_nat_le_iff [iff] (*FIXME*)
  27.155 -declare of_nat_0_le_iff [iff] (*FIXME*)
  27.156 -declare of_nat_less_iff [iff] (*FIXME*)
  27.157 -declare of_nat_less_iff [iff] (*FIXME*)
  27.158 -
  27.159 -lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)"  (*NEEDED?*)
  27.160 -   using of_nat_0_less_iff by blast
  27.161 -
  27.162 -declare of_nat_mult [simp] (*FIXME*)
  27.163 -declare of_nat_power [simp] (*FIXME*)
  27.164 -
  27.165 -lemmas power_real_of_nat = of_nat_power [symmetric]
  27.166 -
  27.167 -declare of_nat_setsum [simp] (*FIXME*)
  27.168 -declare of_nat_setprod [simp] (*FIXME*)
  27.169 -
  27.170  lemma real_of_card: "real (card A) = setsum (\<lambda>x.1) A"
  27.171    by simp
  27.172  
  27.173 -declare of_nat_eq_iff [iff] (*FIXME*)
  27.174 -declare of_nat_eq_0_iff [iff] (*FIXME*)
  27.175 -
  27.176  lemma nat_less_real_le: "(n < m) = (real n + 1 \<le> real m)"
  27.177    by (metis discrete of_nat_1 of_nat_add of_nat_le_iff)
  27.178  
  27.179 @@ -1151,9 +1135,6 @@
  27.180  lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"
  27.181  by (insert real_of_nat_div2 [of n x], simp)
  27.182  
  27.183 -lemma of_nat_nat [simp]: "0 <= x ==> real(nat x) = real x"
  27.184 -  by force
  27.185 -
  27.186  subsection \<open>The Archimedean Property of the Reals\<close>
  27.187  
  27.188  lemmas reals_Archimedean = ex_inverse_of_nat_Suc_less  (*FIXME*)
  27.189 @@ -1276,7 +1257,7 @@
  27.190      by (simp add: divide_less_eq diff_less_eq \<open>0 < q\<close>
  27.191        less_ceiling_iff [symmetric])
  27.192    moreover from r_def have "r \<in> \<rat>" by simp
  27.193 -  ultimately show ?thesis by fast
  27.194 +  ultimately show ?thesis by blast
  27.195  qed
  27.196  
  27.197  lemma of_rat_dense:
  27.198 @@ -1294,8 +1275,6 @@
  27.199    "real_of_int (- numeral k) = - numeral k"
  27.200    by simp_all
  27.201  
  27.202 -
  27.203 -  (*FIXME*)
  27.204  declaration \<open>
  27.205    K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
  27.206      (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
  27.207 @@ -1329,9 +1308,6 @@
  27.208  
  27.209  subsection \<open>Lemmas about powers\<close>
  27.210  
  27.211 -text \<open>FIXME: declare this in Rings.thy or not at all\<close>
  27.212 -declare abs_mult_self [simp]
  27.213 -
  27.214  (* used by Import/HOL/real.imp *)
  27.215  lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
  27.216    by simp
  27.217 @@ -1440,10 +1416,6 @@
  27.218  lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
  27.219  by (simp add: abs_if)
  27.220  
  27.221 -(* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *)
  27.222 -lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
  27.223 -by (force simp add: abs_le_iff)
  27.224 -
  27.225  lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
  27.226  by (simp add: abs_if)
  27.227  
    28.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Nov 12 11:22:26 2015 +0100
    28.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Fri Nov 13 12:27:13 2015 +0000
    28.3 @@ -1062,7 +1062,7 @@
    28.4  subclass topological_space
    28.5  proof
    28.6    have "\<exists>e::real. 0 < e"
    28.7 -    by (fast intro: zero_less_one)
    28.8 +    by (blast intro: zero_less_one)
    28.9    then show "open UNIV"
   28.10      unfolding open_dist by simp
   28.11  next
   28.12 @@ -1076,7 +1076,7 @@
   28.13      done
   28.14  next
   28.15    fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
   28.16 -    unfolding open_dist by fast
   28.17 +    unfolding open_dist by (meson UnionE UnionI) 
   28.18  qed
   28.19  
   28.20  lemma open_ball: "open {y. dist x y < d}"
   28.21 @@ -1260,26 +1260,14 @@
   28.22  by (simp add: sgn_div_norm norm_mult mult.commute)
   28.23  
   28.24  lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>"
   28.25 -by (simp add: sgn_div_norm divide_inverse)
   28.26 -
   28.27 -lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
   28.28 -unfolding real_sgn_eq by simp
   28.29 -
   28.30 -lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
   28.31 -unfolding real_sgn_eq by simp
   28.32 +  by (simp add: sgn_div_norm divide_inverse)
   28.33  
   28.34  lemma zero_le_sgn_iff [simp]: "0 \<le> sgn x \<longleftrightarrow> 0 \<le> (x::real)"
   28.35    by (cases "0::real" x rule: linorder_cases) simp_all
   28.36  
   28.37 -lemma zero_less_sgn_iff [simp]: "0 < sgn x \<longleftrightarrow> 0 < (x::real)"
   28.38 -  by (cases "0::real" x rule: linorder_cases) simp_all
   28.39 -
   28.40  lemma sgn_le_0_iff [simp]: "sgn x \<le> 0 \<longleftrightarrow> (x::real) \<le> 0"
   28.41    by (cases "0::real" x rule: linorder_cases) simp_all
   28.42  
   28.43 -lemma sgn_less_0_iff [simp]: "sgn x < 0 \<longleftrightarrow> (x::real) < 0"
   28.44 -  by (cases "0::real" x rule: linorder_cases) simp_all
   28.45 -
   28.46  lemma norm_conv_dist: "norm x = dist x 0"
   28.47    unfolding dist_norm by simp
   28.48  
   28.49 @@ -1321,7 +1309,7 @@
   28.50    "\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K"
   28.51  proof -
   28.52    obtain K where K: "\<And>x. norm (f x) \<le> norm x * K"
   28.53 -    using bounded by fast
   28.54 +    using bounded by blast
   28.55    show ?thesis
   28.56    proof (intro exI impI conjI allI)
   28.57      show "0 < max 1 K"
   28.58 @@ -1351,7 +1339,7 @@
   28.59    assumes "\<And>r x. f (scaleR r x) = scaleR r (f x)"
   28.60    assumes "\<And>x. norm (f x) \<le> norm x * K"
   28.61    shows "bounded_linear f"
   28.62 -  by standard (fast intro: assms)+
   28.63 +  by standard (blast intro: assms)+
   28.64  
   28.65  locale bounded_bilinear =
   28.66    fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
   28.67 @@ -1481,9 +1469,9 @@
   28.68        by (simp only: f.scaleR g.scaleR)
   28.69    next
   28.70      from f.pos_bounded
   28.71 -    obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
   28.72 +    obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by blast
   28.73      from g.pos_bounded
   28.74 -    obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
   28.75 +    obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by blast
   28.76      show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
   28.77      proof (intro exI allI)
   28.78        fix x
   28.79 @@ -1735,7 +1723,7 @@
   28.80    proof (intro allI impI)
   28.81      fix e :: real assume e: "e > 0"
   28.82      with `Cauchy f` obtain M where "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (f m) (f n) < e"
   28.83 -      unfolding Cauchy_def by fast
   28.84 +      unfolding Cauchy_def by blast
   28.85      thus "\<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e" by (intro exI[of _ M]) force
   28.86    qed
   28.87  qed
   28.88 @@ -1783,9 +1771,9 @@
   28.89    show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
   28.90    proof (intro exI allI impI)
   28.91      fix m assume "N \<le> m"
   28.92 -    hence m: "dist (X m) a < e/2" using N by fast
   28.93 +    hence m: "dist (X m) a < e/2" using N by blast
   28.94      fix n assume "N \<le> n"
   28.95 -    hence n: "dist (X n) a < e/2" using N by fast
   28.96 +    hence n: "dist (X n) a < e/2" using N by blast
   28.97      have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
   28.98        by (rule dist_triangle2)
   28.99      also from m n have "\<dots> < e" by simp
  28.100 @@ -1805,7 +1793,7 @@
  28.101  lemma Cauchy_convergent_iff:
  28.102    fixes X :: "nat \<Rightarrow> 'a::complete_space"
  28.103    shows "Cauchy X = convergent X"
  28.104 -by (fast intro: Cauchy_convergent convergent_Cauchy)
  28.105 +by (blast intro: Cauchy_convergent convergent_Cauchy)
  28.106  
  28.107  subsection \<open>The set of real numbers is a complete metric space\<close>
  28.108  
  28.109 @@ -1881,11 +1869,11 @@
  28.110    hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
  28.111      by (simp only: dist_real_def abs_diff_less_iff)
  28.112  
  28.113 -  from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
  28.114 +  from N have "\<forall>n\<ge>N. X N - r/2 < X n" by blast
  28.115    hence "X N - r/2 \<in> S" by (rule mem_S)
  28.116    hence 1: "X N - r/2 \<le> Sup S" by (simp add: cSup_upper)
  28.117  
  28.118 -  from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
  28.119 +  from N have "\<forall>n\<ge>N. X n < X N + r/2" by blast
  28.120    from bound_isUb[OF this]
  28.121    have 2: "Sup S \<le> X N + r/2"
  28.122      by (intro cSup_least) simp_all
  28.123 @@ -1953,7 +1941,7 @@
  28.124        using ex_le_of_nat[of x] ..
  28.125      note monoD[OF mono this]
  28.126      also have "f (real_of_nat n) \<le> y"
  28.127 -      by (rule LIMSEQ_le_const[OF limseq]) (auto intro: exI[of _ n] monoD[OF mono])
  28.128 +      by (rule LIMSEQ_le_const[OF limseq]) (auto intro!: exI[of _ n] monoD[OF mono])
  28.129      finally have "f x \<le> y" . }
  28.130    note le = this
  28.131    have "eventually (\<lambda>x. real N \<le> x) at_top"
    29.1 --- a/src/HOL/Rings.thy	Thu Nov 12 11:22:26 2015 +0100
    29.2 +++ b/src/HOL/Rings.thy	Fri Nov 13 12:27:13 2015 +0000
    29.3 @@ -1976,7 +1976,7 @@
    29.4    "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
    29.5    by (rule abs_eq_mult) auto
    29.6  
    29.7 -lemma abs_mult_self:
    29.8 +lemma abs_mult_self [simp]:
    29.9    "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
   29.10    by (simp add: abs_if)
   29.11  
    30.1 --- a/src/HOL/Transcendental.thy	Thu Nov 12 11:22:26 2015 +0100
    30.2 +++ b/src/HOL/Transcendental.thy	Fri Nov 13 12:27:13 2015 +0000
    30.3 @@ -10,13 +10,6 @@
    30.4  imports Binomial Series Deriv NthRoot
    30.5  begin
    30.6  
    30.7 -lemma reals_Archimedean4:
    30.8 -  assumes "0 < y" "0 \<le> x"
    30.9 -  obtains n where "real n * y \<le> x" "x < real (Suc n) * y"
   30.10 -  using floor_correct [of "x/y"] assms
   30.11 -  apply (auto simp: field_simps intro!: that [of "nat (floor (x/y))"])
   30.12 -by (metis (no_types, hide_lams)  divide_inverse divide_self_if floor_correct mult.left_commute mult.right_neutral mult_eq_0_iff order_refl order_trans real_mult_le_cancel_iff2)
   30.13 -
   30.14  lemma fact_in_Reals: "fact n \<in> \<real>" by (induction n) auto
   30.15  
   30.16  lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
   30.17 @@ -3556,6 +3549,14 @@
   30.18      done
   30.19  qed
   30.20  
   30.21 +
   30.22 +lemma reals_Archimedean4:
   30.23 +  assumes "0 < y" "0 \<le> x"
   30.24 +  obtains n where "real n * y \<le> x" "x < real (Suc n) * y"
   30.25 +  using floor_correct [of "x/y"] assms
   30.26 +  apply (auto simp: field_simps intro!: that [of "nat (floor (x/y))"])
   30.27 +by (metis (no_types, hide_lams)  divide_inverse divide_self_if floor_correct mult.left_commute mult.right_neutral mult_eq_0_iff order_refl order_trans real_mult_le_cancel_iff2)
   30.28 +
   30.29  lemma cos_zero_lemma:
   30.30       "\<lbrakk>0 \<le> x; cos x = 0\<rbrakk> \<Longrightarrow>
   30.31        \<exists>n::nat. odd n & x = real n * (pi/2)"
   30.32 @@ -4399,7 +4400,7 @@
   30.33    by (metis (no_types, hide_lams) arcsin arcsin_sin minus_minus neg_le_iff_le sin_minus)
   30.34  
   30.35  lemma arcsin_eq_iff: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arcsin x = arcsin y \<longleftrightarrow> x = y)"
   30.36 -  by (metis abs_le_interval_iff arcsin)
   30.37 +  by (metis abs_le_iff arcsin minus_le_iff)
   30.38  
   30.39  lemma cos_arcsin_nonzero: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> cos(arcsin x) \<noteq> 0"
   30.40    using arcsin_lt_bounded cos_gt_zero_pi by force
    31.1 --- a/src/HOL/Word/Word.thy	Thu Nov 12 11:22:26 2015 +0100
    31.2 +++ b/src/HOL/Word/Word.thy	Fri Nov 13 12:27:13 2015 +0000
    31.3 @@ -960,7 +960,7 @@
    31.4    apply auto
    31.5    apply (erule_tac nat_less_iff [THEN iffD2])
    31.6    apply (rule_tac [2] zless_nat_eq_int_zless [THEN iffD1])
    31.7 -  apply (auto simp add : nat_power_eq int_power)
    31.8 +  apply (auto simp add : nat_power_eq of_nat_power)
    31.9    done
   31.10  
   31.11  lemma unats_uints: "unats n = nat ` uints n"
   31.12 @@ -1901,7 +1901,7 @@
   31.13  
   31.14  lemma Abs_fnat_hom_mult:
   31.15    "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
   31.16 -  by (simp add: word_of_nat wi_hom_mult zmult_int)
   31.17 +  by (simp add: word_of_nat wi_hom_mult)
   31.18  
   31.19  lemma Abs_fnat_hom_Suc:
   31.20    "word_succ (of_nat a) = of_nat (Suc a)"
   31.21 @@ -2125,9 +2125,7 @@
   31.22    "(i :: 'a :: len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
   31.23    apply (unfold uint_nat)
   31.24    apply (drule div_lt')
   31.25 -  apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] 
   31.26 -                   nat_power_eq)
   31.27 -  done
   31.28 +  by (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power)
   31.29  
   31.30  lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
   31.31  
   31.32 @@ -2156,22 +2154,14 @@
   31.33  
   31.34  lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
   31.35  
   31.36 -lemma thd1:
   31.37 -  "a div b * b \<le> (a::nat)"
   31.38 -  using gt_or_eq_0 [of b]
   31.39 -  apply (rule disjE)
   31.40 -   apply (erule xtr4 [OF thd mult.commute])
   31.41 -  apply clarsimp
   31.42 -  done
   31.43 -
   31.44 -lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend thd1 
   31.45 +lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle 
   31.46  
   31.47  lemma word_mod_div_equality:
   31.48    "(n div b) * b + (n mod b) = (n :: 'a :: len word)"
   31.49    apply (unfold word_less_nat_alt word_arith_nat_defs)
   31.50    apply (cut_tac y="unat b" in gt_or_eq_0)
   31.51    apply (erule disjE)
   31.52 -   apply (simp add: mod_div_equality uno_simps)
   31.53 +   apply (simp only: mod_div_equality uno_simps Word.word_unat.Rep_inverse)
   31.54    apply simp
   31.55    done
   31.56  
   31.57 @@ -2179,7 +2169,7 @@
   31.58    apply (unfold word_le_nat_alt word_arith_nat_defs)
   31.59    apply (cut_tac y="unat b" in gt_or_eq_0)
   31.60    apply (erule disjE)
   31.61 -   apply (simp add: div_mult_le uno_simps)
   31.62 +   apply (simp only: div_mult_le uno_simps Word.word_unat.Rep_inverse)
   31.63    apply simp
   31.64    done
   31.65  
   31.66 @@ -3305,7 +3295,7 @@
   31.67    apply (unfold dvd_def) 
   31.68    apply auto 
   31.69    apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
   31.70 -  apply (simp add : int_mult int_power)
   31.71 +  apply (simp add : int_mult of_nat_power)
   31.72    apply (simp add : nat_mult_distrib nat_power_eq)
   31.73    done
   31.74  
   31.75 @@ -4653,15 +4643,7 @@
   31.76    "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
   31.77    apply (simp add: word_rec_def unat_word_ariths)
   31.78    apply (subst nat_mod_eq')
   31.79 -   apply (cut_tac x=n in unat_lt2p)
   31.80 -   apply (drule Suc_mono)
   31.81 -   apply (simp add: less_Suc_eq_le)
   31.82 -   apply (simp only: order_less_le, simp)
   31.83 -   apply (erule contrapos_pn, simp)
   31.84 -   apply (drule arg_cong[where f=of_nat])
   31.85 -   apply simp
   31.86 -   apply (subst (asm) word_unat.Rep_inverse[of n])
   31.87 -   apply simp
   31.88 +   apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add)
   31.89    apply simp
   31.90    done
   31.91  
    32.1 --- a/src/HOL/ex/Sqrt.thy	Thu Nov 12 11:22:26 2015 +0100
    32.2 +++ b/src/HOL/ex/Sqrt.thy	Fri Nov 13 12:27:13 2015 +0000
    32.3 @@ -26,7 +26,7 @@
    32.4        by (auto simp add: power2_eq_square)
    32.5      also have "(sqrt p)\<^sup>2 = p" by simp
    32.6      also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
    32.7 -    finally show ?thesis ..
    32.8 +    finally show ?thesis using of_nat_eq_iff by blast
    32.9    qed
   32.10    have "p dvd m \<and> p dvd n"
   32.11    proof
   32.12 @@ -69,7 +69,7 @@
   32.13      by (auto simp add: power2_eq_square)
   32.14    also have "(sqrt p)\<^sup>2 = p" by simp
   32.15    also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
   32.16 -  finally have eq: "m\<^sup>2 = p * n\<^sup>2" ..
   32.17 +  finally have eq: "m\<^sup>2 = p * n\<^sup>2" using of_nat_eq_iff by blast
   32.18    then have "p dvd m\<^sup>2" ..
   32.19    with \<open>prime p\<close> have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
   32.20    then obtain k where "m = p * k" ..
    33.1 --- a/src/HOL/ex/Sum_of_Powers.thy	Thu Nov 12 11:22:26 2015 +0100
    33.2 +++ b/src/HOL/ex/Sum_of_Powers.thy	Fri Nov 13 12:27:13 2015 +0000
    33.3 @@ -175,7 +175,7 @@
    33.4    from sum_of_squares have "real (6 * (\<Sum>k\<le>n. k ^ 2)) = real (2 * n ^ 3 + 3 * n ^ 2 + n)"
    33.5      by (auto simp add: field_simps)
    33.6    then have "6 * (\<Sum>k\<le>n. k ^ 2) = 2 * n ^ 3 + 3 * n ^ 2 + n"
    33.7 -    by blast
    33.8 +    using of_nat_eq_iff by blast
    33.9    then show ?thesis by auto
   33.10  qed
   33.11  
   33.12 @@ -197,7 +197,7 @@
   33.13    from sum_of_cubes have "real (4 * (\<Sum>k\<le>n. k ^ 3)) = real ((n ^ 2 + n) ^ 2)"
   33.14      by (auto simp add: field_simps)
   33.15    then have "4 * (\<Sum>k\<le>n. k ^ 3) = (n ^ 2 + n) ^ 2"
   33.16 -    by blast
   33.17 +    using of_nat_eq_iff by blast
   33.18    then show ?thesis by auto
   33.19  qed
   33.20  
    34.1 --- a/src/HOL/ex/Transfer_Int_Nat.thy	Thu Nov 12 11:22:26 2015 +0100
    34.2 +++ b/src/HOL/ex/Transfer_Int_Nat.thy	Fri Nov 13 12:27:13 2015 +0000
    34.3 @@ -46,7 +46,7 @@
    34.4    unfolding rel_fun_def ZN_def tsub_def by (simp add: zdiff_int)
    34.5  
    34.6  lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
    34.7 -  unfolding rel_fun_def ZN_def by (simp add: int_power)
    34.8 +  unfolding rel_fun_def ZN_def by (simp add: of_nat_power)
    34.9  
   34.10  lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
   34.11    unfolding rel_fun_def ZN_def by simp