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