1.1 --- a/NEWS Thu Oct 31 16:54:22 2013 +0100
1.2 +++ b/NEWS Fri Nov 01 18:51:14 2013 +0100
1.3 @@ -15,6 +15,39 @@
1.4 even_zero_(nat|int) ~> even_zero
1.5 INCOMPATIBILITY.
1.6
1.7 +*** HOL ***
1.8 +
1.9 +* Elimination of fact duplicates:
1.10 + equals_zero_I ~> minus_unique
1.11 + diff_eq_0_iff_eq ~> right_minus_eq
1.12 +INCOMPATIBILITY.
1.13 +
1.14 +* Fact name consolidation:
1.15 + diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
1.16 +INCOMPATIBILITY.
1.17 +
1.18 +* More simplification rules on unary and binary minus:
1.19 +add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1,
1.20 +add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
1.21 +add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
1.22 +le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
1.23 +minus_add_cancel, uminus_add_conv_diff. These correspondingly
1.24 +have been taken away from fact collections algebra_simps and
1.25 +field_simps. INCOMPATIBILITY.
1.26 +
1.27 +To restore proofs, the following patterns are helpful:
1.28 +
1.29 +a) Arbitrary failing proof not involving "diff_def":
1.30 +Consider simplification with algebra_simps or field_simps.
1.31 +
1.32 +b) Lifting rules from addition to subtraction:
1.33 +Try with "using <rule for addition> of [… "- _" …]" by simp".
1.34 +
1.35 +c) Simplification with "diff_def": just drop "diff_def".
1.36 +Consider simplification with algebra_simps or field_simps;
1.37 +or the brute way with
1.38 +"simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
1.39 +
1.40
1.41 New in Isabelle2013-1 (November 2013)
1.42 -------------------------------------
2.1 --- a/src/HOL/Big_Operators.thy Thu Oct 31 16:54:22 2013 +0100
2.2 +++ b/src/HOL/Big_Operators.thy Fri Nov 01 18:51:14 2013 +0100
2.3 @@ -696,11 +696,7 @@
2.4 lemma setsum_subtractf:
2.5 "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
2.6 setsum f A - setsum g A"
2.7 -proof (cases "finite A")
2.8 - case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf)
2.9 -next
2.10 - case False thus ?thesis by simp
2.11 -qed
2.12 + using setsum_addf [of f "- g" A] by (simp add: setsum_negf)
2.13
2.14 lemma setsum_nonneg:
2.15 assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
3.1 --- a/src/HOL/Complex.thy Thu Oct 31 16:54:22 2013 +0100
3.2 +++ b/src/HOL/Complex.thy Fri Nov 01 18:51:14 2013 +0100
3.3 @@ -587,7 +587,7 @@
3.4 by (simp add: cis_def)
3.5
3.6 lemma cis_divide: "cis a / cis b = cis (a - b)"
3.7 - by (simp add: complex_divide_def cis_mult diff_minus)
3.8 + by (simp add: complex_divide_def cis_mult)
3.9
3.10 lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
3.11 by (auto simp add: DeMoivre)
4.1 --- a/src/HOL/Decision_Procs/Approximation.thy Thu Oct 31 16:54:22 2013 +0100
4.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Fri Nov 01 18:51:14 2013 +0100
4.3 @@ -29,7 +29,7 @@
4.4 have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)"
4.5 by auto
4.6 show ?thesis
4.7 - unfolding setsum_right_distrib shift_pow diff_minus setsum_negf[symmetric]
4.8 + unfolding setsum_right_distrib shift_pow uminus_add_conv_diff [symmetric] setsum_negf[symmetric]
4.9 setsum_head_upt_Suc[OF zero_less_Suc]
4.10 setsum_reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n *a n * x^n"] by auto
4.11 qed
4.12 @@ -533,12 +533,12 @@
4.13 have "pi \<le> ub_pi n"
4.14 unfolding ub_pi_def machin_pi Let_def unfolding Float_num
4.15 using lb_arctan[of 239] ub_arctan[of 5] powr_realpow[of 2 2]
4.16 - by (auto intro!: mult_left_mono add_mono simp add: diff_minus)
4.17 + by (auto intro!: mult_left_mono add_mono simp add: uminus_add_conv_diff [symmetric] simp del: uminus_add_conv_diff)
4.18 moreover
4.19 have "lb_pi n \<le> pi"
4.20 unfolding lb_pi_def machin_pi Let_def Float_num
4.21 using lb_arctan[of 5] ub_arctan[of 239] powr_realpow[of 2 2]
4.22 - by (auto intro!: mult_left_mono add_mono simp add: diff_minus)
4.23 + by (auto intro!: mult_left_mono add_mono simp add: uminus_add_conv_diff [symmetric] simp del: uminus_add_conv_diff)
4.24 ultimately show ?thesis by auto
4.25 qed
4.26
4.27 @@ -1208,8 +1208,8 @@
4.28 using x unfolding k[symmetric]
4.29 by (cases "k = 0")
4.30 (auto intro!: add_mono
4.31 - simp add: diff_minus k[symmetric]
4.32 - simp del: float_of_numeral)
4.33 + simp add: k [symmetric] uminus_add_conv_diff [symmetric]
4.34 + simp del: float_of_numeral uminus_add_conv_diff)
4.35 note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
4.36 hence lx_less_ux: "?lx \<le> real ?ux" by (rule order_trans)
4.37
4.38 @@ -1223,7 +1223,7 @@
4.39 also have "\<dots> \<le> cos (x + (-k) * (2 * pi))"
4.40 using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
4.41 by (simp only: uminus_float.rep_eq real_of_int_minus
4.42 - cos_minus diff_minus mult_minus_left)
4.43 + cos_minus mult_minus_left) simp
4.44 finally have "(lb_cos prec (- ?lx)) \<le> cos x"
4.45 unfolding cos_periodic_int . }
4.46 note negative_lx = this
4.47 @@ -1236,7 +1236,7 @@
4.48 have "cos (x + (-k) * (2 * pi)) \<le> cos ?lx"
4.49 using cos_monotone_0_pi'[OF lx_0 lx pi_x]
4.50 by (simp only: real_of_int_minus
4.51 - cos_minus diff_minus mult_minus_left)
4.52 + cos_minus mult_minus_left) simp
4.53 also have "\<dots> \<le> (ub_cos prec ?lx)"
4.54 using lb_cos[OF lx_0 pi_lx] by simp
4.55 finally have "cos x \<le> (ub_cos prec ?lx)"
4.56 @@ -1251,7 +1251,7 @@
4.57 have "cos (x + (-k) * (2 * pi)) \<le> cos (real (- ?ux))"
4.58 using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
4.59 by (simp only: uminus_float.rep_eq real_of_int_minus
4.60 - cos_minus diff_minus mult_minus_left)
4.61 + cos_minus mult_minus_left) simp
4.62 also have "\<dots> \<le> (ub_cos prec (- ?ux))"
4.63 using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
4.64 finally have "cos x \<le> (ub_cos prec (- ?ux))"
4.65 @@ -1268,7 +1268,7 @@
4.66 also have "\<dots> \<le> cos (x + (-k) * (2 * pi))"
4.67 using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
4.68 by (simp only: real_of_int_minus
4.69 - cos_minus diff_minus mult_minus_left)
4.70 + cos_minus mult_minus_left) simp
4.71 finally have "(lb_cos prec ?ux) \<le> cos x"
4.72 unfolding cos_periodic_int . }
4.73 note positive_ux = this
4.74 @@ -1343,7 +1343,7 @@
4.75 also have "\<dots> \<le> cos ((?ux - 2 * ?lpi))"
4.76 using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
4.77 by (simp only: minus_float.rep_eq real_of_int_minus real_of_one minus_one[symmetric]
4.78 - diff_minus mult_minus_left mult_1_left)
4.79 + mult_minus_left mult_1_left) simp
4.80 also have "\<dots> = cos ((- (?ux - 2 * ?lpi)))"
4.81 unfolding uminus_float.rep_eq cos_minus ..
4.82 also have "\<dots> \<le> (ub_cos prec (- (?ux - 2 * ?lpi)))"
4.83 @@ -1387,7 +1387,7 @@
4.84 also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
4.85 using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
4.86 by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
4.87 - minus_one[symmetric] diff_minus mult_minus_left mult_1_left)
4.88 + minus_one[symmetric] mult_minus_left mult_1_left) simp
4.89 also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
4.90 using lb_cos[OF lx_0 pi_lx] by simp
4.91 finally show ?thesis unfolding u by (simp add: real_of_float_max)
4.92 @@ -2164,12 +2164,12 @@
4.93 unfolding divide_inverse interpret_floatarith.simps ..
4.94
4.95 lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
4.96 - unfolding diff_minus interpret_floatarith.simps ..
4.97 + unfolding interpret_floatarith.simps by simp
4.98
4.99 lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
4.100 sin (interpret_floatarith a vs)"
4.101 unfolding sin_cos_eq interpret_floatarith.simps
4.102 - interpret_floatarith_divide interpret_floatarith_diff diff_minus
4.103 + interpret_floatarith_divide interpret_floatarith_diff
4.104 by auto
4.105
4.106 lemma interpret_floatarith_tan:
4.107 @@ -3192,7 +3192,7 @@
4.108
4.109 from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
4.110 have "ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
4.111 - by (auto simp add: diff_minus)
4.112 + by auto
4.113 from order_less_le_trans[OF _ this, of 0] `0 < ly`
4.114 show ?thesis by auto
4.115 qed
4.116 @@ -3214,7 +3214,7 @@
4.117
4.118 from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
4.119 have "ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
4.120 - by (auto simp add: diff_minus)
4.121 + by auto
4.122 from order_trans[OF _ this, of 0] `0 \<le> ly`
4.123 show ?thesis by auto
4.124 qed
5.1 --- a/src/HOL/Decision_Procs/Cooper.thy Thu Oct 31 16:54:22 2013 +0100
5.2 +++ b/src/HOL/Decision_Procs/Cooper.thy Fri Nov 01 18:51:14 2013 +0100
5.3 @@ -1400,9 +1400,8 @@
5.4 also have "\<dots> = (j dvd (- (c*x - ?e)))"
5.5 by (simp only: dvd_minus_iff)
5.6 also have "\<dots> = (j dvd (c* (- x)) + ?e)"
5.7 - apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
5.8 - apply (simp add: algebra_simps)
5.9 - done
5.10 + by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
5.11 + (simp add: algebra_simps)
5.12 also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
5.13 using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
5.14 finally show ?case .
5.15 @@ -1413,9 +1412,8 @@
5.16 also have "\<dots> = (j dvd (- (c*x - ?e)))"
5.17 by (simp only: dvd_minus_iff)
5.18 also have "\<dots> = (j dvd (c* (- x)) + ?e)"
5.19 - apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
5.20 - apply (simp add: algebra_simps)
5.21 - done
5.22 + by (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] add_ac minus_add_distrib)
5.23 + (simp add: algebra_simps)
5.24 also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
5.25 using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] by simp
5.26 finally show ?case by simp
6.1 --- a/src/HOL/Decision_Procs/MIR.thy Thu Oct 31 16:54:22 2013 +0100
6.2 +++ b/src/HOL/Decision_Procs/MIR.thy Fri Nov 01 18:51:14 2013 +0100
6.3 @@ -1727,7 +1727,7 @@
6.4 {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))"
6.5 by (simp add: nb Let_def split_def isint_Floor isint_neg)
6.6 have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
6.7 - also have "\<dots> = (?I (?l (Lt a)))" apply (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) by (simp add: Ia cp cnz Let_def split_def diff_minus)
6.8 + also have "\<dots> = (?I (?l (Lt a)))" apply (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) by (simp add: Ia cp cnz Let_def split_def)
6.9 finally have ?case using l by simp}
6.10 moreover
6.11 {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))"
6.12 @@ -1752,13 +1752,13 @@
6.13 {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))"
6.14 by (simp add: nb Let_def split_def isint_Floor isint_neg)
6.15 have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
6.16 - also have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus)
6.17 + also have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def)
6.18 finally have ?case using l by simp}
6.19 moreover
6.20 {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))"
6.21 by (simp add: nb Let_def split_def isint_Floor isint_neg)
6.22 have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
6.23 - also from cn cnz have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac ,arith)
6.24 + also from cn cnz have "\<dots> = (?I (?l (Le a)))" by (simp only: split_int_le_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
6.25 finally have ?case using l by simp}
6.26 ultimately show ?case by blast
6.27 next
6.28 @@ -1777,13 +1777,13 @@
6.29 {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))"
6.30 by (simp add: nb Let_def split_def isint_Floor isint_neg)
6.31 have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
6.32 - also have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus)
6.33 + also have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def)
6.34 finally have ?case using l by simp}
6.35 moreover
6.36 {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))"
6.37 by (simp add: nb Let_def split_def isint_Floor isint_neg)
6.38 have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
6.39 - also from cn cnz have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac, arith)
6.40 + also from cn cnz have "\<dots> = (?I (?l (Gt a)))" by (simp only: split_int_gt_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
6.41 finally have ?case using l by simp}
6.42 ultimately show ?case by blast
6.43 next
6.44 @@ -1802,13 +1802,13 @@
6.45 {assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))"
6.46 by (simp add: nb Let_def split_def isint_Floor isint_neg)
6.47 have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
6.48 - also have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def diff_minus)
6.49 + also have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia cp cnz Let_def split_def)
6.50 finally have ?case using l by simp}
6.51 moreover
6.52 {assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))"
6.53 by (simp add: nb Let_def split_def isint_Floor isint_neg)
6.54 have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
6.55 - also from cn cnz have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac, arith)
6.56 + also from cn cnz have "\<dots> = (?I (?l (Ge a)))" by (simp only: split_int_ge_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def add_ac, arith)
6.57 finally have ?case using l by simp}
6.58 ultimately show ?case by blast
6.59 next
6.60 @@ -3125,7 +3125,8 @@
6.61 hence pid: "c*i + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
6.62 with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + ?fe = j1" by auto
6.63 hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - ?N i e + real j1"
6.64 - by (simp only: real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps)
6.65 + by (simp only: real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff])
6.66 + (simp add: algebra_simps)
6.67 with nob have ?case by blast }
6.68 ultimately show ?case by blast
6.69 next
6.70 @@ -3148,11 +3149,12 @@
6.71 hence pid: "c*i + 1 + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
6.72 with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + 1+ ?fe = j1" by auto
6.73 hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) + 1= - ?N i e + real j1"
6.74 - by (simp only: real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps real_of_one)
6.75 + by (simp only: real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] real_of_one)
6.76 + (simp add: algebra_simps)
6.77 hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1"
6.78 by (simp only: algebra_simps)
6.79 hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1"
6.80 - by (simp only: add_ac diff_minus)
6.81 + by (simp add: algebra_simps minus_one [symmetric] del: minus_one)
6.82 with nob have ?case by blast }
6.83 ultimately show ?case by blast
6.84 next
6.85 @@ -3477,10 +3479,7 @@
6.86 qed
6.87 next
6.88 case (3 a b) then show ?case
6.89 - apply auto
6.90 - apply (erule_tac x = "(aa, aaa, ba)" in ballE) apply simp_all
6.91 - apply (erule_tac x = "(ab, ac, baa)" in ballE) apply simp_all
6.92 - done
6.93 + by auto
6.94 qed (auto simp add: Let_def split_def algebra_simps)
6.95
6.96 lemma real_in_int_intervals:
6.97 @@ -3615,7 +3614,7 @@
6.98 by(simp only: myle[of _ "real n * x + Inum (x # bs) s - Inum (x # bs) (Floor s)"] less_iff_diff_less_0[where a="real n *x + ?N s - ?N (Floor s)"])
6.99 hence "\<exists> j\<in> {n .. 0}. 0 \<ge> - (real n *x + ?N s - ?N (Floor s) - real j) \<and> - (real n *x + ?N s - ?N (Floor s) - real (j+1)) > 0" by (simp only: th1[rule_format] th2[rule_format])
6.100 hence "\<exists> j\<in> {n.. 0}. ?I (?p (p,n,s) j)"
6.101 - using pns by (simp add: fp_def nn diff_minus add_ac mult_ac
6.102 + using pns by (simp add: fp_def nn algebra_simps
6.103 del: diff_less_0_iff_less diff_le_0_iff_le)
6.104 then obtain "j" where j_def: "j\<in> {n .. 0} \<and> ?I (?p (p,n,s) j)" by blast
6.105 hence "\<exists>x \<in> {?p (p,n,s) j |j. n\<le> j \<and> j \<le> 0 }. ?I x" by auto
6.106 @@ -4832,7 +4831,7 @@
6.107 shows "(Ifm bs (E p)) = (\<exists> (i::int). Ifm (real i#bs) (E (And (And (Ge(CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))) (exsplit p))))" (is "?lhs = ?rhs")
6.108 proof-
6.109 have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
6.110 - by (simp add: myless[of _ "1"] myless[of _ "0"] add_ac diff_minus)
6.111 + by (simp add: myless[of _ "1"] myless[of _ "0"] add_ac)
6.112 also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
6.113 by (simp only: exsplit[OF qf] add_ac)
6.114 also have "\<dots> = (\<exists> x. Ifm (x#bs) p)"
6.115 @@ -5196,7 +5195,7 @@
6.116 hence "\<forall> j\<in> set ?js. bound0 (subst0 (C j) ?smq)"
6.117 by (auto simp only: subst0_bound0[OF qfmq])
6.118 hence th: "\<forall> j\<in> set ?js. bound0 (simpfm (subst0 (C j) ?smq))"
6.119 - by (auto simp add: simpfm_bound0)
6.120 + by auto
6.121 from evaldjf_bound0[OF th] have mdb: "bound0 ?md" by simp
6.122 from Bn jsnb have "\<forall> (b,j) \<in> set ?bjs. numbound0 (Add b (C j))"
6.123 by simp
7.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Oct 31 16:54:22 2013 +0100
7.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Nov 01 18:51:14 2013 +0100
7.3 @@ -1959,7 +1959,7 @@
7.4 by (simp add: field_simps)
7.5 have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Eq (CNP 0 a r))" by (simp only: th)
7.6 also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r = 0"
7.7 - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
7.8 + by (simp add: r [of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
7.9 also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) =0 "
7.10 using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
7.11 also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r =0"
7.12 @@ -2041,7 +2041,7 @@
7.13 by (simp add: field_simps)
7.14 have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (NEq (CNP 0 a r))" by (simp only: th)
7.15 also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r \<noteq> 0"
7.16 - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
7.17 + by (simp add: r [of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
7.18 also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) \<noteq> 0 "
7.19 using c d mult_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
7.20 also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0"
7.21 @@ -2106,7 +2106,7 @@
7.22 by (simp add: field_simps)
7.23 have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
7.24 also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r < 0"
7.25 - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
7.26 + by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
7.27 also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) < 0"
7.28
7.29 using dc' dc'' mult_less_cancel_left_disj[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
7.30 @@ -2127,7 +2127,7 @@
7.31 by (simp add: field_simps)
7.32 have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Lt (CNP 0 a r))" by (simp only: th)
7.33 also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r < 0"
7.34 - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
7.35 + by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
7.36
7.37 also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) > 0"
7.38
7.39 @@ -2251,7 +2251,7 @@
7.40 by (simp add: field_simps)
7.41 have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
7.42 also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r <= 0"
7.43 - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
7.44 + by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
7.45 also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) <= 0"
7.46
7.47 using dc' dc'' mult_le_cancel_left[of "2 * ?c * ?d" "?a * (- (?d * ?t + ?c* ?s)/ (2*?c*?d)) + ?r" 0] by simp
7.48 @@ -2272,7 +2272,7 @@
7.49 by (simp add: field_simps)
7.50 have "?rhs \<longleftrightarrow> Ifm vs (- (?d * ?t + ?c* ?s )/ (2*?c*?d) # bs) (Le (CNP 0 a r))" by (simp only: th)
7.51 also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r <= 0"
7.52 - by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"])
7.53 + by (simp add: r[of "(- (?d * ?t) - (?c *?s)) / (2 * ?c * ?d)"])
7.54
7.55 also have "\<dots> \<longleftrightarrow> (2 * ?c * ?d) * (?a * (- (?d * ?t + ?c* ?s )/ (2*?c*?d)) + ?r) >= 0"
7.56
7.57 @@ -2356,8 +2356,11 @@
7.58
7.59 lemma msubst_I: assumes lp: "islin p" and nc: "isnpoly c" and nd: "isnpoly d"
7.60 shows "Ifm vs (x#bs) (msubst p ((c,t),(d,s))) = Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) p"
7.61 - using lp
7.62 -by (induct p rule: islin.induct, auto simp add: tmbound0_I[where b="(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) + - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2" and b'=x and bs = bs and vs=vs] bound0_I[where b="(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) + - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2" and b'=x and bs = bs and vs=vs] msubsteq msubstneq msubstlt[OF nc nd] msubstle[OF nc nd])
7.63 + using lp by (induct p rule: islin.induct)
7.64 + (auto simp add: tmbound0_I
7.65 + [where b = "(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2"
7.66 + and b' = x and bs = bs and vs = vs]
7.67 + msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd])
7.68
7.69 lemma msubst_nb: assumes lp: "islin p" and t: "tmbound0 t" and s: "tmbound0 s"
7.70 shows "bound0 (msubst p ((c,t),(d,s)))"
7.71 @@ -2429,7 +2432,7 @@
7.72 with evaldjf_bound0[of ?Up "(simpfm o (msubst (simpfm p)))"]
7.73 have "bound0 (evaldjf (simpfm o (msubst (simpfm p))) ?Up)" by blast
7.74 with mp_nb pp_nb
7.75 - have th1: "bound0 (disj ?mp (disj ?pp (evaldjf (simpfm o (msubst ?q)) ?Up )))" by (simp add: disj_nb)
7.76 + have th1: "bound0 (disj ?mp (disj ?pp (evaldjf (simpfm o (msubst ?q)) ?Up )))" by simp
7.77 from decr0_qf[OF th1] have thqf: "qfree (ferrack p)" by (simp add: ferrack_def Let_def)
7.78 have "?lhs \<longleftrightarrow> (\<exists>x. Ifm vs (x#bs) ?q)" by simp
7.79 also have "\<dots> \<longleftrightarrow> ?I ?mp \<or> ?I ?pp \<or> (\<exists>(c, t)\<in>set ?U. \<exists>(d, s)\<in>set ?U. ?I (msubst (simpfm p) ((c, t), d, s)))" using fr_eq_msubst[OF lq, of vs bs x] by simp
7.80 @@ -2612,7 +2615,7 @@
7.81 lemma msubst2_nb: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" and lp: "islin p" and tnb: "tmbound0 t"
7.82 shows "bound0 (msubst2 p c t)"
7.83 using lp tnb
7.84 -by (simp add: msubst2_def msubstneg_nb msubstpos_nb conj_nb disj_nb lt_nb simpfm_bound0)
7.85 +by (simp add: msubst2_def msubstneg_nb msubstpos_nb lt_nb simpfm_bound0)
7.86
7.87 lemma mult_minus2_left: "-2 * (x::'a::comm_ring_1) = - (2 * x)"
7.88 by simp
7.89 @@ -2666,8 +2669,8 @@
7.90 using H(3) by (auto simp add: msubst2_def lt[OF stupid(1)] lt[OF stupid(2)] zero_less_mult_iff mult_less_0_iff)
7.91 from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
7.92 have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p"
7.93 - apply (simp add: add_divide_distrib mult_minus2_left)
7.94 - by (simp add: mult_commute)}
7.95 + by (simp add: add_divide_distrib diff_divide_distrib mult_minus2_left mult_commute)
7.96 + }
7.97 moreover
7.98 {fix c t d s assume H: "(c,t) \<in> set (uset p)" "(d,s) \<in> set (uset p)"
7.99 "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "\<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0" "Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p"
7.100 @@ -2675,7 +2678,9 @@
7.101 hence nn: "isnpoly (C (-2, 1) *\<^sub>p c*\<^sub>p d)" "\<lparr>(C (-2, 1) *\<^sub>p c*\<^sub>p d)\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
7.102 using H(3,4) by (simp_all add: polymul_norm n2)
7.103 from msubst2[OF lp nn, of x bs ] H(3,4,5)
7.104 - have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))" apply (simp add: add_divide_distrib mult_minus2_left) by (simp add: mult_commute)}
7.105 + have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
7.106 + by (simp add: diff_divide_distrib add_divide_distrib mult_minus2_left mult_commute)
7.107 + }
7.108 ultimately show ?thesis by blast
7.109 qed
7.110 from fr_eq2[OF lp, of vs bs x] show ?thesis
8.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy Thu Oct 31 16:54:22 2013 +0100
8.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy Fri Nov 01 18:51:14 2013 +0100
8.3 @@ -419,7 +419,7 @@
8.4
8.5 lemma (in comm_ring_1) poly_add_minus_mult_eq:
8.6 "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
8.7 - by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult distrib_left)
8.8 + by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult algebra_simps)
8.9
8.10 subclass (in idom_char_0) comm_ring_1 ..
8.11
8.12 @@ -445,10 +445,7 @@
8.13 lemma (in comm_ring_1) poly_prime_eq_zero[simp]: "poly [a,1] \<noteq> poly []"
8.14 apply (simp add: fun_eq)
8.15 apply (rule_tac x = "minus one a" in exI)
8.16 - apply (unfold diff_minus)
8.17 - apply (subst add_commute)
8.18 - apply (subst add_assoc)
8.19 - apply simp
8.20 + apply (simp add: add_commute [of a])
8.21 done
8.22
8.23 lemma (in idom) poly_exp_prime_eq_zero: "poly ([a, 1] %^ n) \<noteq> poly []"
8.24 @@ -639,7 +636,7 @@
8.25 have "[- a, 1] %^ n divides mulexp n [- a, 1] q"
8.26 proof (rule dividesI)
8.27 show "poly (mulexp n [- a, 1] q) = poly ([- a, 1] %^ n *** q)"
8.28 - by (induct n) (simp_all add: poly_add poly_cmult poly_mult distrib_left mult_ac)
8.29 + by (induct n) (simp_all add: poly_add poly_cmult poly_mult algebra_simps)
8.30 qed
8.31 moreover have "\<not> [- a, 1] %^ Suc n divides mulexp n [- a, 1] q"
8.32 proof
8.33 @@ -873,7 +870,7 @@
8.34 proof
8.35 assume eq: ?lhs
8.36 hence "\<And>x. poly ((c#cs) +++ -- (d#ds)) x = 0"
8.37 - by (simp only: poly_minus poly_add algebra_simps) simp
8.38 + by (simp only: poly_minus poly_add algebra_simps) (simp add: algebra_simps)
8.39 hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add: fun_eq_iff)
8.40 hence "c = d \<and> list_all (\<lambda>x. x=0) ((cs +++ -- ds))"
8.41 unfolding poly_zero by (simp add: poly_minus_def algebra_simps)
9.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy Thu Oct 31 16:54:22 2013 +0100
9.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy Fri Nov 01 18:51:14 2013 +0100
9.3 @@ -266,12 +266,13 @@
9.4 by (simp add: x y th Nadd_def normNum_def INum_def split_def) }
9.5 moreover {
9.6 assume z: "a * b' + b * a' \<noteq> 0"
9.7 - let ?g = "gcd (a * b' + b * a') (b*b')"
9.8 + let ?g = "gcd (a * b' + b * a') (b * b')"
9.9 have gz: "?g \<noteq> 0" using z by simp
9.10 have ?thesis using aa' bb' z gz
9.11 of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]
9.12 of_int_div[where ?'a = 'a, OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
9.13 - by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib) }
9.14 + by (simp add: x y Nadd_def INum_def normNum_def Let_def) (simp add: field_simps)
9.15 + }
9.16 ultimately have ?thesis using aa' bb'
9.17 by (simp add: x y Nadd_def INum_def normNum_def Let_def) }
9.18 ultimately show ?thesis by blast
10.1 --- a/src/HOL/Decision_Procs/mir_tac.ML Thu Oct 31 16:54:22 2013 +0100
10.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Nov 01 18:51:14 2013 +0100
10.3 @@ -34,7 +34,7 @@
10.4 @{thm "divide_zero"},
10.5 @{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"},
10.6 @{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
10.7 - @{thm "diff_minus"}, @{thm "minus_divide_left"}]
10.8 + @{thm uminus_add_conv_diff [symmetric]}, @{thm "minus_divide_left"}]
10.9 val comp_ths = ths @ comp_arith @ @{thms simp_thms};
10.10
10.11
11.1 --- a/src/HOL/Deriv.thy Thu Oct 31 16:54:22 2013 +0100
11.2 +++ b/src/HOL/Deriv.thy Fri Nov 01 18:51:14 2013 +0100
11.3 @@ -98,7 +98,7 @@
11.4
11.5 lemma FDERIV_diff[simp, FDERIV_intros]:
11.6 "(f has_derivative f') F \<Longrightarrow> (g has_derivative g') F \<Longrightarrow> ((\<lambda>x. f x - g x) has_derivative (\<lambda>x. f' x - g' x)) F"
11.7 - by (simp only: diff_minus FDERIV_add FDERIV_minus)
11.8 + by (simp only: diff_conv_add_uminus FDERIV_add FDERIV_minus)
11.9
11.10 abbreviation
11.11 -- {* Frechet derivative: D is derivative of function f at x within s *}
11.12 @@ -718,13 +718,13 @@
11.13 ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
11.14 apply (rule iffI)
11.15 apply (drule_tac k="- a" in LIM_offset)
11.16 -apply (simp add: diff_minus)
11.17 +apply simp
11.18 apply (drule_tac k="a" in LIM_offset)
11.19 apply (simp add: add_commute)
11.20 done
11.21
11.22 lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) --x --> D"
11.23 - by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
11.24 + by (simp add: deriv_def DERIV_LIM_iff)
11.25
11.26 lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
11.27 DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
11.28 @@ -758,8 +758,7 @@
11.29 let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
11.30 show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
11.31 show "isCont ?g x" using der
11.32 - by (simp add: isCont_iff DERIV_iff diff_minus
11.33 - cong: LIM_equal [rule_format])
11.34 + by (simp add: isCont_iff DERIV_iff cong: LIM_equal [rule_format])
11.35 show "?g x = l" by simp
11.36 qed
11.37 next
11.38 @@ -787,7 +786,7 @@
11.39 proof -
11.40 from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]]
11.41 have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
11.42 - by (simp add: diff_minus)
11.43 + by simp
11.44 then obtain s
11.45 where s: "0 < s"
11.46 and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l"
11.47 @@ -798,8 +797,7 @@
11.48 fix h::real
11.49 assume "0 < h" "h < s"
11.50 with all [of h] show "f x < f (x+h)"
11.51 - proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
11.52 - split add: split_if_asm)
11.53 + proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
11.54 assume "~ (f (x+h) - f x) / h < l" and h: "0 < h"
11.55 with l
11.56 have "0 < (f (x+h) - f x) / h" by arith
11.57 @@ -817,7 +815,7 @@
11.58 proof -
11.59 from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]]
11.60 have "\<exists>s > 0. (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l)"
11.61 - by (simp add: diff_minus)
11.62 + by simp
11.63 then obtain s
11.64 where s: "0 < s"
11.65 and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < -l"
11.66 @@ -828,8 +826,7 @@
11.67 fix h::real
11.68 assume "0 < h" "h < s"
11.69 with all [of "-h"] show "f x < f (x-h)"
11.70 - proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric]
11.71 - split add: split_if_asm)
11.72 + proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
11.73 assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
11.74 with l
11.75 have "0 < (f (x-h) - f x) / h" by arith
11.76 @@ -1131,7 +1128,7 @@
11.77 apply (rule linorder_cases [of a b], auto)
11.78 apply (drule_tac [!] f = f in MVT)
11.79 apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def)
11.80 -apply (auto dest: DERIV_unique simp add: ring_distribs diff_minus)
11.81 +apply (auto dest: DERIV_unique simp add: ring_distribs)
11.82 done
11.83
11.84 lemma DERIV_const_ratio_const2:
12.1 --- a/src/HOL/Divides.thy Thu Oct 31 16:54:22 2013 +0100
12.2 +++ b/src/HOL/Divides.thy Fri Nov 01 18:51:14 2013 +0100
12.3 @@ -439,24 +439,23 @@
12.4
12.5 text {* Subtraction respects modular equivalence. *}
12.6
12.7 -lemma mod_diff_left_eq: "(a - b) mod c = (a mod c - b) mod c"
12.8 - unfolding diff_minus
12.9 - by (intro mod_add_cong mod_minus_cong) simp_all
12.10 -
12.11 -lemma mod_diff_right_eq: "(a - b) mod c = (a - b mod c) mod c"
12.12 - unfolding diff_minus
12.13 - by (intro mod_add_cong mod_minus_cong) simp_all
12.14 -
12.15 -lemma mod_diff_eq: "(a - b) mod c = (a mod c - b mod c) mod c"
12.16 - unfolding diff_minus
12.17 - by (intro mod_add_cong mod_minus_cong) simp_all
12.18 +lemma mod_diff_left_eq:
12.19 + "(a - b) mod c = (a mod c - b) mod c"
12.20 + using mod_add_cong [of a c "a mod c" "- b" "- b"] by simp
12.21 +
12.22 +lemma mod_diff_right_eq:
12.23 + "(a - b) mod c = (a - b mod c) mod c"
12.24 + using mod_add_cong [of a c a "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
12.25 +
12.26 +lemma mod_diff_eq:
12.27 + "(a - b) mod c = (a mod c - b mod c) mod c"
12.28 + using mod_add_cong [of a c "a mod c" "- b" "- (b mod c)"] mod_minus_cong [of "b mod c" c b] by simp
12.29
12.30 lemma mod_diff_cong:
12.31 assumes "a mod c = a' mod c"
12.32 assumes "b mod c = b' mod c"
12.33 shows "(a - b) mod c = (a' - b') mod c"
12.34 - unfolding diff_minus using assms
12.35 - by (intro mod_add_cong mod_minus_cong)
12.36 + using assms mod_add_cong [of a c a' "- b" "- b'"] mod_minus_cong [of b c "b'"] by simp
12.37
12.38 lemma dvd_neg_div: "y dvd x \<Longrightarrow> -x div y = - (x div y)"
12.39 apply (case_tac "y = 0") apply simp
12.40 @@ -502,10 +501,7 @@
12.41
12.42 lemma minus_mod_self1 [simp]:
12.43 "(b - a) mod b = - a mod b"
12.44 -proof -
12.45 - have "b - a = - a + b" by (simp add: diff_minus add.commute)
12.46 - then show ?thesis by simp
12.47 -qed
12.48 + using mod_add_self2 [of "- a" b] by simp
12.49
12.50 end
12.51
12.52 @@ -1749,7 +1745,7 @@
12.53 val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
12.54
12.55 val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
12.56 - (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
12.57 + (@{thm diff_conv_add_uminus} :: @{thms add_0s} @ @{thms add_ac}))
12.58 )
12.59 *}
12.60
13.1 --- a/src/HOL/Fields.thy Thu Oct 31 16:54:22 2013 +0100
13.2 +++ b/src/HOL/Fields.thy Fri Nov 01 18:51:14 2013 +0100
13.3 @@ -156,7 +156,7 @@
13.4 by (simp add: divide_inverse)
13.5
13.6 lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
13.7 - by (simp add: diff_minus add_divide_distrib)
13.8 + using add_divide_distrib [of a "- b" c] by simp
13.9
13.10 lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
13.11 proof -
13.12 @@ -845,7 +845,7 @@
13.13 fix x y :: 'a
13.14 from less_add_one show "\<exists>y. x < y" ..
13.15 from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono)
13.16 - then have "x - 1 < x + 1 - 1" by (simp only: diff_minus [symmetric])
13.17 + then have "x - 1 < x + 1 - 1" by simp
13.18 then have "x - 1 < x" by (simp add: algebra_simps)
13.19 then show "\<exists>y. y < x" ..
13.20 show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
14.1 --- a/src/HOL/Groups.thy Thu Oct 31 16:54:22 2013 +0100
14.2 +++ b/src/HOL/Groups.thy Fri Nov 01 18:51:14 2013 +0100
14.3 @@ -321,9 +321,13 @@
14.4
14.5 class group_add = minus + uminus + monoid_add +
14.6 assumes left_minus [simp]: "- a + a = 0"
14.7 - assumes diff_minus: "a - b = a + (- b)"
14.8 + assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"
14.9 begin
14.10
14.11 +lemma diff_conv_add_uminus:
14.12 + "a - b = a + (- b)"
14.13 + by simp
14.14 +
14.15 lemma minus_unique:
14.16 assumes "a + b = 0" shows "- a = b"
14.17 proof -
14.18 @@ -332,8 +336,6 @@
14.19 finally show ?thesis .
14.20 qed
14.21
14.22 -lemmas equals_zero_I = minus_unique (* legacy name *)
14.23 -
14.24 lemma minus_zero [simp]: "- 0 = 0"
14.25 proof -
14.26 have "0 + 0 = 0" by (rule add_0_right)
14.27 @@ -346,13 +348,17 @@
14.28 thus "- (- a) = a" by (rule minus_unique)
14.29 qed
14.30
14.31 -lemma right_minus [simp]: "a + - a = 0"
14.32 +lemma right_minus: "a + - a = 0"
14.33 proof -
14.34 have "a + - a = - (- a) + - a" by simp
14.35 also have "\<dots> = 0" by (rule left_minus)
14.36 finally show ?thesis .
14.37 qed
14.38
14.39 +lemma diff_self [simp]:
14.40 + "a - a = 0"
14.41 + using right_minus [of a] by simp
14.42 +
14.43 subclass cancel_semigroup_add
14.44 proof
14.45 fix a b c :: 'a
14.46 @@ -367,41 +373,57 @@
14.47 then show "b = c" unfolding add_assoc by simp
14.48 qed
14.49
14.50 -lemma minus_add_cancel: "- a + (a + b) = b"
14.51 -by (simp add: add_assoc [symmetric])
14.52 +lemma minus_add_cancel [simp]:
14.53 + "- a + (a + b) = b"
14.54 + by (simp add: add_assoc [symmetric])
14.55
14.56 -lemma add_minus_cancel: "a + (- a + b) = b"
14.57 -by (simp add: add_assoc [symmetric])
14.58 +lemma add_minus_cancel [simp]:
14.59 + "a + (- a + b) = b"
14.60 + by (simp add: add_assoc [symmetric])
14.61
14.62 -lemma minus_add: "- (a + b) = - b + - a"
14.63 +lemma diff_add_cancel [simp]:
14.64 + "a - b + b = a"
14.65 + by (simp only: diff_conv_add_uminus add_assoc) simp
14.66 +
14.67 +lemma add_diff_cancel [simp]:
14.68 + "a + b - b = a"
14.69 + by (simp only: diff_conv_add_uminus add_assoc) simp
14.70 +
14.71 +lemma minus_add:
14.72 + "- (a + b) = - b + - a"
14.73 proof -
14.74 have "(a + b) + (- b + - a) = 0"
14.75 - by (simp add: add_assoc add_minus_cancel)
14.76 - thus "- (a + b) = - b + - a"
14.77 + by (simp only: add_assoc add_minus_cancel) simp
14.78 + then show "- (a + b) = - b + - a"
14.79 by (rule minus_unique)
14.80 qed
14.81
14.82 -lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
14.83 +lemma right_minus_eq [simp]:
14.84 + "a - b = 0 \<longleftrightarrow> a = b"
14.85 proof
14.86 assume "a - b = 0"
14.87 - have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
14.88 + have "a = (a - b) + b" by (simp add: add_assoc)
14.89 also have "\<dots> = b" using `a - b = 0` by simp
14.90 finally show "a = b" .
14.91 next
14.92 - assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
14.93 + assume "a = b" thus "a - b = 0" by simp
14.94 qed
14.95
14.96 -lemma diff_self [simp]: "a - a = 0"
14.97 -by (simp add: diff_minus)
14.98 +lemma eq_iff_diff_eq_0:
14.99 + "a = b \<longleftrightarrow> a - b = 0"
14.100 + by (fact right_minus_eq [symmetric])
14.101
14.102 -lemma diff_0 [simp]: "0 - a = - a"
14.103 -by (simp add: diff_minus)
14.104 +lemma diff_0 [simp]:
14.105 + "0 - a = - a"
14.106 + by (simp only: diff_conv_add_uminus add_0_left)
14.107
14.108 -lemma diff_0_right [simp]: "a - 0 = a"
14.109 -by (simp add: diff_minus)
14.110 +lemma diff_0_right [simp]:
14.111 + "a - 0 = a"
14.112 + by (simp only: diff_conv_add_uminus minus_zero add_0_right)
14.113
14.114 -lemma diff_minus_eq_add [simp]: "a - - b = a + b"
14.115 -by (simp add: diff_minus)
14.116 +lemma diff_minus_eq_add [simp]:
14.117 + "a - - b = a + b"
14.118 + by (simp only: diff_conv_add_uminus minus_minus)
14.119
14.120 lemma neg_equal_iff_equal [simp]:
14.121 "- a = - b \<longleftrightarrow> a = b"
14.122 @@ -416,11 +438,11 @@
14.123
14.124 lemma neg_equal_0_iff_equal [simp]:
14.125 "- a = 0 \<longleftrightarrow> a = 0"
14.126 -by (subst neg_equal_iff_equal [symmetric], simp)
14.127 + by (subst neg_equal_iff_equal [symmetric]) simp
14.128
14.129 lemma neg_0_equal_iff_equal [simp]:
14.130 "0 = - a \<longleftrightarrow> 0 = a"
14.131 -by (subst neg_equal_iff_equal [symmetric], simp)
14.132 + by (subst neg_equal_iff_equal [symmetric]) simp
14.133
14.134 text{*The next two equations can make the simplifier loop!*}
14.135
14.136 @@ -438,15 +460,8 @@
14.137 thus ?thesis by (simp add: eq_commute)
14.138 qed
14.139
14.140 -lemma diff_add_cancel: "a - b + b = a"
14.141 -by (simp add: diff_minus add_assoc)
14.142 -
14.143 -lemma add_diff_cancel: "a + b - b = a"
14.144 -by (simp add: diff_minus add_assoc)
14.145 -
14.146 -declare diff_minus[symmetric, algebra_simps, field_simps]
14.147 -
14.148 -lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
14.149 +lemma eq_neg_iff_add_eq_0:
14.150 + "a = - b \<longleftrightarrow> a + b = 0"
14.151 proof
14.152 assume "a = - b" then show "a + b = 0" by simp
14.153 next
14.154 @@ -456,72 +471,88 @@
14.155 ultimately show "a = - b" by simp
14.156 qed
14.157
14.158 -lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y = - x"
14.159 - unfolding eq_neg_iff_add_eq_0 [symmetric]
14.160 - by (rule equation_minus_iff)
14.161 +lemma add_eq_0_iff2:
14.162 + "a + b = 0 \<longleftrightarrow> a = - b"
14.163 + by (fact eq_neg_iff_add_eq_0 [symmetric])
14.164
14.165 -lemma minus_diff_eq [simp]: "- (a - b) = b - a"
14.166 - by (simp add: diff_minus minus_add)
14.167 +lemma neg_eq_iff_add_eq_0:
14.168 + "- a = b \<longleftrightarrow> a + b = 0"
14.169 + by (auto simp add: add_eq_0_iff2)
14.170
14.171 -lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
14.172 - by (simp add: diff_minus add_assoc)
14.173 +lemma add_eq_0_iff:
14.174 + "a + b = 0 \<longleftrightarrow> b = - a"
14.175 + by (auto simp add: neg_eq_iff_add_eq_0 [symmetric])
14.176
14.177 -lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
14.178 - by (auto simp add: diff_minus add_assoc)
14.179 +lemma minus_diff_eq [simp]:
14.180 + "- (a - b) = b - a"
14.181 + by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add_assoc minus_add_cancel) simp
14.182
14.183 -lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
14.184 - by (auto simp add: diff_minus add_assoc)
14.185 +lemma add_diff_eq [algebra_simps, field_simps]:
14.186 + "a + (b - c) = (a + b) - c"
14.187 + by (simp only: diff_conv_add_uminus add_assoc)
14.188
14.189 -lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
14.190 - by (simp add: diff_minus minus_add add_assoc)
14.191 +lemma diff_add_eq_diff_diff_swap:
14.192 + "a - (b + c) = a - c - b"
14.193 + by (simp only: diff_conv_add_uminus add_assoc minus_add)
14.194
14.195 -lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
14.196 - by (fact right_minus_eq [symmetric])
14.197 +lemma diff_eq_eq [algebra_simps, field_simps]:
14.198 + "a - b = c \<longleftrightarrow> a = c + b"
14.199 + by auto
14.200 +
14.201 +lemma eq_diff_eq [algebra_simps, field_simps]:
14.202 + "a = c - b \<longleftrightarrow> a + b = c"
14.203 + by auto
14.204 +
14.205 +lemma diff_diff_eq2 [algebra_simps, field_simps]:
14.206 + "a - (b - c) = (a + c) - b"
14.207 + by (simp only: diff_conv_add_uminus add_assoc) simp
14.208
14.209 lemma diff_eq_diff_eq:
14.210 "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
14.211 - by (simp add: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
14.212 + by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
14.213
14.214 end
14.215
14.216 class ab_group_add = minus + uminus + comm_monoid_add +
14.217 assumes ab_left_minus: "- a + a = 0"
14.218 - assumes ab_diff_minus: "a - b = a + (- b)"
14.219 + assumes ab_add_uminus_conv_diff: "a - b = a + (- b)"
14.220 begin
14.221
14.222 subclass group_add
14.223 - proof qed (simp_all add: ab_left_minus ab_diff_minus)
14.224 + proof qed (simp_all add: ab_left_minus ab_add_uminus_conv_diff)
14.225
14.226 subclass cancel_comm_monoid_add
14.227 proof
14.228 fix a b c :: 'a
14.229 assume "a + b = a + c"
14.230 then have "- a + a + b = - a + a + c"
14.231 - unfolding add_assoc by simp
14.232 + by (simp only: add_assoc)
14.233 then show "b = c" by simp
14.234 qed
14.235
14.236 -lemma uminus_add_conv_diff[algebra_simps, field_simps]:
14.237 +lemma uminus_add_conv_diff [simp]:
14.238 "- a + b = b - a"
14.239 -by (simp add:diff_minus add_commute)
14.240 + by (simp add: add_commute)
14.241
14.242 lemma minus_add_distrib [simp]:
14.243 "- (a + b) = - a + - b"
14.244 -by (rule minus_unique) (simp add: add_ac)
14.245 + by (simp add: algebra_simps)
14.246
14.247 -lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
14.248 -by (simp add: diff_minus add_ac)
14.249 +lemma diff_add_eq [algebra_simps, field_simps]:
14.250 + "(a - b) + c = (a + c) - b"
14.251 + by (simp add: algebra_simps)
14.252
14.253 -lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
14.254 -by (simp add: diff_minus add_ac)
14.255 +lemma diff_diff_eq [algebra_simps, field_simps]:
14.256 + "(a - b) - c = a - (b + c)"
14.257 + by (simp add: algebra_simps)
14.258
14.259 -(* FIXME: duplicates right_minus_eq from class group_add *)
14.260 -(* but only this one is declared as a simp rule. *)
14.261 -lemma diff_eq_0_iff_eq [simp]: "a - b = 0 \<longleftrightarrow> a = b"
14.262 - by (rule right_minus_eq)
14.263 +lemma diff_add_eq_diff_diff:
14.264 + "a - (b + c) = a - b - c"
14.265 + using diff_add_eq_diff_diff_swap [of a c b] by (simp add: add.commute)
14.266
14.267 -lemma add_diff_cancel_left: "(c + a) - (c + b) = a - b"
14.268 - by (simp add: diff_minus add_ac)
14.269 +lemma add_diff_cancel_left [simp]:
14.270 + "(c + a) - (c + b) = a - b"
14.271 + by (simp add: algebra_simps)
14.272
14.273 end
14.274
14.275 @@ -622,19 +653,19 @@
14.276
14.277 lemma add_less_cancel_left [simp]:
14.278 "c + a < c + b \<longleftrightarrow> a < b"
14.279 -by (blast intro: add_less_imp_less_left add_strict_left_mono)
14.280 + by (blast intro: add_less_imp_less_left add_strict_left_mono)
14.281
14.282 lemma add_less_cancel_right [simp]:
14.283 "a + c < b + c \<longleftrightarrow> a < b"
14.284 -by (blast intro: add_less_imp_less_right add_strict_right_mono)
14.285 + by (blast intro: add_less_imp_less_right add_strict_right_mono)
14.286
14.287 lemma add_le_cancel_left [simp]:
14.288 "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
14.289 -by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)
14.290 + by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)
14.291
14.292 lemma add_le_cancel_right [simp]:
14.293 "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
14.294 -by (simp add: add_commute [of a c] add_commute [of b c])
14.295 + by (simp add: add_commute [of a c] add_commute [of b c])
14.296
14.297 lemma add_le_imp_le_right:
14.298 "a + c \<le> b + c \<Longrightarrow> a \<le> b"
14.299 @@ -806,6 +837,22 @@
14.300 then show "x + y = 0" by simp
14.301 qed
14.302
14.303 +lemma add_increasing:
14.304 + "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
14.305 + by (insert add_mono [of 0 a b c], simp)
14.306 +
14.307 +lemma add_increasing2:
14.308 + "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
14.309 + by (simp add: add_increasing add_commute [of a])
14.310 +
14.311 +lemma add_strict_increasing:
14.312 + "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
14.313 + by (insert add_less_le_mono [of 0 a b c], simp)
14.314 +
14.315 +lemma add_strict_increasing2:
14.316 + "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
14.317 + by (insert add_le_less_mono [of 0 a b c], simp)
14.318 +
14.319 end
14.320
14.321 class ordered_ab_group_add =
14.322 @@ -825,21 +872,53 @@
14.323
14.324 subclass ordered_comm_monoid_add ..
14.325
14.326 +lemma add_less_same_cancel1 [simp]:
14.327 + "b + a < b \<longleftrightarrow> a < 0"
14.328 + using add_less_cancel_left [of _ _ 0] by simp
14.329 +
14.330 +lemma add_less_same_cancel2 [simp]:
14.331 + "a + b < b \<longleftrightarrow> a < 0"
14.332 + using add_less_cancel_right [of _ _ 0] by simp
14.333 +
14.334 +lemma less_add_same_cancel1 [simp]:
14.335 + "a < a + b \<longleftrightarrow> 0 < b"
14.336 + using add_less_cancel_left [of _ 0] by simp
14.337 +
14.338 +lemma less_add_same_cancel2 [simp]:
14.339 + "a < b + a \<longleftrightarrow> 0 < b"
14.340 + using add_less_cancel_right [of 0] by simp
14.341 +
14.342 +lemma add_le_same_cancel1 [simp]:
14.343 + "b + a \<le> b \<longleftrightarrow> a \<le> 0"
14.344 + using add_le_cancel_left [of _ _ 0] by simp
14.345 +
14.346 +lemma add_le_same_cancel2 [simp]:
14.347 + "a + b \<le> b \<longleftrightarrow> a \<le> 0"
14.348 + using add_le_cancel_right [of _ _ 0] by simp
14.349 +
14.350 +lemma le_add_same_cancel1 [simp]:
14.351 + "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
14.352 + using add_le_cancel_left [of _ 0] by simp
14.353 +
14.354 +lemma le_add_same_cancel2 [simp]:
14.355 + "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
14.356 + using add_le_cancel_right [of 0] by simp
14.357 +
14.358 lemma max_diff_distrib_left:
14.359 shows "max x y - z = max (x - z) (y - z)"
14.360 -by (simp add: diff_minus, rule max_add_distrib_left)
14.361 + using max_add_distrib_left [of x y "- z"] by simp
14.362
14.363 lemma min_diff_distrib_left:
14.364 shows "min x y - z = min (x - z) (y - z)"
14.365 -by (simp add: diff_minus, rule min_add_distrib_left)
14.366 + using min_add_distrib_left [of x y "- z"] by simp
14.367
14.368 lemma le_imp_neg_le:
14.369 assumes "a \<le> b" shows "-b \<le> -a"
14.370 proof -
14.371 have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono)
14.372 - hence "0 \<le> -a+b" by simp
14.373 - hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
14.374 - thus ?thesis by (simp add: add_assoc)
14.375 + then have "0 \<le> -a+b" by simp
14.376 + then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
14.377 + then show ?thesis by (simp add: algebra_simps)
14.378 qed
14.379
14.380 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
14.381 @@ -899,30 +978,32 @@
14.382 lemma diff_less_0_iff_less [simp]:
14.383 "a - b < 0 \<longleftrightarrow> a < b"
14.384 proof -
14.385 - have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
14.386 + have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by simp
14.387 also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
14.388 finally show ?thesis .
14.389 qed
14.390
14.391 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
14.392
14.393 -lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
14.394 +lemma diff_less_eq [algebra_simps, field_simps]:
14.395 + "a - b < c \<longleftrightarrow> a < c + b"
14.396 apply (subst less_iff_diff_less_0 [of a])
14.397 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
14.398 -apply (simp add: diff_minus add_ac)
14.399 +apply (simp add: algebra_simps)
14.400 done
14.401
14.402 -lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
14.403 +lemma less_diff_eq[algebra_simps, field_simps]:
14.404 + "a < c - b \<longleftrightarrow> a + b < c"
14.405 apply (subst less_iff_diff_less_0 [of "a + b"])
14.406 apply (subst less_iff_diff_less_0 [of a])
14.407 -apply (simp add: diff_minus add_ac)
14.408 +apply (simp add: algebra_simps)
14.409 done
14.410
14.411 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
14.412 -by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
14.413 +by (auto simp add: le_less diff_less_eq )
14.414
14.415 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
14.416 -by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
14.417 +by (auto simp add: le_less less_diff_eq)
14.418
14.419 lemma diff_le_0_iff_le [simp]:
14.420 "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
14.421 @@ -1118,21 +1199,11 @@
14.422
14.423 lemma le_minus_self_iff:
14.424 "a \<le> - a \<longleftrightarrow> a \<le> 0"
14.425 -proof -
14.426 - from add_le_cancel_left [of "- a" "a + a" 0]
14.427 - have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"
14.428 - by (simp add: add_assoc [symmetric])
14.429 - thus ?thesis by simp
14.430 -qed
14.431 + by (fact less_eq_neg_nonpos)
14.432
14.433 lemma minus_le_self_iff:
14.434 "- a \<le> a \<longleftrightarrow> 0 \<le> a"
14.435 -proof -
14.436 - from add_le_cancel_left [of "- a" 0 "a + a"]
14.437 - have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
14.438 - by (simp add: add_assoc [symmetric])
14.439 - thus ?thesis by simp
14.440 -qed
14.441 + by (fact neg_less_eq_nonneg)
14.442
14.443 lemma minus_max_eq_min:
14.444 "- max x y = min (-x) (-y)"
14.445 @@ -1144,27 +1215,6 @@
14.446
14.447 end
14.448
14.449 -context ordered_comm_monoid_add
14.450 -begin
14.451 -
14.452 -lemma add_increasing:
14.453 - "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
14.454 - by (insert add_mono [of 0 a b c], simp)
14.455 -
14.456 -lemma add_increasing2:
14.457 - "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
14.458 - by (simp add: add_increasing add_commute [of a])
14.459 -
14.460 -lemma add_strict_increasing:
14.461 - "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
14.462 - by (insert add_less_le_mono [of 0 a b c], simp)
14.463 -
14.464 -lemma add_strict_increasing2:
14.465 - "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
14.466 - by (insert add_le_less_mono [of 0 a b c], simp)
14.467 -
14.468 -end
14.469 -
14.470 class abs =
14.471 fixes abs :: "'a \<Rightarrow> 'a"
14.472 begin
14.473 @@ -1299,7 +1349,7 @@
14.474 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
14.475 proof -
14.476 have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
14.477 - by (simp add: algebra_simps add_diff_cancel)
14.478 + by (simp add: algebra_simps)
14.479 then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
14.480 by (simp add: abs_triangle_ineq)
14.481 then show ?thesis
14.482 @@ -1314,14 +1364,14 @@
14.483
14.484 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
14.485 proof -
14.486 - have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
14.487 + have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (simp add: algebra_simps)
14.488 also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
14.489 finally show ?thesis by simp
14.490 qed
14.491
14.492 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
14.493 proof -
14.494 - have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
14.495 + have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: algebra_simps)
14.496 also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
14.497 finally show ?thesis .
14.498 qed
14.499 @@ -1362,10 +1412,5 @@
14.500 code_identifier
14.501 code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
14.502
14.503 -
14.504 -text {* Legacy *}
14.505 -
14.506 -lemmas diff_def = diff_minus
14.507 -
14.508 end
14.509
15.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy Thu Oct 31 16:54:22 2013 +0100
15.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy Fri Nov 01 18:51:14 2013 +0100
15.3 @@ -112,7 +112,7 @@
15.4 proof -
15.5 assume x: "x \<in> V"
15.6 have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
15.7 - by (simp add: diff_minus)
15.8 + by simp
15.9 also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
15.10 by (rule add_mult_distrib2)
15.11 also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
16.1 --- a/src/HOL/Int.thy Thu Oct 31 16:54:22 2013 +0100
16.2 +++ b/src/HOL/Int.thy Fri Nov 01 18:51:14 2013 +0100
16.3 @@ -220,7 +220,7 @@
16.4 by (transfer fixing: uminus) clarsimp
16.5
16.6 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
16.7 -by (simp add: diff_minus Groups.diff_minus)
16.8 + using of_int_add [of w "- z"] by simp
16.9
16.10 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
16.11 by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
16.12 @@ -749,7 +749,7 @@
16.13
16.14 lemmas int_arith_rules =
16.15 neg_le_iff_le numeral_One
16.16 - minus_zero diff_minus left_minus right_minus
16.17 + minus_zero left_minus right_minus
16.18 mult_zero_left mult_zero_right mult_1_left mult_1_right
16.19 mult_minus_left mult_minus_right
16.20 minus_add_distrib minus_minus mult_assoc
16.21 @@ -793,7 +793,6 @@
16.22 subsection{*The functions @{term nat} and @{term int}*}
16.23
16.24 text{*Simplify the term @{term "w + - z"}*}
16.25 -lemmas diff_int_def_symmetric = diff_def [where 'a=int, symmetric, simp]
16.26
16.27 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
16.28 apply (insert zless_nat_conj [of 1 z])
16.29 @@ -1510,10 +1509,13 @@
16.30 "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
16.31 "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
16.32 "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
16.33 - unfolding sub_def dup_def numeral.simps Pos_def Neg_def
16.34 - neg_numeral_def numeral_BitM
16.35 - by (simp_all only: algebra_simps)
16.36 -
16.37 + apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def
16.38 + neg_numeral_def numeral_BitM)
16.39 + apply (simp_all only: algebra_simps minus_diff_eq)
16.40 + apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
16.41 + apply (simp_all only: minus_add add.assoc left_minus)
16.42 + apply (simp_all only: algebra_simps right_minus)
16.43 + done
16.44
16.45 text {* Implementations *}
16.46
17.1 --- a/src/HOL/Library/BigO.thy Thu Oct 31 16:54:22 2013 +0100
17.2 +++ b/src/HOL/Library/BigO.thy Fri Nov 01 18:51:14 2013 +0100
17.3 @@ -215,7 +215,7 @@
17.4 f : lb +o O(g)"
17.5 apply (rule set_minus_imp_plus)
17.6 apply (rule bigo_bounded)
17.7 - apply (auto simp add: diff_minus fun_Compl_def func_plus)
17.8 + apply (auto simp add: fun_Compl_def func_plus)
17.9 apply (drule_tac x = x in spec)+
17.10 apply force
17.11 apply (drule_tac x = x in spec)+
17.12 @@ -390,7 +390,7 @@
17.13 apply (rule set_minus_imp_plus)
17.14 apply (drule set_plus_imp_minus)
17.15 apply (drule bigo_minus)
17.16 - apply (simp add: diff_minus)
17.17 + apply simp
17.18 done
17.19
17.20 lemma bigo_minus3: "O(-f) = O(f)"
17.21 @@ -446,7 +446,7 @@
17.22 apply (rule bigo_minus)
17.23 apply (subst set_minus_plus)
17.24 apply assumption
17.25 - apply (simp add: diff_minus add_ac)
17.26 + apply (simp add: add_ac)
17.27 done
17.28
17.29 lemma bigo_add_commute: "(f : g +o O(h)) = (g : f +o O(h))"
17.30 @@ -545,10 +545,9 @@
17.31
17.32 lemma bigo_compose2: "f =o g +o O(h) ==> (%x. f(k x)) =o (%x. g(k x)) +o
17.33 O(%x. h(k x))"
17.34 - apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def
17.35 - func_plus)
17.36 - apply (erule bigo_compose1)
17.37 -done
17.38 + apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)
17.39 + apply (drule bigo_compose1) apply (simp add: fun_diff_def)
17.40 + done
17.41
17.42
17.43 subsection {* Setsum *}
17.44 @@ -779,7 +778,7 @@
17.45 apply (subst abs_of_nonneg)
17.46 apply (drule_tac x = x in spec) back
17.47 apply (simp add: algebra_simps)
17.48 - apply (subst diff_minus)+
17.49 + apply (subst diff_conv_add_uminus)+
17.50 apply (rule add_right_mono)
17.51 apply (erule spec)
17.52 apply (rule order_trans)
17.53 @@ -803,7 +802,7 @@
17.54 apply (subst abs_of_nonneg)
17.55 apply (drule_tac x = x in spec) back
17.56 apply (simp add: algebra_simps)
17.57 - apply (subst diff_minus)+
17.58 + apply (subst diff_conv_add_uminus)+
17.59 apply (rule add_left_mono)
17.60 apply (rule le_imp_neg_le)
17.61 apply (erule spec)
18.1 --- a/src/HOL/Library/Convex.thy Thu Oct 31 16:54:22 2013 +0100
18.2 +++ b/src/HOL/Library/Convex.thy Fri Nov 01 18:51:14 2013 +0100
18.3 @@ -362,7 +362,7 @@
18.4 shows "convex {x - y| x y. x \<in> s \<and> y \<in> t}"
18.5 proof -
18.6 have "{x - y| x y. x \<in> s \<and> y \<in> t} = {x + y |x y. x \<in> s \<and> y \<in> uminus ` t}"
18.7 - unfolding diff_def by auto
18.8 + by (auto simp add: diff_conv_add_uminus simp del: add_uminus_conv_diff)
18.9 then show ?thesis
18.10 using convex_sums[OF assms(1) convex_negations[OF assms(2)]] by auto
18.11 qed
19.1 --- a/src/HOL/Library/Float.thy Thu Oct 31 16:54:22 2013 +0100
19.2 +++ b/src/HOL/Library/Float.thy Fri Nov 01 18:51:14 2013 +0100
19.3 @@ -88,7 +88,7 @@
19.4 done
19.5
19.6 lemma minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x - y \<in> float"
19.7 - unfolding ab_diff_minus by (intro uminus_float plus_float)
19.8 + using plus_float [of x "- y"] by simp
19.9
19.10 lemma abs_float[simp]: "x \<in> float \<Longrightarrow> abs x \<in> float"
19.11 by (cases x rule: linorder_cases[of 0]) auto
19.12 @@ -960,7 +960,7 @@
19.13 also have "... < (1 / 2) * 2 powr real (rat_precision n (int x) (int y))"
19.14 apply (rule mult_strict_right_mono) by (insert assms) auto
19.15 also have "\<dots> = 2 powr real (rat_precision n (int x) (int y) - 1)"
19.16 - by (simp add: powr_add diff_def powr_neg_numeral)
19.17 + using powr_add [of 2 _ "- 1", simplified add_uminus_conv_diff] by (simp add: powr_neg_numeral)
19.18 also have "\<dots> = 2 ^ nat (rat_precision n (int x) (int y) - 1)"
19.19 using rat_precision_pos[of x y n] assms by (simp add: powr_realpow[symmetric])
19.20 also have "\<dots> \<le> 2 ^ nat (rat_precision n (int x) (int y)) - 1"
20.1 --- a/src/HOL/Library/Formal_Power_Series.thy Thu Oct 31 16:54:22 2013 +0100
20.2 +++ b/src/HOL/Library/Formal_Power_Series.thy Fri Nov 01 18:51:14 2013 +0100
20.3 @@ -231,7 +231,7 @@
20.4 proof
20.5 fix a b :: "'a fps"
20.6 show "- a + a = 0" by (simp add: fps_ext)
20.7 - show "a - b = a + - b" by (simp add: fps_ext diff_minus)
20.8 + show "a + - b = a - b" by (simp add: fps_ext)
20.9 qed
20.10
20.11 instance fps :: (ab_group_add) ab_group_add
20.12 @@ -348,10 +348,10 @@
20.13 instance fps :: (ring) ring ..
20.14
20.15 instance fps :: (ring_1) ring_1
20.16 - by (intro_classes, auto simp add: diff_minus distrib_right)
20.17 + by (intro_classes, auto simp add: distrib_right)
20.18
20.19 instance fps :: (comm_ring_1) comm_ring_1
20.20 - by (intro_classes, auto simp add: diff_minus distrib_right)
20.21 + by (intro_classes, auto simp add: distrib_right)
20.22
20.23 instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors
20.24 proof
20.25 @@ -888,7 +888,7 @@
20.26 using fps_deriv_linear[of 1 f 1 g] by simp
20.27
20.28 lemma fps_deriv_sub[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) - g) = fps_deriv f - fps_deriv g"
20.29 - unfolding diff_minus by simp
20.30 + using fps_deriv_add [of f "- g"] by simp
20.31
20.32 lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
20.33 by (simp add: fps_ext fps_deriv_def fps_const_def)
20.34 @@ -978,7 +978,7 @@
20.35
20.36 lemma fps_nth_deriv_sub[simp]:
20.37 "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
20.38 - unfolding diff_minus fps_nth_deriv_add by simp
20.39 + using fps_nth_deriv_add [of n f "- g"] by simp
20.40
20.41 lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0"
20.42 by (induct n) simp_all
20.43 @@ -2634,7 +2634,7 @@
20.44 by (simp add: fps_eq_iff fps_compose_nth field_simps setsum_negf[symmetric])
20.45
20.46 lemma fps_compose_sub_distrib: "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
20.47 - unfolding diff_minus fps_compose_uminus fps_compose_add_distrib ..
20.48 + using fps_compose_add_distrib [of a "- b" c] by (simp add: fps_compose_uminus)
20.49
20.50 lemma X_fps_compose: "X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
20.51 by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta)
21.1 --- a/src/HOL/Library/Fraction_Field.thy Thu Oct 31 16:54:22 2013 +0100
21.2 +++ b/src/HOL/Library/Fraction_Field.thy Fri Nov 01 18:51:14 2013 +0100
21.3 @@ -132,7 +132,7 @@
21.4 lemma diff_fract [simp]:
21.5 assumes "b \<noteq> 0" and "d \<noteq> 0"
21.6 shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
21.7 - using assms by (simp add: diff_fract_def diff_minus)
21.8 + using assms by (simp add: diff_fract_def)
21.9
21.10 definition mult_fract_def:
21.11 "q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
22.1 --- a/src/HOL/Library/Function_Algebras.thy Thu Oct 31 16:54:22 2013 +0100
22.2 +++ b/src/HOL/Library/Function_Algebras.thy Fri Nov 01 18:51:14 2013 +0100
22.3 @@ -83,10 +83,10 @@
22.4
22.5 instance "fun" :: (type, group_add) group_add
22.6 by default
22.7 - (simp_all add: fun_eq_iff diff_minus)
22.8 + (simp_all add: fun_eq_iff)
22.9
22.10 instance "fun" :: (type, ab_group_add) ab_group_add
22.11 - by default (simp_all add: diff_minus)
22.12 + by default simp_all
22.13
22.14
22.15 text {* Multiplicative structures *}
23.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Thu Oct 31 16:54:22 2013 +0100
23.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Fri Nov 01 18:51:14 2013 +0100
23.3 @@ -224,12 +224,12 @@
23.4 from unimodular_reduce_norm[OF th0] o
23.5 have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
23.6 apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
23.7 - apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_minus)
23.8 + apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp del: minus_one add: minus_one [symmetric])
23.9 apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
23.10 apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
23.11 apply (rule_tac x="- ii" in exI, simp add: m power_mult)
23.12 - apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_minus)
23.13 - apply (rule_tac x="ii" in exI, simp add: m power_mult diff_minus)
23.14 + apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult)
23.15 + apply (rule_tac x="ii" in exI, simp add: m power_mult)
23.16 done
23.17 then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
23.18 let ?w = "v / complex_of_real (root n (cmod b))"
23.19 @@ -954,7 +954,7 @@
23.20
23.21 lemma mpoly_sub_conv:
23.22 "poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
23.23 - by (simp add: diff_minus)
23.24 + by simp
23.25
23.26 lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
23.27
24.1 --- a/src/HOL/Library/Inner_Product.thy Thu Oct 31 16:54:22 2013 +0100
24.2 +++ b/src/HOL/Library/Inner_Product.thy Fri Nov 01 18:51:14 2013 +0100
24.3 @@ -41,7 +41,7 @@
24.4 using inner_add_left [of x "- x" y] by simp
24.5
24.6 lemma inner_diff_left: "inner (x - y) z = inner x z - inner y z"
24.7 - by (simp add: diff_minus inner_add_left)
24.8 + using inner_add_left [of x "- y" z] by simp
24.9
24.10 lemma inner_setsum_left: "inner (\<Sum>x\<in>A. f x) y = (\<Sum>x\<in>A. inner (f x) y)"
24.11 by (cases "finite A", induct set: finite, simp_all add: inner_add_left)
25.1 --- a/src/HOL/Library/Lattice_Algebras.thy Thu Oct 31 16:54:22 2013 +0100
25.2 +++ b/src/HOL/Library/Lattice_Algebras.thy Fri Nov 01 18:51:14 2013 +0100
25.3 @@ -13,9 +13,7 @@
25.4 apply (rule antisym)
25.5 apply (simp_all add: le_infI)
25.6 apply (rule add_le_imp_le_left [of "uminus a"])
25.7 - apply (simp only: add_assoc [symmetric], simp)
25.8 - apply rule
25.9 - apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
25.10 + apply (simp only: add_assoc [symmetric], simp add: diff_le_eq add.commute)
25.11 done
25.12
25.13 lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)"
25.14 @@ -33,11 +31,10 @@
25.15 lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)"
25.16 apply (rule antisym)
25.17 apply (rule add_le_imp_le_left [of "uminus a"])
25.18 - apply (simp only: add_assoc[symmetric], simp)
25.19 - apply rule
25.20 + apply (simp only: add_assoc [symmetric], simp)
25.21 + apply (simp add: le_diff_eq add.commute)
25.22 + apply (rule le_supI)
25.23 apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
25.24 - apply (rule le_supI)
25.25 - apply (simp_all)
25.26 done
25.27
25.28 lemma add_sup_distrib_right: "sup a b + c = sup (a+c) (b+c)"
25.29 @@ -87,9 +84,15 @@
25.30 lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)"
25.31 by (simp add: inf_eq_neg_sup)
25.32
25.33 +lemma diff_inf_eq_sup: "a - inf b c = a + sup (- b) (- c)"
25.34 + using neg_inf_eq_sup [of b c, symmetric] by simp
25.35 +
25.36 lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)"
25.37 by (simp add: sup_eq_neg_inf)
25.38
25.39 +lemma diff_sup_eq_inf: "a - sup b c = a + inf (- b) (- c)"
25.40 + using neg_sup_eq_inf [of b c, symmetric] by simp
25.41 +
25.42 lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
25.43 proof -
25.44 have "0 = - inf 0 (a-b) + inf (a-b) 0"
25.45 @@ -97,8 +100,8 @@
25.46 hence "0 = sup 0 (b-a) + inf (a-b) 0"
25.47 by (simp add: inf_eq_neg_sup)
25.48 hence "0 = (-a + sup a b) + (inf a b + (-b))"
25.49 - by (simp add: add_sup_distrib_left add_inf_distrib_right) (simp add: algebra_simps)
25.50 - thus ?thesis by (simp add: algebra_simps)
25.51 + by (simp only: add_sup_distrib_left add_inf_distrib_right) simp
25.52 + then show ?thesis by (simp add: algebra_simps)
25.53 qed
25.54
25.55
25.56 @@ -251,7 +254,7 @@
25.57 apply assumption
25.58 apply (rule notI)
25.59 unfolding double_zero [symmetric, of a]
25.60 - apply simp
25.61 + apply blast
25.62 done
25.63 qed
25.64
25.65 @@ -259,7 +262,8 @@
25.66 "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
25.67 proof -
25.68 have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
25.69 - moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by simp
25.70 + moreover have "\<dots> \<longleftrightarrow> a \<le> 0"
25.71 + by (simp only: minus_add_distrib zero_le_double_add_iff_zero_le_single_add) simp
25.72 ultimately show ?thesis by blast
25.73 qed
25.74
25.75 @@ -267,11 +271,12 @@
25.76 "a + a < 0 \<longleftrightarrow> a < 0"
25.77 proof -
25.78 have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
25.79 - moreover have "\<dots> \<longleftrightarrow> a < 0" by simp
25.80 + moreover have "\<dots> \<longleftrightarrow> a < 0"
25.81 + by (simp only: minus_add_distrib zero_less_double_add_iff_zero_less_single_add) simp
25.82 ultimately show ?thesis by blast
25.83 qed
25.84
25.85 -declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp]
25.86 +declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp] diff_inf_eq_sup [simp] diff_sup_eq_inf [simp]
25.87
25.88 lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
25.89 proof -
25.90 @@ -326,7 +331,7 @@
25.91 then have "0 \<le> sup a (- a)" unfolding abs_lattice .
25.92 then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
25.93 then show ?thesis
25.94 - by (simp add: add_sup_inf_distribs sup_aci pprt_def nprt_def diff_minus abs_lattice)
25.95 + by (simp add: add_sup_inf_distribs ac_simps pprt_def nprt_def abs_lattice)
25.96 qed
25.97
25.98 subclass ordered_ab_group_add_abs
25.99 @@ -355,16 +360,17 @@
25.100 show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
25.101 proof -
25.102 have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
25.103 - by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
25.104 + by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps)
25.105 have a: "a + b <= sup ?m ?n" by simp
25.106 have b: "- a - b <= ?n" by simp
25.107 have c: "?n <= sup ?m ?n" by simp
25.108 from b c have d: "-a-b <= sup ?m ?n" by (rule order_trans)
25.109 - have e:"-a-b = -(a+b)" by (simp add: diff_minus)
25.110 + have e:"-a-b = -(a+b)" by simp
25.111 from a d e have "abs(a+b) <= sup ?m ?n"
25.112 apply -
25.113 apply (drule abs_leI)
25.114 - apply auto
25.115 + apply (simp_all only: algebra_simps ac_simps minus_add)
25.116 + apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
25.117 done
25.118 with g[symmetric] show ?thesis by simp
25.119 qed
25.120 @@ -421,14 +427,12 @@
25.121 }
25.122 note b = this[OF refl[of a] refl[of b]]
25.123 have xy: "- ?x <= ?y"
25.124 - apply (simp)
25.125 - apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
25.126 - apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
25.127 + apply simp
25.128 + apply (metis (full_types) add_increasing add_uminus_conv_diff lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg mult_nonpos_nonpos nprt_le_zero zero_le_pprt)
25.129 done
25.130 have yx: "?y <= ?x"
25.131 - apply (simp add:diff_minus)
25.132 - apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
25.133 - apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
25.134 + apply simp
25.135 + apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos mult_nonpos_nonneg nprt_le_zero zero_le_pprt)
25.136 done
25.137 have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
25.138 have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
25.139 @@ -549,7 +553,7 @@
25.140 by simp
25.141 then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
25.142 by (simp only: minus_le_iff)
25.143 - then show ?thesis by simp
25.144 + then show ?thesis by (simp add: algebra_simps)
25.145 qed
25.146
25.147 instance int :: lattice_ring
25.148 @@ -567,3 +571,4 @@
25.149 qed
25.150
25.151 end
25.152 +
26.1 --- a/src/HOL/Library/Polynomial.thy Thu Oct 31 16:54:22 2013 +0100
26.2 +++ b/src/HOL/Library/Polynomial.thy Fri Nov 01 18:51:14 2013 +0100
26.3 @@ -667,7 +667,7 @@
26.4 show "- p + p = 0"
26.5 by (simp add: poly_eq_iff)
26.6 show "p - q = p + - q"
26.7 - by (simp add: poly_eq_iff diff_minus)
26.8 + by (simp add: poly_eq_iff)
26.9 qed
26.10
26.11 end
26.12 @@ -714,15 +714,15 @@
26.13
26.14 lemma degree_diff_le_max: "degree (p - q) \<le> max (degree p) (degree q)"
26.15 using degree_add_le [where p=p and q="-q"]
26.16 - by (simp add: diff_minus)
26.17 + by simp
26.18
26.19 lemma degree_diff_le:
26.20 "\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p - q) \<le> n"
26.21 - by (simp add: diff_minus degree_add_le)
26.22 + using degree_add_le [of p n "- q"] by simp
26.23
26.24 lemma degree_diff_less:
26.25 "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n"
26.26 - by (simp add: diff_minus degree_add_less)
26.27 + using degree_add_less [of p n "- q"] by simp
26.28
26.29 lemma add_monom: "monom a n + monom b n = monom (a + b) n"
26.30 by (rule poly_eqI) simp
26.31 @@ -793,7 +793,7 @@
26.32 lemma poly_diff [simp]:
26.33 fixes x :: "'a::comm_ring"
26.34 shows "poly (p - q) x = poly p x - poly q x"
26.35 - by (simp add: diff_minus)
26.36 + using poly_add [of p "- q" x] by simp
26.37
26.38 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
26.39 by (induct A rule: infinite_finite_induct) simp_all
27.1 --- a/src/HOL/Library/Product_plus.thy Thu Oct 31 16:54:22 2013 +0100
27.2 +++ b/src/HOL/Library/Product_plus.thy Fri Nov 01 18:51:14 2013 +0100
27.3 @@ -104,7 +104,7 @@
27.4 (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
27.5
27.6 instance prod :: (group_add, group_add) group_add
27.7 - by default (simp_all add: prod_eq_iff diff_minus)
27.8 + by default (simp_all add: prod_eq_iff)
27.9
27.10 instance prod :: (ab_group_add, ab_group_add) ab_group_add
27.11 by default (simp_all add: prod_eq_iff)
28.1 --- a/src/HOL/Library/Set_Algebras.thy Thu Oct 31 16:54:22 2013 +0100
28.2 +++ b/src/HOL/Library/Set_Algebras.thy Fri Nov 01 18:51:14 2013 +0100
28.3 @@ -190,12 +190,12 @@
28.4 done
28.5
28.6 lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
28.7 - by (auto simp add: elt_set_plus_def add_ac diff_minus)
28.8 + by (auto simp add: elt_set_plus_def add_ac)
28.9
28.10 lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
28.11 - apply (auto simp add: elt_set_plus_def add_ac diff_minus)
28.12 + apply (auto simp add: elt_set_plus_def add_ac)
28.13 apply (subgoal_tac "a = (a + - b) + b")
28.14 - apply (rule bexI, assumption, assumption)
28.15 + apply (rule bexI, assumption)
28.16 apply (auto simp add: add_ac)
28.17 done
28.18
29.1 --- a/src/HOL/Limits.thy Thu Oct 31 16:54:22 2013 +0100
29.2 +++ b/src/HOL/Limits.thy Fri Nov 01 18:51:14 2013 +0100
29.3 @@ -179,7 +179,7 @@
29.4 apply (rule_tac x = K in exI, simp)
29.5 apply (rule exI [where x = 0], auto)
29.6 apply (erule order_less_le_trans, simp)
29.7 -apply (drule_tac x=n in spec, fold diff_minus)
29.8 +apply (drule_tac x=n in spec)
29.9 apply (drule order_trans [OF norm_triangle_ineq2])
29.10 apply simp
29.11 done
29.12 @@ -192,9 +192,11 @@
29.13 then obtain K
29.14 where *: "0 < K" and **: "\<And>n. norm (X n) \<le> K" by (auto simp add: Bseq_def)
29.15 from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp
29.16 - moreover from ** have "\<forall>n. norm (X n + - X 0) \<le> K + norm (X 0)"
29.17 - by (auto intro: order_trans norm_triangle_ineq)
29.18 - ultimately show ?Q by blast
29.19 + from ** have "\<forall>n. norm (X n - X 0) \<le> K + norm (X 0)"
29.20 + by (auto intro: order_trans norm_triangle_ineq4)
29.21 + then have "\<forall>n. norm (X n + - X 0) \<le> K + norm (X 0)"
29.22 + by simp
29.23 + with `0 < K + norm (X 0)` show ?Q by blast
29.24 next
29.25 assume ?Q then show ?P by (auto simp add: Bseq_iff2)
29.26 qed
29.27 @@ -205,6 +207,7 @@
29.28 apply (drule_tac x = n in spec, arith)
29.29 done
29.30
29.31 +
29.32 subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
29.33
29.34 lemma Bseq_isUb:
29.35 @@ -342,7 +345,7 @@
29.36 unfolding Zfun_def by simp
29.37
29.38 lemma Zfun_diff: "\<lbrakk>Zfun f F; Zfun g F\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x - g x) F"
29.39 - by (simp only: diff_minus Zfun_add Zfun_minus)
29.40 + using Zfun_add [of f F "\<lambda>x. - g x"] by (simp add: Zfun_minus)
29.41
29.42 lemma (in bounded_linear) Zfun:
29.43 assumes g: "Zfun g F"
29.44 @@ -532,7 +535,7 @@
29.45 lemma tendsto_diff [tendsto_intros]:
29.46 fixes a b :: "'a::real_normed_vector"
29.47 shows "\<lbrakk>(f ---> a) F; (g ---> b) F\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) F"
29.48 - by (simp add: diff_minus tendsto_add tendsto_minus)
29.49 + using tendsto_add [of f a F "\<lambda>x. - g x" "- b"] by (simp add: tendsto_minus)
29.50
29.51 lemma continuous_diff [continuous_intros]:
29.52 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
30.1 --- a/src/HOL/Matrix_LP/LP.thy Thu Oct 31 16:54:22 2013 +0100
30.2 +++ b/src/HOL/Matrix_LP/LP.thy Fri Nov 01 18:51:14 2013 +0100
30.3 @@ -72,8 +72,7 @@
30.4 proof -
30.5 have "0 <= A - A1"
30.6 proof -
30.7 - have 1: "A - A1 = A + (- A1)" by simp
30.8 - show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified assms])
30.9 + from assms add_right_mono [of A1 A "- A1"] show ?thesis by simp
30.10 qed
30.11 then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
30.12 with assms show "abs (A-A1) <= (A2-A1)" by simp
30.13 @@ -147,9 +146,9 @@
30.14 then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
30.15 then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
30.16 have s2: "c - y * A <= c2 - y * A1"
30.17 - by (simp add: diff_minus assms add_mono mult_left_mono)
30.18 + by (simp add: assms add_mono mult_left_mono algebra_simps)
30.19 have s1: "c1 - y * A2 <= c - y * A"
30.20 - by (simp add: diff_minus assms add_mono mult_left_mono)
30.21 + by (simp add: assms add_mono mult_left_mono algebra_simps)
30.22 have prts: "(c - y * A) * x <= ?C"
30.23 apply (simp add: Let_def)
30.24 apply (rule mult_le_prts)
31.1 --- a/src/HOL/Matrix_LP/Matrix.thy Thu Oct 31 16:54:22 2013 +0100
31.2 +++ b/src/HOL/Matrix_LP/Matrix.thy Fri Nov 01 18:51:14 2013 +0100
31.3 @@ -1542,8 +1542,8 @@
31.4 fix A B :: "'a matrix"
31.5 show "- A + A = 0"
31.6 by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
31.7 - show "A - B = A + - B"
31.8 - by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext diff_minus)
31.9 + show "A + - B = A - B"
31.10 + by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext)
31.11 qed
31.12
31.13 instance matrix :: (ab_group_add) ab_group_add
32.1 --- a/src/HOL/Metis_Examples/Big_O.thy Thu Oct 31 16:54:22 2013 +0100
32.2 +++ b/src/HOL/Metis_Examples/Big_O.thy Fri Nov 01 18:51:14 2013 +0100
32.3 @@ -493,8 +493,10 @@
32.4
32.5 lemma bigo_compose2:
32.6 "f =o g +o O(h) \<Longrightarrow> (\<lambda>x. f(k x)) =o (\<lambda>x. g(k x)) +o O(\<lambda>x. h(k x))"
32.7 -apply (simp only: set_minus_plus [symmetric] diff_minus fun_Compl_def func_plus)
32.8 -by (erule bigo_compose1)
32.9 +apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)
32.10 +apply (drule bigo_compose1 [of "f - g" h k])
32.11 +apply (simp add: fun_diff_def)
32.12 +done
32.13
32.14 subsection {* Setsum *}
32.15
33.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Oct 31 16:54:22 2013 +0100
33.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Nov 01 18:51:14 2013 +0100
33.3 @@ -1099,8 +1099,8 @@
33.4 shows "(\<lambda>x. m *s x + c) o (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
33.5 "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) o (\<lambda>x. m *s x + c) = id"
33.6 using m0
33.7 - apply (auto simp add: fun_eq_iff vector_add_ldistrib)
33.8 - apply (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric])
33.9 + apply (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff)
33.10 + apply (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1 [symmetric])
33.11 done
33.12
33.13 lemma vector_affinity_eq:
33.14 @@ -1114,7 +1114,7 @@
33.15 using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
33.16 next
33.17 assume h: "x = inverse m *s y + - (inverse m *s c)"
33.18 - show "m *s x + c = y" unfolding h diff_minus[symmetric]
33.19 + show "m *s x + c = y" unfolding h
33.20 using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
33.21 qed
33.22
34.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Oct 31 16:54:22 2013 +0100
34.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 01 18:51:14 2013 +0100
34.3 @@ -858,9 +858,10 @@
34.4 assumes "affine_parallel A B"
34.5 shows "affine_parallel B A"
34.6 proof -
34.7 - from assms obtain a where "B = (\<lambda>x. a + x) ` A"
34.8 + from assms obtain a where B: "B = (\<lambda>x. a + x) ` A"
34.9 unfolding affine_parallel_def by auto
34.10 - then show ?thesis
34.11 + have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
34.12 + from B show ?thesis
34.13 using translation_galois [of B a A]
34.14 unfolding affine_parallel_def by auto
34.15 qed
34.16 @@ -980,6 +981,7 @@
34.17 assumes "affine S" "a \<in> S"
34.18 shows "subspace ((\<lambda>x. (-a)+x) ` S)"
34.19 proof -
34.20 + have [simp]: "(\<lambda>x. x - a) = plus (- a)" by (simp add: fun_eq_iff)
34.21 have "affine ((\<lambda>x. (-a)+x) ` S)"
34.22 using affine_translation assms by auto
34.23 moreover have "0 : ((\<lambda>x. (-a)+x) ` S)"
34.24 @@ -992,15 +994,12 @@
34.25 assumes "L \<equiv> {y. \<exists>x \<in> S. (-a)+x=y}"
34.26 shows "subspace L & affine_parallel S L"
34.27 proof -
34.28 - have par: "affine_parallel S L"
34.29 - unfolding affine_parallel_def using assms by auto
34.30 + from assms have "L = plus (- a) ` S" by auto
34.31 + then have par: "affine_parallel S L"
34.32 + unfolding affine_parallel_def ..
34.33 then have "affine L" using assms parallel_is_affine by auto
34.34 moreover have "0 \<in> L"
34.35 - using assms
34.36 - apply auto
34.37 - using exI[of "(\<lambda>x. x:S \<and> -a+x=0)" a]
34.38 - apply auto
34.39 - done
34.40 + using assms by auto
34.41 ultimately show ?thesis
34.42 using subspace_affine par by auto
34.43 qed
34.44 @@ -2390,7 +2389,7 @@
34.45 ultimately have h1: "affine hull ((\<lambda>x. a + x) ` S) \<subseteq> (\<lambda>x. a + x) ` (affine hull S)"
34.46 by (metis hull_minimal)
34.47 have "affine((\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) ` S)))"
34.48 - using affine_translation affine_affine_hull by auto
34.49 + using affine_translation affine_affine_hull by (auto simp del: uminus_add_conv_diff)
34.50 moreover have "(\<lambda>x. -a + x) ` (\<lambda>x. a + x) ` S \<subseteq> (\<lambda>x. -a + x) ` (affine hull ((\<lambda>x. a + x) ` S))"
34.51 using hull_subset[of "(\<lambda>x. a + x) ` S"] by auto
34.52 moreover have "S = (\<lambda>x. -a + x) ` (\<lambda>x. a + x) ` S"
34.53 @@ -2478,7 +2477,7 @@
34.54 using affine_dependent_translation_eq[of "(insert a S)" "-a"]
34.55 affine_dependent_imp_dependent2 assms
34.56 dependent_imp_affine_dependent[of a S]
34.57 - by auto
34.58 + by (auto simp del: uminus_add_conv_diff)
34.59 qed
34.60
34.61 lemma affine_dependent_iff_dependent2:
34.62 @@ -2512,7 +2511,7 @@
34.63 then have "insert 0 ((\<lambda>x. -a+x) ` (s - {a})) = (\<lambda>x. -a+x) ` s"
34.64 by auto
34.65 then have "span ((\<lambda>x. -a+x) ` (s - {a}))=span ((\<lambda>x. -a+x) ` s)"
34.66 - using span_insert_0[of "op + (- a) ` (s - {a})"] by auto
34.67 + using span_insert_0[of "op + (- a) ` (s - {a})"] by (auto simp del: uminus_add_conv_diff)
34.68 moreover have "{x - a |x. x \<in> (s - {a})} = ((\<lambda>x. -a+x) ` (s - {a}))"
34.69 by auto
34.70 moreover have "insert a (s - {a}) = insert a s"
34.71 @@ -2652,7 +2651,7 @@
34.72 moreover have h1: "card ((\<lambda>x. -a + x) ` (B-{a})) = card (B-{a})"
34.73 apply (rule card_image)
34.74 using translate_inj_on
34.75 - apply auto
34.76 + apply (auto simp del: uminus_add_conv_diff)
34.77 done
34.78 ultimately have "card (B-{a}) > 0" by auto
34.79 then have *: "finite (B - {a})"
35.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Oct 31 16:54:22 2013 +0100
35.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Nov 01 18:51:14 2013 +0100
35.3 @@ -516,7 +516,7 @@
35.4 unfolding e_def
35.5 using c[THEN conjunct1]
35.6 using norm_minus_cancel[of "f' i - f'' i"]
35.7 - by (auto simp add: add.commute ab_diff_minus)
35.8 + by auto
35.9 finally show False
35.10 using c
35.11 using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R i"]
36.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Oct 31 16:54:22 2013 +0100
36.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Nov 01 18:51:14 2013 +0100
36.3 @@ -115,7 +115,7 @@
36.4 instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
36.5
36.6 instance vec :: (group_add, finite) group_add
36.7 - by default (simp_all add: vec_eq_iff diff_minus)
36.8 + by default (simp_all add: vec_eq_iff)
36.9
36.10 instance vec :: (ab_group_add, finite) ab_group_add
36.11 by default (simp_all add: vec_eq_iff)
37.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Oct 31 16:54:22 2013 +0100
37.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Nov 01 18:51:14 2013 +0100
37.3 @@ -44,9 +44,7 @@
37.4 by auto
37.5 also have "\<dots> \<le> e"
37.6 apply (rule cSup_asclose)
37.7 - apply (auto simp add: S)
37.8 - apply (metis abs_minus_add_cancel b add_commute diff_minus)
37.9 - done
37.10 + using abs_minus_add_cancel b by (auto simp add: S)
37.11 finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
37.12 then show ?thesis
37.13 by (simp add: Inf_real_def)
37.14 @@ -380,7 +378,7 @@
37.15 using Basis_le_norm[OF k, of "?z - y"] unfolding dist_norm by auto
37.16 then have "y\<bullet>k < a\<bullet>k"
37.17 using e[THEN conjunct1] k
37.18 - by (auto simp add: field_simps as inner_Basis inner_simps)
37.19 + by (auto simp add: field_simps abs_less_iff as inner_Basis inner_simps)
37.20 then have "y \<notin> i"
37.21 unfolding ab mem_interval by (auto intro!: bexI[OF _ k])
37.22 then show False using yi by auto
37.23 @@ -11975,7 +11973,7 @@
37.24 and "g absolutely_integrable_on s"
37.25 shows "(\<lambda>x. f x - g x) absolutely_integrable_on s"
37.26 using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]]
37.27 - by (simp only: algebra_simps)
37.28 + by (simp add: algebra_simps)
37.29
37.30 lemma absolutely_integrable_linear:
37.31 fixes f :: "'m::ordered_euclidean_space \<Rightarrow> 'n::ordered_euclidean_space"
38.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Oct 31 16:54:22 2013 +0100
38.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Nov 01 18:51:14 2013 +0100
38.3 @@ -303,7 +303,7 @@
38.4 by (metis linear_iff)
38.5
38.6 lemma linear_sub: "linear f \<Longrightarrow> f (x - y) = f x - f y"
38.7 - by (simp add: diff_minus linear_add linear_neg)
38.8 + using linear_add [of f x "- y"] by (simp add: linear_neg)
38.9
38.10 lemma linear_setsum:
38.11 assumes lin: "linear f"
38.12 @@ -384,10 +384,10 @@
38.13 using bilinear_radd [OF assms, of x 0 0 ] by (simp add: eq_add_iff field_simps)
38.14
38.15 lemma bilinear_lsub: "bilinear h \<Longrightarrow> h (x - y) z = h x z - h y z"
38.16 - by (simp add: diff_minus bilinear_ladd bilinear_lneg)
38.17 + using bilinear_ladd [of h x "- y"] by (simp add: bilinear_lneg)
38.18
38.19 lemma bilinear_rsub: "bilinear h \<Longrightarrow> h z (x - y) = h z x - h z y"
38.20 - by (simp add: diff_minus bilinear_radd bilinear_rneg)
38.21 + using bilinear_radd [of h _ x "- y"] by (simp add: bilinear_rneg)
38.22
38.23 lemma bilinear_setsum:
38.24 assumes bh: "bilinear h"
38.25 @@ -730,7 +730,7 @@
38.26 by (metis scaleR_minus1_left subspace_mul)
38.27
38.28 lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
38.29 - by (metis diff_minus subspace_add subspace_neg)
38.30 + using subspace_add [of S x "- y"] by (simp add: subspace_neg)
38.31
38.32 lemma (in real_vector) subspace_setsum:
38.33 assumes sA: "subspace A"
38.34 @@ -1021,8 +1021,7 @@
38.35 apply safe
38.36 apply (rule_tac x=k in exI, simp)
38.37 apply (erule rev_image_eqI [OF SigmaI [OF rangeI]])
38.38 - apply simp
38.39 - apply (rule right_minus)
38.40 + apply auto
38.41 done
38.42 then show ?thesis by simp
38.43 qed
38.44 @@ -2064,7 +2063,7 @@
38.45 using C by simp
38.46 have "orthogonal ?a y"
38.47 unfolding orthogonal_def
38.48 - unfolding inner_diff inner_setsum_left diff_eq_0_iff_eq
38.49 + unfolding inner_diff inner_setsum_left right_minus_eq
38.50 unfolding setsum_diff1' [OF `finite C` `y \<in> C`]
38.51 apply (clarsimp simp add: inner_commute[of y a])
38.52 apply (rule setsum_0')
38.53 @@ -3026,7 +3025,7 @@
38.54 norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) = 0)"
38.55 using x y
38.56 unfolding inner_simps
38.57 - unfolding power2_norm_eq_inner[symmetric] power2_eq_square diff_eq_0_iff_eq
38.58 + unfolding power2_norm_eq_inner[symmetric] power2_eq_square right_minus_eq
38.59 apply (simp add: inner_commute)
38.60 apply (simp add: field_simps)
38.61 apply metis
39.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Oct 31 16:54:22 2013 +0100
39.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Nov 01 18:51:14 2013 +0100
39.3 @@ -4858,8 +4858,8 @@
39.4 assumes "uniformly_continuous_on s f"
39.5 and "uniformly_continuous_on s g"
39.6 shows "uniformly_continuous_on s (\<lambda>x. f x - g x)"
39.7 - unfolding ab_diff_minus using assms
39.8 - by (intro uniformly_continuous_on_add uniformly_continuous_on_minus)
39.9 + using assms uniformly_continuous_on_add [of s f "- g"]
39.10 + by (simp add: fun_Compl_def uniformly_continuous_on_minus)
39.11
39.12 text{* Continuity of all kinds is preserved under composition. *}
39.13
39.14 @@ -5680,8 +5680,6 @@
39.15 apply auto
39.16 apply (rule_tac x= xa in exI)
39.17 apply auto
39.18 - apply (rule_tac x=xa in exI)
39.19 - apply auto
39.20 done
39.21 then show ?thesis
39.22 using compact_sums[OF assms(1) compact_negations[OF assms(2)]] by auto
39.23 @@ -7032,7 +7030,8 @@
39.24 unfolding homeomorphic_minimal
39.25 apply (rule_tac x="\<lambda>x. a + x" in exI)
39.26 apply (rule_tac x="\<lambda>x. -a + x" in exI)
39.27 - using continuous_on_add[OF continuous_on_const continuous_on_id]
39.28 + using continuous_on_add [OF continuous_on_const continuous_on_id, of s a]
39.29 + continuous_on_add [OF continuous_on_const continuous_on_id, of "plus a ` s" "- a"]
39.30 apply auto
39.31 done
39.32
40.1 --- a/src/HOL/NSA/CLim.thy Thu Oct 31 16:54:22 2013 +0100
40.2 +++ b/src/HOL/NSA/CLim.thy Fri Nov 01 18:51:14 2013 +0100
40.3 @@ -22,11 +22,11 @@
40.4 lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))";
40.5 apply auto
40.6 apply (drule_tac x="x+a" in spec)
40.7 -apply (simp add: diff_minus add_assoc)
40.8 +apply (simp add: add_assoc)
40.9 done
40.10
40.11 lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)"
40.12 -by (simp add: diff_eq_eq diff_minus [symmetric])
40.13 +by (simp add: diff_eq_eq)
40.14
40.15 lemma complex_add_eq_0_iff [iff]: "(x+y = (0::complex)) = (y = -x)"
40.16 apply auto
41.1 --- a/src/HOL/NSA/HDeriv.thy Thu Oct 31 16:54:22 2013 +0100
41.2 +++ b/src/HOL/NSA/HDeriv.thy Fri Nov 01 18:51:14 2013 +0100
41.3 @@ -81,8 +81,7 @@
41.4 text{*second equivalence *}
41.5 lemma NSDERIV_NSLIM_iff2:
41.6 "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --NS> D)"
41.7 -by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff diff_minus [symmetric]
41.8 - LIM_NSLIM_iff [symmetric])
41.9 + by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric])
41.10
41.11 (* while we're at it! *)
41.12
41.13 @@ -120,11 +119,10 @@
41.14 hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)"
41.15 apply (auto simp add: nsderiv_def)
41.16 apply (case_tac "h = (0::hypreal) ")
41.17 -apply (auto simp add: diff_minus)
41.18 +apply auto
41.19 apply (drule_tac x = h in bspec)
41.20 apply (drule_tac [2] c = h in approx_mult1)
41.21 -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
41.22 - simp add: diff_minus)
41.23 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
41.24 done
41.25
41.26 lemma NSDERIVD3:
41.27 @@ -135,8 +133,7 @@
41.28 apply (auto simp add: nsderiv_def)
41.29 apply (rule ccontr, drule_tac x = h in bspec)
41.30 apply (drule_tac [2] c = h in approx_mult1)
41.31 -apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
41.32 - simp add: mult_assoc diff_minus)
41.33 +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult_assoc)
41.34 done
41.35
41.36 text{*Differentiability implies continuity
41.37 @@ -174,7 +171,7 @@
41.38 apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
41.39 apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
41.40 apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
41.41 -apply (auto simp add: diff_minus add_ac)
41.42 +apply (auto simp add: add_ac algebra_simps)
41.43 done
41.44
41.45 text{*Product of functions - Proof is trivial but tedious
41.46 @@ -234,9 +231,11 @@
41.47 hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D"
41.48 by (rule NSLIM_minus)
41.49 have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
41.50 - by (simp add: minus_divide_left diff_minus)
41.51 + by (simp add: minus_divide_left)
41.52 with deriv
41.53 - show "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
41.54 + have "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
41.55 + then show "(\<lambda>h. (f (x + h) - f x) / h) -- 0 --NS> D \<Longrightarrow>
41.56 + (\<lambda>h. (f x - f (x + h)) / h) -- 0 --NS> - D" by simp
41.57 qed
41.58
41.59 text{*Subtraction*}
41.60 @@ -244,11 +243,8 @@
41.61 by (blast dest: NSDERIV_add NSDERIV_minus)
41.62
41.63 lemma NSDERIV_diff:
41.64 - "[| NSDERIV f x :> Da; NSDERIV g x :> Db |]
41.65 - ==> NSDERIV (%x. f x - g x) x :> Da-Db"
41.66 -apply (simp add: diff_minus)
41.67 -apply (blast intro: NSDERIV_add_minus)
41.68 -done
41.69 + "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x - g x) x :> Da-Db"
41.70 + using NSDERIV_add_minus [of f x Da g Db] by simp
41.71
41.72 text{* Similarly to the above, the chain rule admits an entirely
41.73 straightforward derivation. Compare this with Harrison's
41.74 @@ -294,7 +290,7 @@
41.75 - star_of (f (g x)))
41.76 / (( *f* g) (star_of(x) + xa) - star_of (g x))
41.77 \<approx> star_of(Da)"
41.78 -by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def diff_minus [symmetric])
41.79 +by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
41.80
41.81 (*--------------------------------------------------------------
41.82 from other version of differentiability
41.83 @@ -354,13 +350,23 @@
41.84 from h_Inf have "h * star_of x \<in> Infinitesimal" by (rule Infinitesimal_HFinite_mult) simp
41.85 with assms have "inverse (- (h * star_of x) + - (star_of x * star_of x)) \<approx>
41.86 inverse (- (star_of x * star_of x))"
41.87 - by (auto intro: inverse_add_Infinitesimal_approx2
41.88 + apply - apply (rule inverse_add_Infinitesimal_approx2)
41.89 + apply (auto
41.90 dest!: hypreal_of_real_HFinite_diff_Infinitesimal
41.91 simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
41.92 - with not_0 `h \<noteq> 0` assms have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
41.93 + done
41.94 + moreover from not_0 `h \<noteq> 0` assms
41.95 + have "inverse (- (h * star_of x) + - (star_of x * star_of x)) =
41.96 + (inverse (star_of x + h) - inverse (star_of x)) / h"
41.97 + apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric]
41.98 + nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs)
41.99 + apply (subst nonzero_inverse_minus_eq [symmetric])
41.100 + using distrib_right [symmetric, of h "star_of x" "star_of x"] apply simp
41.101 + apply (simp add: field_simps)
41.102 + done
41.103 + ultimately have "(inverse (star_of x + h) - inverse (star_of x)) / h \<approx>
41.104 - (inverse (star_of x) * inverse (star_of x))"
41.105 - by (simp add: inverse_add nonzero_inverse_mult_distrib [symmetric]
41.106 - nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_minus ring_distribs)
41.107 + using assms by (simp add: nonzero_inverse_mult_distrib [symmetric] nonzero_inverse_minus_eq [symmetric])
41.108 } then show ?thesis by (simp add: nsderiv_def)
41.109 qed
41.110
42.1 --- a/src/HOL/NSA/HLim.thy Thu Oct 31 16:54:22 2013 +0100
42.2 +++ b/src/HOL/NSA/HLim.thy Fri Nov 01 18:51:14 2013 +0100
42.3 @@ -71,7 +71,7 @@
42.4
42.5 lemma NSLIM_diff:
42.6 "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
42.7 -by (simp only: diff_minus NSLIM_add NSLIM_minus)
42.8 + by (simp only: NSLIM_add NSLIM_minus diff_conv_add_uminus)
42.9
42.10 lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
42.11 by (simp only: NSLIM_add NSLIM_minus)
42.12 @@ -95,7 +95,7 @@
42.13
42.14 lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
42.15 apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
42.16 -apply (auto simp add: diff_minus add_assoc)
42.17 +apply (auto simp add: add_assoc)
42.18 done
42.19
42.20 lemma NSLIM_const_not_eq:
42.21 @@ -243,14 +243,14 @@
42.22 apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
42.23 apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
42.24 apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
42.25 - prefer 2 apply (simp add: add_commute diff_minus [symmetric])
42.26 + prefer 2 apply (simp add: add_commute)
42.27 apply (rule_tac x = x in star_cases)
42.28 apply (rule_tac [2] x = x in star_cases)
42.29 -apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
42.30 +apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc star_n_zero_num)
42.31 done
42.32
42.33 lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
42.34 -by (rule NSLIM_h_iff)
42.35 + by (fact NSLIM_h_iff)
42.36
42.37 lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
42.38 by (simp add: isNSCont_def)
43.1 --- a/src/HOL/NSA/HSEQ.thy Thu Oct 31 16:54:22 2013 +0100
43.2 +++ b/src/HOL/NSA/HSEQ.thy Fri Nov 01 18:51:14 2013 +0100
43.3 @@ -73,14 +73,14 @@
43.4 lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
43.5 by (drule NSLIMSEQ_minus, simp)
43.6
43.7 +lemma NSLIMSEQ_diff:
43.8 + "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
43.9 + using NSLIMSEQ_add [of X a "- Y" "- b"] by (simp add: NSLIMSEQ_minus fun_Compl_def)
43.10 +
43.11 (* FIXME: delete *)
43.12 lemma NSLIMSEQ_add_minus:
43.13 "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
43.14 -by (simp add: NSLIMSEQ_add NSLIMSEQ_minus)
43.15 -
43.16 -lemma NSLIMSEQ_diff:
43.17 - "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
43.18 -by (simp add: diff_minus NSLIMSEQ_add NSLIMSEQ_minus)
43.19 + by (simp add: NSLIMSEQ_diff)
43.20
43.21 lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
43.22 by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
43.23 @@ -233,11 +233,11 @@
43.24
43.25 lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
43.26 "(%n. r + -inverse(real(Suc n))) ----NS> r"
43.27 -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus)
43.28 + using LIMSEQ_inverse_real_of_nat_add_minus by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
43.29
43.30 lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
43.31 "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
43.32 -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)
43.33 + using LIMSEQ_inverse_real_of_nat_add_minus_mult by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
43.34
43.35
43.36 subsection {* Convergence *}
44.1 --- a/src/HOL/NSA/HSeries.thy Thu Oct 31 16:54:22 2013 +0100
44.2 +++ b/src/HOL/NSA/HSeries.thy Fri Nov 01 18:51:14 2013 +0100
44.3 @@ -131,7 +131,7 @@
44.4 apply (auto simp add: approx_refl)
44.5 apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
44.6 apply (auto dest: approx_hrabs
44.7 - simp add: sumhr_split_diff diff_minus [symmetric])
44.8 + simp add: sumhr_split_diff)
44.9 done
44.10
44.11 (*----------------------------------------------------------------
44.12 @@ -172,7 +172,7 @@
44.13 apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
44.14 apply (rule_tac [2] approx_minus_iff [THEN iffD2])
44.15 apply (auto dest: approx_hrabs_zero_cancel
44.16 - simp add: sumhr_split_diff diff_minus [symmetric])
44.17 + simp add: sumhr_split_diff)
44.18 done
44.19
44.20
45.1 --- a/src/HOL/NSA/HTranscendental.thy Thu Oct 31 16:54:22 2013 +0100
45.2 +++ b/src/HOL/NSA/HTranscendental.thy Fri Nov 01 18:51:14 2013 +0100
45.3 @@ -258,7 +258,7 @@
45.4 simp add: mult_assoc)
45.5 apply (rule approx_add_right_cancel [where d="-1"])
45.6 apply (rule approx_sym [THEN [2] approx_trans2])
45.7 -apply (auto simp add: diff_minus mem_infmal_iff)
45.8 +apply (auto simp add: mem_infmal_iff minus_one [symmetric] simp del: minus_one)
45.9 done
45.10
45.11 lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
45.12 @@ -450,7 +450,7 @@
45.13 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
45.14 simp add: mult_assoc)
45.15 apply (rule approx_add_right_cancel [where d = "-1"])
45.16 -apply (simp add: diff_minus)
45.17 +apply (simp add: minus_one [symmetric] del: minus_one)
45.18 done
45.19
45.20 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
45.21 @@ -587,7 +587,7 @@
45.22 "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x\<^sup>2"
45.23 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
45.24 apply (auto simp add: Infinitesimal_approx_minus [symmetric]
45.25 - diff_minus add_assoc [symmetric] numeral_2_eq_2)
45.26 + add_assoc [symmetric] numeral_2_eq_2)
45.27 done
45.28
45.29 lemma STAR_cos_Infinitesimal_approx2:
46.1 --- a/src/HOL/NSA/NSA.thy Thu Oct 31 16:54:22 2013 +0100
46.2 +++ b/src/HOL/NSA/NSA.thy Fri Nov 01 18:51:14 2013 +0100
46.3 @@ -368,7 +368,7 @@
46.4
46.5 lemma Infinitesimal_diff:
46.6 "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
46.7 -by (simp add: diff_minus Infinitesimal_add)
46.8 + using Infinitesimal_add [of x "- y"] by simp
46.9
46.10 lemma Infinitesimal_mult:
46.11 fixes x y :: "'a::real_normed_algebra star"
46.12 @@ -491,7 +491,9 @@
46.13 "[|(x::hypreal) \<in> HInfinite; y \<le> 0; x \<le> 0|] ==> (x + y): HInfinite"
46.14 apply (drule HInfinite_minus_iff [THEN iffD2])
46.15 apply (rule HInfinite_minus_iff [THEN iffD1])
46.16 -apply (auto intro: HInfinite_add_ge_zero)
46.17 +apply (simp only: minus_add add.commute)
46.18 +apply (rule HInfinite_add_ge_zero)
46.19 +apply simp_all
46.20 done
46.21
46.22 lemma HInfinite_add_lt_zero:
46.23 @@ -620,7 +622,7 @@
46.24 by (simp add: approx_def)
46.25
46.26 lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)"
46.27 -by (simp add: approx_def diff_minus add_commute)
46.28 +by (simp add: approx_def add_commute)
46.29
46.30 lemma approx_refl [iff]: "x @= x"
46.31 by (simp add: approx_def Infinitesimal_def)
46.32 @@ -637,7 +639,7 @@
46.33 lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"
46.34 apply (simp add: approx_def)
46.35 apply (drule (1) Infinitesimal_add)
46.36 -apply (simp add: diff_minus)
46.37 +apply simp
46.38 done
46.39
46.40 lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"
46.41 @@ -687,7 +689,7 @@
46.42 lemma approx_minus: "a @= b ==> -a @= -b"
46.43 apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
46.44 apply (drule approx_minus_iff [THEN iffD1])
46.45 -apply (simp add: add_commute diff_minus)
46.46 +apply (simp add: add_commute)
46.47 done
46.48
46.49 lemma approx_minus2: "-a @= -b ==> a @= b"
46.50 @@ -700,7 +702,7 @@
46.51 by (blast intro!: approx_add approx_minus)
46.52
46.53 lemma approx_diff: "[| a @= b; c @= d |] ==> a - c @= b - d"
46.54 -by (simp only: diff_minus approx_add approx_minus)
46.55 + using approx_add [of a b "- c" "- d"] by simp
46.56
46.57 lemma approx_mult1:
46.58 fixes a b c :: "'a::real_normed_algebra star"
46.59 @@ -1213,7 +1215,9 @@
46.60 r \<in> Reals; 0 < r |]
46.61 ==> -(x + -t) \<le> r"
46.62 apply (subgoal_tac "(t + -r \<le> x)")
46.63 -apply (auto intro: lemma_st_part_le2)
46.64 +apply simp
46.65 +apply (rule lemma_st_part_le2)
46.66 +apply auto
46.67 done
46.68
46.69 lemma lemma_SReal_ub:
46.70 @@ -1238,7 +1242,7 @@
46.71 ==> x + -t \<noteq> r"
46.72 apply auto
46.73 apply (frule isLubD1a [THEN Reals_minus])
46.74 -apply (drule Reals_add_cancel, assumption)
46.75 +using Reals_add_cancel [of x "- t"] apply simp
46.76 apply (drule_tac x = x in lemma_SReal_lub)
46.77 apply (drule hypreal_isLub_unique, assumption, auto)
46.78 done
46.79 @@ -1250,8 +1254,7 @@
46.80 ==> -(x + -t) \<noteq> r"
46.81 apply (auto)
46.82 apply (frule isLubD1a)
46.83 -apply (drule Reals_add_cancel, assumption)
46.84 -apply (drule_tac a = "-x" in Reals_minus, simp)
46.85 +using Reals_add_cancel [of "- x" t] apply simp
46.86 apply (drule_tac x = x in lemma_SReal_lub)
46.87 apply (drule hypreal_isLub_unique, assumption, auto)
46.88 done
47.1 --- a/src/HOL/NSA/NSCA.thy Thu Oct 31 16:54:22 2013 +0100
47.2 +++ b/src/HOL/NSA/NSCA.thy Fri Nov 01 18:51:14 2013 +0100
47.3 @@ -165,7 +165,7 @@
47.4
47.5 lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)"
47.6 apply (subst hnorm_minus_commute)
47.7 -apply (simp add: approx_def Infinitesimal_hcmod_iff diff_minus)
47.8 +apply (simp add: approx_def Infinitesimal_hcmod_iff)
47.9 done
47.10
47.11 lemma approx_approx_zero_iff: "(x @= 0) = (hcmod x @= 0)"
47.12 @@ -178,14 +178,14 @@
47.13 "u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
47.14 apply (drule approx_approx_zero_iff [THEN iffD1])
47.15 apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
47.16 -apply (auto simp add: mem_infmal_iff [symmetric] diff_minus)
47.17 +apply (auto simp add: mem_infmal_iff [symmetric])
47.18 apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])
47.19 -apply (auto simp add: diff_minus [symmetric])
47.20 +apply auto
47.21 done
47.22
47.23 lemma approx_hcmod_add_hcmod: "u @= 0 ==> hcmod(x + u) @= hcmod x"
47.24 apply (rule approx_minus_iff [THEN iffD2])
47.25 -apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric])
47.26 +apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric])
47.27 done
47.28
47.29
48.1 --- a/src/HOL/NSA/StarDef.thy Thu Oct 31 16:54:22 2013 +0100
48.2 +++ b/src/HOL/NSA/StarDef.thy Fri Nov 01 18:51:14 2013 +0100
48.3 @@ -803,7 +803,7 @@
48.4 instance star :: (ab_group_add) ab_group_add
48.5 apply (intro_classes)
48.6 apply (transfer, rule left_minus)
48.7 -apply (transfer, rule diff_minus)
48.8 +apply (transfer, rule diff_conv_add_uminus)
48.9 done
48.10
48.11 instance star :: (ordered_ab_semigroup_add) ordered_ab_semigroup_add
49.1 --- a/src/HOL/Num.thy Thu Oct 31 16:54:22 2013 +0100
49.2 +++ b/src/HOL/Num.thy Fri Nov 01 18:51:14 2013 +0100
49.3 @@ -407,7 +407,7 @@
49.4 apply (simp add: add_assoc [symmetric], simp add: add_assoc)
49.5 apply (rule_tac a=x in add_left_imp_eq)
49.6 apply (rule_tac a=x in add_right_imp_eq)
49.7 - apply (simp add: add_assoc minus_add_cancel add_minus_cancel)
49.8 + apply (simp add: add_assoc)
49.9 apply (simp add: add_assoc, simp add: add_assoc [symmetric])
49.10 done
49.11
49.12 @@ -418,7 +418,7 @@
49.13 lemmas is_num_normalize =
49.14 add_assoc is_num_add_commute is_num_add_left_commute
49.15 is_num.intros is_num_numeral
49.16 - diff_minus minus_add add_minus_cancel minus_add_cancel
49.17 + minus_add
49.18
49.19 definition dbl :: "'a \<Rightarrow> 'a" where "dbl x = x + x"
49.20 definition dbl_inc :: "'a \<Rightarrow> 'a" where "dbl_inc x = x + x + 1"
49.21 @@ -435,24 +435,21 @@
49.22 "dbl 0 = 0"
49.23 "dbl 1 = 2"
49.24 "dbl (numeral k) = numeral (Bit0 k)"
49.25 - unfolding dbl_def neg_numeral_def numeral.simps
49.26 - by (simp_all add: minus_add)
49.27 + by (simp_all add: dbl_def neg_numeral_def numeral.simps minus_add)
49.28
49.29 lemma dbl_inc_simps [simp]:
49.30 "dbl_inc (neg_numeral k) = neg_numeral (BitM k)"
49.31 "dbl_inc 0 = 1"
49.32 "dbl_inc 1 = 3"
49.33 "dbl_inc (numeral k) = numeral (Bit1 k)"
49.34 - unfolding dbl_inc_def neg_numeral_def numeral.simps numeral_BitM
49.35 - by (simp_all add: is_num_normalize)
49.36 + by (simp_all add: dbl_inc_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize algebra_simps del: add_uminus_conv_diff)
49.37
49.38 lemma dbl_dec_simps [simp]:
49.39 "dbl_dec (neg_numeral k) = neg_numeral (Bit1 k)"
49.40 "dbl_dec 0 = -1"
49.41 "dbl_dec 1 = 1"
49.42 "dbl_dec (numeral k) = numeral (BitM k)"
49.43 - unfolding dbl_dec_def neg_numeral_def numeral.simps numeral_BitM
49.44 - by (simp_all add: is_num_normalize)
49.45 + by (simp_all add: dbl_dec_def neg_numeral_def numeral.simps numeral_BitM is_num_normalize)
49.46
49.47 lemma sub_num_simps [simp]:
49.48 "sub One One = 0"
49.49 @@ -464,38 +461,35 @@
49.50 "sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)"
49.51 "sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)"
49.52 "sub (Bit1 k) (Bit1 l) = dbl (sub k l)"
49.53 - unfolding dbl_def dbl_dec_def dbl_inc_def sub_def
49.54 - unfolding neg_numeral_def numeral.simps numeral_BitM
49.55 - by (simp_all add: is_num_normalize)
49.56 + by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def neg_numeral_def numeral.simps
49.57 + numeral_BitM is_num_normalize del: add_uminus_conv_diff add: diff_conv_add_uminus)
49.58
49.59 lemma add_neg_numeral_simps:
49.60 "numeral m + neg_numeral n = sub m n"
49.61 "neg_numeral m + numeral n = sub n m"
49.62 "neg_numeral m + neg_numeral n = neg_numeral (m + n)"
49.63 - unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps
49.64 - by (simp_all add: is_num_normalize)
49.65 + by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize
49.66 + del: add_uminus_conv_diff add: diff_conv_add_uminus)
49.67
49.68 lemma add_neg_numeral_special:
49.69 "1 + neg_numeral m = sub One m"
49.70 "neg_numeral m + 1 = sub One m"
49.71 - unfolding sub_def diff_minus neg_numeral_def numeral_add numeral.simps
49.72 - by (simp_all add: is_num_normalize)
49.73 + by (simp_all add: sub_def neg_numeral_def numeral_add numeral.simps is_num_normalize)
49.74
49.75 lemma diff_numeral_simps:
49.76 "numeral m - numeral n = sub m n"
49.77 "numeral m - neg_numeral n = numeral (m + n)"
49.78 "neg_numeral m - numeral n = neg_numeral (m + n)"
49.79 "neg_numeral m - neg_numeral n = sub n m"
49.80 - unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps
49.81 - by (simp_all add: is_num_normalize)
49.82 + by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps is_num_normalize
49.83 + del: add_uminus_conv_diff add: diff_conv_add_uminus)
49.84
49.85 lemma diff_numeral_special:
49.86 "1 - numeral n = sub One n"
49.87 "1 - neg_numeral n = numeral (One + n)"
49.88 "numeral m - 1 = sub m One"
49.89 "neg_numeral m - 1 = neg_numeral (m + One)"
49.90 - unfolding neg_numeral_def sub_def diff_minus numeral_add numeral.simps
49.91 - by (simp_all add: is_num_normalize)
49.92 + by (simp_all add: neg_numeral_def sub_def numeral_add numeral.simps add: is_num_normalize)
49.93
49.94 lemma minus_one: "- 1 = -1"
49.95 unfolding neg_numeral_def numeral.simps ..
50.1 --- a/src/HOL/Number_Theory/Cong.thy Thu Oct 31 16:54:22 2013 +0100
50.2 +++ b/src/HOL/Number_Theory/Cong.thy Fri Nov 01 18:51:14 2013 +0100
50.3 @@ -543,7 +543,8 @@
50.4 apply (subgoal_tac "a * b = (-a * -b)")
50.5 apply (erule ssubst)
50.6 apply (subst zmod_zmult2_eq)
50.7 - apply (auto simp add: mod_add_left_eq)
50.8 + apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right)
50.9 + apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 semiring_numeral_div_class.diff_zero)+
50.10 done
50.11
50.12 lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
51.1 --- a/src/HOL/Probability/Borel_Space.thy Thu Oct 31 16:54:22 2013 +0100
51.2 +++ b/src/HOL/Probability/Borel_Space.thy Fri Nov 01 18:51:14 2013 +0100
51.3 @@ -677,7 +677,7 @@
51.4 assumes f: "f \<in> borel_measurable M"
51.5 assumes g: "g \<in> borel_measurable M"
51.6 shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
51.7 - unfolding diff_minus using assms by simp
51.8 + using borel_measurable_add [of f M "- g"] assms by (simp add: fun_Compl_def)
51.9
51.10 lemma borel_measurable_times[measurable (raw)]:
51.11 fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_algebra}"
51.12 @@ -719,7 +719,8 @@
51.13 proof cases
51.14 assume "b \<noteq> 0"
51.15 with `open S` have "open ((\<lambda>x. (- a + x) /\<^sub>R b) ` S)" (is "open ?S")
51.16 - by (auto intro!: open_affinity simp: scaleR_add_right)
51.17 + using open_affinity [of S "inverse b" "- a /\<^sub>R b"]
51.18 + by (auto simp: algebra_simps)
51.19 hence "?S \<in> sets borel" by auto
51.20 moreover
51.21 from `b \<noteq> 0` have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"
52.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Oct 31 16:54:22 2013 +0100
52.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Fri Nov 01 18:51:14 2013 +0100
52.3 @@ -1528,7 +1528,7 @@
52.4 using mono by auto
52.5 ultimately show ?thesis using fg
52.6 by (auto intro!: add_mono positive_integral_mono_AE real_of_ereal_positive_mono
52.7 - simp: positive_integral_positive lebesgue_integral_def diff_minus)
52.8 + simp: positive_integral_positive lebesgue_integral_def algebra_simps)
52.9 qed
52.10
52.11 lemma integral_mono:
52.12 @@ -1732,7 +1732,7 @@
52.13 shows "integrable M (\<lambda>t. f t - g t)"
52.14 and "(\<integral> t. f t - g t \<partial>M) = integral\<^sup>L M f - integral\<^sup>L M g"
52.15 using integral_add[OF f integral_minus(1)[OF g]]
52.16 - unfolding diff_minus integral_minus(2)[OF g]
52.17 + unfolding integral_minus(2)[OF g]
52.18 by auto
52.19
52.20 lemma integral_indicator[simp, intro]:
53.1 --- a/src/HOL/Rat.thy Thu Oct 31 16:54:22 2013 +0100
53.2 +++ b/src/HOL/Rat.thy Fri Nov 01 18:51:14 2013 +0100
53.3 @@ -468,7 +468,7 @@
53.4 unfolding less_eq_rat_def less_rat_def
53.5 by (auto, drule (1) positive_add, simp add: positive_zero)
53.6 show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
53.7 - unfolding less_eq_rat_def less_rat_def by (auto simp: diff_minus)
53.8 + unfolding less_eq_rat_def less_rat_def by auto
53.9 show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
53.10 by (rule sgn_rat_def)
53.11 show "a \<le> b \<or> b \<le> a"
53.12 @@ -665,7 +665,7 @@
53.13 by transfer simp
53.14
53.15 lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b"
53.16 -by (simp only: diff_minus of_rat_add of_rat_minus)
53.17 + using of_rat_add [of a "- b"] by (simp add: of_rat_minus)
53.18
53.19 lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b"
53.20 apply transfer
54.1 --- a/src/HOL/Real.thy Thu Oct 31 16:54:22 2013 +0100
54.2 +++ b/src/HOL/Real.thy Fri Nov 01 18:51:14 2013 +0100
54.3 @@ -98,7 +98,7 @@
54.4 lemma vanishes_diff:
54.5 assumes X: "vanishes X" and Y: "vanishes Y"
54.6 shows "vanishes (\<lambda>n. X n - Y n)"
54.7 -unfolding diff_minus by (intro vanishes_add vanishes_minus X Y)
54.8 + unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus X Y)
54.9
54.10 lemma vanishes_mult_bounded:
54.11 assumes X: "\<exists>a>0. \<forall>n. \<bar>X n\<bar> < a"
54.12 @@ -170,7 +170,7 @@
54.13 lemma cauchy_diff [simp]:
54.14 assumes X: "cauchy X" and Y: "cauchy Y"
54.15 shows "cauchy (\<lambda>n. X n - Y n)"
54.16 -using assms unfolding diff_minus by simp
54.17 + using assms unfolding diff_conv_add_uminus by (simp del: add_uminus_conv_diff)
54.18
54.19 lemma cauchy_imp_bounded:
54.20 assumes "cauchy X" shows "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
54.21 @@ -456,7 +456,7 @@
54.22 lemma diff_Real:
54.23 assumes X: "cauchy X" and Y: "cauchy Y"
54.24 shows "Real X - Real Y = Real (\<lambda>n. X n - Y n)"
54.25 - unfolding minus_real_def diff_minus
54.26 + unfolding minus_real_def
54.27 by (simp add: minus_Real add_Real X Y)
54.28
54.29 lemma mult_Real:
54.30 @@ -607,7 +607,7 @@
54.31 unfolding less_eq_real_def less_real_def
54.32 by (auto, drule (1) positive_add, simp add: positive_zero)
54.33 show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
54.34 - unfolding less_eq_real_def less_real_def by (auto simp: diff_minus) (* by auto *)
54.35 + unfolding less_eq_real_def less_real_def by auto
54.36 (* FIXME: Procedure int_combine_numerals: c + b - (c + a) \<equiv> b + - a *)
54.37 (* Should produce c + b - (c + a) \<equiv> b - a *)
54.38 show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
55.1 --- a/src/HOL/Real_Vector_Spaces.thy Thu Oct 31 16:54:22 2013 +0100
55.2 +++ b/src/HOL/Real_Vector_Spaces.thy Fri Nov 01 18:51:14 2013 +0100
55.3 @@ -31,7 +31,7 @@
55.4 qed
55.5
55.6 lemma diff: "f (x - y) = f x - f y"
55.7 -by (simp add: add minus diff_minus)
55.8 + using add [of x "- y"] by (simp add: minus)
55.9
55.10 lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
55.11 apply (cases "finite A")
55.12 @@ -553,8 +553,7 @@
55.13 proof -
55.14 have "norm (a + - b) \<le> norm a + norm (- b)"
55.15 by (rule norm_triangle_ineq)
55.16 - thus ?thesis
55.17 - by (simp only: diff_minus norm_minus_cancel)
55.18 + then show ?thesis by simp
55.19 qed
55.20
55.21 lemma norm_diff_ineq:
55.22 @@ -571,7 +570,7 @@
55.23 shows "norm ((a + b) - (c + d)) \<le> norm (a - c) + norm (b - d)"
55.24 proof -
55.25 have "norm ((a + b) - (c + d)) = norm ((a - c) + (b - d))"
55.26 - by (simp add: diff_minus add_ac)
55.27 + by (simp add: algebra_simps)
55.28 also have "\<dots> \<le> norm (a - c) + norm (b - d)"
55.29 by (rule norm_triangle_ineq)
55.30 finally show ?thesis .
56.1 --- a/src/HOL/Rings.thy Thu Oct 31 16:54:22 2013 +0100
56.2 +++ b/src/HOL/Rings.thy Fri Nov 01 18:51:14 2013 +0100
56.3 @@ -255,11 +255,13 @@
56.4 lemma minus_mult_commute: "- a * b = a * - b"
56.5 by simp
56.6
56.7 -lemma right_diff_distrib[algebra_simps, field_simps]: "a * (b - c) = a * b - a * c"
56.8 -by (simp add: distrib_left diff_minus)
56.9 +lemma right_diff_distrib [algebra_simps, field_simps]:
56.10 + "a * (b - c) = a * b - a * c"
56.11 + using distrib_left [of a b "-c "] by simp
56.12
56.13 -lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
56.14 -by (simp add: distrib_right diff_minus)
56.15 +lemma left_diff_distrib [algebra_simps, field_simps]:
56.16 + "(a - b) * c = a * c - b * c"
56.17 + using distrib_right [of a "- b" c] by simp
56.18
56.19 lemmas ring_distribs =
56.20 distrib_left distrib_right left_diff_distrib right_diff_distrib
56.21 @@ -331,8 +333,9 @@
56.22 then show "- x dvd y" ..
56.23 qed
56.24
56.25 -lemma dvd_diff[simp]: "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
56.26 -by (simp only: diff_minus dvd_add dvd_minus_iff)
56.27 +lemma dvd_diff [simp]:
56.28 + "x dvd y \<Longrightarrow> x dvd z \<Longrightarrow> x dvd (y - z)"
56.29 + using dvd_add [of x y "- z"] by simp
56.30
56.31 end
56.32
56.33 @@ -755,9 +758,7 @@
56.34 proof
56.35 fix a b
56.36 show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
56.37 - by (auto simp add: abs_if not_less)
56.38 - (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
56.39 - auto intro!: less_imp_le add_neg_neg)
56.40 + by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg)
56.41 qed (auto simp add: abs_if)
56.42
56.43 lemma zero_le_square [simp]: "0 \<le> a * a"
57.1 --- a/src/HOL/Semiring_Normalization.thy Thu Oct 31 16:54:22 2013 +0100
57.2 +++ b/src/HOL/Semiring_Normalization.thy Fri Nov 01 18:51:14 2013 +0100
57.3 @@ -137,7 +137,7 @@
57.4 lemma normalizing_ring_rules:
57.5 "- x = (- 1) * x"
57.6 "x - y = x + (- y)"
57.7 - by (simp_all add: diff_minus)
57.8 + by simp_all
57.9
57.10 lemmas normalizing_comm_ring_1_axioms =
57.11 comm_ring_1_axioms [normalizer
58.1 --- a/src/HOL/Series.thy Thu Oct 31 16:54:22 2013 +0100
58.2 +++ b/src/HOL/Series.thy Fri Nov 01 18:51:14 2013 +0100
58.3 @@ -34,7 +34,7 @@
58.4
58.5 lemma sumr_diff_mult_const:
58.6 "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
58.7 -by (simp add: diff_minus setsum_addf real_of_nat_def)
58.8 + by (simp add: setsum_subtractf real_of_nat_def)
58.9
58.10 lemma real_setsum_nat_ivl_bounded:
58.11 "(!!p. p < n \<Longrightarrow> f(p) \<le> K)
59.1 --- a/src/HOL/Tools/group_cancel.ML Thu Oct 31 16:54:22 2013 +0100
59.2 +++ b/src/HOL/Tools/group_cancel.ML Fri Nov 01 18:51:14 2013 +0100
59.3 @@ -25,7 +25,7 @@
59.4 val sub1 = @{lemma "(A::'a::ab_group_add) == k + a ==> A - b == k + (a - b)"
59.5 by (simp only: add_diff_eq)}
59.6 val sub2 = @{lemma "(B::'a::ab_group_add) == k + b ==> a - B == - k + (a - b)"
59.7 - by (simp only: diff_minus minus_add add_ac)}
59.8 + by (simp only: minus_add diff_conv_add_uminus add_ac)}
59.9 val neg1 = @{lemma "(A::'a::ab_group_add) == k + a ==> - A == - k + - a"
59.10 by (simp only: minus_add_distrib)}
59.11 val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
60.1 --- a/src/HOL/Tools/numeral_simprocs.ML Thu Oct 31 16:54:22 2013 +0100
60.2 +++ b/src/HOL/Tools/numeral_simprocs.ML Fri Nov 01 18:51:14 2013 +0100
60.3 @@ -220,7 +220,7 @@
60.4 val minus_simps = [@{thm minus_zero}, @{thm minus_one}, @{thm minus_numeral}, @{thm minus_neg_numeral}];
60.5
60.6 (*To let us treat subtraction as addition*)
60.7 -val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}];
60.8 +val diff_simps = [@{thm diff_conv_add_uminus}, @{thm minus_add_distrib}, @{thm minus_minus}];
60.9
60.10 (*To let us treat division as multiplication*)
60.11 val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
60.12 @@ -719,7 +719,7 @@
60.13 @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
60.14 @{thm "times_divide_times_eq"},
60.15 @{thm "divide_divide_eq_right"},
60.16 - @{thm "diff_minus"}, @{thm "minus_divide_left"},
60.17 + @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"},
60.18 @{thm "add_divide_distrib"} RS sym,
60.19 @{thm field_divide_inverse} RS sym, @{thm inverse_divide},
60.20 Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute}))))
61.1 --- a/src/HOL/Transcendental.thy Thu Oct 31 16:54:22 2013 +0100
61.2 +++ b/src/HOL/Transcendental.thy Fri Nov 01 18:51:14 2013 +0100
61.3 @@ -453,7 +453,7 @@
61.4 apply simp
61.5 apply (simp only: lemma_termdiff1 setsum_right_distrib)
61.6 apply (rule setsum_cong [OF refl])
61.7 - apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
61.8 + apply (simp add: less_iff_Suc_add)
61.9 apply (clarify)
61.10 apply (simp add: setsum_right_distrib lemma_realpow_diff_sumr2 mult_ac
61.11 del: setsum_op_ivl_Suc power_Suc)
61.12 @@ -1129,8 +1129,7 @@
61.13 by (rule inverse_unique [symmetric], simp add: mult_exp_exp)
61.14
61.15 lemma exp_diff: "exp (x - y) = exp x / exp y"
61.16 - unfolding diff_minus divide_inverse
61.17 - by (simp add: exp_add exp_minus)
61.18 + using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
61.19
61.20
61.21 subsubsection {* Properties of the Exponential Function on Reals *}
61.22 @@ -2410,13 +2409,13 @@
61.23 using sin_cos_minus_lemma [where x=x] by simp
61.24
61.25 lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
61.26 - by (simp add: diff_minus sin_add)
61.27 + using sin_add [of x "- y"] by simp
61.28
61.29 lemma sin_diff2: "sin (x - y) = cos y * sin x - sin y * cos x"
61.30 by (simp add: sin_diff mult_commute)
61.31
61.32 lemma cos_diff: "cos (x - y) = cos x * cos y + sin x * sin y"
61.33 - by (simp add: diff_minus cos_add)
61.34 + using cos_add [of x "- y"] by simp
61.35
61.36 lemma cos_diff2: "cos (x - y) = cos y * cos x + sin y * sin x"
61.37 by (simp add: cos_diff mult_commute)
61.38 @@ -2526,8 +2525,9 @@
61.39 by (simp add: inverse_eq_divide less_divide_eq)
61.40 }
61.41 note *** = this
61.42 + have [simp]: "\<And>x y::real. 0 < x - y \<longleftrightarrow> y < x" by arith
61.43 from ** show ?thesis by (rule sumr_pos_lt_pair)
61.44 - (simp add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] ***)
61.45 + (simp add: divide_inverse mult_assoc [symmetric] ***)
61.46 qed
61.47 ultimately have "0 < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
61.48 by (rule order_less_trans)
61.49 @@ -2810,7 +2810,7 @@
61.50 apply (cut_tac x="-x" in cos_zero_lemma, simp, simp)
61.51 apply (force simp add: minus_equation_iff [of x])
61.52 apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc distrib_right)
61.53 -apply (auto simp add: cos_add)
61.54 +apply (auto simp add: cos_diff cos_add)
61.55 done
61.56
61.57 (* ditto: but to a lesser extent *)
61.58 @@ -3833,7 +3833,7 @@
61.59 by (rule DERIV_arctan_suminf[OF `0 < r` `r < 1` `\<bar>x\<bar> < r`])
61.60 from DERIV_add_minus[OF this DERIV_arctan]
61.61 show "DERIV (\<lambda> x. suminf (?c x) - arctan x) x :> 0"
61.62 - unfolding diff_minus by auto
61.63 + by auto
61.64 qed
61.65 hence DERIV_in_rball: "\<forall> y. a \<le> y \<and> y \<le> b \<longrightarrow> DERIV (\<lambda> x. suminf (?c x) - arctan x) y :> 0"
61.66 using `-r < a` `b < r` by auto
61.67 @@ -3922,9 +3922,10 @@
61.68 }
61.69 hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
61.70 moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
61.71 - unfolding diff_minus divide_inverse
61.72 + unfolding diff_conv_add_uminus divide_inverse
61.73 by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan
61.74 - isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum)
61.75 + isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum
61.76 + simp del: add_uminus_conv_diff)
61.77 ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
61.78 by (rule LIM_less_bound)
61.79 hence "?diff 1 n \<le> ?a 1 n" by auto
62.1 --- a/src/HOL/Word/Bit_Representation.thy Thu Oct 31 16:54:22 2013 +0100
62.2 +++ b/src/HOL/Word/Bit_Representation.thy Fri Nov 01 18:51:14 2013 +0100
62.3 @@ -636,12 +636,12 @@
62.4 unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp
62.5
62.6 lemma sb_dec_lem:
62.7 - "(0::int) <= - (2^k) + a ==> (a + 2^k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
62.8 - by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified])
62.9 + "(0::int) \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
62.10 + using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp
62.11
62.12 lemma sb_dec_lem':
62.13 - "(2::int) ^ k <= a ==> (a + 2 ^ k) mod (2 * 2 ^ k) <= - (2 ^ k) + a"
62.14 - by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified])
62.15 + "(2::int) ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
62.16 + by (rule sb_dec_lem) simp
62.17
62.18 lemma sbintrunc_dec:
62.19 "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
63.1 --- a/src/HOL/Word/WordBitwise.thy Thu Oct 31 16:54:22 2013 +0100
63.2 +++ b/src/HOL/Word/WordBitwise.thy Fri Nov 01 18:51:14 2013 +0100
63.3 @@ -65,7 +65,7 @@
63.4
63.5 lemma bl_word_sub:
63.6 "to_bl (x - y) = to_bl (x + (- y))"
63.7 - by (simp add: diff_def)
63.8 + by simp
63.9
63.10 lemma rbl_word_1:
63.11 "rev (to_bl (1 :: ('a :: len0) word))
64.1 --- a/src/HOL/ex/Dedekind_Real.thy Thu Oct 31 16:54:22 2013 +0100
64.2 +++ b/src/HOL/ex/Dedekind_Real.thy Fri Nov 01 18:51:14 2013 +0100
64.3 @@ -1520,14 +1520,14 @@
64.4 have "z + x - (z + y) = (z + -z) + (x - y)"
64.5 by (simp add: algebra_simps)
64.6 with le show ?thesis
64.7 - by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"] diff_minus)
64.8 + by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"])
64.9 qed
64.10
64.11 lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)"
64.12 -by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus)
64.13 +by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S])
64.14
64.15 lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))"
64.16 -by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus)
64.17 +by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S])
64.18
64.19 lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
64.20 apply (cases x, cases y)
64.21 @@ -1543,7 +1543,7 @@
64.22 apply (rule real_sum_gt_zero_less)
64.23 apply (drule real_less_sum_gt_zero [of x y])
64.24 apply (drule real_mult_order, assumption)
64.25 -apply (simp add: distrib_left)
64.26 +apply (simp add: algebra_simps)
64.27 done
64.28
64.29 instantiation real :: distrib_lattice
65.1 --- a/src/HOL/ex/Gauge_Integration.thy Thu Oct 31 16:54:22 2013 +0100
65.2 +++ b/src/HOL/ex/Gauge_Integration.thy Fri Nov 01 18:51:14 2013 +0100
65.3 @@ -511,9 +511,9 @@
65.4 case False
65.5 then have "inverse (z - x) * (f z - f x - f' x * (z - x)) = (f z - f x) / (z - x) - f' x"
65.6 apply (subst mult_commute)
65.7 - apply (simp add: distrib_right diff_minus)
65.8 + apply (simp add: left_diff_distrib)
65.9 apply (simp add: mult_assoc divide_inverse)
65.10 - apply (simp add: distrib_right)
65.11 + apply (simp add: ring_distribs)
65.12 done
65.13 moreover from False `\<bar>z - x\<bar> < s` have "\<bar>(f z - f x) / (z - x) - f' x\<bar> < e / 2"
65.14 by (rule P)