--- a/src/HOL/Complex.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Complex.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Deriv.thy Wed Jul 21 16:50:42 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"
@@ -1255,8 +1255,9 @@
assume "~ f a \<le> f b"
assume "a = b"
with prems show False by auto
- next assume "~ f a \<le> f b"
- assume "a ~= b"
+next
+ assume A: "~ f a \<le> f b"
+ assume B: "a ~= b"
with assms have "EX l z. a < z & z < b & DERIV f z :> l
& f b - f a = (b - a) * l"
apply -
@@ -1266,11 +1267,11 @@
apply (metis differentiableI less_le)
done
then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
- and "f b - f a = (b - a) * l"
+ and C: "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
- split_mult_pos_le)
+ with A have "a < b" "f b < f a" by auto
+ with C have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps)
+ (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono real_add_left_mono real_le_linear real_le_refl)
with prems show False
by (metis DERIV_unique order_less_imp_le)
qed
--- a/src/HOL/Groups.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Groups.thy Wed Jul 21 16:50:42 2010 +0200
@@ -6,7 +6,7 @@
theory Groups
imports Orderings
-uses ("~~/src/Provers/Arith/abel_cancel.ML")
+uses ("~~/src/HOL/Tools/abel_cancel.ML")
begin
subsection {* Fact collections *}
@@ -146,8 +146,6 @@
class times =
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
-use "~~/src/Provers/Arith/abel_cancel.ML"
-
subsection {* Semigroups and Monoids *}
@@ -453,8 +451,13 @@
lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
by (simp add: algebra_simps)
+lemma diff_eq_diff_eq:
+ "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
+ by (auto simp add: algebra_simps)
+
end
+
subsection {* (Partially) Ordered Groups *}
text {*
@@ -755,14 +758,16 @@
lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
by (auto simp add: le_less minus_less_iff)
-lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"
+lemma diff_less_0_iff_less [simp, no_atp]:
+ "a - b < 0 \<longleftrightarrow> a < b"
proof -
- have "(a < b) = (a + (- b) < b + (-b))"
- by (simp only: add_less_cancel_right)
- also have "... = (a - b < 0)" by (simp add: diff_minus)
+ have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
+ also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
finally show ?thesis .
qed
+lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
+
lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
apply (subst less_iff_diff_less_0 [of a])
apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
@@ -781,11 +786,32 @@
lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
-lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
-by (simp add: algebra_simps)
+lemma diff_le_0_iff_le [simp, no_atp]:
+ "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
+ by (simp add: algebra_simps)
+
+lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
+
+lemma diff_eq_diff_less:
+ "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
+ by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
+
+lemma diff_eq_diff_less_eq:
+ "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
+ by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
end
+use "~~/src/HOL/Tools/abel_cancel.ML"
+
+simproc_setup abel_cancel_sum
+ ("a + b::'a::ab_group_add" | "a - b::'a::ab_group_add") =
+ {* fn phi => Abel_Cancel.sum_proc *}
+
+simproc_setup abel_cancel_relation
+ ("a < (b::'a::ordered_ab_group_add)" | "a \<le> (b::'a::ordered_ab_group_add)" | "c = (d::'b::ab_group_add)") =
+ {* fn phi => Abel_Cancel.rel_proc *}
+
class linordered_ab_semigroup_add =
linorder + ordered_ab_semigroup_add
@@ -1167,42 +1193,6 @@
end
-text {* Needed for abelian cancellation simprocs: *}
-
-lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
-apply (subst add_left_commute)
-apply (subst add_left_cancel)
-apply simp
-done
-
-lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"
-apply (subst add_cancel_21[of _ _ _ 0, simplified])
-apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified])
-done
-
-lemma less_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (x < y) = (x' < y')"
-by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y'])
-
-lemma le_eqI: "(x::'a::ordered_ab_group_add) - y = x' - y' \<Longrightarrow> (y <= x) = (y' <= x')"
-apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of y' x'])
-apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])
-done
-
-lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
-by (simp only: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
-
-lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
-by (simp add: diff_minus)
-
-lemma le_add_right_mono:
- assumes
- "a <= b + (c::'a::ordered_ab_group_add)"
- "c <= d"
- shows "a <= b + d"
- apply (rule_tac order_trans[where y = "b+c"])
- apply (simp_all add: prems)
- done
-
subsection {* Tools setup *}
@@ -1224,64 +1214,6 @@
by (auto intro: add_strict_right_mono add_strict_left_mono
add_less_le_mono add_le_less_mono add_strict_mono)
-text{*Simplification of @{term "x-y < 0"}, etc.*}
-lemmas diff_less_0_iff_less [simp, no_atp] = less_iff_diff_less_0 [symmetric]
-lemmas diff_le_0_iff_le [simp, no_atp] = le_iff_diff_le_0 [symmetric]
-
-ML {*
-structure ab_group_add_cancel = Abel_Cancel
-(
-
-(* term order for abelian groups *)
-
-fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
- [@{const_name Groups.zero}, @{const_name Groups.plus},
- @{const_name Groups.uminus}, @{const_name Groups.minus}]
- | agrp_ord _ = ~1;
-
-fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
-
-local
- val ac1 = mk_meta_eq @{thm add_assoc};
- val ac2 = mk_meta_eq @{thm add_commute};
- val ac3 = mk_meta_eq @{thm add_left_commute};
- fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) =
- SOME ac1
- | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) =
- if termless_agrp (y, x) then SOME ac3 else NONE
- | solve_add_ac thy _ (_ $ x $ y) =
- if termless_agrp (y, x) then SOME ac2 else NONE
- | solve_add_ac thy _ _ = NONE
-in
- val add_ac_proc = Simplifier.simproc @{theory}
- "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
-end;
-
-val eq_reflection = @{thm eq_reflection};
-
-val T = @{typ "'a::ab_group_add"};
-
-val cancel_ss = HOL_basic_ss settermless termless_agrp
- addsimprocs [add_ac_proc] addsimps
- [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
- @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
- @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
- @{thm minus_add_cancel}];
-
-val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
-
-val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
-
-val dest_eqI =
- fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
-
-);
-*}
-
-ML {*
- Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
-*}
-
code_modulename SML
Groups Arith
@@ -1291,4 +1223,9 @@
code_modulename Haskell
Groups Arith
+
+text {* Legacy *}
+
+lemmas diff_def = diff_minus
+
end
--- a/src/HOL/HOL.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/HOL.thy Wed Jul 21 16:50:42 2010 +0200
@@ -1928,7 +1928,7 @@
(Haskell "True" and "False" and "not"
and infixl 3 "&&" and infixl 2 "||"
and "!(if (_)/ then (_)/ else (_))")
- (Scala "true" and "false" and "'! _"
+ (Scala "true" and "false" and "'!/ _"
and infixl 3 "&&" and infixl 1 "||"
and "!(if ((_))/ (_)/ else (_))")
--- a/src/HOL/Hahn_Banach/Vector_Space.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy Wed Jul 21 16:50:42 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/Imperative_HOL/Heap_Monad.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Jul 21 16:50:42 2010 +0200
@@ -124,10 +124,10 @@
*}
definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
- crel_def: "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
+ crel_def: "crel c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
lemma crelI:
- "Heap_Monad.execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
+ "execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
by (simp add: crel_def)
lemma crelE:
@@ -300,9 +300,9 @@
using assms by (auto simp add: crel_def bind_def split: option.split_asm)
lemma execute_bind_eq_SomeI:
- assumes "Heap_Monad.execute f h = Some (x, h')"
- and "Heap_Monad.execute (g x) h' = Some (y, h'')"
- shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
+ assumes "execute f h = Some (x, h')"
+ and "execute (g x) h' = Some (y, h'')"
+ shows "execute (f \<guillemotright>= g) h = Some (y, h'')"
using assms by (simp add: bind_def)
lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
@@ -487,7 +487,7 @@
code_reserved Scala Heap
code_type Heap (Scala "Unit/ =>/ _")
-code_const bind (Scala "!Heap.bind((_), (_))")
+code_const bind (Scala "bind")
code_const return (Scala "('_: Unit)/ =>/ _")
code_const Heap_Monad.raise' (Scala "!error((_))")
--- a/src/HOL/Imperative_HOL/Ref.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Wed Jul 21 16:50:42 2010 +0200
@@ -296,11 +296,11 @@
text {* Scala *}
-code_type ref (Scala "!Heap.Ref[_]")
+code_type ref (Scala "!Ref[_]")
code_const Ref (Scala "!error(\"bare Ref\")")
-code_const ref (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))")
+code_const ref (Scala "('_: Unit)/ =>/ Ref((_))")
+code_const Ref.lookup (Scala "('_: Unit)/ =>/ lookup((_))")
+code_const Ref.update (Scala "('_: Unit)/ =>/ update((_), (_))")
end
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Wed Jul 21 16:50:42 2010 +0200
@@ -1014,6 +1014,6 @@
ML {* @{code test_2} () *}
ML {* @{code test_3} () *}
-export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell?
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
end
--- a/src/HOL/Import/HOL/poly.imp Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Import/HOL/poly.imp Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Import/HOL/real.imp Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Int.thy Wed Jul 21 16:50:42 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/IsaMakefile Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Jul 21 16:50:42 2010 +0200
@@ -168,6 +168,7 @@
SAT.thy \
Set.thy \
Sum_Type.thy \
+ Tools/abel_cancel.ML \
Tools/arith_data.ML \
Tools/cnf_funcs.ML \
Tools/Datatype/datatype_abs_proofs.ML \
@@ -219,7 +220,6 @@
Transitive_Closure.thy \
Typedef.thy \
Wellfounded.thy \
- $(SRC)/Provers/Arith/abel_cancel.ML \
$(SRC)/Provers/Arith/cancel_div_mod.ML \
$(SRC)/Provers/Arith/cancel_sums.ML \
$(SRC)/Provers/Arith/fast_lin_arith.ML \
--- a/src/HOL/Library/Efficient_Nat.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Wed Jul 21 16:50:42 2010 +0200
@@ -312,7 +312,7 @@
def equals(that: Nat): Boolean = this.value == that.value
def as_BigInt: BigInt = this.value
- def as_Int: Int = if (this.value >= Math.MIN_INT && this.value <= Math.MAX_INT)
+ def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
this.value.intValue
else this.value.intValue
@@ -337,7 +337,7 @@
code_type nat
(Haskell "Nat.Nat")
- (Scala "Nat.Nat")
+ (Scala "Nat")
code_instance nat :: eq
(Haskell -)
@@ -405,7 +405,7 @@
code_const int and nat
(Haskell "toInteger" and "fromInteger")
- (Scala "!_.as'_BigInt" and "!Nat.Nat((_))")
+ (Scala "!_.as'_BigInt" and "Nat")
text {* Conversion from and to indices. *}
@@ -419,7 +419,7 @@
(SML "IntInf.fromInt")
(OCaml "_")
(Haskell "toEnum")
- (Scala "!Nat.Nat((_))")
+ (Scala "Nat")
text {* Using target language arithmetic operations whenever appropriate *}
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Wed Jul 21 16:50:42 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/Lattice_Algebras.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Library/Lattice_Algebras.thy Wed Jul 21 16:50:42 2010 +0200
@@ -376,9 +376,10 @@
"a + b <= (c::'a::lattice_ab_group_add_abs) \<Longrightarrow> a <= c + abs b"
proof -
assume "a+b <= c"
- hence 2: "a <= c+(-b)" by (simp add: algebra_simps)
- have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
- show ?thesis by (rule le_add_right_mono[OF 2 3])
+ then have "a <= c+(-b)" by (simp add: algebra_simps)
+ have "(-b) <= abs b" by (rule abs_ge_minus_self)
+ then have "c + (- b) \<le> c + \<bar>b\<bar>" by (rule add_left_mono)
+ with `a \<le> c + (- b)` show ?thesis by (rule order_trans)
qed
class lattice_ring = ordered_ring + lattice_ab_group_add_abs
@@ -411,7 +412,7 @@
apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
done
have yx: "?y <= ?x"
- apply (simp add:diff_def)
+ apply (simp add:diff_minus)
apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
done
--- a/src/HOL/Library/Univ_Poly.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Wed Jul 21 16:50:42 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/List.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/List.thy Wed Jul 21 16:50:42 2010 +0200
@@ -4819,7 +4819,7 @@
(SML "[]")
(OCaml "[]")
(Haskell "[]")
- (Scala "Nil")
+ (Scala "!Nil")
code_instance list :: eq
(Haskell -)
--- a/src/HOL/Matrix/LP.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Matrix/LP.thy Wed Jul 21 16:50:42 2010 +0200
@@ -6,6 +6,15 @@
imports Main Lattice_Algebras
begin
+lemma le_add_right_mono:
+ assumes
+ "a <= b + (c::'a::ordered_ab_group_add)"
+ "c <= d"
+ shows "a <= b + d"
+ apply (rule_tac order_trans[where y = "b+c"])
+ apply (simp_all add: prems)
+ done
+
lemma linprog_dual_estimate:
assumes
"A * x \<le> (b::'a::lattice_ring)"
@@ -49,8 +58,8 @@
done
from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"
by (simp)
- show ?thesis
- apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
+ show ?thesis
+ apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
done
qed
@@ -138,9 +147,9 @@
then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
have s2: "c - y * A <= c2 - y * A1"
- by (simp add: diff_def prems add_mono mult_left_mono)
+ by (simp add: diff_minus prems add_mono mult_left_mono)
have s1: "c1 - y * A2 <= c - y * A"
- by (simp add: diff_def prems add_mono mult_left_mono)
+ by (simp add: diff_minus prems add_mono mult_left_mono)
have prts: "(c - y * A) * x <= ?C"
apply (simp add: Let_def)
apply (rule mult_le_prts)
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/NSA/HDeriv.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/NSA/HLim.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/NSA/HTranscendental.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/NSA/NSA.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/NSA/NSCA.thy Wed Jul 21 16:50:42 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/Numeral_Simprocs.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Numeral_Simprocs.thy Wed Jul 21 16:50:42 2010 +0200
@@ -92,7 +92,6 @@
"(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
by (simp add: nat_mult_div_cancel1)
-
use "Tools/numeral_simprocs.ML"
use "Tools/nat_numeral_simprocs.ML"
@@ -117,4 +116,4 @@
#> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
*}
-end
\ No newline at end of file
+end
--- a/src/HOL/Option.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Option.thy Wed Jul 21 16:50:42 2010 +0200
@@ -114,7 +114,7 @@
(SML "NONE" and "SOME")
(OCaml "None" and "Some _")
(Haskell "Nothing" and "Just")
- (Scala "None" and "!Some((_))")
+ (Scala "!None" and "Some")
code_instance option :: eq
(Haskell -)
--- a/src/HOL/Probability/Borel.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Probability/Borel.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/RComplete.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/RealVector.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/SEQ.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/SupInf.thy Wed Jul 21 16:50:42 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/abel_cancel.ML Wed Jul 21 16:50:42 2010 +0200
@@ -0,0 +1,131 @@
+(* Title: HOL/Tools/abel_cancel.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Simplification procedures for abelian groups:
+- Cancel complementary terms in sums.
+- Cancel like terms on opposite sides of relations.
+*)
+
+signature ABEL_CANCEL =
+sig
+ val sum_proc: simpset -> cterm -> thm option
+ val rel_proc: simpset -> cterm -> thm option
+end;
+
+structure Abel_Cancel: ABEL_CANCEL =
+struct
+
+(** compute cancellation **)
+
+fun add_atoms pos (Const (@{const_name Groups.plus}, _) $ x $ y) =
+ add_atoms pos x #> add_atoms pos y
+ | add_atoms pos (Const (@{const_name Groups.minus}, _) $ x $ y) =
+ add_atoms pos x #> add_atoms (not pos) y
+ | add_atoms pos (Const (@{const_name Groups.uminus}, _) $ x) =
+ add_atoms (not pos) x
+ | add_atoms pos x = cons (pos, x);
+
+fun atoms t = add_atoms true t [];
+
+fun zerofy pt ((c as Const (@{const_name Groups.plus}, _)) $ x $ y) =
+ (case zerofy pt x of NONE =>
+ (case zerofy pt y of NONE => NONE
+ | SOME z => SOME (c $ x $ z))
+ | SOME z => SOME (c $ z $ y))
+ | zerofy pt ((c as Const (@{const_name Groups.minus}, _)) $ x $ y) =
+ (case zerofy pt x of NONE =>
+ (case zerofy (apfst not pt) y of NONE => NONE
+ | SOME z => SOME (c $ x $ z))
+ | SOME z => SOME (c $ z $ y))
+ | zerofy pt ((c as Const (@{const_name Groups.uminus}, _)) $ x) =
+ (case zerofy (apfst not pt) x of NONE => NONE
+ | SOME z => SOME (c $ z))
+ | zerofy (pos, t) u =
+ if pos andalso (t aconv u)
+ then SOME (Const (@{const_name Groups.zero}, fastype_of t))
+ else NONE
+
+exception Cancel;
+
+fun find_common _ [] _ = raise Cancel
+ | find_common opp ((p, l) :: ls) rs =
+ let val pr = if opp then not p else p
+ in if exists (fn (q, r) => pr = q andalso l aconv r) rs then (p, l)
+ else find_common opp ls rs
+ end
+
+(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
+ If OP = +, it must be t2(-t) rather than t2(t)
+*)
+fun cancel (c $ lhs $ rhs) =
+ let
+ val opp = case c of Const(@{const_name Groups.plus}, _) => true | _ => false;
+ val (pos, l) = find_common opp (atoms lhs) (atoms rhs);
+ val posr = if opp then not pos else pos;
+ in c $ the (zerofy (pos, l) lhs) $ the (zerofy (posr, l) rhs) end;
+
+
+(** prove cancellation **)
+
+fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
+ [@{const_name Groups.zero}, @{const_name Groups.plus},
+ @{const_name Groups.uminus}, @{const_name Groups.minus}]
+ | agrp_ord _ = ~1;
+
+fun less_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
+
+fun solve (_ $ (Const (@{const_name Groups.plus}, _) $ _ $ _) $ _) =
+ SOME @{thm add_assoc [THEN eq_reflection]}
+ | solve (_ $ x $ (Const (@{const_name Groups.plus}, _) $ y $ _)) =
+ if less_agrp (y, x) then
+ SOME @{thm add_left_commute [THEN eq_reflection]}
+ else NONE
+ | solve (_ $ x $ y) =
+ if less_agrp (y, x) then
+ SOME @{thm add_commute [THEN eq_reflection]} else
+ NONE
+ | solve _ = NONE;
+
+val simproc = Simplifier.simproc @{theory}
+ "add_ac_proc" ["x + y::'a::ab_semigroup_add"] ((K o K) solve);
+
+val cancel_ss = HOL_basic_ss settermless less_agrp
+ addsimprocs [simproc] addsimps
+ [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_minus},
+ @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
+ @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
+ @{thm minus_add_cancel}];
+
+fun cancel_simp_tac ss = simp_tac (Simplifier.inherit_context ss cancel_ss);
+
+
+(** simprocs **)
+
+(* cancel complementary terms in arbitrary sums *)
+
+fun sum_proc ss ct =
+ let
+ val t = Thm.term_of ct;
+ val prop = Logic.mk_equals (t, cancel t);
+ val thm = Goal.prove (Simplifier.the_context ss) [] [] prop
+ (fn _ => cancel_simp_tac ss 1)
+ in SOME thm end handle Cancel => NONE;
+
+
+(* cancel like terms on the opposite sides of relations:
+ (x + y - z < -z + x) = (y < 0)
+ Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
+ Reduces the problem to subtraction. *)
+
+fun rel_proc ss ct =
+ let
+ val t = Thm.term_of ct;
+ val prop = Logic.mk_equals (t, cancel t);
+ val thm = Goal.prove (Simplifier.the_context ss) [] [] prop
+ (fn _ => rtac @{thm eq_reflection} 1 THEN
+ resolve_tac [@{thm diff_eq_diff_less}, @{thm diff_eq_diff_less_eq}, @{thm diff_eq_diff_eq}] 1 THEN
+ cancel_simp_tac ss 1)
+ in SOME thm end handle Cancel => NONE;
+
+end;
--- a/src/HOL/Tools/lin_arith.ML Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed Jul 21 16:50:42 2010 +0200
@@ -818,7 +818,7 @@
@{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
@{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
@{thm "not_one_less_zero"}]
- addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
+ addsimprocs [@{simproc abel_cancel_sum}, @{simproc abel_cancel_relation}]
(*abel_cancel helps it work in abstract algebraic domains*)
addsimprocs Nat_Arith.nat_cancel_sums_add
addcongs [@{thm if_weak_cong}],
--- a/src/HOL/Tools/list_code.ML Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Tools/list_code.ML Wed Jul 21 16:50:42 2010 +0200
@@ -46,8 +46,8 @@
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
| NONE =>
default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in Code_Target.add_syntax_const target
- @{const_name Cons} (SOME (2, ([@{const_name Nil}, @{const_name Cons}], pretty)))
+ in Code_Target.add_syntax_const target @{const_name Cons}
+ (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
end
end;
--- a/src/HOL/Tools/numeral.ML Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Tools/numeral.ML Wed Jul 21 16:50:42 2010 +0200
@@ -77,8 +77,8 @@
(Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
in
thy |> Code_Target.add_syntax_const target number_of
- (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
- @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
+ (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
+ @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
end;
end; (*local*)
--- a/src/HOL/Tools/numeral_simprocs.ML Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Wed Jul 21 16:50:42 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/Tools/string_code.ML Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Tools/string_code.ML Wed Jul 21 16:50:42 2010 +0200
@@ -60,7 +60,7 @@
| NONE =>
List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
in Code_Target.add_syntax_const target
- @{const_name Cons} (SOME (2, (cs_summa, pretty)))
+ @{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
end;
fun add_literal_char target =
@@ -70,7 +70,7 @@
of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
| NONE => Code_Printer.eqn_error thm "Illegal character expression";
in Code_Target.add_syntax_const target
- @{const_name Char} (SOME (2, (cs_nibbles, pretty)))
+ @{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
end;
fun add_literal_string target =
@@ -83,7 +83,7 @@
| NONE => Code_Printer.eqn_error thm "Illegal message expression")
| NONE => Code_Printer.eqn_error thm "Illegal message expression";
in Code_Target.add_syntax_const target
- @{const_name STR} (SOME (1, (cs_summa, pretty)))
+ @{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
end;
end;
--- a/src/HOL/Transcendental.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Transcendental.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Wed Jul 21 16:50:42 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 Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/Word/Word.thy Wed Jul 21 16:50:42 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
--- a/src/HOL/ex/Lagrange.thy Wed Jul 21 16:49:52 2010 +0200
+++ b/src/HOL/ex/Lagrange.thy Wed Jul 21 16:50:42 2010 +0200
@@ -22,12 +22,6 @@
However, this is an abstract theorem about commutative rings. It has,
a priori, nothing to do with nat. *}
-(* These two simprocs are even less efficient than ordered rewriting
- and kill the second example: *)
-ML {*
- Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
-*}
-
lemma Lagrange_lemma: fixes x1 :: "'a::comm_ring" shows
"(sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) =
sq (x1*y1 - x2*y2 - x3*y3 - x4*y4) +
--- a/src/Provers/Arith/abel_cancel.ML Wed Jul 21 16:49:52 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(* Title: Provers/Arith/abel_cancel.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Simplification procedures for abelian groups (e.g. integers, reals,
-polymorphic types).
-
-- Cancel complementary terms in sums
-- Cancel like terms on opposite sides of relations
-*)
-
-signature ABEL_CANCEL =
-sig
- val eq_reflection : thm (*object-equality to meta-equality*)
- val T : typ (*the type of group elements*)
- val cancel_ss : simpset (*abelian group cancel simpset*)
- val sum_pats : cterm list
- val eqI_rules : thm list
- val dest_eqI : thm -> term
-end;
-
-
-functor Abel_Cancel (Data: ABEL_CANCEL) =
-struct
-
-open Data;
-
-(* FIXME dependent on abstract syntax *)
-
-fun zero t = Const (@{const_name Groups.zero}, t);
-fun minus t = Const (@{const_name Groups.uminus}, t --> t);
-
-fun add_terms pos (Const (@{const_name Groups.plus}, _) $ x $ y, ts) =
- add_terms pos (x, add_terms pos (y, ts))
- | add_terms pos (Const (@{const_name Groups.minus}, _) $ x $ y, ts) =
- add_terms pos (x, add_terms (not pos) (y, ts))
- | add_terms pos (Const (@{const_name Groups.uminus}, _) $ x, ts) =
- add_terms (not pos) (x, ts)
- | add_terms pos (x, ts) = (pos,x) :: ts;
-
-fun terms fml = add_terms true (fml, []);
-
-fun zero1 pt (u as (c as Const(@{const_name Groups.plus},_)) $ x $ y) =
- (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
- | SOME z => SOME(c $ x $ z))
- | SOME z => SOME(c $ z $ y))
- | zero1 (pos,t) (u as (c as Const(@{const_name Groups.minus},_)) $ x $ y) =
- (case zero1 (pos,t) x of
- NONE => (case zero1 (not pos,t) y of NONE => NONE
- | SOME z => SOME(c $ x $ z))
- | SOME z => SOME(c $ z $ y))
- | zero1 (pos,t) (u as (c as Const(@{const_name Groups.uminus},_)) $ x) =
- (case zero1 (not pos,t) x of NONE => NONE
- | SOME z => SOME(c $ z))
- | zero1 (pos,t) u =
- if pos andalso (t aconv u) then SOME(zero(fastype_of t)) else NONE
-
-exception Cancel;
-
-fun find_common _ [] _ = raise Cancel
- | find_common opp ((p,l)::ls) rs =
- let val pr = if opp then not p else p
- in if exists (fn (q,r) => pr = q andalso l aconv r) rs then (p,l)
- else find_common opp ls rs
- end
-
-(* turns t1(t) OP t2(t) into t1(0) OP t2(0) where OP can be +, -, =, etc.
- If OP = +, it must be t2(-t) rather than t2(t)
-*)
-fun cancel t =
- let
- val c $ lhs $ rhs = t
- val opp = case c of Const(@{const_name Groups.plus},_) => true | _ => false;
- val (pos,l) = find_common opp (terms lhs) (terms rhs)
- val posr = if opp then not pos else pos
- val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
- in t' end;
-
-
-(*A simproc to cancel complementary terms in arbitrary sums.*)
-fun sum_proc ss t =
- let
- val t' = cancel t
- val thm =
- Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
- (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
- in SOME thm end handle Cancel => NONE;
-
-val sum_conv =
- Simplifier.mk_simproc "cancel_sums"
- (map (Drule.cterm_fun Logic.varify_global) Data.sum_pats) (K sum_proc);
-
-
-(*A simproc to cancel like terms on the opposite sides of relations:
- (x + y - z < -z + x) = (y < 0)
- Works for (=) and (<=) as well as (<), if the necessary rules are supplied.
- Reduces the problem to subtraction.*)
-fun rel_proc ss t =
- let
- val t' = cancel t
- val thm = Goal.prove (Simplifier.the_context ss) [] [] (Logic.mk_equals (t, t'))
- (fn _ => rtac eq_reflection 1 THEN
- resolve_tac eqI_rules 1 THEN
- simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
- in SOME thm end handle Cancel => NONE;
-
-val rel_conv =
- Simplifier.mk_simproc "cancel_relations"
- (map (fn th => Thm.cterm_of (Thm.theory_of_thm th) (Data.dest_eqI th)) eqI_rules) (K rel_proc);
-
-end;
--- a/src/Pure/Isar/locale.ML Wed Jul 21 16:49:52 2010 +0200
+++ b/src/Pure/Isar/locale.ML Wed Jul 21 16:50:42 2010 +0200
@@ -77,6 +77,9 @@
val print_locales: theory -> unit
val print_locale: theory -> bool -> xstring -> unit
val print_registrations: theory -> string -> unit
+ val locale_deps: theory ->
+ { params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list } Graph.T
+ * term list list Symtab.table Symtab.table
end;
structure Locale: LOCALE =
@@ -567,10 +570,10 @@
(*** diagnostic commands and interfaces ***)
-fun all_locales thy = map #1 (Name_Space.extern_table (Locales.get thy));
+val all_locales = Symtab.keys o snd o Locales.get;
fun print_locales thy =
- Pretty.strs ("locales:" :: all_locales thy)
+ Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
|> Pretty.writeln;
fun print_locale thy show_facts raw_name =
@@ -593,4 +596,32 @@
| regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
|> Pretty.writeln;
+fun locale_deps thy =
+ let
+ val names = all_locales thy
+ fun add_locale_node name =
+ let
+ val params = params_of thy name;
+ val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
+ val registrations = map (instance_of thy name o snd)
+ (these_registrations thy name);
+ in
+ Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
+ end;
+ fun add_locale_deps name =
+ let
+ val dependencies = (map o apsnd) (instance_of thy name o op $>)
+ (dependencies_of thy name);
+ in
+ fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
+ deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
+ dependencies
+ end;
+ in
+ Graph.empty
+ |> fold add_locale_node names
+ |> rpair Symtab.empty
+ |> fold add_locale_deps names
+ end;
+
end;
--- a/src/Tools/Code/code_haskell.ML Wed Jul 21 16:49:52 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Wed Jul 21 16:50:42 2010 +0200
@@ -218,30 +218,35 @@
| print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
let
val tyvars = intro_vars (map fst vs) reserved;
- fun print_classparam_instance ((classparam, const), (thm, _)) = case syntax_const classparam
- of NONE => semicolon [
- (str o deresolve_base) classparam,
- str "=",
- print_app tyvars (SOME thm) reserved NOBR (const, [])
- ]
- | SOME (k, pr) =>
- let
- val (c, (_, tys)) = const;
- val (vs, rhs) = (apfst o map) fst
- (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
- val s = if (is_some o syntax_const) c
- then NONE else (SOME o Long_Name.base_name o deresolve) c;
- val vars = reserved
- |> intro_vars (map_filter I (s :: vs));
- val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
- (*dictionaries are not relevant at this late stage*)
- in
- semicolon [
- print_term tyvars (SOME thm) vars NOBR lhs,
+ fun requires_args classparam = case syntax_const classparam
+ of NONE => 0
+ | SOME (Code_Printer.Plain_const_syntax _) => 0
+ | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k;
+ fun print_classparam_instance ((classparam, const), (thm, _)) =
+ case requires_args classparam
+ of 0 => semicolon [
+ (str o deresolve_base) classparam,
str "=",
- print_term tyvars (SOME thm) vars NOBR rhs
+ print_app tyvars (SOME thm) reserved NOBR (const, [])
]
- end;
+ | k =>
+ let
+ val (c, (_, tys)) = const;
+ val (vs, rhs) = (apfst o map) fst
+ (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
+ val s = if (is_some o syntax_const) c
+ then NONE else (SOME o Long_Name.base_name o deresolve) c;
+ val vars = reserved
+ |> intro_vars (map_filter I (s :: vs));
+ val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
+ (*dictionaries are not relevant at this late stage*)
+ in
+ semicolon [
+ print_term tyvars (SOME thm) vars NOBR lhs,
+ str "=",
+ print_term tyvars (SOME thm) vars NOBR rhs
+ ]
+ end;
in
Pretty.block_enclose (
Pretty.block [
@@ -459,7 +464,7 @@
in if target = target' then
thy
|> Code_Target.add_syntax_const target c_bind
- (SOME (pretty_haskell_monad c_bind))
+ (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
else error "Only Haskell target allows for monad syntax" end;
--- a/src/Tools/Code/code_printer.ML Wed Jul 21 16:49:52 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Wed Jul 21 16:50:42 2010 +0200
@@ -67,20 +67,22 @@
type tyco_syntax
type simple_const_syntax
- type proto_const_syntax
+ type complex_const_syntax
type const_syntax
- val parse_infix: ('a -> 'b) -> lrx * int -> string
- -> int * ((fixity -> 'b -> Pretty.T)
- -> fixity -> 'a list -> Pretty.T)
- val parse_syntax: ('a -> 'b) -> Token.T list
- -> (int * ((fixity -> 'b -> Pretty.T)
- -> fixity -> 'a list -> Pretty.T)) option * Token.T list
- val simple_const_syntax: simple_const_syntax -> proto_const_syntax
+ type activated_complex_const_syntax
+ datatype activated_const_syntax = Plain_const_syntax of int * string
+ | Complex_const_syntax of activated_complex_const_syntax
+ val requires_args: const_syntax -> int
+ val parse_const_syntax: Token.T list -> const_syntax option * Token.T list
+ val parse_tyco_syntax: Token.T list -> tyco_syntax option * Token.T list
+ val plain_const_syntax: string -> const_syntax
+ val simple_const_syntax: simple_const_syntax -> const_syntax
+ val complex_const_syntax: complex_const_syntax -> const_syntax
val activate_const_syntax: theory -> literals
- -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
+ -> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
-> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
- -> (string -> const_syntax option)
+ -> (string -> activated_const_syntax option)
-> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm option -> fixity
@@ -243,31 +245,45 @@
type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
-> fixity -> (iterm * itype) list -> Pretty.T);
-type proto_const_syntax = int * (string list * (literals -> string list
+
+type complex_const_syntax = int * (string list * (literals -> string list
-> (var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
-type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
- -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+
+datatype const_syntax = plain_const_syntax of string
+ | complex_const_syntax of complex_const_syntax;
+
+fun requires_args (plain_const_syntax _) = 0
+ | requires_args (complex_const_syntax (k, _)) = k;
fun simple_const_syntax syn =
- apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn;
+ complex_const_syntax (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
-fun activate_const_syntax thy literals (n, (cs, f)) naming =
- fold_map (Code_Thingol.ensure_declared_const thy) cs naming
- |-> (fn cs' => pair (n, f literals cs'));
+type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
+
+datatype activated_const_syntax = Plain_const_syntax of int * string
+ | Complex_const_syntax of activated_complex_const_syntax;
-fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) =
+fun activate_const_syntax thy literals c (plain_const_syntax s) naming =
+ (Plain_const_syntax (Code.args_number thy c, s), naming)
+ | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming =
+ fold_map (Code_Thingol.ensure_declared_const thy) cs naming
+ |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
+
+fun gen_print_app print_app_expr print_term syntax_const some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
case syntax_const c
- of NONE => brackify fxy (print_app_expr thm vars app)
- | SOME (k, print) =>
+ of NONE => brackify fxy (print_app_expr some_thm vars app)
+ | SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts)
+ | SOME (Complex_const_syntax (k, print)) =>
let
- fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs);
+ fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
in if k = length ts
then print' fxy ts
else if k < length ts
then case chop k ts of (ts1, ts2) =>
- brackify fxy (print' APP ts1 :: map (print_term thm vars BR) ts2)
- else print_term thm vars fxy (Code_Thingol.eta_expand k app)
+ brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
+ else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
end;
fun gen_print_bind print_term thm (fxy : fixity) pat vars =
@@ -281,7 +297,8 @@
datatype 'a mixfix =
Arg of fixity
- | Pretty of Pretty.T;
+ | String of string
+ | Break;
fun mk_mixfix prep_arg (fixity_this, mfx) =
let
@@ -292,8 +309,10 @@
[]
| fillin print (Arg fxy :: mfx) (a :: args) =
(print fxy o prep_arg) a :: fillin print mfx args
- | fillin print (Pretty p :: mfx) args =
- p :: fillin print mfx args;
+ | fillin print (String s :: mfx) args =
+ str s :: fillin print mfx args
+ | fillin print (Break :: mfx) args =
+ Pretty.brk 1 :: fillin print mfx args;
in
(i, fn print => fn fixity_ctxt => fn args =>
gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args))
@@ -304,42 +323,45 @@
val l = case x of L => INFX (i, L) | _ => INFX (i, X);
val r = case x of R => INFX (i, R) | _ => INFX (i, X);
in
- mk_mixfix prep_arg (INFX (i, x),
- [Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
+ mk_mixfix prep_arg (INFX (i, x), [Arg l, String " ", String s, Break, Arg r])
end;
-fun parse_mixfix prep_arg s =
+fun parse_mixfix mk_plain mk_complex prep_arg s =
let
val sym_any = Scan.one Symbol.is_regular;
val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
|| ($$ "_" >> K (Arg BR))
- || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
+ || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break))
|| (Scan.repeat1
( $$ "'" |-- sym_any
|| Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
- sym_any) >> (Pretty o str o implode)));
+ sym_any) >> (String o implode)));
in case Scan.finite Symbol.stopper parse (Symbol.explode s)
- of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
- | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
+ of ((false, [String s]), []) => mk_plain s
+ | ((_, p as [_]), []) => mk_complex (mk_mixfix prep_arg (NOBR, p))
+ | ((b, p as _ :: _ :: _), []) => mk_complex (mk_mixfix prep_arg (if b then NOBR else BR, p))
| _ => Scan.!!
(the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
end;
val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
-fun parse_syntax prep_arg xs =
- Scan.option ((
+fun parse_syntax mk_plain mk_complex prep_arg =
+ Scan.option (
((Parse.$$$ infixK >> K X)
|| (Parse.$$$ infixlK >> K L)
|| (Parse.$$$ infixrK >> K R))
- -- Parse.nat >> parse_infix prep_arg
- || Scan.succeed (parse_mixfix prep_arg))
- -- Parse.string
- >> (fn (parse, s) => parse s)) xs;
+ -- Parse.nat -- Parse.string
+ >> (fn ((x, i), s) => mk_complex (parse_infix prep_arg (x, i) s))
+ || Parse.string >> (fn s => (parse_mixfix mk_plain mk_complex prep_arg s)));
val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
+val parse_tyco_syntax = parse_syntax (fn s => (0, (K o K o K o str) s)) I I;
+
+val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst;
+
(** module name spaces **)
--- a/src/Tools/Code/code_scala.ML Wed Jul 21 16:49:52 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Wed Jul 21 16:50:42 2010 +0200
@@ -76,17 +76,20 @@
(app as ((c, ((arg_typs, _), function_typs)), ts)) =
let
val k = length ts;
- val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
val arg_typs' = if is_pat orelse
(is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
- val (no_syntax, print') = case syntax_const c
- of NONE => (true, fn ts => applify "(" ")"
+ val (l, print') = case syntax_const c
+ of NONE => (args_num c, fn ts => applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
NOBR ((str o deresolve) c) arg_typs') ts)
- | SOME (_, print) => (false, fn ts =>
- print (print_term tyvars is_pat some_thm) some_thm vars fxy
- (ts ~~ take l function_typs));
+ | SOME (Plain_const_syntax (k, s)) => (k, fn ts => applify "(" ")"
+ (print_term tyvars is_pat some_thm vars NOBR) fxy
+ (applify "[" "]" (print_typ tyvars NOBR)
+ NOBR (str s) arg_typs') ts)
+ | SOME (Complex_const_syntax (k, print)) =>
+ (k, fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
+ (ts ~~ take k function_typs))
in if k = l then print' ts
else if k < l then
print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
@@ -211,7 +214,7 @@
];
in
Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
- NOBR ((concat o map str) ["sealed", "class", deresolve_base name]) vs
+ NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_base name]) vs
:: map print_co cos)
end
| print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
@@ -355,20 +358,22 @@
| _ => false;
val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
reserved args_num is_singleton_constr deresolver;
- fun print_module name content =
- (name, Pretty.chunks [
- str ("object " ^ name ^ " {"),
- str "",
+ fun print_module name imports content =
+ (name, Pretty.chunks (
+ str ("object " ^ name ^ " {")
+ :: (if null imports then []
+ else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports)
+ @ [str "",
content,
str "",
- str "}"
- ]);
+ str "}"]
+ ));
fun serialize_module the_module_name sca_program =
let
val content = Pretty.chunks2 (map_filter
(fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
| (_, (_, NONE)) => NONE) sca_program);
- in print_module the_module_name content end;
+ in print_module the_module_name (map fst includes) content end;
fun check_destination destination =
(File.check destination; destination);
fun write_module destination (modlname, content) =
@@ -385,7 +390,7 @@
(fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
(write_module (check_destination file)))
(rpair [] o cat_lines o map (code_of_pretty o snd))
- (map (uncurry print_module) includes
+ (map (fn (name, content) => print_module name [] content) includes
@| serialize_module the_module_name sca_program)
destination
end;
@@ -405,7 +410,7 @@
literal_char = Library.enclose "'" "'" o char_scala,
literal_string = quote o translate_string char_scala,
literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
- literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
+ literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
literal_naive_numeral = fn k => if k >= 0
then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
--- a/src/Tools/Code/code_target.ML Wed Jul 21 16:49:52 2010 +0200
+++ b/src/Tools/Code/code_target.ML Wed Jul 21 16:50:42 2010 +0200
@@ -41,11 +41,11 @@
val allow_abort: string -> theory -> theory
type tyco_syntax = Code_Printer.tyco_syntax
- type proto_const_syntax = Code_Printer.proto_const_syntax
+ type const_syntax = Code_Printer.const_syntax
val add_syntax_class: string -> class -> string option -> theory -> theory
val add_syntax_inst: string -> class * string -> unit option -> theory -> theory
val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
- val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
+ val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
val add_reserved: string -> string -> theory -> theory
val add_include: string -> string * (string * string list) option -> theory -> theory
end;
@@ -57,7 +57,7 @@
type literals = Code_Printer.literals;
type tyco_syntax = Code_Printer.tyco_syntax;
-type proto_const_syntax = Code_Printer.proto_const_syntax;
+type const_syntax = Code_Printer.const_syntax;
(** basics **)
@@ -83,7 +83,7 @@
class: string Symtab.table,
instance: unit Symreltab.table,
tyco: Code_Printer.tyco_syntax Symtab.table,
- const: Code_Printer.proto_const_syntax Symtab.table
+ const: Code_Printer.const_syntax Symtab.table
};
fun mk_name_syntax_table ((class, instance), (tyco, const)) =
@@ -108,7 +108,7 @@
-> (string -> string option) (*module aliasses*)
-> (string -> string option) (*class syntax*)
-> (string -> Code_Printer.tyco_syntax option)
- -> (string -> Code_Printer.const_syntax option)
+ -> (string -> Code_Printer.activated_const_syntax option)
-> ((Pretty.T -> string) * (Pretty.T -> unit))
-> Code_Thingol.program
-> string list (*selected statements*)
@@ -244,11 +244,11 @@
|>> map_filter I;
fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
- |> fold_map (fn thing_identifier => fn (tab, naming) =>
- case Code_Thingol.lookup_const naming thing_identifier
+ |> fold_map (fn c => fn (tab, naming) =>
+ case Code_Thingol.lookup_const naming c
of SOME name => let
val (syn, naming') = Code_Printer.activate_const_syntax thy
- literals (the (Symtab.lookup src_tab thing_identifier)) naming
+ literals c (the (Symtab.lookup src_tab c)) naming
in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
| NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
|>> map_filter I;
@@ -445,12 +445,12 @@
then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
else syn);
-fun gen_add_syntax_const prep_const prep_syn =
+fun gen_add_syntax_const prep_const =
gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
- (fn thy => fn c => fn raw_syn => let val syn = prep_syn raw_syn in
- if fst syn > Code.args_number thy c
+ (fn thy => fn c => fn syn =>
+ if Code_Printer.requires_args syn > Code.args_number thy c
then error ("Too many arguments in syntax for constant " ^ quote c)
- else syn end);
+ else syn);
fun add_reserved target =
let
@@ -496,22 +496,23 @@
fun zip_list (x::xs) f g =
f
- #-> (fn y =>
+ :|-- (fn y =>
fold_map (fn x => g |-- f >> pair x) xs
- #-> (fn xys => pair ((x, y) :: xys)));
+ :|-- (fn xys => pair ((x, y) :: xys)));
-fun parse_multi_syntax parse_thing parse_syntax =
- Parse.and_list1 parse_thing
- #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
- (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"));
+fun process_multi_syntax parse_thing parse_syntax change =
+ (Parse.and_list1 parse_thing
+ :|-- (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
+ (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")")))
+ >> (Toplevel.theory oo fold)
+ (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
in
val add_syntax_class = gen_add_syntax_class cert_class;
val add_syntax_inst = gen_add_syntax_inst cert_inst;
val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
-val add_syntax_const_simple = gen_add_syntax_const (K I) Code_Printer.simple_const_syntax;
-val add_syntax_const = gen_add_syntax_const (K I) I;
+val add_syntax_const = gen_add_syntax_const (K I);
val allow_abort = gen_allow_abort (K I);
val add_reserved = add_reserved;
val add_include = add_include;
@@ -519,9 +520,7 @@
val add_syntax_class_cmd = gen_add_syntax_class read_class;
val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
-val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const Code_Printer.simple_const_syntax;
-val add_syntax_const_cmd = gen_add_syntax_const Code.read_const I;
-
+val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
val allow_abort_cmd = gen_allow_abort Code.read_const;
fun parse_args f args =
@@ -550,32 +549,24 @@
val _ =
Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
- parse_multi_syntax Parse.xname (Scan.option Parse.string)
- >> (Toplevel.theory oo fold) (fn (target, syns) =>
- fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
- );
+ process_multi_syntax Parse.xname (Scan.option Parse.string)
+ add_syntax_class_cmd);
val _ =
Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
- parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
+ process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
(Scan.option (Parse.minus >> K ()))
- >> (Toplevel.theory oo fold) (fn (target, syns) =>
- fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
- );
+ add_syntax_inst_cmd);
val _ =
Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
- parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I)
- >> (Toplevel.theory oo fold) (fn (target, syns) =>
- fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
- );
+ process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
+ add_syntax_tyco_cmd);
val _ =
Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
- parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst)
- >> (Toplevel.theory oo fold) (fn (target, syns) =>
- fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
- );
+ process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
+ add_syntax_const_cmd);
val _ =
Outer_Syntax.command "code_reserved" "declare words as reserved for target language"