explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
--- a/NEWS Sun Sep 21 16:56:06 2014 +0200
+++ b/NEWS Sun Sep 21 16:56:11 2014 +0200
@@ -20,6 +20,11 @@
* Command "class_deps" takes optional sort arguments constraining
the search space.
+* Lexical separation of signed and unsigend numerals: categories "num"
+and "float" are unsigend. INCOMPATIBILITY: subtle change in precedence
+of numeral signs, particulary in expressions involving infix syntax like
+"(- 1) ^ n".
+
*** HOL ***
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sun Sep 21 16:56:11 2014 +0200
@@ -599,8 +599,8 @@
@{syntax_def (inner) var} & = & @{syntax_ref var} \\
@{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
@{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
- @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat} \\
- @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text " | "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
+ @{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\
+ @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
@{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\
@{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
@{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
--- a/src/HOL/Decision_Procs/Approximation.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Sun Sep 21 16:56:11 2014 +0200
@@ -40,7 +40,7 @@
lemma horner_schema:
fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
assumes f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
- shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / (f (j' + j))) * x ^ j)"
+ shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. (- 1) ^ j * (1 / (f (j' + j))) * x ^ j)"
proof (induct n arbitrary: j')
case 0
then show ?case by auto
@@ -86,8 +86,8 @@
and lb_Suc: "\<And> n i k x. lb (Suc n) i k x = lapprox_rat prec 1 k - x * (ub n (F i) (G i k) x)"
and ub_0: "\<And> i k x. ub 0 i k x = 0"
and ub_Suc: "\<And> n i k x. ub (Suc n) i k x = rapprox_rat prec 1 k - x * (lb n (F i) (G i k) x)"
- shows "(lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. -1 ^ j * (1 / (f (j' + j))) * (x ^ j))" (is "?lb") and
- "(\<Sum>j=0..<n. -1 ^ j * (1 / (f (j' + j))) * (x ^ j)) \<le> (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
+ shows "(lb n ((F ^^ j') s) (f j') x) \<le> (\<Sum>j=0..<n. (- 1) ^ j * (1 / (f (j' + j))) * (x ^ j))" (is "?lb") and
+ "(\<Sum>j=0..<n. (- 1) ^ j * (1 / (f (j' + j))) * (x ^ j)) \<le> (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
proof -
have "?lb \<and> ?ub"
using horner_bounds'[where lb=lb, OF `0 \<le> real x` f_Suc lb_0 lb_Suc ub_0 ub_Suc]
@@ -107,7 +107,7 @@
proof -
{ fix x y z :: float have "x - y * z = x + - y * z" by simp } note diff_mult_minus = this
have sum_eq: "(\<Sum>j=0..<n. (1 / (f (j' + j))) * real x ^ j) =
- (\<Sum>j = 0..<n. -1 ^ j * (1 / (f (j' + j))) * real (- x) ^ j)"
+ (\<Sum>j = 0..<n. (- 1) ^ j * (1 / (f (j' + j))) * real (- x) ^ j)"
by (auto simp add: field_simps power_mult_distrib[symmetric])
have "0 \<le> real (-x)" using assms by auto
from horner_bounds[where G=G and F=F and f=f and s=s and prec=prec
@@ -166,13 +166,13 @@
fun sqrt_iteration :: "nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where
"sqrt_iteration prec 0 x = Float 1 ((bitlen \<bar>mantissa x\<bar> + exponent x) div 2 + 1)" |
"sqrt_iteration prec (Suc m) x = (let y = sqrt_iteration prec m x
- in Float 1 -1 * (y + float_divr prec x y))"
+ in Float 1 (- 1) * (y + float_divr prec x y))"
lemma compute_sqrt_iteration_base[code]:
shows "sqrt_iteration prec n (Float m e) =
(if n = 0 then Float 1 ((if m = 0 then 0 else bitlen \<bar>m\<bar> + e) div 2 + 1)
else (let y = sqrt_iteration prec (n - 1) (Float m e) in
- Float 1 -1 * (y + float_divr prec (Float m e) y)))"
+ Float 1 (- 1) * (y + float_divr prec (Float m e) y)))"
using bitlen_Float by (cases n) simp_all
function ub_sqrt lb_sqrt :: "nat \<Rightarrow> float \<Rightarrow> float" where
@@ -262,7 +262,7 @@
also have "\<dots> < real ?b" using Suc .
finally have "sqrt x < (?b + x / ?b)/2" using sqrt_ub_pos_pos_1[OF Suc _ `0 < real x`] by auto
also have "\<dots> \<le> (?b + (float_divr prec x ?b))/2" by (rule divide_right_mono, auto simp add: float_divr)
- also have "\<dots> = (Float 1 -1) * (?b + (float_divr prec x ?b))" by simp
+ also have "\<dots> = (Float 1 (- 1)) * (?b + (float_divr prec x ?b))" by simp
finally show ?case unfolding sqrt_iteration.simps Let_def distrib_left .
qed
@@ -359,7 +359,7 @@
assumes "0 \<le> real x" "real x \<le> 1" and "even n"
shows "arctan x \<in> {(x * lb_arctan_horner prec n 1 (x * x)) .. (x * ub_arctan_horner prec (Suc n) 1 (x * x))}"
proof -
- let ?c = "\<lambda>i. -1^i * (1 / (i * 2 + (1::nat)) * real x ^ (i * 2 + 1))"
+ let ?c = "\<lambda>i. (- 1) ^ i * (1 / (i * 2 + (1::nat)) * real x ^ (i * 2 + 1))"
let ?S = "\<lambda>n. \<Sum> i=0..<n. ?c i"
have "0 \<le> real (x * x)" by auto
@@ -471,20 +471,20 @@
"lb_arctan prec x = (let ub_horner = \<lambda> x. x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x) ;
lb_horner = \<lambda> x. x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)
in (if x < 0 then - ub_arctan prec (-x) else
- if x \<le> Float 1 -1 then lb_horner x else
+ if x \<le> Float 1 (- 1) then lb_horner x else
if x \<le> Float 1 1 then Float 1 1 * lb_horner (float_divl prec x (1 + ub_sqrt prec (1 + x * x)))
else (let inv = float_divr prec 1 x
in if inv > 1 then 0
- else lb_pi prec * Float 1 -1 - ub_horner inv)))"
+ else lb_pi prec * Float 1 (- 1) - ub_horner inv)))"
| "ub_arctan prec x = (let lb_horner = \<lambda> x. x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x) ;
ub_horner = \<lambda> x. x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x)
in (if x < 0 then - lb_arctan prec (-x) else
- if x \<le> Float 1 -1 then ub_horner x else
+ if x \<le> Float 1 (- 1) then ub_horner x else
if x \<le> Float 1 1 then let y = float_divr prec x (1 + lb_sqrt prec (1 + x * x))
- in if y > 1 then ub_pi prec * Float 1 -1
+ in if y > 1 then ub_pi prec * Float 1 (- 1)
else Float 1 1 * ub_horner y
- else ub_pi prec * Float 1 -1 - lb_horner (float_divl prec 1 x)))"
+ else ub_pi prec * Float 1 (- 1) - lb_horner (float_divl prec 1 x)))"
by pat_completeness auto
termination by (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 0 then 1 else 0))", auto)
@@ -499,7 +499,7 @@
and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)"
show ?thesis
- proof (cases "x \<le> Float 1 -1")
+ proof (cases "x \<le> Float 1 (- 1)")
case True hence "real x \<le> 1" by auto
show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True]
using arctan_0_1_bounds[OF `0 \<le> real x` `real x \<le> 1`] by auto
@@ -543,7 +543,7 @@
also have "\<dots> \<le> 2 * arctan (x / ?R)"
using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
also have "2 * arctan (x / ?R) = arctan x" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
- finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF True] .
+ finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_P[OF True] .
next
case False
hence "2 < real x" by auto
@@ -555,7 +555,7 @@
show ?thesis
proof (cases "1 < ?invx")
case True
- show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF False] if_P[OF True]
+ show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_not_P[OF False] if_P[OF True]
using `0 \<le> arctan x` by auto
next
case False
@@ -570,10 +570,10 @@
using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
moreover
- have "lb_pi prec * Float 1 -1 \<le> pi / 2"
+ have "lb_pi prec * Float 1 (- 1) \<le> pi / 2"
unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp
ultimately
- show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF `\<not> x \<le> Float 1 1`] if_not_P[OF False]
+ show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_not_P[OF `\<not> x \<le> Float 1 1`] if_not_P[OF False]
by auto
qed
qed
@@ -589,7 +589,7 @@
and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)"
show ?thesis
- proof (cases "x \<le> Float 1 -1")
+ proof (cases "x \<le> Float 1 (- 1)")
case True hence "real x \<le> 1" by auto
show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True]
using arctan_0_1_bounds[OF `0 \<le> real x` `real x \<le> 1`] by auto
@@ -623,9 +623,9 @@
show ?thesis
proof (cases "?DIV > 1")
case True
- have "pi / 2 \<le> ub_pi prec * Float 1 -1" unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto
+ have "pi / 2 \<le> ub_pi prec * Float 1 (- 1)" unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto
from order_less_le_trans[OF arctan_ubound this, THEN less_imp_le]
- show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_P[OF True] .
+ show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_P[OF `x \<le> Float 1 1`] if_P[OF True] .
next
case False
hence "real ?DIV \<le> 1" by auto
@@ -638,7 +638,7 @@
using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
also have "\<dots> \<le> (Float 1 1 * ?ub_horner ?DIV)" unfolding Float_num
using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
- finally show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_not_P[OF False] .
+ finally show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_P[OF `x \<le> Float 1 1`] if_not_P[OF False] .
qed
next
case False
@@ -661,9 +661,9 @@
using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
unfolding real_sgn_pos[OF `0 < 1 / x`] le_diff_eq by auto
moreover
- have "pi / 2 \<le> ub_pi prec * Float 1 -1" unfolding Float_num times_divide_eq_right mult_1_right using pi_boundaries by auto
+ have "pi / 2 \<le> ub_pi prec * Float 1 (- 1)" unfolding Float_num times_divide_eq_right mult_1_right using pi_boundaries by auto
ultimately
- show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`]if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF False]
+ show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`]if_not_P[OF `\<not> x \<le> Float 1 (- 1)`] if_not_P[OF False]
by auto
qed
qed
@@ -715,8 +715,8 @@
(lapprox_rat prec 1 k) - x * (ub_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)"
lemma cos_aux:
- shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^(2 * i))" (is "?lb")
- and "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub")
+ shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x ^(2 * i))" (is "?lb")
+ and "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub")
proof -
have "0 \<le> real (x * x)" by auto
let "?f n" = "fact (2 * n)"
@@ -738,15 +738,15 @@
hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
have "0 < x * x" using `0 < x` by simp
- { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^ (2 * i))
- = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
+ { fix x n have "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x ^ (2 * i))
+ = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
proof -
have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto
also have "\<dots> =
- (\<Sum> j = 0 ..< n. -1 ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
- also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then -1 ^ (i div 2) / (real (fact i)) * x ^ i else 0)"
+ (\<Sum> j = 0 ..< n. (- 1) ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
+ also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then (- 1) ^ (i div 2) / (real (fact i)) * x ^ i else 0)"
unfolding sum_split_even_odd atLeast0LessThan ..
- also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then -1 ^ (i div 2) / (real (fact i)) else 0) * x ^ i)"
+ also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then (- 1) ^ (i div 2) / (real (fact i)) else 0) * x ^ i)"
by (rule setsum.cong) auto
finally show ?thesis by assumption
qed } note morph_to_if_power = this
@@ -755,16 +755,16 @@
{ fix n :: nat assume "0 < n"
hence "0 < 2 * n" by auto
obtain t where "0 < t" and "t < real x" and
- cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
+ cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
+ (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
(is "_ = ?SUM + ?rest / ?fact * ?pow")
using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
unfolding cos_coeff_def atLeast0LessThan by auto
- have "cos t * -1^n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
+ have "cos t * (- 1) ^ n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
also have "\<dots> = cos (t + n * pi)" using cos_add by auto
also have "\<dots> = ?rest" by auto
- finally have "cos t * -1^n = ?rest" .
+ finally have "cos t * (- 1) ^ n = ?rest" .
moreover
have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto
hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
@@ -828,8 +828,8 @@
qed
lemma sin_aux: assumes "0 \<le> real x"
- shows "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> (\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1))" (is "?lb")
- and "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1)) \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))" (is "?ub")
+ shows "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1))" (is "?lb")
+ and "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1)) \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))" (is "?ub")
proof -
have "0 \<le> real (x * x)" by auto
let "?f n" = "fact (2 * n + 1)"
@@ -854,14 +854,14 @@
hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
have "0 < x * x" using `0 < x` by simp
- { fix x n have "(\<Sum> j = 0 ..< n. -1 ^ (((2 * j + 1) - Suc 0) div 2) / (real (fact (2 * j + 1))) * x ^(2 * j + 1))
- = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _")
+ { fix x n have "(\<Sum> j = 0 ..< n. (- 1) ^ (((2 * j + 1) - Suc 0) div 2) / (real (fact (2 * j + 1))) * x ^(2 * j + 1))
+ = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _")
proof -
have pow: "!!i. x ^ (2 * i + 1) = x * x ^ (2 * i)" by auto
have "?SUM = (\<Sum> j = 0 ..< n. 0) + ?SUM" by auto
- also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i)) * x ^ i)"
+ also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / (real (fact i)) * x ^ i)"
unfolding sum_split_even_odd atLeast0LessThan ..
- also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i))) * x ^ i)"
+ also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / (real (fact i))) * x ^ i)"
by (rule setsum.cong) auto
finally show ?thesis by assumption
qed } note setsum_morph = this
@@ -869,13 +869,13 @@
{ fix n :: nat assume "0 < n"
hence "0 < 2 * n + 1" by auto
obtain t where "0 < t" and "t < real x" and
- sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
+ sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
+ (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
(is "_ = ?SUM + ?rest / ?fact * ?pow")
using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
unfolding sin_coeff_def atLeast0LessThan by auto
- have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto
+ have "?rest = cos t * (- 1) ^ n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto
moreover
have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto
hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
@@ -887,7 +887,7 @@
{
assume "even n"
have "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le>
- (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
+ (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
also have "\<dots> \<le> ?SUM" by auto
also have "\<dots> \<le> sin x"
@@ -908,7 +908,7 @@
by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
thus ?thesis unfolding sin_eq by auto
qed
- also have "\<dots> \<le> (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
+ also have "\<dots> \<le> (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
by auto
also have "\<dots> \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))"
using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
@@ -945,17 +945,17 @@
"lb_cos prec x = (let
horner = \<lambda> x. lb_sin_cos_aux prec (get_even (prec div 4 + 1)) 1 1 (x * x) ;
half = \<lambda> x. if x < 0 then - 1 else Float 1 1 * x * x - 1
- in if x < Float 1 -1 then horner x
-else if x < 1 then half (horner (x * Float 1 -1))
- else half (half (horner (x * Float 1 -2))))"
+ in if x < Float 1 (- 1) then horner x
+else if x < 1 then half (horner (x * Float 1 (- 1)))
+ else half (half (horner (x * Float 1 (- 2)))))"
definition ub_cos :: "nat \<Rightarrow> float \<Rightarrow> float" where
"ub_cos prec x = (let
horner = \<lambda> x. ub_sin_cos_aux prec (get_odd (prec div 4 + 1)) 1 1 (x * x) ;
half = \<lambda> x. Float 1 1 * x * x - 1
- in if x < Float 1 -1 then horner x
-else if x < 1 then half (horner (x * Float 1 -1))
- else half (half (horner (x * Float 1 -2))))"
+ in if x < Float 1 (- 1) then horner x
+else if x < 1 then half (horner (x * Float 1 (- 1)))
+ else half (half (horner (x * Float 1 (- 2)))))"
lemma lb_cos: assumes "0 \<le> real x" and "x \<le> pi"
shows "cos x \<in> {(lb_cos prec x) .. (ub_cos prec x)}" (is "?cos x \<in> {(?lb x) .. (?ub x) }")
@@ -975,13 +975,13 @@
let "?lb_half x" = "if x < 0 then - 1 else Float 1 1 * x * x - 1"
show ?thesis
- proof (cases "x < Float 1 -1")
+ proof (cases "x < Float 1 (- 1)")
case True hence "x \<le> pi / 2" using pi_ge_two by auto
- show ?thesis unfolding lb_cos_def[where x=x] ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_P[OF `x < Float 1 -1`] Let_def
+ show ?thesis unfolding lb_cos_def[where x=x] ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_P[OF `x < Float 1 (- 1)`] Let_def
using cos_boundaries[OF `0 \<le> real x` `x \<le> pi / 2`] .
next
case False
- { fix y x :: float let ?x2 = "(x * Float 1 -1)"
+ { fix y x :: float let ?x2 = "(x * Float 1 (- 1))"
assume "y \<le> cos ?x2" and "-pi \<le> x" and "x \<le> pi"
hence "- (pi / 2) \<le> ?x2" and "?x2 \<le> pi / 2" using pi_ge_two unfolding Float_num by auto
hence "0 \<le> cos ?x2" by (rule cos_ge_zero)
@@ -1000,7 +1000,7 @@
qed
} note lb_half = this
- { fix y x :: float let ?x2 = "(x * Float 1 -1)"
+ { fix y x :: float let ?x2 = "(x * Float 1 (- 1))"
assume ub: "cos ?x2 \<le> y" and "- pi \<le> x" and "x \<le> pi"
hence "- (pi / 2) \<le> ?x2" and "?x2 \<le> pi / 2" using pi_ge_two unfolding Float_num by auto
hence "0 \<le> cos ?x2" by (rule cos_ge_zero)
@@ -1016,8 +1016,8 @@
qed
} note ub_half = this
- let ?x2 = "x * Float 1 -1"
- let ?x4 = "x * Float 1 -1 * Float 1 -1"
+ let ?x2 = "x * Float 1 (- 1)"
+ let ?x4 = "x * Float 1 (- 1) * Float 1 (- 1)"
have "-pi \<le> x" using pi_ge_zero[THEN le_imp_neg_le, unfolded minus_zero] `0 \<le> real x` by (rule order_trans)
@@ -1031,12 +1031,12 @@
have "(?lb x) \<le> ?cos x"
proof -
from lb_half[OF lb `-pi \<le> x` `x \<le> pi`]
- show ?thesis unfolding lb_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
+ show ?thesis unfolding lb_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 (- 1)` `x < 1` by auto
qed
moreover have "?cos x \<le> (?ub x)"
proof -
from ub_half[OF ub `-pi \<le> x` `x \<le> pi`]
- show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
+ show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 (- 1)` `x < 1` by auto
qed
ultimately show ?thesis by auto
next
@@ -1045,19 +1045,19 @@
from cos_boundaries[OF this]
have lb: "(?lb_horner ?x4) \<le> ?cos ?x4" and ub: "?cos ?x4 \<le> (?ub_horner ?x4)" by auto
- have eq_4: "?x2 * Float 1 -1 = x * Float 1 -2" by transfer simp
+ have eq_4: "?x2 * Float 1 (- 1) = x * Float 1 (- 2)" by transfer simp
have "(?lb x) \<le> ?cos x"
proof -
have "-pi \<le> ?x2" and "?x2 \<le> pi" using pi_ge_two `0 \<le> real x` `x \<le> pi` by auto
from lb_half[OF lb_half[OF lb this] `-pi \<le> x` `x \<le> pi`, unfolded eq_4]
- show ?thesis unfolding lb_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 -1`] if_not_P[OF `\<not> x < 1`] Let_def .
+ show ?thesis unfolding lb_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 (- 1)`] if_not_P[OF `\<not> x < 1`] Let_def .
qed
moreover have "?cos x \<le> (?ub x)"
proof -
have "-pi \<le> ?x2" and "?x2 \<le> pi" using pi_ge_two `0 \<le> real x` ` x \<le> pi` by auto
from ub_half[OF ub_half[OF ub this] `-pi \<le> x` `x \<le> pi`, unfolded eq_4]
- show ?thesis unfolding ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 -1`] if_not_P[OF `\<not> x < 1`] Let_def .
+ show ?thesis unfolding ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 (- 1)`] if_not_P[OF `\<not> x < 1`] Let_def .
qed
ultimately show ?thesis by auto
qed
@@ -1081,9 +1081,9 @@
in if - lpi \<le> lx \<and> ux \<le> 0 then (lb_cos prec (-lx), ub_cos prec (-ux))
else if 0 \<le> lx \<and> ux \<le> lpi then (lb_cos prec ux, ub_cos prec lx)
else if - lpi \<le> lx \<and> ux \<le> lpi then (min (lb_cos prec (-lx)) (lb_cos prec ux), Float 1 0)
- else if 0 \<le> lx \<and> ux \<le> 2 * lpi then (Float -1 0, max (ub_cos prec lx) (ub_cos prec (- (ux - 2 * lpi))))
- else if -2 * lpi \<le> lx \<and> ux \<le> 0 then (Float -1 0, max (ub_cos prec (lx + 2 * lpi)) (ub_cos prec (-ux)))
- else (Float -1 0, Float 1 0))"
+ else if 0 \<le> lx \<and> ux \<le> 2 * lpi then (Float (- 1) 0, max (ub_cos prec lx) (ub_cos prec (- (ux - 2 * lpi))))
+ else if -2 * lpi \<le> lx \<and> ux \<le> 0 then (Float (- 1) 0, max (ub_cos prec (lx + 2 * lpi)) (ub_cos prec (-ux)))
+ else (Float (- 1) 0, Float 1 0))"
lemma floor_int:
obtains k :: int where "real k = (floor_fl f)"
@@ -1233,7 +1233,7 @@
next case False note 3 = this show ?thesis
proof (cases "0 \<le> ?lx \<and> ?ux \<le> 2 * ?lpi")
case True note Cond = this with bnds 1 2 3
- have l: "l = Float -1 0"
+ have l: "l = Float (- 1) 0"
and u: "u = max (ub_cos prec ?lx) (ub_cos prec (- (?ux - 2 * ?lpi)))"
by (auto simp add: bnds_cos_def Let_def)
@@ -1275,7 +1275,7 @@
next case False note 4 = this show ?thesis
proof (cases "-2 * ?lpi \<le> ?lx \<and> ?ux \<le> 0")
case True note Cond = this with bnds 1 2 3 4
- have l: "l = Float -1 0"
+ have l: "l = Float (- 1) 0"
and u: "u = max (ub_cos prec (?lx + 2 * ?lpi)) (ub_cos prec (-?ux))"
by (auto simp add: bnds_cos_def Let_def)
@@ -1379,7 +1379,7 @@
function ub_exp :: "nat \<Rightarrow> float \<Rightarrow> float" and lb_exp :: "nat \<Rightarrow> float \<Rightarrow> float" where
"lb_exp prec x = (if 0 < x then float_divl prec 1 (ub_exp prec (-x))
else let
- horner = (\<lambda> x. let y = lb_exp_horner prec (get_even (prec + 2)) 1 1 x in if y \<le> 0 then Float 1 -2 else y)
+ horner = (\<lambda> x. let y = lb_exp_horner prec (get_even (prec + 2)) 1 1 x in if y \<le> 0 then Float 1 (- 2) else y)
in if x < - 1 then (horner (float_divl prec x (- floor_fl x))) ^ nat (- int_floor_fl x)
else horner x)" |
"ub_exp prec x = (if 0 < x then float_divr prec 1 (lb_exp prec (-x))
@@ -1392,7 +1392,7 @@
proof -
have eq4: "4 = Suc (Suc (Suc (Suc 0)))" by auto
- have "1 / 4 = (Float 1 -2)" unfolding Float_num by auto
+ have "1 / 4 = (Float 1 (- 2))" unfolding Float_num by auto
also have "\<dots> \<le> lb_exp_horner 1 (get_even 4) 1 1 (- 1)"
unfolding get_even_def eq4
by (auto simp add: Float.compute_lapprox_rat Float.compute_rapprox_rat
@@ -1404,7 +1404,7 @@
lemma lb_exp_pos: assumes "\<not> 0 < x" shows "0 < lb_exp prec x"
proof -
let "?lb_horner x" = "lb_exp_horner prec (get_even (prec + 2)) 1 1 x"
- let "?horner x" = "let y = ?lb_horner x in if y \<le> 0 then Float 1 -2 else y"
+ let "?horner x" = "let y = ?lb_horner x in if y \<le> 0 then Float 1 (- 2) else y"
have pos_horner: "\<And> x. 0 < ?horner x" unfolding Let_def by (cases "?lb_horner x \<le> 0", auto)
moreover { fix x :: float fix num :: nat
have "0 < real (?horner x) ^ num" using `0 < ?horner x` by simp
@@ -1431,7 +1431,7 @@
from `\<not> x < - 1` have "- 1 \<le> real x" by auto
hence "exp (- 1) \<le> exp x" unfolding exp_le_cancel_iff .
from order_trans[OF exp_m1_ge_quarter this]
- have "Float 1 -2 \<le> exp x" unfolding Float_num .
+ have "Float 1 (- 2) \<le> exp x" unfolding Float_num .
moreover case True
ultimately show ?thesis using bnds_exp_horner `real x \<le> 0` `\<not> x > 0` `\<not> x < - 1` by auto
next
@@ -1502,8 +1502,8 @@
from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
have "- 1 \<le> x / (- floor_fl x)" unfolding minus_float.rep_eq by auto
from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
- have "Float 1 -2 \<le> exp (x / (- floor_fl x))" unfolding Float_num .
- hence "real (Float 1 -2) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
+ have "Float 1 (- 2) \<le> exp (x / (- floor_fl x))" unfolding Float_num .
+ hence "real (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
by (auto intro!: power_mono)
also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
finally show ?thesis
@@ -1582,12 +1582,12 @@
lemma ln_bounds:
assumes "0 \<le> x" and "x < 1"
- shows "(\<Sum>i=0..<2*n. -1^i * (1 / real (i + 1)) * x ^ (Suc i)) \<le> ln (x + 1)" (is "?lb")
- and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x ^ (Suc i))" (is "?ub")
+ shows "(\<Sum>i=0..<2*n. (- 1) ^ i * (1 / real (i + 1)) * x ^ (Suc i)) \<le> ln (x + 1)" (is "?lb")
+ and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. (- 1) ^ i * (1 / real (i + 1)) * x ^ (Suc i))" (is "?ub")
proof -
let "?a n" = "(1/real (n +1)) * x ^ (Suc n)"
- have ln_eq: "(\<Sum> i. -1^i * ?a i) = ln (x + 1)"
+ have ln_eq: "(\<Sum> i. (- 1) ^ i * ?a i) = ln (x + 1)"
using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
have "norm x < 1" using assms by auto
@@ -1613,7 +1613,7 @@
obtain ev where ev: "get_even n = 2 * ev" using get_even_double ..
obtain od where od: "get_odd n = 2 * od + 1" using get_odd_double ..
- let "?s n" = "-1^n * (1 / real (1 + n)) * (real x)^(Suc n)"
+ let "?s n" = "(- 1) ^ n * (1 / real (1 + n)) * (real x)^(Suc n)"
have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 mult.assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric] unfolding mult.commute[of "real x"] ev
using horner_bounds(1)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*ev",
@@ -1643,10 +1643,10 @@
subsection "Compute the logarithm of 2"
definition ub_ln2 where "ub_ln2 prec = (let third = rapprox_rat (max prec 1) 1 3
- in (Float 1 -1 * ub_ln_horner prec (get_odd prec) 1 (Float 1 -1)) +
+ in (Float 1 (- 1) * ub_ln_horner prec (get_odd prec) 1 (Float 1 (- 1))) +
(third * ub_ln_horner prec (get_odd prec) 1 third))"
definition lb_ln2 where "lb_ln2 prec = (let third = lapprox_rat prec 1 3
- in (Float 1 -1 * lb_ln_horner prec (get_even prec) 1 (Float 1 -1)) +
+ in (Float 1 (- 1) * lb_ln_horner prec (get_even prec) 1 (Float 1 (- 1))) +
(third * lb_ln_horner prec (get_even prec) 1 third))"
lemma ub_ln2: "ln 2 \<le> ub_ln2 prec" (is "?ub_ln2")
@@ -1663,7 +1663,7 @@
have ub3: "1 / 3 \<le> ?uthird" using rapprox_rat[of 1 3] by auto
hence ub3_lb: "0 \<le> real ?uthird" by auto
- have lb2: "0 \<le> real (Float 1 -1)" and ub2: "real (Float 1 -1) < 1" unfolding Float_num by auto
+ have lb2: "0 \<le> real (Float 1 (- 1))" and ub2: "real (Float 1 (- 1)) < 1" unfolding Float_num by auto
have "0 \<le> (1::int)" and "0 < (3::int)" by auto
have ub3_ub: "real ?uthird < 1" by (simp add: Float.compute_rapprox_rat rapprox_posrat_less1)
@@ -1694,15 +1694,15 @@
"ub_ln prec x = (if x \<le> 0 then None
else if x < 1 then Some (- the (lb_ln prec (float_divl (max prec 1) 1 x)))
else let horner = \<lambda>x. x * ub_ln_horner prec (get_odd prec) 1 x in
- if x \<le> Float 3 -1 then Some (horner (x - 1))
- else if x < Float 1 1 then Some (horner (Float 1 -1) + horner (x * rapprox_rat prec 2 3 - 1))
+ if x \<le> Float 3 (- 1) then Some (horner (x - 1))
+ else if x < Float 1 1 then Some (horner (Float 1 (- 1)) + horner (x * rapprox_rat prec 2 3 - 1))
else let l = bitlen (mantissa x) - 1 in
Some (ub_ln2 prec * (Float (exponent x + l) 0) + horner (Float (mantissa x) (- l) - 1)))" |
"lb_ln prec x = (if x \<le> 0 then None
else if x < 1 then Some (- the (ub_ln prec (float_divr prec 1 x)))
else let horner = \<lambda>x. x * lb_ln_horner prec (get_even prec) 1 x in
- if x \<le> Float 3 -1 then Some (horner (x - 1))
- else if x < Float 1 1 then Some (horner (Float 1 -1) +
+ if x \<le> Float 3 (- 1) then Some (horner (x - 1))
+ else if x < Float 1 1 then Some (horner (Float 1 (- 1)) +
horner (max (x * lapprox_rat prec 2 3 - 1) 0))
else let l = bitlen (mantissa x) - 1 in
Some (lb_ln2 prec * (Float (exponent x + l) 0) + horner (Float (mantissa x) (- l) - 1)))"
@@ -1761,16 +1761,16 @@
shows "ub_ln prec x = (if x \<le> 0 then None
else if x < 1 then Some (- the (lb_ln prec (float_divl (max prec 1) 1 x)))
else let horner = \<lambda>x. x * ub_ln_horner prec (get_odd prec) 1 x in
- if x \<le> Float 3 -1 then Some (horner (x - 1))
- else if x < Float 1 1 then Some (horner (Float 1 -1) + horner (x * rapprox_rat prec 2 3 - 1))
+ if x \<le> Float 3 (- 1) then Some (horner (x - 1))
+ else if x < Float 1 1 then Some (horner (Float 1 (- 1)) + horner (x * rapprox_rat prec 2 3 - 1))
else let l = bitlen m - 1 in
Some (ub_ln2 prec * (Float (e + l) 0) + horner (Float m (- l) - 1)))"
(is ?th1)
and "lb_ln prec x = (if x \<le> 0 then None
else if x < 1 then Some (- the (ub_ln prec (float_divr prec 1 x)))
else let horner = \<lambda>x. x * lb_ln_horner prec (get_even prec) 1 x in
- if x \<le> Float 3 -1 then Some (horner (x - 1))
- else if x < Float 1 1 then Some (horner (Float 1 -1) +
+ if x \<le> Float 3 (- 1) then Some (horner (x - 1))
+ else if x < Float 1 1 then Some (horner (Float 1 (- 1)) +
horner (max (x * lapprox_rat prec 2 3 - 1) 0))
else let l = bitlen m - 1 in
Some (lb_ln2 prec * (Float (e + l) 0) + horner (Float m (- l) - 1)))"
@@ -1816,10 +1816,10 @@
have "\<not> x \<le> 0" and "\<not> x < 1" using `1 \<le> x` by auto
hence "0 \<le> real (x - 1)" using `1 \<le> x` by auto
- have [simp]: "(Float 3 -1) = 3 / 2" by simp
+ have [simp]: "(Float 3 (- 1)) = 3 / 2" by simp
show ?thesis
- proof (cases "x \<le> Float 3 -1")
+ proof (cases "x \<le> Float 3 (- 1)")
case True
show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
using ln_float_bounds[OF `0 \<le> real (x - 1)` `real (x - 1) < 1`, of prec] `\<not> x \<le> 0` `\<not> x < 1` True
@@ -1856,9 +1856,9 @@
show "0 \<le> real (x * rapprox_rat prec 2 3 - 1)" using pos by auto
qed
finally have "ln x
- \<le> ?ub_horner (Float 1 -1)
+ \<le> ?ub_horner (Float 1 (- 1))
+ ?ub_horner (x * rapprox_rat prec 2 3 - 1)"
- using ln_float_bounds(2)[of "Float 1 -1" prec prec] add by auto }
+ using ln_float_bounds(2)[of "Float 1 (- 1)" prec prec] add by auto }
moreover
{ let ?max = "max (x * lapprox_rat prec 2 3 - 1) 0"
@@ -1884,16 +1884,16 @@
by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
auto simp add: max_def)
qed
- finally have "?lb_horner (Float 1 -1) + ?lb_horner ?max
+ finally have "?lb_horner (Float 1 (- 1)) + ?lb_horner ?max
\<le> ln x"
- using ln_float_bounds(1)[of "Float 1 -1" prec prec] add by auto }
+ using ln_float_bounds(1)[of "Float 1 (- 1)" prec prec] add by auto }
ultimately
show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
using `\<not> x \<le> 0` `\<not> x < 1` True False by auto
qed
next
case False
- hence "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" "\<not> x \<le> Float 3 -1"
+ hence "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" "\<not> x \<le> Float 3 (- 1)"
using `1 \<le> x` by auto
show ?thesis
proof -
@@ -1946,7 +1946,7 @@
unfolding Float ln_shifted_float[OF `0 < m`, of e] by auto
}
ultimately show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps
- unfolding if_not_P[OF `\<not> x \<le> 0`] if_not_P[OF `\<not> x < 1`] if_not_P[OF False] if_not_P[OF `\<not> x \<le> Float 3 -1`] Let_def
+ unfolding if_not_P[OF `\<not> x \<le> 0`] if_not_P[OF `\<not> x < 1`] if_not_P[OF False] if_not_P[OF `\<not> x \<le> Float 3 (- 1)`] Let_def
unfolding plus_float.rep_eq e_def[symmetric] m_def[symmetric] by simp
qed
qed
@@ -2079,14 +2079,14 @@
lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
unfolding interpret_floatarith.simps by simp
-lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
+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
by auto
lemma interpret_floatarith_tan:
- "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (Inverse (Cos a))) vs =
+ "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) (Inverse (Cos a))) vs =
tan (interpret_floatarith a vs)"
unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse
by auto
@@ -2472,7 +2472,7 @@
fun approx_form' and approx_form :: "nat \<Rightarrow> form \<Rightarrow> (float * float) option list \<Rightarrow> nat list \<Rightarrow> bool" where
"approx_form' prec f 0 n l u bs ss = approx_form prec f (bs[n := Some (l, u)]) ss" |
"approx_form' prec f (Suc s) n l u bs ss =
- (let m = (l + u) * Float 1 -1
+ (let m = (l + u) * Float 1 (- 1)
in (if approx_form' prec f s n l m bs ss then approx_form' prec f s n m u bs ss else False))" |
"approx_form prec (Bound (Var n) a b f) bs ss =
(case (approx prec a bs, approx prec b bs)
@@ -2509,7 +2509,7 @@
next
case (Suc s)
- let ?m = "(l + u) * Float 1 -1"
+ let ?m = "(l + u) * Float 1 (- 1)"
have "real l \<le> ?m" and "?m \<le> real u"
unfolding less_eq_float_def using Suc.prems by auto
@@ -2644,7 +2644,7 @@
"DERIV_floatarith x (Mult a b) = Add (Mult a (DERIV_floatarith x b)) (Mult (DERIV_floatarith x a) b)" |
"DERIV_floatarith x (Minus a) = Minus (DERIV_floatarith x a)" |
"DERIV_floatarith x (Inverse a) = Minus (Mult (DERIV_floatarith x a) (Inverse (Power a 2)))" |
-"DERIV_floatarith x (Cos a) = Minus (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (DERIV_floatarith x a))" |
+"DERIV_floatarith x (Cos a) = Minus (Mult (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) (DERIV_floatarith x a))" |
"DERIV_floatarith x (Arctan a) = Mult (Inverse (Add (Num 1) (Power a 2))) (DERIV_floatarith x a)" |
"DERIV_floatarith x (Min a b) = Num 0" |
"DERIV_floatarith x (Max a b) = Num 0" |
@@ -3040,10 +3040,10 @@
fun approx_tse_form' where
"approx_tse_form' prec t f 0 l u cmp =
- (case approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)]
+ (case approx_tse prec 0 t ((l + u) * Float 1 (- 1)) 1 f [Some (l, u)]
of Some (l, u) \<Rightarrow> cmp l u | None \<Rightarrow> False)" |
"approx_tse_form' prec t f (Suc s) l u cmp =
- (let m = (l + u) * Float 1 -1
+ (let m = (l + u) * Float 1 (- 1)
in (if approx_tse_form' prec t f s l m cmp then
approx_tse_form' prec t f s m u cmp else False))"
@@ -3051,16 +3051,16 @@
fixes x :: real
assumes "approx_tse_form' prec t f s l u cmp" and "x \<in> {l .. u}"
shows "\<exists> l' u' ly uy. x \<in> { l' .. u' } \<and> real l \<le> l' \<and> u' \<le> real u \<and> cmp ly uy \<and>
- approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)"
+ approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 f [Some (l', u')] = Some (ly, uy)"
using assms proof (induct s arbitrary: l u)
case 0
then obtain ly uy
- where *: "approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)] = Some (ly, uy)"
+ where *: "approx_tse prec 0 t ((l + u) * Float 1 (- 1)) 1 f [Some (l, u)] = Some (ly, uy)"
and **: "cmp ly uy" by (auto elim!: case_optionE)
with 0 show ?case by auto
next
case (Suc s)
- let ?m = "(l + u) * Float 1 -1"
+ let ?m = "(l + u) * Float 1 (- 1)"
from Suc.prems
have l: "approx_tse_form' prec t f s l ?m cmp"
and u: "approx_tse_form' prec t f s ?m u cmp"
@@ -3077,14 +3077,14 @@
from Suc.hyps[OF l this]
obtain l' u' ly uy
where "x \<in> { l' .. u' } \<and> real l \<le> l' \<and> real u' \<le> ?m \<and> cmp ly uy \<and>
- approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)" by blast
+ approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 f [Some (l', u')] = Some (ly, uy)" by blast
with m_u show ?thesis by (auto intro!: exI)
next
assume "x \<in> { ?m .. u }"
from Suc.hyps[OF u this]
obtain l' u' ly uy
where "x \<in> { l' .. u' } \<and> ?m \<le> real l' \<and> u' \<le> real u \<and> cmp ly uy \<and>
- approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)" by blast
+ approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 f [Some (l', u')] = Some (ly, uy)" by blast
with m_u show ?thesis by (auto intro!: exI)
qed
qed
@@ -3099,7 +3099,7 @@
obtain l' u' ly uy
where x': "x \<in> { l' .. u' }" and "l \<le> real l'"
and "real u' \<le> u" and "0 < ly"
- and tse: "approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
+ and tse: "approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
by blast
hence "bounded_by [x] [Some (l', u')]" by (auto simp add: bounded_by_def)
@@ -3121,7 +3121,7 @@
obtain l' u' ly uy
where x': "x \<in> { l' .. u' }" and "l \<le> real l'"
and "real u' \<le> u" and "0 \<le> ly"
- and tse: "approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
+ and tse: "approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
by blast
hence "bounded_by [x] [Some (l', u')]" by (auto simp add: bounded_by_def)
--- a/src/HOL/Decision_Procs/Cooper.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Sun Sep 21 16:56:11 2014 +0200
@@ -1458,22 +1458,22 @@
recdef \<beta> "measure size"
"\<beta> (And p q) = (\<beta> p @ \<beta> q)"
"\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
- "\<beta> (Eq (CN 0 c e)) = [Sub (C -1) e]"
+ "\<beta> (Eq (CN 0 c e)) = [Sub (C (- 1)) e]"
"\<beta> (NEq (CN 0 c e)) = [Neg e]"
"\<beta> (Lt (CN 0 c e)) = []"
"\<beta> (Le (CN 0 c e)) = []"
"\<beta> (Gt (CN 0 c e)) = [Neg e]"
- "\<beta> (Ge (CN 0 c e)) = [Sub (C -1) e]"
+ "\<beta> (Ge (CN 0 c e)) = [Sub (C (- 1)) e]"
"\<beta> p = []"
consts \<alpha> :: "fm \<Rightarrow> num list"
recdef \<alpha> "measure size"
"\<alpha> (And p q) = \<alpha> p @ \<alpha> q"
"\<alpha> (Or p q) = \<alpha> p @ \<alpha> q"
- "\<alpha> (Eq (CN 0 c e)) = [Add (C -1) e]"
+ "\<alpha> (Eq (CN 0 c e)) = [Add (C (- 1)) e]"
"\<alpha> (NEq (CN 0 c e)) = [e]"
"\<alpha> (Lt (CN 0 c e)) = [e]"
- "\<alpha> (Le (CN 0 c e)) = [Add (C -1) e]"
+ "\<alpha> (Le (CN 0 c e)) = [Add (C (- 1)) e]"
"\<alpha> (Gt (CN 0 c e)) = []"
"\<alpha> (Ge (CN 0 c e)) = []"
"\<alpha> p = []"
@@ -2082,7 +2082,7 @@
moreover
{
assume H: "\<not> (x - d) + ?e \<ge> 0"
- let ?v = "Sub (C -1) e"
+ let ?v = "Sub (C (- 1)) e"
have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))"
by simp
from 8(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="x" and bs="bs"]]
@@ -2109,7 +2109,7 @@
and bn: "numbound0 e"
by simp_all
let ?e = "Inum (x # bs) e"
- let ?v="(Sub (C -1) e)"
+ let ?v="(Sub (C (- 1)) e)"
have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))"
by simp
from p have "x= - ?e"
--- a/src/HOL/Decision_Procs/MIR.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Sun Sep 21 16:56:11 2014 +0200
@@ -2304,21 +2304,21 @@
recdef \<beta> "measure size"
"\<beta> (And p q) = (\<beta> p @ \<beta> q)"
"\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
- "\<beta> (Eq (CN 0 c e)) = [Sub (C -1) e]"
+ "\<beta> (Eq (CN 0 c e)) = [Sub (C (- 1)) e]"
"\<beta> (NEq (CN 0 c e)) = [Neg e]"
"\<beta> (Lt (CN 0 c e)) = []"
"\<beta> (Le (CN 0 c e)) = []"
"\<beta> (Gt (CN 0 c e)) = [Neg e]"
- "\<beta> (Ge (CN 0 c e)) = [Sub (C -1) e]"
+ "\<beta> (Ge (CN 0 c e)) = [Sub (C (- 1)) e]"
"\<beta> p = []"
recdef \<alpha> "measure size"
"\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)"
"\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)"
- "\<alpha> (Eq (CN 0 c e)) = [Add (C -1) e]"
+ "\<alpha> (Eq (CN 0 c e)) = [Add (C (- 1)) e]"
"\<alpha> (NEq (CN 0 c e)) = [e]"
"\<alpha> (Lt (CN 0 c e)) = [e]"
- "\<alpha> (Le (CN 0 c e)) = [Add (C -1) e]"
+ "\<alpha> (Le (CN 0 c e)) = [Add (C (- 1)) e]"
"\<alpha> (Gt (CN 0 c e)) = []"
"\<alpha> (Ge (CN 0 c e)) = []"
"\<alpha> p = []"
@@ -2636,7 +2636,7 @@
by (simp del: real_of_int_minus)}
moreover
{assume H: "\<not> real (x-d) + ?e \<ge> 0"
- let ?v="Sub (C -1) e"
+ let ?v="Sub (C (- 1)) e"
have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
from 8(5)[simplified simp_thms Inum.simps \<beta>.simps list.set bex_simps numbound0_I[OF bn,where b="a" and b'="real x" and bs="bs"]]
have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x = - ?e - 1 + real j)" by auto
@@ -2656,7 +2656,7 @@
case (3 c e) hence p: "Ifm (real x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1"
and bn:"numbound0 e" and ie1: "isint e (a #bs)" using dvd1_eq1[where x="c"] by simp+
let ?e = "Inum (real x # bs) e"
- let ?v="(Sub (C -1) e)"
+ let ?v="(Sub (C (- 1)) e)"
have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
from p have "real x= - ?e" by (simp add: c1) with 3(5) show ?case using dp
by simp (erule ballE[where x="1"],
@@ -2796,7 +2796,7 @@
recdef \<rho> "measure size"
"\<rho> (And p q) = (\<rho> p @ \<rho> q)"
"\<rho> (Or p q) = (\<rho> p @ \<rho> q)"
- "\<rho> (Eq (CN 0 c e)) = [(Sub (C -1) e,c)]"
+ "\<rho> (Eq (CN 0 c e)) = [(Sub (C (- 1)) e,c)]"
"\<rho> (NEq (CN 0 c e)) = [(Neg e,c)]"
"\<rho> (Lt (CN 0 c e)) = []"
"\<rho> (Le (CN 0 c e)) = []"
@@ -2828,10 +2828,10 @@
recdef \<alpha>_\<rho> "measure size"
"\<alpha>_\<rho> (And p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
"\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)"
- "\<alpha>_\<rho> (Eq (CN 0 c e)) = [(Add (C -1) e,c)]"
+ "\<alpha>_\<rho> (Eq (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
"\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
"\<alpha>_\<rho> (Lt (CN 0 c e)) = [(e,c)]"
- "\<alpha>_\<rho> (Le (CN 0 c e)) = [(Add (C -1) e,c)]"
+ "\<alpha>_\<rho> (Le (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
"\<alpha>_\<rho> p = []"
(* Simulates normal substituion by modifying the formula see correctness theorem *)
@@ -4856,9 +4856,9 @@
let ?P = "?I x (plusinf ?rq)"
have MF: "?M = False"
apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
- by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
+ by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))", simp_all)
have PF: "?P = False" apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
- by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
+ by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))", simp_all)
have "(\<exists> x. ?I x ?q ) =
((?I x (minusinf ?rq)) \<or> (?I x (plusinf ?rq )) \<or> (\<exists> (t,n) \<in> set (\<Upsilon> ?rq). \<exists> (s,m) \<in> set (\<Upsilon> ?rq ). ?I x (\<upsilon> ?rq (Add (Mul m t) (Mul n s), 2*n*m))))"
(is "(\<exists> x. ?I x ?q) = (?M \<or> ?P \<or> ?F)" is "?E = ?D")
--- a/src/HOL/Divides.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Divides.thy Sun Sep 21 16:56:11 2014 +0200
@@ -1664,7 +1664,7 @@
lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)"
by (subst posDivAlg.simps, auto)
-lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)"
+lemma negDivAlg_minus1 [simp]: "negDivAlg (- 1) b = (- 1, b - 1)"
by (subst negDivAlg.simps, auto)
lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Sun Sep 21 16:56:11 2014 +0200
@@ -252,7 +252,7 @@
definition "test3_ivl =
''x'' ::= N 0;; ''y'' ::= N 100;; ''z'' ::= Plus (V ''x'') (V ''y'');;
WHILE Less (V ''x'') (N 11)
- DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N -1))"
+ DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N (- 1)))"
value "list_up(AI_ivl test3_ivl Top)"
definition "test4_ivl =
@@ -264,7 +264,7 @@
text{* Nontermination not detected: *}
definition "test5_ivl =
''x'' ::= N 0;;
- WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
+ WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N (- 1))"
value "list_up(AI_ivl test5_ivl Top)"
end
--- a/src/HOL/IMP/Abs_Int_Tests.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Tests.thy Sun Sep 21 16:56:11 2014 +0200
@@ -63,6 +63,6 @@
definition "test6_ivl =
''x'' ::= N 0;;
- WHILE Less (N -1) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
+ WHILE Less (N (- 1)) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
end
--- a/src/HOL/IMP/Hoare_Examples.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy Sun Sep 21 16:56:11 2014 +0200
@@ -17,7 +17,7 @@
abbreviation "wsum ==
WHILE Less (N 0) (V ''x'')
DO (''y'' ::= Plus (V ''y'') (V ''x'');;
- ''x'' ::= Plus (V ''x'') (N -1))"
+ ''x'' ::= Plus (V ''x'') (N (- 1)))"
subsubsection{* Proof by Operational Semantics *}
--- a/src/HOL/Library/Float.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Library/Float.thy Sun Sep 21 16:56:11 2014 +0200
@@ -205,7 +205,7 @@
done
assume "a < b"
then show "\<exists>c. a < c \<and> c < b"
- apply (intro exI[of _ "(a + b) * Float 1 -1"])
+ apply (intro exI[of _ "(a + b) * Float 1 (- 1)"])
apply transfer
apply (simp add: powr_minus)
done
@@ -1085,8 +1085,8 @@
lemma Float_num[simp]: shows
"real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
- "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and
- "real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
+ "real (Float 1 (- 1)) = 1/2" and "real (Float 1 (- 2)) = 1/4" and "real (Float 1 (- 3)) = 1/8" and
+ "real (Float (- 1) 0) = -1" and "real (Float (number_of n) 0) = number_of n"
using two_powr_int_float[of 2] two_powr_int_float[of "-1"] two_powr_int_float[of "-2"] two_powr_int_float[of "-3"]
using powr_realpow[of 2 2] powr_realpow[of 2 3]
using powr_minus[of 2 1] powr_minus[of 2 2] powr_minus[of 2 3]
--- a/src/HOL/MacLaurin.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/MacLaurin.thy Sun Sep 21 16:56:11 2014 +0200
@@ -221,10 +221,10 @@
by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
then guess t ..
moreover
- have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
+ have "(- 1) ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
by (auto simp add: power_mult_distrib[symmetric])
moreover
- have "(SUM m<n. -1 ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m<n. diff m 0 * h ^ m / real (fact m))"
+ have "(SUM m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m<n. diff m 0 * h ^ m / real (fact m))"
by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
ultimately have " h < - t \<and>
- t < 0 \<and>
@@ -561,7 +561,7 @@
?diff n t / real (fact n) * x ^ n" by fast
have diff_m_0:
"\<And>m. ?diff m 0 = (if even m then 0
- else -1 ^ ((m - Suc 0) div 2))"
+ else (- 1) ^ ((m - Suc 0) div 2))"
apply (subst even_even_mod_4_iff)
apply (cut_tac m=m in mod_exhaust_less_4)
apply (elim disjE, simp_all)
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Sun Sep 21 16:56:11 2014 +0200
@@ -146,7 +146,7 @@
using UNIV_2 by auto
have 1: "box (- 1) (1::real^2) \<noteq> {}"
unfolding interval_eq_empty_cart by auto
- have 2: "continuous_on (cbox -1 1) (negatex \<circ> sqprojection \<circ> ?F)"
+ have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
apply (intro continuous_intros continuous_on_component)
unfolding *
apply (rule assms)+
@@ -179,7 +179,7 @@
proof -
case goal1
then obtain y :: "real^2" where y:
- "y \<in> cbox -1 1"
+ "y \<in> cbox (- 1) 1"
"x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y"
unfolding image_iff ..
have "?F y \<noteq> 0"
@@ -208,9 +208,9 @@
qed
qed
obtain x :: "real^2" where x:
- "x \<in> cbox -1 1"
+ "x \<in> cbox (- 1) 1"
"(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
- apply (rule brouwer_weak[of "cbox -1 (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
+ apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
apply (rule compact_cbox convex_box)+
unfolding interior_cbox
apply (rule 1 2 3)+
@@ -362,7 +362,7 @@
unfolding iscale_def by auto
have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
proof (rule fashoda_unit)
- show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1"
+ show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1"
using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
have *: "continuous_on {- 1..1} iscale"
unfolding iscale_def by (rule continuous_intros)+
@@ -506,7 +506,7 @@
"y \<in> {0..1}"
"x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
unfolding image_iff ..
- show "x \<in> cbox -1 1"
+ show "x \<in> cbox (- 1) 1"
unfolding y o_def
apply (rule in_interval_interval_bij)
using y(1)
@@ -520,7 +520,7 @@
"y \<in> {0..1}"
"x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
unfolding image_iff ..
- show "x \<in> cbox -1 1"
+ show "x \<in> cbox (- 1) 1"
unfolding y o_def
apply (rule in_interval_interval_bij)
using y(1)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Sun Sep 21 16:56:11 2014 +0200
@@ -11000,7 +11000,7 @@
shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
proof -
note assm = assms[rule_format]
- have *: "{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R -1 ` {integral s (f k)| k. True}"
+ have *: "{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R (- 1) ` {integral s (f k)| k. True}"
apply safe
unfolding image_iff
apply (rule_tac x="integral s (f k)" in bexI)
--- a/src/HOL/NSA/HyperDef.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/NSA/HyperDef.thy Sun Sep 21 16:56:11 2014 +0200
@@ -523,7 +523,7 @@
done
lemma hyperpow_minus_one2 [simp]:
- "\<And>n. -1 pow (2*n) = (1::hypreal)"
+ "\<And>n. (- 1) pow (2*n) = (1::hypreal)"
by transfer (rule power_minus1_even)
lemma hyperpow_less_le:
--- a/src/HOL/Num.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Num.thy Sun Sep 21 16:56:11 2014 +0200
@@ -280,31 +280,14 @@
syntax
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
+ML_file "Tools/numeral.ML"
+
parse_translation {*
let
- fun num_of_int n =
- if n > 0 then
- (case IntInf.quotRem (n, 2) of
- (0, 1) => Syntax.const @{const_syntax One}
- | (n, 0) => Syntax.const @{const_syntax Bit0} $ num_of_int n
- | (n, 1) => Syntax.const @{const_syntax Bit1} $ num_of_int n)
- else raise Match
- val numeral = Syntax.const @{const_syntax numeral}
- val uminus = Syntax.const @{const_syntax uminus}
- val one = Syntax.const @{const_syntax Groups.one}
- val zero = Syntax.const @{const_syntax Groups.zero}
fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
c $ numeral_tr [t] $ u
| numeral_tr [Const (num, _)] =
- let
- val {value, ...} = Lexicon.read_xnum num;
- in
- if value = 0 then zero else
- if value > 0
- then numeral $ num_of_int value
- else if value = ~1 then uminus $ one
- else uminus $ (numeral $ num_of_int (~ value))
- end
+ (Numeral.mk_number_syntax o #value o Lexicon.read_xnum) num
| numeral_tr ts = raise TERM ("numeral_tr", ts);
in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
*}
@@ -334,8 +317,6 @@
end
*}
-ML_file "Tools/numeral.ML"
-
subsection {* Class-specific numeral rules *}
--- a/src/HOL/Number_Theory/Binomial.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy Sun Sep 21 16:56:11 2014 +0200
@@ -695,19 +695,19 @@
lemma card_UNION:
assumes "finite A" and "\<forall>k \<in> A. finite k"
- shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * int (card (\<Inter>I)))"
+ shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
(is "?lhs = ?rhs")
proof -
- have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
- also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. -1 ^ (card I + 1)))" (is "_ = nat ?rhs")
+ have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
+ also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))" (is "_ = nat ?rhs")
by(subst setsum_right_distrib) simp
- also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. -1 ^ (card I + 1))"
+ also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
using assms by(subst setsum.Sigma)(auto)
- also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). -1 ^ (card I + 1))"
+ also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
by (rule setsum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta)
- also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). -1 ^ (card I + 1))"
+ also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
using assms by(auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
- also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. -1 ^ (card I + 1)))"
+ also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. (- 1) ^ (card I + 1)))"
using assms by(subst setsum.Sigma) auto
also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "setsum ?lhs _ = _")
proof(rule setsum.cong[OF refl])
@@ -722,13 +722,13 @@
using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a]
simp add: card_gt_0_iff[folded Suc_le_eq]
dest: finite_subset intro: card_mono)
- ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))"
+ ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
by (rule setsum.reindex_cong [where l = snd]) fastforce
- also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. -1 ^ (i + 1)))"
+ also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. (- 1) ^ (i + 1)))"
using assms by(subst setsum.Sigma) auto
- also have "\<dots> = (\<Sum>i=1..card A. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
+ also have "\<dots> = (\<Sum>i=1..card A. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
by(subst setsum_right_distrib) simp
- also have "\<dots> = (\<Sum>i=1..card K. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
+ also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
proof(rule setsum.mono_neutral_cong_right[rule_format])
show "{1..card K} \<subseteq> {1..card A}" using `finite A`
by(auto simp add: K_def intro: card_mono)
@@ -740,22 +740,22 @@
by(auto simp add: K_def)
also have "\<dots> = {}" using `finite A` i
by(auto simp add: K_def dest: card_mono[rotated 1])
- finally show "-1 ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
+ finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
by(simp only:) simp
next
fix i
have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)"
(is "?lhs = ?rhs")
by(rule setsum.cong)(auto simp add: K_def)
- thus "-1 ^ (i + 1) * ?lhs = -1 ^ (i + 1) * ?rhs" by simp
+ thus "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs" by simp
qed simp
also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" using assms
by(auto simp add: card_eq_0_iff K_def dest: finite_subset)
- hence "?rhs = (\<Sum>i = 0..card K. -1 ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
+ hence "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
by(subst (2) setsum_head_Suc)(simp_all )
- also have "\<dots> = (\<Sum>i = 0..card K. -1 * (-1 ^ i * int (card K choose i))) + 1"
+ also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
using K by(subst n_subsets[symmetric]) simp_all
- also have "\<dots> = - (\<Sum>i = 0..card K. -1 ^ i * int (card K choose i)) + 1"
+ also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
by(subst setsum_right_distrib[symmetric]) simp
also have "\<dots> = - ((-1 + 1) ^ card K) + 1"
by(subst binomial_ring)(simp add: ac_simps)
--- a/src/HOL/Number_Theory/Gauss.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy Sun Sep 21 16:56:11 2014 +0200
@@ -318,7 +318,7 @@
subsection {* Gauss' Lemma *}
-lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
+lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
theorem pre_gauss_lemma:
@@ -363,7 +363,7 @@
apply (rule cong_trans_int)
apply (simp add: aux cong del:setprod.cong)
done
- with A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
+ with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
by (metis cong_mult_lcancel_int)
then show ?thesis
by (simp add: A_card_eq cong_sym_int)
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Sun Sep 21 16:56:11 2014 +0200
@@ -240,8 +240,8 @@
(* Powers of -1 and parity *)
lemma neg_one_special: "finite A ==>
- ((-1 :: int) ^ card A) * (-1 ^ card A) = 1"
- by (induct set: finite) auto
+ ((- 1) ^ card A) * ((- 1) ^ card A) = (1 :: int)"
+ unfolding power_add [symmetric] by simp
lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1"
by (induct n) auto
--- a/src/HOL/Old_Number_Theory/Gauss.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Sun Sep 21 16:56:11 2014 +0200
@@ -436,7 +436,7 @@
subsection {* Gauss' Lemma *}
-lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
+lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
by (auto simp add: finite_E neg_one_special)
theorem pre_gauss_lemma:
@@ -488,8 +488,8 @@
apply (rule zcong_trans)
apply (simp add: aux cong del:setprod.cong)
done
- with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
- p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
+ with this zcong_cancel2 [of p "setprod id A" "(- 1) ^ card E" "a ^ card A"]
+ p_g_0 A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
by (simp add: order_less_imp_le)
from this show ?thesis
by (simp add: A_card_eq zcong_sym)
--- a/src/HOL/Power.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Power.thy Sun Sep 21 16:56:11 2014 +0200
@@ -214,7 +214,7 @@
by (rule power_minus_Bit0)
lemma power_minus1_even [simp]:
- "-1 ^ (2*n) = 1"
+ "(- 1) ^ (2*n) = 1"
proof (induct n)
case 0 show ?case by simp
next
@@ -222,7 +222,7 @@
qed
lemma power_minus1_odd:
- "-1 ^ Suc (2*n) = -1"
+ "(- 1) ^ Suc (2*n) = -1"
by simp
lemma power_minus_even [simp]:
--- a/src/HOL/Rat.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Rat.thy Sun Sep 21 16:56:11 2014 +0200
@@ -1151,29 +1151,13 @@
parse_translation {*
let
- fun mk_number i =
- let
- fun mk 1 = Syntax.const @{const_syntax Num.One}
- | mk i =
- let
- val (q, r) = Integer.div_mod i 2;
- val bit = if r = 0 then @{const_syntax Num.Bit0} else @{const_syntax Num.Bit1};
- in Syntax.const bit $ (mk q) end;
- in
- if i = 0 then Syntax.const @{const_syntax Groups.zero}
- else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
- else
- Syntax.const @{const_syntax Groups.uminus} $
- (Syntax.const @{const_syntax Num.numeral} $ mk (~ i))
- end;
-
fun mk_frac str =
let
val {mant = i, exp = n} = Lexicon.read_float str;
val exp = Syntax.const @{const_syntax Power.power};
- val ten = mk_number 10;
- val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
- in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
+ val ten = Numeral.mk_number_syntax 10;
+ val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n;;
+ in Syntax.const @{const_syntax divide} $ Numeral.mk_number_syntax i $ exp10 end;
fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
| float_tr [t as Const (str, _)] = mk_frac str
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy Sun Sep 21 16:56:11 2014 +0200
@@ -27,7 +27,7 @@
lemma "27 + 11 = (6::5 word)" by smt
lemma "7 * 3 = (21::8 word)" by smt
lemma "11 - 27 = (-16::8 word)" by smt
-lemma "- -11 = (11::5 word)" by smt
+lemma "- (- 11) = (11::5 word)" by smt
lemma "-40 + 1 = (-39::7 word)" by smt
lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by smt
lemma "x = (5 :: 4 word) \<Longrightarrow> 4 * x = 4" by smt
--- a/src/HOL/Tools/numeral.ML Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Tools/numeral.ML Sun Sep 21 16:56:11 2014 +0200
@@ -8,6 +8,7 @@
sig
val mk_cnumeral: int -> cterm
val mk_cnumber: ctyp -> int -> cterm
+ val mk_number_syntax: int -> term
val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
end;
@@ -60,6 +61,19 @@
end;
+fun mk_num_syntax n =
+ if n > 0 then
+ (case IntInf.quotRem (n, 2) of
+ (0, 1) => Syntax.const @{const_syntax One}
+ | (n, 0) => Syntax.const @{const_syntax Bit0} $ mk_num_syntax n
+ | (n, 1) => Syntax.const @{const_syntax Bit1} $ mk_num_syntax n)
+ else raise Match
+
+fun mk_number_syntax n =
+ if n = 0 then Syntax.const @{const_syntax Groups.zero}
+ else if n = 1 then Syntax.const @{const_syntax Groups.one}
+ else Syntax.const @{const_syntax numeral} $ mk_num_syntax n;
+
(* code generator *)
--- a/src/HOL/Transcendental.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Transcendental.thy Sun Sep 21 16:56:11 2014 +0200
@@ -247,8 +247,8 @@
lemma sums_alternating_upper_lower:
fixes a :: "nat \<Rightarrow> real"
assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
- shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. -1^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. -1^i*a i) ----> l) \<and>
- ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. -1^i*a i) ----> l)"
+ shows "\<exists>l. ((\<forall>n. (\<Sum>i<2*n. (- 1)^i*a i) \<le> l) \<and> (\<lambda> n. \<Sum>i<2*n. (- 1)^i*a i) ----> l) \<and>
+ ((\<forall>n. l \<le> (\<Sum>i<2*n + 1. (- 1)^i*a i)) \<and> (\<lambda> n. \<Sum>i<2*n + 1. (- 1)^i*a i) ----> l)"
(is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
proof (rule nested_sequence_unique)
have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
@@ -367,11 +367,11 @@
assumes a_zero: "a ----> 0" and "monoseq a"
shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable")
and "0 < a 0 \<longrightarrow>
- (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i<2*n. -1^i * a i .. \<Sum>i<2*n+1. -1^i * a i})" (is "?pos")
+ (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n. (- 1)^i * a i .. \<Sum>i<2*n+1. (- 1)^i * a i})" (is "?pos")
and "a 0 < 0 \<longrightarrow>
- (\<forall>n. (\<Sum>i. -1^i*a i) \<in> { \<Sum>i<2*n+1. -1^i * a i .. \<Sum>i<2*n. -1^i * a i})" (is "?neg")
- and "(\<lambda>n. \<Sum>i<2*n. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?f")
- and "(\<lambda>n. \<Sum>i<2*n+1. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?g")
+ (\<forall>n. (\<Sum>i. (- 1)^i*a i) \<in> { \<Sum>i<2*n+1. (- 1)^i * a i .. \<Sum>i<2*n. (- 1)^i * a i})" (is "?neg")
+ and "(\<lambda>n. \<Sum>i<2*n. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?f")
+ and "(\<lambda>n. \<Sum>i<2*n+1. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?g")
proof -
have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g"
proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)")
@@ -413,7 +413,7 @@
unfolding minus_diff_minus by auto
from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
- have move_minus: "(\<Sum>n. - (-1 ^ n * a n)) = - (\<Sum>n. -1 ^ n * a n)"
+ have move_minus: "(\<Sum>n. - ((- 1) ^ n * a n)) = - (\<Sum>n. (- 1) ^ n * a n)"
by auto
have ?pos using `0 \<le> ?a 0` by auto
@@ -1383,7 +1383,7 @@
fix x :: real
assume "x \<in> {- 1<..<1}"
hence "norm (-x) < 1" by auto
- show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
+ show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
unfolding One_nat_def
by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
qed
@@ -2216,10 +2216,10 @@
subsection {* Sine and Cosine *}
definition sin_coeff :: "nat \<Rightarrow> real" where
- "sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))"
+ "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
definition cos_coeff :: "nat \<Rightarrow> real" where
- "cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
+ "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
definition sin :: "real \<Rightarrow> real"
where "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
@@ -2472,7 +2472,7 @@
hence define pi.*}
lemma sin_paired:
- "(\<lambda>n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums sin x"
+ "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums sin x"
proof -
have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
by (rule sin_converges [THEN sums_group], simp)
@@ -2483,7 +2483,7 @@
assumes "0 < x" and "x < 2"
shows "0 < sin x"
proof -
- let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. -1 ^ k / real (fact (2*k+1)) * x^(2*k+1)"
+ let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
have pos: "\<forall>n. 0 < ?f n"
proof
fix n :: nat
@@ -2508,7 +2508,7 @@
lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
using sin_gt_zero [where x = x] by (auto simp add: cos_squared_eq cos_double)
-lemma cos_paired: "(\<lambda>n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
+lemma cos_paired: "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
proof -
have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
by (rule cos_converges [THEN sums_group], simp)
@@ -2541,16 +2541,16 @@
proof -
note fact_Suc [simp del]
from cos_paired
- have "(\<lambda>n. - (-1 ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
+ have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
by (rule sums_minus)
- then have *: "(\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
+ then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
by simp
- then have **: "summable (\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
by (rule sums_summable)
- have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
- moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))
- < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))
+ < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
proof -
{ fix d
have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
@@ -2569,9 +2569,9 @@
from ** show ?thesis by (rule sumr_pos_lt_pair)
(simp add: divide_inverse mult.assoc [symmetric] ***)
qed
- ultimately have "0 < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
by (rule order_less_trans)
- moreover from * have "- cos 2 = (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
+ moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
by (rule sums_unique)
ultimately have "0 < - cos 2" by simp
then show ?thesis by simp
@@ -2677,10 +2677,10 @@
lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
by (simp add: cos_add cos_double)
-lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
+lemma cos_npi [simp]: "cos (real n * pi) = (- 1) ^ n"
by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
-lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
+lemma cos_npi2 [simp]: "cos (pi * real n) = (- 1) ^ n"
by (metis cos_npi mult.commute)
lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
@@ -3754,9 +3754,9 @@
fix x :: real
assume "\<bar>x\<bar> < 1"
hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
- have "summable (\<lambda> n. -1 ^ n * (x\<^sup>2) ^n)"
+ have "summable (\<lambda> n. (- 1) ^ n * (x\<^sup>2) ^n)"
by (rule summable_Leibniz(1), auto intro!: LIMSEQ_realpow_zero monoseq_realpow `x\<^sup>2 < 1` order_less_imp_le[OF `x\<^sup>2 < 1`])
- hence "summable (\<lambda> n. -1 ^ n * x^(2*n))" unfolding power_mult .
+ hence "summable (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
} note summable_Integral = this
{
@@ -3778,17 +3778,17 @@
} note sums_even = this
have Int_eq: "(\<Sum>n. ?f n * real (Suc n) * x^n) = ?Int"
- unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. -1 ^ n * x ^ (2 * n)", symmetric]
+ unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * x ^ (2 * n)", symmetric]
by auto
{
fix x :: real
- have if_eq': "\<And>n. (if even n then -1 ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
- (if even n then -1 ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
+ have if_eq': "\<And>n. (if even n then (- 1) ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
+ (if even n then (- 1) ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
using n_even by auto
have idx_eq: "\<And>n. n * 2 + 1 = Suc (2 * n)" by auto
have "(\<Sum>n. ?f n * x^(Suc n)) = ?arctan x"
- unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. -1 ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
+ unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
by auto
} note arctan_eq = this
@@ -3798,11 +3798,18 @@
{
fix x' :: real
assume x'_bounds: "x' \<in> {- 1 <..< 1}"
- hence "\<bar>x'\<bar> < 1" by auto
-
+ then have "\<bar>x'\<bar> < 1" by auto
+ then
+ have *: "summable (\<lambda>n. (- 1) ^ n * x' ^ (2 * n))"
+ by (rule summable_Integral)
let ?S = "\<Sum> n. (-1)^n * x'^(2 * n)"
show "summable (\<lambda> n. ?f n * real (Suc n) * x'^n)" unfolding if_eq
- by (rule sums_summable[where l="0 + ?S"], rule sums_if, rule sums_zero, rule summable_sums, rule summable_Integral[OF `\<bar>x'\<bar> < 1`])
+ apply (rule sums_summable [where l="0 + ?S"])
+ apply (rule sums_if)
+ apply (rule sums_zero)
+ apply (rule summable_sums)
+ apply (rule *)
+ done
}
qed auto
thus ?thesis unfolding Int_eq arctan_eq .
--- a/src/HOL/Word/Bit_Representation.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Bit_Representation.thy Sun Sep 21 16:56:11 2014 +0200
@@ -98,7 +98,7 @@
lemma bin_last_numeral_simps [simp]:
"\<not> bin_last 0"
"bin_last 1"
- "bin_last -1"
+ "bin_last (- 1)"
"bin_last Numeral1"
"\<not> bin_last (numeral (Num.Bit0 w))"
"bin_last (numeral (Num.Bit1 w))"
@@ -109,7 +109,7 @@
lemma bin_rest_numeral_simps [simp]:
"bin_rest 0 = 0"
"bin_rest 1 = 0"
- "bin_rest -1 = -1"
+ "bin_rest (- 1) = - 1"
"bin_rest Numeral1 = 0"
"bin_rest (numeral (Num.Bit0 w)) = numeral w"
"bin_rest (numeral (Num.Bit1 w)) = numeral w"
@@ -182,7 +182,7 @@
lemma bin_induct:
assumes PPls: "P 0"
- and PMin: "P -1"
+ and PMin: "P (- 1)"
and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
shows "P bin"
apply (rule_tac P=P and a=bin and f1="nat o abs"
@@ -242,7 +242,7 @@
lemma bin_nth_1 [simp]: "bin_nth 1 n \<longleftrightarrow> n = 0"
by (cases n) simp_all
-lemma bin_nth_minus1 [simp]: "bin_nth -1 n"
+lemma bin_nth_minus1 [simp]: "bin_nth (- 1) n"
by (induct n) auto
lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 \<longleftrightarrow> b"
@@ -328,12 +328,12 @@
lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
by (induct n) auto
-lemma sbintrunc_n_minus1 [simp]: "sbintrunc n -1 = -1"
+lemma sbintrunc_n_minus1 [simp]: "sbintrunc n (- 1) = -1"
by (induct n) auto
lemma bintrunc_Suc_numeral:
"bintrunc (Suc n) 1 = 1"
- "bintrunc (Suc n) -1 = bintrunc n -1 BIT True"
+ "bintrunc (Suc n) (- 1) = bintrunc n (- 1) BIT True"
"bintrunc (Suc n) (numeral (Num.Bit0 w)) = bintrunc n (numeral w) BIT False"
"bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT True"
"bintrunc (Suc n) (- numeral (Num.Bit0 w)) =
@@ -678,7 +678,7 @@
lemma bintr_lt2p: "bintrunc n w < 2 ^ n"
by (simp add: bintrunc_mod2p)
-lemma bintr_Min: "bintrunc n -1 = 2 ^ n - 1"
+lemma bintr_Min: "bintrunc n (- 1) = 2 ^ n - 1"
by (simp add: bintrunc_mod2p m1mod2k)
lemma sbintr_ge: "- (2 ^ n) \<le> sbintrunc n w"
--- a/src/HOL/Word/Bits_Int.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Bits_Int.thy Sun Sep 21 16:56:11 2014 +0200
@@ -462,7 +462,7 @@
lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
by (induct n) auto
-lemma bin_sc_TM [simp]: "bin_sc n True -1 = -1"
+lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1"
by (induct n) auto
lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
@@ -583,7 +583,7 @@
by (induct n) auto
lemma bin_split_minus1 [simp]:
- "bin_split n -1 = (-1, bintrunc n -1)"
+ "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
by (induct n) auto
lemma bin_split_trunc:
--- a/src/HOL/Word/Bool_List_Representation.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy Sun Sep 21 16:56:11 2014 +0200
@@ -105,8 +105,8 @@
by (cases n) auto
lemma bin_to_bl_aux_minus1_minus_simp [simp]:
- "0 < n ==> bin_to_bl_aux n -1 bl =
- bin_to_bl_aux (n - 1) -1 (True # bl)"
+ "0 < n ==> bin_to_bl_aux n (- 1) bl =
+ bin_to_bl_aux (n - 1) (- 1) (True # bl)"
by (cases n) auto
lemma bin_to_bl_aux_one_minus_simp [simp]:
@@ -206,10 +206,10 @@
unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux)
lemma bin_to_bl_minus1_aux:
- "bin_to_bl_aux n -1 bl = replicate n True @ bl"
+ "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
-lemma bin_to_bl_minus1: "bin_to_bl n -1 = replicate n True"
+lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux)
lemma bl_to_bin_rep_F:
--- a/src/HOL/Word/Examples/WordExamples.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Examples/WordExamples.thy Sun Sep 21 16:56:11 2014 +0200
@@ -33,13 +33,13 @@
"27 + 11 = (6::5 word)"
"7 * 3 = (21::'a::len word)"
"11 - 27 = (-16::'a::len word)"
- "- -11 = (11::'a::len word)"
+ "- (- 11) = (11::'a::len word)"
"-40 + 1 = (-39::'a::len word)"
by simp_all
lemma "word_pred 2 = 1" by simp
-lemma "word_succ -3 = -2" by simp
+lemma "word_succ (- 3) = -2" by simp
lemma "23 < (27::8 word)" by simp
lemma "23 \<le> (27::8 word)" by simp
@@ -147,11 +147,11 @@
lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp
lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp
lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp
-lemma "word_roti -2 0b0110 = (0b1001::4 word)" by simp
+lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)" by simp
lemma "word_rotr 2 0 = (0::4 word)" by simp
lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops
lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops
-lemma "word_roti -2 1 = (0b0100::4 word)" apply simp? oops
+lemma "word_roti (- 2) 1 = (0b0100::4 word)" apply simp? oops
lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
proof -
--- a/src/HOL/Word/Word.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Word.thy Sun Sep 21 16:56:11 2014 +0200
@@ -1275,7 +1275,7 @@
lemma scast_0 [simp]: "scast 0 = 0"
unfolding scast_def by simp
-lemma sint_n1 [simp] : "sint -1 = -1"
+lemma sint_n1 [simp] : "sint (- 1) = - 1"
unfolding word_m1_wi word_sbin.eq_norm by simp
lemma scast_n1 [simp]: "scast (- 1) = - 1"
@@ -1349,7 +1349,7 @@
lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
-lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
+lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)"
unfolding word_pred_m1 by simp
lemma succ_pred_no [simp]:
@@ -1360,7 +1360,7 @@
unfolding word_succ_p1 word_pred_m1 by simp_all
lemma word_sp_01 [simp] :
- "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
+ "word_succ (- 1) = 0 & word_succ 0 = 1 & word_pred 0 = - 1 & word_pred 1 = 0"
unfolding word_succ_p1 word_pred_m1 by simp_all
(* alternative approach to lifting arithmetic equalities *)
@@ -2803,7 +2803,7 @@
lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
unfolding sshiftr1_def by simp
-lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
+lemma sshiftr1_n1 [simp] : "sshiftr1 (- 1) = - 1"
unfolding sshiftr1_def by simp
lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
@@ -3243,7 +3243,7 @@
lemma mask_bl: "mask n = of_bl (replicate n True)"
by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
-lemma mask_bin: "mask n = word_of_int (bintrunc n -1)"
+lemma mask_bin: "mask n = word_of_int (bintrunc n (- 1))"
by (auto simp add: nth_bintr word_size intro: word_eqI)
lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
@@ -4729,7 +4729,7 @@
done
lemma word_rec_max:
- "\<forall>m\<ge>n. m \<noteq> -1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f -1 = word_rec z f n"
+ "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
apply simp
apply simp
--- a/src/HOL/ex/BinEx.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/ex/BinEx.thy Sun Sep 21 16:56:11 2014 +0200
@@ -98,7 +98,7 @@
lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"
by arith
-lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - -1 < j+j - 3"
+lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - (- 1) < j+j - 3"
by arith
lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"
@@ -262,7 +262,7 @@
lemma "2 ^ 10 = (1024::int)"
by simp
-lemma "-3 ^ 7 = (-2187::int)"
+lemma "(- 3) ^ 7 = (-2187::int)"
by simp
lemma "13 ^ 7 = (62748517::int)"
@@ -271,7 +271,7 @@
lemma "3 ^ 15 = (14348907::int)"
by simp
-lemma "-5 ^ 11 = (-48828125::int)"
+lemma "(- 5) ^ 11 = (-48828125::int)"
by simp
@@ -446,7 +446,7 @@
lemma "2 ^ 15 = (32768::real)"
by simp
-lemma "-3 ^ 7 = (-2187::real)"
+lemma "(- 3) ^ 7 = (-2187::real)"
by simp
lemma "13 ^ 7 = (62748517::real)"
@@ -455,7 +455,7 @@
lemma "3 ^ 15 = (14348907::real)"
by simp
-lemma "-5 ^ 11 = (-48828125::real)"
+lemma "(- 5) ^ 11 = (-48828125::real)"
by simp
--- a/src/Pure/Syntax/lexicon.ML Sun Sep 21 16:56:06 2014 +0200
+++ b/src/Pure/Syntax/lexicon.ML Sun Sep 21 16:56:11 2014 +0200
@@ -98,9 +98,8 @@
val scan_tid = $$$ "'" @@@ scan_id;
val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
+val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat;
val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
-val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat;
-val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot;
val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
@@ -264,15 +263,16 @@
(if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
$$$ "_" @@@ $$$ "_";
- val scan_num = scan_hex || scan_bin || scan_int;
+ val scan_num_unsigned = scan_hex || scan_bin || scan_nat;
+ val scan_num_signed = scan_hex || scan_bin || scan_int;
val scan_val =
scan_tvar >> token TVarSy ||
scan_var >> token VarSy ||
scan_tid >> token TFreeSy ||
scan_float >> token FloatSy ||
- scan_num >> token NumSy ||
- $$$ "#" @@@ scan_num >> token XNumSy ||
+ scan_num_unsigned >> token NumSy ||
+ $$$ "#" @@@ scan_num_signed >> token XNumSy ||
scan_longid >> token LongIdentSy ||
scan_xid >> token IdentSy;