--- a/src/HOL/Complex.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Complex.thy Mon Jul 19 16:09:44 2010 +0200
@@ -686,12 +686,12 @@
by (simp add: divide_inverse rcis_def)
lemma cis_divide: "cis a / cis b = cis (a - b)"
-by (simp add: complex_divide_def cis_mult diff_def)
+by (simp add: complex_divide_def cis_mult diff_minus)
lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
apply (simp add: complex_divide_def)
apply (case_tac "r2=0", simp)
-apply (simp add: rcis_inverse rcis_mult diff_def)
+apply (simp add: rcis_inverse rcis_mult diff_minus)
done
lemma Re_cis [simp]: "Re(cis a) = cos a"
--- a/src/HOL/Decision_Procs/Approximation.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Jul 19 16:09:44 2010 +0200
@@ -18,7 +18,7 @@
shows "a 0 - x * (\<Sum> i=0..<n. (-1)^i * a (Suc i) * x^i) = (\<Sum> i=0..<Suc n. (-1)^i * a i * x^i)"
proof -
have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)" by auto
- show ?thesis unfolding setsum_right_distrib shift_pow diff_def setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
+ show ?thesis unfolding setsum_right_distrib shift_pow diff_minus setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
setsum_reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n *a n * x^n"] by auto
qed
@@ -45,14 +45,14 @@
case 0 thus ?case unfolding lb_0 ub_0 horner.simps by auto
next
case (Suc n)
- have "?lb (Suc n) j' \<le> ?horner (Suc n) j'" unfolding lb_Suc ub_Suc horner.simps real_of_float_sub diff_def
+ have "?lb (Suc n) j' \<le> ?horner (Suc n) j'" unfolding lb_Suc ub_Suc horner.simps real_of_float_sub diff_minus
proof (rule add_mono)
show "real (lapprox_rat prec 1 (int (f j'))) \<le> 1 / real (f j')" using lapprox_rat[of prec 1 "int (f j')"] by auto
from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct2] `0 \<le> real x`
show "- real (x * ub n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x) \<le> - (real x * horner F G n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) (real x))"
unfolding real_of_float_mult neg_le_iff_le by (rule mult_left_mono)
qed
- moreover have "?horner (Suc n) j' \<le> ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps real_of_float_sub diff_def
+ moreover have "?horner (Suc n) j' \<le> ?ub (Suc n) j'" unfolding ub_Suc ub_Suc horner.simps real_of_float_sub diff_minus
proof (rule add_mono)
show "1 / real (f j') \<le> real (rapprox_rat prec 1 (int (f j')))" using rapprox_rat[of 1 "int (f j')" prec] by auto
from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct1] `0 \<le> real x`
@@ -1213,7 +1213,7 @@
round_down[of prec "lb_pi prec"] by auto
hence "real ?lx \<le> x - real k * 2 * pi \<and> x - real k * 2 * pi \<le> real ?ux"
using x by (cases "k = 0") (auto intro!: add_mono
- simp add: diff_def k[symmetric] less_float_def)
+ simp add: diff_minus k[symmetric] less_float_def)
note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
hence lx_less_ux: "real ?lx \<le> real ?ux" by (rule order_trans)
@@ -1227,7 +1227,7 @@
also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus diff_def mult_minus_left)
+ cos_minus diff_minus mult_minus_left)
finally have "real (lb_cos prec (- ?lx)) \<le> cos x"
unfolding cos_periodic_int . }
note negative_lx = this
@@ -1240,7 +1240,7 @@
have "cos (x + real (-k) * 2 * pi) \<le> cos (real ?lx)"
using cos_monotone_0_pi'[OF lx_0 lx pi_x]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus diff_def mult_minus_left)
+ cos_minus diff_minus mult_minus_left)
also have "\<dots> \<le> real (ub_cos prec ?lx)"
using lb_cos[OF lx_0 pi_lx] by simp
finally have "cos x \<le> real (ub_cos prec ?lx)"
@@ -1255,7 +1255,7 @@
have "cos (x + real (-k) * 2 * pi) \<le> cos (real (- ?ux))"
using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus diff_def mult_minus_left)
+ cos_minus diff_minus mult_minus_left)
also have "\<dots> \<le> real (ub_cos prec (- ?ux))"
using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
finally have "cos x \<le> real (ub_cos prec (- ?ux))"
@@ -1272,7 +1272,7 @@
also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus diff_def mult_minus_left)
+ cos_minus diff_minus mult_minus_left)
finally have "real (lb_cos prec ?ux) \<le> cos x"
unfolding cos_periodic_int . }
note positive_ux = this
@@ -1347,7 +1347,7 @@
also have "\<dots> \<le> cos (real (?ux - 2 * ?lpi))"
using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
by (simp only: real_of_float_minus real_of_int_minus real_of_one
- number_of_Min diff_def mult_minus_left mult_1_left)
+ number_of_Min diff_minus mult_minus_left mult_1_left)
also have "\<dots> = cos (real (- (?ux - 2 * ?lpi)))"
unfolding real_of_float_minus cos_minus ..
also have "\<dots> \<le> real (ub_cos prec (- (?ux - 2 * ?lpi)))"
@@ -1391,7 +1391,7 @@
also have "\<dots> \<le> cos (real (?lx + 2 * ?lpi))"
using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
by (simp only: real_of_float_minus real_of_int_minus real_of_one
- number_of_Min diff_def mult_minus_left mult_1_left)
+ number_of_Min diff_minus mult_minus_left mult_1_left)
also have "\<dots> \<le> real (ub_cos prec (?lx + 2 * ?lpi))"
using lb_cos[OF lx_0 pi_lx] by simp
finally show ?thesis unfolding u by (simp add: real_of_float_max)
@@ -2091,12 +2091,12 @@
unfolding divide_inverse interpret_floatarith.simps ..
lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
- unfolding diff_def interpret_floatarith.simps ..
+ unfolding diff_minus interpret_floatarith.simps ..
lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
sin (interpret_floatarith a vs)"
unfolding sin_cos_eq interpret_floatarith.simps
- interpret_floatarith_divide interpret_floatarith_diff diff_def
+ interpret_floatarith_divide interpret_floatarith_diff diff_minus
by auto
lemma interpret_floatarith_tan:
--- a/src/HOL/Decision_Procs/Cooper.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Mon Jul 19 16:09:44 2010 +0200
@@ -1356,7 +1356,7 @@
also have "\<dots> = (j dvd (- (c*x - ?e)))"
by (simp only: dvd_minus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
- apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
+ apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
by (simp add: algebra_simps)
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
@@ -1368,7 +1368,7 @@
also have "\<dots> = (j dvd (- (c*x - ?e)))"
by (simp only: dvd_minus_iff)
also have "\<dots> = (j dvd (c* (- x)) + ?e)"
- apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_def zadd_ac zminus_zadd_distrib)
+ apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
by (simp add: algebra_simps)
also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
--- a/src/HOL/Decision_Procs/MIR.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Mon Jul 19 16:09:44 2010 +0200
@@ -1768,7 +1768,7 @@
have th: "(real a + b >0) = (real (-a) + (-b)< 0)" by arith
show ?thesis using myless[rule_format, where b="real (floor b)"]
by (simp only:th split_int_less_real'[where a="-a" and b="-b"])
- (simp add: algebra_simps diff_def[symmetric],arith)
+ (simp add: algebra_simps diff_minus[symmetric],arith)
qed
lemma split_int_le_real:
@@ -1795,7 +1795,7 @@
proof-
have th: "(real a + b \<ge>0) = (real (-a) + (-b) \<le> 0)" by arith
show ?thesis by (simp only: th split_int_le_real'[where a="-a" and b="-b"])
- (simp add: algebra_simps diff_def[symmetric],arith)
+ (simp add: algebra_simps diff_minus[symmetric],arith)
qed
lemma split_int_eq_real: "(real (a::int) = b) = ( a = floor b \<and> b = real (floor b))" (is "?l = ?r")
@@ -1828,13 +1828,13 @@
{assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
- 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_def)
+ 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)
finally have ?case using l by simp}
moreover
{assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Lt a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Lt a) = (real (?c * i) + (?N ?r) < 0)" using Ia by (simp add: Let_def split_def)
- also from cn cnz have "\<dots> = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_def[symmetric] add_ac, arith)
+ also from cn cnz have "\<dots> = (?I (?l (Lt a)))" by (simp only: split_int_less_real'[where a="?c*i" and b="?N ?r"]) (simp add: Ia Let_def split_def diff_minus[symmetric] add_ac, arith)
finally have ?case using l by simp}
ultimately show ?case by blast
next
@@ -1853,13 +1853,13 @@
{assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
- 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_def)
+ 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)
finally have ?case using l by simp}
moreover
{assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Le a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Le a) = (real (?c * i) + (?N ?r) \<le> 0)" using Ia by (simp add: Let_def split_def)
- 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_def[symmetric] add_ac ,arith)
+ 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)
finally have ?case using l by simp}
ultimately show ?case by blast
next
@@ -1878,13 +1878,13 @@
{assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
- 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_def)
+ 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)
finally have ?case using l by simp}
moreover
{assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Gt a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Gt a) = (real (?c * i) + (?N ?r) > 0)" using Ia by (simp add: Let_def split_def)
- 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_def[symmetric] add_ac, arith)
+ 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)
finally have ?case using l by simp}
ultimately show ?case by blast
next
@@ -1903,13 +1903,13 @@
{assume cp: "?c > 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
- 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_def)
+ 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)
finally have ?case using l by simp}
moreover
{assume cn: "?c < 0" and cnz: "?c\<noteq>0" hence l: "?L (?l (Ge a))"
by (simp add: nb Let_def split_def isint_Floor isint_neg)
have "?I (Ge a) = (real (?c * i) + (?N ?r) \<ge> 0)" using Ia by (simp add: Let_def split_def)
- 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_def[symmetric] add_ac, arith)
+ 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)
finally have ?case using l by simp}
ultimately show ?case by blast
next
@@ -3337,7 +3337,7 @@
hence pid: "c*i + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + ?fe = j1" by auto
hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - ?N i e + real j1"
- by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps)
+ by (simp only: diff_minus[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps)
with nob have ?case by blast }
ultimately show ?case by blast
next
@@ -3360,11 +3360,11 @@
hence pid: "c*i + 1 + ?fe \<le> c*d" by (simp only: real_of_int_le_iff)
with pi' have "\<exists> j1\<in> {1 .. c*d}. c*i + 1+ ?fe = j1" by auto
hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) + 1= - ?N i e + real j1"
- by (simp only: diff_def[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps real_of_one)
+ by (simp only: diff_minus[symmetric] real_of_int_mult real_of_int_add real_of_int_inject[symmetric] ei[simplified isint_iff] algebra_simps real_of_one)
hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = (- ?N i e + real j1) - 1"
- by (simp only: algebra_simps diff_def[symmetric])
+ by (simp only: algebra_simps diff_minus[symmetric])
hence "\<exists> j1\<in> {1 .. c*d}. real (c*i) = - 1 - ?N i e + real j1"
- by (simp only: add_ac diff_def)
+ by (simp only: add_ac diff_minus)
with nob have ?case by blast }
ultimately show ?case by blast
next
@@ -3822,7 +3822,7 @@
by(simp only: myl[rule_format, where b="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)"])
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])
hence "\<exists> j\<in> {n.. 0}. ?I (?p (p,n,s) j)"
- using pns by (simp add: fp_def nn diff_def add_ac mult_ac numfloor numadd numneg
+ using pns by (simp add: fp_def nn diff_minus add_ac mult_ac numfloor numadd numneg
del: diff_less_0_iff_less diff_le_0_iff_le)
then obtain "j" where j_def: "j\<in> {n .. 0} \<and> ?I (?p (p,n,s) j)" by blast
hence "\<exists>x \<in> {?p (p,n,s) j |j. n\<le> j \<and> j \<le> 0 }. ?I x" by auto
@@ -4036,7 +4036,7 @@
from foldr_disj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
have "Ifm (x#bs) (DVDJ i n s) = (\<exists> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))"
by (simp add: iupt_set np DVDJ_def del: iupt.simps)
- also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: algebra_simps diff_def[symmetric])
+ also have "\<dots> = (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s)))" by (simp add: algebra_simps diff_minus[symmetric])
also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"]
have "\<dots> = (real i rdvd real n * x - (-?s))" by simp
finally show ?thesis by simp
@@ -4051,7 +4051,7 @@
from foldr_conj_map[where xs="iupt(0,n - 1)" and bs="x#bs" and f="?f"]
have "Ifm (x#bs) (NDVDJ i n s) = (\<forall> j\<in> {0 .. (n - 1)}. Ifm (x#bs) (?f j))"
by (simp add: iupt_set np NDVDJ_def del: iupt.simps)
- also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: algebra_simps diff_def[symmetric])
+ also have "\<dots> = (\<not> (\<exists> j\<in> {0 .. (n - 1)}. real n * x = (- ?s) - real (floor (- ?s)) + real j \<and> real i rdvd real (j - floor (- ?s))))" by (simp add: algebra_simps diff_minus[symmetric])
also from rdvd01_cs[OF xp x1 np, where i="i" and s="-?s"]
have "\<dots> = (\<not> (real i rdvd real n * x - (-?s)))" by simp
finally show ?thesis by simp
@@ -5093,7 +5093,7 @@
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")
proof-
have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real i)#bs) (exsplit p))"
- by (simp add: myless[rule_format, where b="1"] myless[rule_format, where b="0"] add_ac diff_def)
+ by (simp add: myless[rule_format, where b="1"] myless[rule_format, where b="0"] add_ac diff_minus)
also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real i + x) #bs) p)"
by (simp only: exsplit[OF qf] add_ac)
also have "\<dots> = (\<exists> x. Ifm (x#bs) p)"
--- a/src/HOL/Decision_Procs/mir_tac.ML Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Mon Jul 19 16:09:44 2010 +0200
@@ -36,7 +36,7 @@
@{thm "divide_zero"},
@{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"},
@{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
- @{thm "diff_def"}, @{thm "minus_divide_left"}]
+ @{thm "diff_minus"}, @{thm "minus_divide_left"}]
val comp_ths = ths @ comp_arith @ simp_thms
--- a/src/HOL/Deriv.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Deriv.thy Mon Jul 19 16:09:44 2010 +0200
@@ -57,7 +57,7 @@
lemma DERIV_diff:
"\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x :> D - E"
-by (simp only: diff_def DERIV_add DERIV_minus)
+by (simp only: diff_minus DERIV_add DERIV_minus)
lemma DERIV_add_minus:
"\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + - g x) x :> D + - E"
@@ -1269,7 +1269,7 @@
and "f b - f a = (b - a) * l"
by auto
from prems have "~(l >= 0)"
- by (metis diff_self le_eqI le_iff_diff_le_0 order_antisym linear
+ by (metis diff_self diff_eq_diff_less_eq' le_iff_diff_le_0 order_antisym linear
split_mult_pos_le)
with prems show False
by (metis DERIV_unique order_less_imp_le)
--- a/src/HOL/Hahn_Banach/Vector_Space.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy Mon Jul 19 16:09:44 2010 +0200
@@ -118,7 +118,7 @@
proof -
assume x: "x \<in> V"
have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
- by (simp add: diff_def)
+ by (simp add: diff_minus)
also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
by (rule add_mult_distrib2)
also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
--- a/src/HOL/Import/HOL/poly.imp Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Import/HOL/poly.imp Mon Jul 19 16:09:44 2010 +0200
@@ -13,7 +13,7 @@
"poly_add" > "poly_add_primdef"
"poly" > "poly_primdef"
"normalize" > "normalize_def"
- "diff" > "diff_def"
+ "diff" > "diff_minus"
"degree" > "degree_def"
"##" > "##_def"
--- a/src/HOL/Import/HOL/real.imp Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Import/HOL/real.imp Mon Jul 19 16:09:44 2010 +0200
@@ -25,7 +25,7 @@
"sumc" > "HOL4Real.real.sumc"
"sum_def" > "HOL4Real.real.sum_def"
"sum" > "HOL4Real.real.sum"
- "real_sub" > "Groups.diff_def"
+ "real_sub" > "Groups.diff_minus"
"real_of_num" > "HOL4Compat.real_of_num"
"real_lte" > "HOL4Compat.real_lte"
"real_lt" > "Orderings.linorder_not_le"
--- a/src/HOL/Int.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Int.thy Mon Jul 19 16:09:44 2010 +0200
@@ -566,7 +566,7 @@
obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
apply (cases z rule: eq_Abs_Integ)
apply (rule_tac m=x and n=y in diff)
-apply (simp add: int_def diff_def minus add)
+apply (simp add: int_def minus add diff_minus)
done
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Mon Jul 19 16:09:44 2010 +0200
@@ -221,12 +221,12 @@
from unimodular_reduce_norm[OF th0] o
have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
- apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_def)
+ apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_minus)
apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
apply (rule_tac x="- ii" in exI, simp add: m power_mult)
- apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_def)
- apply (rule_tac x="ii" in exI, simp add: m power_mult diff_def)
+ apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_minus)
+ apply (rule_tac x="ii" in exI, simp add: m power_mult diff_minus)
done
then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
let ?w = "v / complex_of_real (root n (cmod b))"
@@ -959,7 +959,7 @@
lemma mpoly_sub_conv:
"poly p (x::complex) - poly q x \<equiv> poly p x + -1 * poly q x"
- by (simp add: diff_def)
+ by (simp add: diff_minus)
lemma poly_pad_rule: "poly p x = 0 ==> poly (pCons 0 p) x = (0::complex)" by simp
--- a/src/HOL/Library/Univ_Poly.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Mon Jul 19 16:09:44 2010 +0200
@@ -204,7 +204,7 @@
from Cons.hyps[rule_format, of x]
obtain q r where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast
have "h#x#xs = [a*r + h] +++ [-a, 1] *** (r#q)"
- using qr by(cases q, simp_all add: algebra_simps diff_def[symmetric]
+ using qr by(cases q, simp_all add: algebra_simps diff_minus[symmetric]
minus_mult_left[symmetric] right_minus)
hence "\<exists>q r. h#x#xs = [r] +++ [-a, 1] *** q" by blast}
thus ?case by blast
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Jul 19 16:09:44 2010 +0200
@@ -523,7 +523,7 @@
lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def)
lemma linear_sub: "linear f ==> f(x - y) = f x - f y"
- by (simp add: diff_def linear_add linear_neg)
+ by (simp add: diff_minus linear_add linear_neg)
lemma linear_setsum:
assumes lf: "linear f" and fS: "finite S"
@@ -592,10 +592,10 @@
by (simp add: eq_add_iff field_simps)
lemma bilinear_lsub: "bilinear h ==> h (x - y) z = h x z - h y z"
- by (simp add: diff_def bilinear_ladd bilinear_lneg)
+ by (simp add: diff_minus bilinear_ladd bilinear_lneg)
lemma bilinear_rsub: "bilinear h ==> h z (x - y) = h z x - h z y"
- by (simp add: diff_def bilinear_radd bilinear_rneg)
+ by (simp add: diff_minus bilinear_radd bilinear_rneg)
lemma bilinear_setsum:
assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T"
@@ -902,7 +902,7 @@
by (metis scaleR_minus1_left subspace_mul)
lemma subspace_sub: "subspace S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
- by (metis diff_def subspace_add subspace_neg)
+ by (metis diff_minus subspace_add subspace_neg)
lemma (in real_vector) subspace_setsum:
assumes sA: "subspace A" and fB: "finite B"
@@ -3082,7 +3082,7 @@
from infnorm_triangle[of "x - y" " y"] infnorm_triangle[of "x - y" "-x"]
have ths: "infnorm x \<le> infnorm (x - y) + infnorm y"
"infnorm y \<le> infnorm (x - y) + infnorm x"
- by (simp_all add: field_simps infnorm_neg diff_def[symmetric])
+ by (simp_all add: field_simps infnorm_neg diff_minus[symmetric])
from th[OF ths] show ?thesis .
qed
--- a/src/HOL/NSA/HDeriv.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/NSA/HDeriv.thy Mon Jul 19 16:09:44 2010 +0200
@@ -174,7 +174,7 @@
apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def)
apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec)
apply (drule_tac b = "star_of Da" and d = "star_of Db" in approx_add)
-apply (auto simp add: diff_def add_ac)
+apply (auto simp add: diff_minus add_ac)
done
text{*Product of functions - Proof is trivial but tedious
@@ -234,7 +234,7 @@
hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D"
by (rule NSLIM_minus)
have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
- by (simp add: minus_divide_left diff_def)
+ by (simp add: minus_divide_left diff_minus)
with deriv
show "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
qed
@@ -353,7 +353,7 @@
(*apply (auto simp add: starfun_inverse_inverse realpow_two
simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])*)
apply (simp add: inverse_add nonzero_inverse_mult_distrib [symmetric] power_Suc
- nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_def
+ nonzero_inverse_minus_eq [symmetric] add_ac mult_ac diff_minus
del: inverse_mult_distrib inverse_minus_eq
minus_mult_left [symmetric] minus_mult_right [symmetric])
apply (subst mult_commute, simp add: nonzero_mult_divide_cancel_right)
--- a/src/HOL/NSA/HLim.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/NSA/HLim.thy Mon Jul 19 16:09:44 2010 +0200
@@ -73,7 +73,7 @@
lemma NSLIM_diff:
"\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
-by (simp only: diff_def NSLIM_add NSLIM_minus)
+by (simp only: diff_minus NSLIM_add NSLIM_minus)
lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
by (simp only: NSLIM_add NSLIM_minus)
@@ -245,7 +245,7 @@
apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
- prefer 2 apply (simp add: add_commute diff_def [symmetric])
+ prefer 2 apply (simp add: add_commute diff_minus [symmetric])
apply (rule_tac x = x in star_cases)
apply (rule_tac [2] x = x in star_cases)
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
--- a/src/HOL/NSA/HTranscendental.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/NSA/HTranscendental.thy Mon Jul 19 16:09:44 2010 +0200
@@ -258,7 +258,7 @@
simp add: mult_assoc)
apply (rule approx_add_right_cancel [where d="-1"])
apply (rule approx_sym [THEN [2] approx_trans2])
-apply (auto simp add: diff_def mem_infmal_iff)
+apply (auto simp add: diff_minus mem_infmal_iff)
done
lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
@@ -450,7 +450,7 @@
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
simp add: mult_assoc)
apply (rule approx_add_right_cancel [where d = "-1"])
-apply (simp add: diff_def)
+apply (simp add: diff_minus)
done
lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
--- a/src/HOL/NSA/NSA.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/NSA/NSA.thy Mon Jul 19 16:09:44 2010 +0200
@@ -368,7 +368,7 @@
lemma Infinitesimal_diff:
"[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
-by (simp add: diff_def Infinitesimal_add)
+by (simp add: diff_minus Infinitesimal_add)
lemma Infinitesimal_mult:
fixes x y :: "'a::real_normed_algebra star"
@@ -637,7 +637,7 @@
lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"
apply (simp add: approx_def)
apply (drule (1) Infinitesimal_add)
-apply (simp add: diff_def)
+apply (simp add: diff_minus)
done
lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"
@@ -714,7 +714,7 @@
lemma approx_minus: "a @= b ==> -a @= -b"
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
apply (drule approx_minus_iff [THEN iffD1])
-apply (simp add: add_commute diff_def)
+apply (simp add: add_commute diff_minus)
done
lemma approx_minus2: "-a @= -b ==> a @= b"
--- a/src/HOL/NSA/NSCA.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/NSA/NSCA.thy Mon Jul 19 16:09:44 2010 +0200
@@ -178,7 +178,7 @@
"u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
apply (drule approx_approx_zero_iff [THEN iffD1])
apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
-apply (auto simp add: mem_infmal_iff [symmetric] diff_def)
+apply (auto simp add: mem_infmal_iff [symmetric] diff_minus)
apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1])
apply (auto simp add: diff_minus [symmetric])
done
--- a/src/HOL/Probability/Borel.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Probability/Borel.thy Mon Jul 19 16:09:44 2010 +0200
@@ -357,7 +357,7 @@
borel_measurable_uminus_borel_measurable f g)
finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
show ?thesis
- apply (simp add: times_eq_sum_squares diff_def)
+ apply (simp add: times_eq_sum_squares diff_minus)
using 1 2 apply (simp add: borel_measurable_add_borel_measurable)
done
qed
@@ -366,7 +366,7 @@
assumes f: "f \<in> borel_measurable M"
assumes g: "g \<in> borel_measurable M"
shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
-unfolding diff_def
+unfolding diff_minus
by (fast intro: borel_measurable_add_borel_measurable
borel_measurable_uminus_borel_measurable f g)
@@ -626,11 +626,11 @@
proof -
from assms have "y - z > 0" by simp
hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
- unfolding incseq_def LIMSEQ_def dist_real_def diff_def
+ unfolding incseq_def LIMSEQ_def dist_real_def diff_minus
by simp
have "\<forall>m. x m \<le> y" using incseq_le assms by auto
hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
- by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le diff_def)
+ by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le diff_minus)
from A B show ?thesis by auto
qed
--- a/src/HOL/RComplete.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/RComplete.thy Mon Jul 19 16:09:44 2010 +0200
@@ -153,7 +153,7 @@
have "x = y-(y-x)" by simp
also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith
also have "\<dots> = real p / real q"
- by (simp only: inverse_eq_divide diff_def real_of_nat_Suc
+ by (simp only: inverse_eq_divide diff_minus real_of_nat_Suc
minus_divide_left add_divide_distrib[THEN sym]) simp
finally have "x<r" by (unfold r_def)
have "p<Suc p" .. also note main[THEN sym]
--- a/src/HOL/RealVector.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/RealVector.thy Mon Jul 19 16:09:44 2010 +0200
@@ -30,7 +30,7 @@
qed
lemma diff: "f (x - y) = f x - f y"
-by (simp add: diff_def add minus)
+by (simp add: add minus diff_minus)
lemma setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))"
apply (cases "finite A")
--- a/src/HOL/SEQ.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/SEQ.thy Mon Jul 19 16:09:44 2010 +0200
@@ -506,8 +506,7 @@
from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
by blast
thus "lim f \<le> x"
- by (metis add_cancel_end add_minus_cancel diff_def linorder_linear
- linorder_not_le minus_diff_eq abs_diff_less_iff fn_le)
+ by (metis 1 LIMSEQ_le_const2 fn_le)
qed
qed
@@ -971,7 +970,7 @@
apply (rule_tac x = K in exI, simp)
apply (rule exI [where x = 0], auto)
apply (erule order_less_le_trans, simp)
-apply (drule_tac x=n in spec, fold diff_def)
+apply (drule_tac x=n in spec, fold diff_minus)
apply (drule order_trans [OF norm_triangle_ineq2])
apply simp
done
--- a/src/HOL/SupInf.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/SupInf.thy Mon Jul 19 16:09:44 2010 +0200
@@ -417,7 +417,7 @@
also have "... \<le> e"
apply (rule Sup_asclose)
apply (auto simp add: S)
- apply (metis abs_minus_add_cancel b add_commute diff_def)
+ apply (metis abs_minus_add_cancel b add_commute diff_minus)
done
finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
thus ?thesis
--- a/src/HOL/Tools/numeral_simprocs.ML Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Mon Jul 19 16:09:44 2010 +0200
@@ -734,7 +734,7 @@
@{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
@{thm "times_divide_times_eq"},
@{thm "divide_divide_eq_right"},
- @{thm "diff_def"}, @{thm "minus_divide_left"},
+ @{thm "diff_minus"}, @{thm "minus_divide_left"},
@{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
@{thm field_divide_inverse} RS sym, @{thm inverse_divide},
Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute}))))
--- a/src/HOL/Transcendental.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Transcendental.thy Mon Jul 19 16:09:44 2010 +0200
@@ -2952,7 +2952,7 @@
}
hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
- unfolding diff_def divide_inverse
+ unfolding diff_minus divide_inverse
by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum)
ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound)
hence "?diff 1 n \<le> ?a 1 n" by auto
@@ -2968,7 +2968,7 @@
have "norm (?diff 1 n - 0) < r" by auto }
thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
qed
- from this[unfolded LIMSEQ_rabs_zero diff_def add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
+ from this[unfolded LIMSEQ_rabs_zero diff_minus add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)
--- a/src/HOL/Word/Misc_Numeric.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Mon Jul 19 16:09:44 2010 +0200
@@ -292,7 +292,7 @@
(* two alternative proofs of this *)
lemma RI_eq_diff': "(a, b) : Rep_Integ (int a - int b)"
- apply (unfold diff_def)
+ apply (unfold diff_minus)
apply (rule mem_same)
apply (rule RI_minus RI_add RI_int)+
apply simp
--- a/src/HOL/Word/Word.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Word/Word.thy Mon Jul 19 16:09:44 2010 +0200
@@ -1130,14 +1130,14 @@
lemmas wi_hom_syms = wi_homs [symmetric]
lemma word_sub_def: "a - b == a + - (b :: 'a :: len0 word)"
- unfolding word_sub_wi diff_def
+ unfolding word_sub_wi diff_minus
by (simp only : word_uint.Rep_inverse wi_hom_syms)
lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard]
lemma word_of_int_sub_hom:
"(word_of_int a) - word_of_int b = word_of_int (a - b)"
- unfolding word_sub_def diff_def by (simp only : wi_homs)
+ unfolding word_sub_def diff_minus by (simp only : wi_homs)
lemmas new_word_of_int_homs =
word_of_int_sub_hom wi_homs word_0_wi word_1_wi