explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
authorhaftmann
Sun Sep 21 16:56:11 2014 +0200 (2014-09-21)
changeset 584106d46ad54a2ab
parent 58409 24096e89c131
child 58411 e3d0354d2129
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
NEWS
src/Doc/Isar_Ref/Inner_Syntax.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Divides.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
src/HOL/IMP/Abs_Int_Tests.thy
src/HOL/IMP/Hoare_Examples.thy
src/HOL/Library/Float.thy
src/HOL/MacLaurin.thy
src/HOL/Multivariate_Analysis/Fashoda.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/NSA/HyperDef.thy
src/HOL/Num.thy
src/HOL/Number_Theory/Binomial.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Old_Number_Theory/EvenOdd.thy
src/HOL/Old_Number_Theory/Gauss.thy
src/HOL/Power.thy
src/HOL/Rat.thy
src/HOL/SMT_Examples/SMT_Word_Examples.thy
src/HOL/Tools/numeral.ML
src/HOL/Transcendental.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Bits_Int.thy
src/HOL/Word/Bool_List_Representation.thy
src/HOL/Word/Examples/WordExamples.thy
src/HOL/Word/Word.thy
src/HOL/ex/BinEx.thy
src/Pure/Syntax/lexicon.ML
     1.1 --- a/NEWS	Sun Sep 21 16:56:06 2014 +0200
     1.2 +++ b/NEWS	Sun Sep 21 16:56:11 2014 +0200
     1.3 @@ -20,6 +20,11 @@
     1.4  * Command "class_deps" takes optional sort arguments constraining
     1.5  the search space.
     1.6  
     1.7 +* Lexical separation of signed and unsigend numerals: categories "num"
     1.8 +and "float" are unsigend.  INCOMPATIBILITY: subtle change in precedence
     1.9 +of numeral signs, particulary in expressions involving infix syntax like
    1.10 +"(- 1) ^ n".
    1.11 +
    1.12  
    1.13  *** HOL ***
    1.14  
     2.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Sep 21 16:56:06 2014 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Sep 21 16:56:11 2014 +0200
     2.3 @@ -599,8 +599,8 @@
     2.4      @{syntax_def (inner) var} & = & @{syntax_ref var} \\
     2.5      @{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
     2.6      @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
     2.7 -    @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat} \\
     2.8 -    @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
     2.9 +    @{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\
    2.10 +    @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
    2.11      @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
    2.12      @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
    2.13      @{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
     3.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sun Sep 21 16:56:06 2014 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Sep 21 16:56:11 2014 +0200
     3.3 @@ -40,7 +40,7 @@
     3.4  lemma horner_schema:
     3.5    fixes f :: "nat \<Rightarrow> nat" and G :: "nat \<Rightarrow> nat \<Rightarrow> nat" and F :: "nat \<Rightarrow> nat"
     3.6    assumes f_Suc: "\<And>n. f (Suc n) = G ((F ^^ n) s) (f n)"
     3.7 -  shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. -1 ^ j * (1 / (f (j' + j))) * x ^ j)"
     3.8 +  shows "horner F G n ((F ^^ j') s) (f j') x = (\<Sum> j = 0..< n. (- 1) ^ j * (1 / (f (j' + j))) * x ^ j)"
     3.9  proof (induct n arbitrary: j')
    3.10    case 0
    3.11    then show ?case by auto
    3.12 @@ -86,8 +86,8 @@
    3.13      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)"
    3.14      and ub_0: "\<And> i k x. ub 0 i k x = 0"
    3.15      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)"
    3.16 -  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
    3.17 -    "(\<Sum>j=0..<n. -1 ^ j * (1 / (f (j' + j))) * (x ^ j)) \<le> (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
    3.18 +  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
    3.19 +    "(\<Sum>j=0..<n. (- 1) ^ j * (1 / (f (j' + j))) * (x ^ j)) \<le> (ub n ((F ^^ j') s) (f j') x)" (is "?ub")
    3.20  proof -
    3.21    have "?lb  \<and> ?ub"
    3.22      using horner_bounds'[where lb=lb, OF `0 \<le> real x` f_Suc lb_0 lb_Suc ub_0 ub_Suc]
    3.23 @@ -107,7 +107,7 @@
    3.24  proof -
    3.25    { fix x y z :: float have "x - y * z = x + - y * z" by simp } note diff_mult_minus = this
    3.26    have sum_eq: "(\<Sum>j=0..<n. (1 / (f (j' + j))) * real x ^ j) =
    3.27 -    (\<Sum>j = 0..<n. -1 ^ j * (1 / (f (j' + j))) * real (- x) ^ j)"
    3.28 +    (\<Sum>j = 0..<n. (- 1) ^ j * (1 / (f (j' + j))) * real (- x) ^ j)"
    3.29      by (auto simp add: field_simps power_mult_distrib[symmetric])
    3.30    have "0 \<le> real (-x)" using assms by auto
    3.31    from horner_bounds[where G=G and F=F and f=f and s=s and prec=prec
    3.32 @@ -166,13 +166,13 @@
    3.33  fun sqrt_iteration :: "nat \<Rightarrow> nat \<Rightarrow> float \<Rightarrow> float" where
    3.34  "sqrt_iteration prec 0 x = Float 1 ((bitlen \<bar>mantissa x\<bar> + exponent x) div 2 + 1)" |
    3.35  "sqrt_iteration prec (Suc m) x = (let y = sqrt_iteration prec m x
    3.36 -                                  in Float 1 -1 * (y + float_divr prec x y))"
    3.37 +                                  in Float 1 (- 1) * (y + float_divr prec x y))"
    3.38  
    3.39  lemma compute_sqrt_iteration_base[code]:
    3.40    shows "sqrt_iteration prec n (Float m e) =
    3.41      (if n = 0 then Float 1 ((if m = 0 then 0 else bitlen \<bar>m\<bar> + e) div 2 + 1)
    3.42      else (let y = sqrt_iteration prec (n - 1) (Float m e) in
    3.43 -      Float 1 -1 * (y + float_divr prec (Float m e) y)))"
    3.44 +      Float 1 (- 1) * (y + float_divr prec (Float m e) y)))"
    3.45    using bitlen_Float by (cases n) simp_all
    3.46  
    3.47  function ub_sqrt lb_sqrt :: "nat \<Rightarrow> float \<Rightarrow> float" where
    3.48 @@ -262,7 +262,7 @@
    3.49    also have "\<dots> < real ?b" using Suc .
    3.50    finally have "sqrt x < (?b + x / ?b)/2" using sqrt_ub_pos_pos_1[OF Suc _ `0 < real x`] by auto
    3.51    also have "\<dots> \<le> (?b + (float_divr prec x ?b))/2" by (rule divide_right_mono, auto simp add: float_divr)
    3.52 -  also have "\<dots> = (Float 1 -1) * (?b + (float_divr prec x ?b))" by simp
    3.53 +  also have "\<dots> = (Float 1 (- 1)) * (?b + (float_divr prec x ?b))" by simp
    3.54    finally show ?case unfolding sqrt_iteration.simps Let_def distrib_left .
    3.55  qed
    3.56  
    3.57 @@ -359,7 +359,7 @@
    3.58    assumes "0 \<le> real x" "real x \<le> 1" and "even n"
    3.59    shows "arctan x \<in> {(x * lb_arctan_horner prec n 1 (x * x)) .. (x * ub_arctan_horner prec (Suc n) 1 (x * x))}"
    3.60  proof -
    3.61 -  let ?c = "\<lambda>i. -1^i * (1 / (i * 2 + (1::nat)) * real x ^ (i * 2 + 1))"
    3.62 +  let ?c = "\<lambda>i. (- 1) ^ i * (1 / (i * 2 + (1::nat)) * real x ^ (i * 2 + 1))"
    3.63    let ?S = "\<lambda>n. \<Sum> i=0..<n. ?c i"
    3.64  
    3.65    have "0 \<le> real (x * x)" by auto
    3.66 @@ -471,20 +471,20 @@
    3.67    "lb_arctan prec x = (let ub_horner = \<lambda> x. x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x) ;
    3.68                             lb_horner = \<lambda> x. x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)
    3.69      in (if x < 0          then - ub_arctan prec (-x) else
    3.70 -        if x \<le> Float 1 -1 then lb_horner x else
    3.71 +        if x \<le> Float 1 (- 1) then lb_horner x else
    3.72          if x \<le> Float 1 1  then Float 1 1 * lb_horner (float_divl prec x (1 + ub_sqrt prec (1 + x * x)))
    3.73                            else (let inv = float_divr prec 1 x
    3.74                                  in if inv > 1 then 0
    3.75 -                                              else lb_pi prec * Float 1 -1 - ub_horner inv)))"
    3.76 +                                              else lb_pi prec * Float 1 (- 1) - ub_horner inv)))"
    3.77  
    3.78  | "ub_arctan prec x = (let lb_horner = \<lambda> x. x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x) ;
    3.79                             ub_horner = \<lambda> x. x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x)
    3.80      in (if x < 0          then - lb_arctan prec (-x) else
    3.81 -        if x \<le> Float 1 -1 then ub_horner x else
    3.82 +        if x \<le> Float 1 (- 1) then ub_horner x else
    3.83          if x \<le> Float 1 1  then let y = float_divr prec x (1 + lb_sqrt prec (1 + x * x))
    3.84 -                               in if y > 1 then ub_pi prec * Float 1 -1
    3.85 +                               in if y > 1 then ub_pi prec * Float 1 (- 1)
    3.86                                             else Float 1 1 * ub_horner y
    3.87 -                          else ub_pi prec * Float 1 -1 - lb_horner (float_divl prec 1 x)))"
    3.88 +                          else ub_pi prec * Float 1 (- 1) - lb_horner (float_divl prec 1 x)))"
    3.89  by pat_completeness auto
    3.90  termination by (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 0 then 1 else 0))", auto)
    3.91  
    3.92 @@ -499,7 +499,7 @@
    3.93      and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)"
    3.94  
    3.95    show ?thesis
    3.96 -  proof (cases "x \<le> Float 1 -1")
    3.97 +  proof (cases "x \<le> Float 1 (- 1)")
    3.98      case True hence "real x \<le> 1" by auto
    3.99      show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True]
   3.100        using arctan_0_1_bounds[OF `0 \<le> real x` `real x \<le> 1`] by auto
   3.101 @@ -543,7 +543,7 @@
   3.102        also have "\<dots> \<le> 2 * arctan (x / ?R)"
   3.103          using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
   3.104        also have "2 * arctan (x / ?R) = arctan x" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
   3.105 -      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] .
   3.106 +      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] .
   3.107      next
   3.108        case False
   3.109        hence "2 < real x" by auto
   3.110 @@ -555,7 +555,7 @@
   3.111        show ?thesis
   3.112        proof (cases "1 < ?invx")
   3.113          case True
   3.114 -        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]
   3.115 +        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]
   3.116            using `0 \<le> arctan x` by auto
   3.117        next
   3.118          case False
   3.119 @@ -570,10 +570,10 @@
   3.120            using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
   3.121            unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
   3.122          moreover
   3.123 -        have "lb_pi prec * Float 1 -1 \<le> pi / 2"
   3.124 +        have "lb_pi prec * Float 1 (- 1) \<le> pi / 2"
   3.125            unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp
   3.126          ultimately
   3.127 -        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]
   3.128 +        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]
   3.129            by auto
   3.130        qed
   3.131      qed
   3.132 @@ -589,7 +589,7 @@
   3.133      and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)"
   3.134  
   3.135    show ?thesis
   3.136 -  proof (cases "x \<le> Float 1 -1")
   3.137 +  proof (cases "x \<le> Float 1 (- 1)")
   3.138      case True hence "real x \<le> 1" by auto
   3.139      show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_P[OF True]
   3.140        using arctan_0_1_bounds[OF `0 \<le> real x` `real x \<le> 1`] by auto
   3.141 @@ -623,9 +623,9 @@
   3.142        show ?thesis
   3.143        proof (cases "?DIV > 1")
   3.144          case True
   3.145 -        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
   3.146 +        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
   3.147          from order_less_le_trans[OF arctan_ubound this, THEN less_imp_le]
   3.148 -        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] .
   3.149 +        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] .
   3.150        next
   3.151          case False
   3.152          hence "real ?DIV \<le> 1" by auto
   3.153 @@ -638,7 +638,7 @@
   3.154            using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
   3.155          also have "\<dots> \<le> (Float 1 1 * ?ub_horner ?DIV)" unfolding Float_num
   3.156            using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
   3.157 -        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] .
   3.158 +        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] .
   3.159        qed
   3.160      next
   3.161        case False
   3.162 @@ -661,9 +661,9 @@
   3.163          using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
   3.164          unfolding real_sgn_pos[OF `0 < 1 / x`] le_diff_eq by auto
   3.165        moreover
   3.166 -      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
   3.167 +      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
   3.168        ultimately
   3.169 -      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]
   3.170 +      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]
   3.171          by auto
   3.172      qed
   3.173    qed
   3.174 @@ -715,8 +715,8 @@
   3.175      (lapprox_rat prec 1 k) - x * (ub_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)"
   3.176  
   3.177  lemma cos_aux:
   3.178 -  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")
   3.179 -  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")
   3.180 +  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")
   3.181 +  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")
   3.182  proof -
   3.183    have "0 \<le> real (x * x)" by auto
   3.184    let "?f n" = "fact (2 * n)"
   3.185 @@ -738,15 +738,15 @@
   3.186    hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
   3.187    have "0 < x * x" using `0 < x` by simp
   3.188  
   3.189 -  { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^ (2 * i))
   3.190 -    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
   3.191 +  { fix x n have "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x ^ (2 * i))
   3.192 +    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
   3.193    proof -
   3.194      have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto
   3.195      also have "\<dots> =
   3.196 -      (\<Sum> j = 0 ..< n. -1 ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
   3.197 -    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then -1 ^ (i div 2) / (real (fact i)) * x ^ i else 0)"
   3.198 +      (\<Sum> j = 0 ..< n. (- 1) ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
   3.199 +    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then (- 1) ^ (i div 2) / (real (fact i)) * x ^ i else 0)"
   3.200        unfolding sum_split_even_odd atLeast0LessThan ..
   3.201 -    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then -1 ^ (i div 2) / (real (fact i)) else 0) * x ^ i)"
   3.202 +    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then (- 1) ^ (i div 2) / (real (fact i)) else 0) * x ^ i)"
   3.203        by (rule setsum.cong) auto
   3.204      finally show ?thesis by assumption
   3.205    qed } note morph_to_if_power = this
   3.206 @@ -755,16 +755,16 @@
   3.207    { fix n :: nat assume "0 < n"
   3.208      hence "0 < 2 * n" by auto
   3.209      obtain t where "0 < t" and "t < real x" and
   3.210 -      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)
   3.211 +      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)
   3.212        + (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
   3.213        (is "_ = ?SUM + ?rest / ?fact * ?pow")
   3.214        using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
   3.215        unfolding cos_coeff_def atLeast0LessThan by auto
   3.216  
   3.217 -    have "cos t * -1^n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
   3.218 +    have "cos t * (- 1) ^ n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
   3.219      also have "\<dots> = cos (t + n * pi)"  using cos_add by auto
   3.220      also have "\<dots> = ?rest" by auto
   3.221 -    finally have "cos t * -1^n = ?rest" .
   3.222 +    finally have "cos t * (- 1) ^ n = ?rest" .
   3.223      moreover
   3.224      have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto
   3.225      hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
   3.226 @@ -828,8 +828,8 @@
   3.227  qed
   3.228  
   3.229  lemma sin_aux: assumes "0 \<le> real x"
   3.230 -  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")
   3.231 -  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")
   3.232 +  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")
   3.233 +  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")
   3.234  proof -
   3.235    have "0 \<le> real (x * x)" by auto
   3.236    let "?f n" = "fact (2 * n + 1)"
   3.237 @@ -854,14 +854,14 @@
   3.238    hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
   3.239    have "0 < x * x" using `0 < x` by simp
   3.240  
   3.241 -  { 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))
   3.242 -    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _")
   3.243 +  { 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))
   3.244 +    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _")
   3.245      proof -
   3.246        have pow: "!!i. x ^ (2 * i + 1) = x * x ^ (2 * i)" by auto
   3.247        have "?SUM = (\<Sum> j = 0 ..< n. 0) + ?SUM" by auto
   3.248 -      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)"
   3.249 +      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)"
   3.250          unfolding sum_split_even_odd atLeast0LessThan ..
   3.251 -      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)"
   3.252 +      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)"
   3.253          by (rule setsum.cong) auto
   3.254        finally show ?thesis by assumption
   3.255      qed } note setsum_morph = this
   3.256 @@ -869,13 +869,13 @@
   3.257    { fix n :: nat assume "0 < n"
   3.258      hence "0 < 2 * n + 1" by auto
   3.259      obtain t where "0 < t" and "t < real x" and
   3.260 -      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)
   3.261 +      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)
   3.262        + (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
   3.263        (is "_ = ?SUM + ?rest / ?fact * ?pow")
   3.264        using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
   3.265        unfolding sin_coeff_def atLeast0LessThan by auto
   3.266  
   3.267 -    have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto
   3.268 +    have "?rest = cos t * (- 1) ^ n" unfolding sin_add cos_add real_of_nat_add distrib_right distrib_left by auto
   3.269      moreover
   3.270      have "t \<le> pi / 2" using `t < real x` and `x \<le> pi / 2` by auto
   3.271      hence "0 \<le> cos t" using `0 < t` and cos_ge_zero by auto
   3.272 @@ -887,7 +887,7 @@
   3.273      {
   3.274        assume "even n"
   3.275        have "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le>
   3.276 -            (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
   3.277 +            (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
   3.278          using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
   3.279        also have "\<dots> \<le> ?SUM" by auto
   3.280        also have "\<dots> \<le> sin x"
   3.281 @@ -908,7 +908,7 @@
   3.282            by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
   3.283          thus ?thesis unfolding sin_eq by auto
   3.284        qed
   3.285 -      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)"
   3.286 +      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)"
   3.287           by auto
   3.288        also have "\<dots> \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))"
   3.289          using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
   3.290 @@ -945,17 +945,17 @@
   3.291  "lb_cos prec x = (let
   3.292      horner = \<lambda> x. lb_sin_cos_aux prec (get_even (prec div 4 + 1)) 1 1 (x * x) ;
   3.293      half = \<lambda> x. if x < 0 then - 1 else Float 1 1 * x * x - 1
   3.294 -  in if x < Float 1 -1 then horner x
   3.295 -else if x < 1          then half (horner (x * Float 1 -1))
   3.296 -                       else half (half (horner (x * Float 1 -2))))"
   3.297 +  in if x < Float 1 (- 1) then horner x
   3.298 +else if x < 1          then half (horner (x * Float 1 (- 1)))
   3.299 +                       else half (half (horner (x * Float 1 (- 2)))))"
   3.300  
   3.301  definition ub_cos :: "nat \<Rightarrow> float \<Rightarrow> float" where
   3.302  "ub_cos prec x = (let
   3.303      horner = \<lambda> x. ub_sin_cos_aux prec (get_odd (prec div 4 + 1)) 1 1 (x * x) ;
   3.304      half = \<lambda> x. Float 1 1 * x * x - 1
   3.305 -  in if x < Float 1 -1 then horner x
   3.306 -else if x < 1          then half (horner (x * Float 1 -1))
   3.307 -                       else half (half (horner (x * Float 1 -2))))"
   3.308 +  in if x < Float 1 (- 1) then horner x
   3.309 +else if x < 1          then half (horner (x * Float 1 (- 1)))
   3.310 +                       else half (half (horner (x * Float 1 (- 2)))))"
   3.311  
   3.312  lemma lb_cos: assumes "0 \<le> real x" and "x \<le> pi"
   3.313    shows "cos x \<in> {(lb_cos prec x) .. (ub_cos prec x)}" (is "?cos x \<in> {(?lb x) .. (?ub x) }")
   3.314 @@ -975,13 +975,13 @@
   3.315    let "?lb_half x" = "if x < 0 then - 1 else Float 1 1 * x * x - 1"
   3.316  
   3.317    show ?thesis
   3.318 -  proof (cases "x < Float 1 -1")
   3.319 +  proof (cases "x < Float 1 (- 1)")
   3.320      case True hence "x \<le> pi / 2" using pi_ge_two by auto
   3.321 -    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
   3.322 +    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
   3.323        using cos_boundaries[OF `0 \<le> real x` `x \<le> pi / 2`] .
   3.324    next
   3.325      case False
   3.326 -    { fix y x :: float let ?x2 = "(x * Float 1 -1)"
   3.327 +    { fix y x :: float let ?x2 = "(x * Float 1 (- 1))"
   3.328        assume "y \<le> cos ?x2" and "-pi \<le> x" and "x \<le> pi"
   3.329        hence "- (pi / 2) \<le> ?x2" and "?x2 \<le> pi / 2" using pi_ge_two unfolding Float_num by auto
   3.330        hence "0 \<le> cos ?x2" by (rule cos_ge_zero)
   3.331 @@ -1000,7 +1000,7 @@
   3.332        qed
   3.333      } note lb_half = this
   3.334  
   3.335 -    { fix y x :: float let ?x2 = "(x * Float 1 -1)"
   3.336 +    { fix y x :: float let ?x2 = "(x * Float 1 (- 1))"
   3.337        assume ub: "cos ?x2 \<le> y" and "- pi \<le> x" and "x \<le> pi"
   3.338        hence "- (pi / 2) \<le> ?x2" and "?x2 \<le> pi / 2" using pi_ge_two unfolding Float_num by auto
   3.339        hence "0 \<le> cos ?x2" by (rule cos_ge_zero)
   3.340 @@ -1016,8 +1016,8 @@
   3.341        qed
   3.342      } note ub_half = this
   3.343  
   3.344 -    let ?x2 = "x * Float 1 -1"
   3.345 -    let ?x4 = "x * Float 1 -1 * Float 1 -1"
   3.346 +    let ?x2 = "x * Float 1 (- 1)"
   3.347 +    let ?x4 = "x * Float 1 (- 1) * Float 1 (- 1)"
   3.348  
   3.349      have "-pi \<le> x" using pi_ge_zero[THEN le_imp_neg_le, unfolded minus_zero] `0 \<le> real x` by (rule order_trans)
   3.350  
   3.351 @@ -1031,12 +1031,12 @@
   3.352        have "(?lb x) \<le> ?cos x"
   3.353        proof -
   3.354          from lb_half[OF lb `-pi \<le> x` `x \<le> pi`]
   3.355 -        show ?thesis unfolding lb_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
   3.356 +        show ?thesis unfolding lb_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 (- 1)` `x < 1` by auto
   3.357        qed
   3.358        moreover have "?cos x \<le> (?ub x)"
   3.359        proof -
   3.360          from ub_half[OF ub `-pi \<le> x` `x \<le> pi`]
   3.361 -        show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
   3.362 +        show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 (- 1)` `x < 1` by auto
   3.363        qed
   3.364        ultimately show ?thesis by auto
   3.365      next
   3.366 @@ -1045,19 +1045,19 @@
   3.367        from cos_boundaries[OF this]
   3.368        have lb: "(?lb_horner ?x4) \<le> ?cos ?x4" and ub: "?cos ?x4 \<le> (?ub_horner ?x4)" by auto
   3.369  
   3.370 -      have eq_4: "?x2 * Float 1 -1 = x * Float 1 -2" by transfer simp
   3.371 +      have eq_4: "?x2 * Float 1 (- 1) = x * Float 1 (- 2)" by transfer simp
   3.372  
   3.373        have "(?lb x) \<le> ?cos x"
   3.374        proof -
   3.375          have "-pi \<le> ?x2" and "?x2 \<le> pi" using pi_ge_two `0 \<le> real x` `x \<le> pi` by auto
   3.376          from lb_half[OF lb_half[OF lb this] `-pi \<le> x` `x \<le> pi`, unfolded eq_4]
   3.377 -        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 .
   3.378 +        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 .
   3.379        qed
   3.380        moreover have "?cos x \<le> (?ub x)"
   3.381        proof -
   3.382          have "-pi \<le> ?x2" and "?x2 \<le> pi" using pi_ge_two `0 \<le> real x` ` x \<le> pi` by auto
   3.383          from ub_half[OF ub_half[OF ub this] `-pi \<le> x` `x \<le> pi`, unfolded eq_4]
   3.384 -        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 .
   3.385 +        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 .
   3.386        qed
   3.387        ultimately show ?thesis by auto
   3.388      qed
   3.389 @@ -1081,9 +1081,9 @@
   3.390    in   if - lpi \<le> lx \<and> ux \<le> 0    then (lb_cos prec (-lx), ub_cos prec (-ux))
   3.391    else if 0 \<le> lx \<and> ux \<le> lpi      then (lb_cos prec ux, ub_cos prec lx)
   3.392    else if - lpi \<le> lx \<and> ux \<le> lpi  then (min (lb_cos prec (-lx)) (lb_cos prec ux), Float 1 0)
   3.393 -  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))))
   3.394 -  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)))
   3.395 -                                 else (Float -1 0, Float 1 0))"
   3.396 +  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))))
   3.397 +  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)))
   3.398 +                                 else (Float (- 1) 0, Float 1 0))"
   3.399  
   3.400  lemma floor_int:
   3.401    obtains k :: int where "real k = (floor_fl f)"
   3.402 @@ -1233,7 +1233,7 @@
   3.403    next case False note 3 = this show ?thesis
   3.404    proof (cases "0 \<le> ?lx \<and> ?ux \<le> 2 * ?lpi")
   3.405      case True note Cond = this with bnds 1 2 3
   3.406 -    have l: "l = Float -1 0"
   3.407 +    have l: "l = Float (- 1) 0"
   3.408        and u: "u = max (ub_cos prec ?lx) (ub_cos prec (- (?ux - 2 * ?lpi)))"
   3.409        by (auto simp add: bnds_cos_def Let_def)
   3.410  
   3.411 @@ -1275,7 +1275,7 @@
   3.412    next case False note 4 = this show ?thesis
   3.413    proof (cases "-2 * ?lpi \<le> ?lx \<and> ?ux \<le> 0")
   3.414      case True note Cond = this with bnds 1 2 3 4
   3.415 -    have l: "l = Float -1 0"
   3.416 +    have l: "l = Float (- 1) 0"
   3.417        and u: "u = max (ub_cos prec (?lx + 2 * ?lpi)) (ub_cos prec (-?ux))"
   3.418        by (auto simp add: bnds_cos_def Let_def)
   3.419  
   3.420 @@ -1379,7 +1379,7 @@
   3.421  function ub_exp :: "nat \<Rightarrow> float \<Rightarrow> float" and lb_exp :: "nat \<Rightarrow> float \<Rightarrow> float" where
   3.422  "lb_exp prec x = (if 0 < x then float_divl prec 1 (ub_exp prec (-x))
   3.423               else let
   3.424 -                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)
   3.425 +                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)
   3.426               in if x < - 1 then (horner (float_divl prec x (- floor_fl x))) ^ nat (- int_floor_fl x)
   3.427                             else horner x)" |
   3.428  "ub_exp prec x = (if 0 < x    then float_divr prec 1 (lb_exp prec (-x))
   3.429 @@ -1392,7 +1392,7 @@
   3.430  proof -
   3.431    have eq4: "4 = Suc (Suc (Suc (Suc 0)))" by auto
   3.432  
   3.433 -  have "1 / 4 = (Float 1 -2)" unfolding Float_num by auto
   3.434 +  have "1 / 4 = (Float 1 (- 2))" unfolding Float_num by auto
   3.435    also have "\<dots> \<le> lb_exp_horner 1 (get_even 4) 1 1 (- 1)"
   3.436      unfolding get_even_def eq4
   3.437      by (auto simp add: Float.compute_lapprox_rat Float.compute_rapprox_rat
   3.438 @@ -1404,7 +1404,7 @@
   3.439  lemma lb_exp_pos: assumes "\<not> 0 < x" shows "0 < lb_exp prec x"
   3.440  proof -
   3.441    let "?lb_horner x" = "lb_exp_horner prec (get_even (prec + 2)) 1 1 x"
   3.442 -  let "?horner x" = "let  y = ?lb_horner x  in if y \<le> 0 then Float 1 -2 else y"
   3.443 +  let "?horner x" = "let  y = ?lb_horner x  in if y \<le> 0 then Float 1 (- 2) else y"
   3.444    have pos_horner: "\<And> x. 0 < ?horner x" unfolding Let_def by (cases "?lb_horner x \<le> 0", auto)
   3.445    moreover { fix x :: float fix num :: nat
   3.446      have "0 < real (?horner x) ^ num" using `0 < ?horner x` by simp
   3.447 @@ -1431,7 +1431,7 @@
   3.448        from `\<not> x < - 1` have "- 1 \<le> real x" by auto
   3.449        hence "exp (- 1) \<le> exp x" unfolding exp_le_cancel_iff .
   3.450        from order_trans[OF exp_m1_ge_quarter this]
   3.451 -      have "Float 1 -2 \<le> exp x" unfolding Float_num .
   3.452 +      have "Float 1 (- 2) \<le> exp x" unfolding Float_num .
   3.453        moreover case True
   3.454        ultimately show ?thesis using bnds_exp_horner `real x \<le> 0` `\<not> x > 0` `\<not> x < - 1` by auto
   3.455      next
   3.456 @@ -1502,8 +1502,8 @@
   3.457          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`]]
   3.458          have "- 1 \<le> x / (- floor_fl x)" unfolding minus_float.rep_eq by auto
   3.459          from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
   3.460 -        have "Float 1 -2 \<le> exp (x / (- floor_fl x))" unfolding Float_num .
   3.461 -        hence "real (Float 1 -2) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
   3.462 +        have "Float 1 (- 2) \<le> exp (x / (- floor_fl x))" unfolding Float_num .
   3.463 +        hence "real (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
   3.464            by (auto intro!: power_mono)
   3.465          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
   3.466          finally show ?thesis
   3.467 @@ -1582,12 +1582,12 @@
   3.468  
   3.469  lemma ln_bounds:
   3.470    assumes "0 \<le> x" and "x < 1"
   3.471 -  shows "(\<Sum>i=0..<2*n. -1^i * (1 / real (i + 1)) * x ^ (Suc i)) \<le> ln (x + 1)" (is "?lb")
   3.472 -  and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. -1^i * (1 / real (i + 1)) * x ^ (Suc i))" (is "?ub")
   3.473 +  shows "(\<Sum>i=0..<2*n. (- 1) ^ i * (1 / real (i + 1)) * x ^ (Suc i)) \<le> ln (x + 1)" (is "?lb")
   3.474 +  and "ln (x + 1) \<le> (\<Sum>i=0..<2*n + 1. (- 1) ^ i * (1 / real (i + 1)) * x ^ (Suc i))" (is "?ub")
   3.475  proof -
   3.476    let "?a n" = "(1/real (n +1)) * x ^ (Suc n)"
   3.477  
   3.478 -  have ln_eq: "(\<Sum> i. -1^i * ?a i) = ln (x + 1)"
   3.479 +  have ln_eq: "(\<Sum> i. (- 1) ^ i * ?a i) = ln (x + 1)"
   3.480      using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
   3.481  
   3.482    have "norm x < 1" using assms by auto
   3.483 @@ -1613,7 +1613,7 @@
   3.484    obtain ev where ev: "get_even n = 2 * ev" using get_even_double ..
   3.485    obtain od where od: "get_odd n = 2 * od + 1" using get_odd_double ..
   3.486  
   3.487 -  let "?s n" = "-1^n * (1 / real (1 + n)) * (real x)^(Suc n)"
   3.488 +  let "?s n" = "(- 1) ^ n * (1 / real (1 + n)) * (real x)^(Suc n)"
   3.489  
   3.490    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
   3.491      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",
   3.492 @@ -1643,10 +1643,10 @@
   3.493  subsection "Compute the logarithm of 2"
   3.494  
   3.495  definition ub_ln2 where "ub_ln2 prec = (let third = rapprox_rat (max prec 1) 1 3
   3.496 -                                        in (Float 1 -1 * ub_ln_horner prec (get_odd prec) 1 (Float 1 -1)) +
   3.497 +                                        in (Float 1 (- 1) * ub_ln_horner prec (get_odd prec) 1 (Float 1 (- 1))) +
   3.498                                             (third * ub_ln_horner prec (get_odd prec) 1 third))"
   3.499  definition lb_ln2 where "lb_ln2 prec = (let third = lapprox_rat prec 1 3
   3.500 -                                        in (Float 1 -1 * lb_ln_horner prec (get_even prec) 1 (Float 1 -1)) +
   3.501 +                                        in (Float 1 (- 1) * lb_ln_horner prec (get_even prec) 1 (Float 1 (- 1))) +
   3.502                                             (third * lb_ln_horner prec (get_even prec) 1 third))"
   3.503  
   3.504  lemma ub_ln2: "ln 2 \<le> ub_ln2 prec" (is "?ub_ln2")
   3.505 @@ -1663,7 +1663,7 @@
   3.506    have ub3: "1 / 3 \<le> ?uthird" using rapprox_rat[of 1 3] by auto
   3.507    hence ub3_lb: "0 \<le> real ?uthird" by auto
   3.508  
   3.509 -  have lb2: "0 \<le> real (Float 1 -1)" and ub2: "real (Float 1 -1) < 1" unfolding Float_num by auto
   3.510 +  have lb2: "0 \<le> real (Float 1 (- 1))" and ub2: "real (Float 1 (- 1)) < 1" unfolding Float_num by auto
   3.511  
   3.512    have "0 \<le> (1::int)" and "0 < (3::int)" by auto
   3.513    have ub3_ub: "real ?uthird < 1" by (simp add: Float.compute_rapprox_rat rapprox_posrat_less1)
   3.514 @@ -1694,15 +1694,15 @@
   3.515  "ub_ln prec x = (if x \<le> 0          then None
   3.516              else if x < 1          then Some (- the (lb_ln prec (float_divl (max prec 1) 1 x)))
   3.517              else let horner = \<lambda>x. x * ub_ln_horner prec (get_odd prec) 1 x in
   3.518 -                 if x \<le> Float 3 -1 then Some (horner (x - 1))
   3.519 -            else if x < Float 1 1  then Some (horner (Float 1 -1) + horner (x * rapprox_rat prec 2 3 - 1))
   3.520 +                 if x \<le> Float 3 (- 1) then Some (horner (x - 1))
   3.521 +            else if x < Float 1 1  then Some (horner (Float 1 (- 1)) + horner (x * rapprox_rat prec 2 3 - 1))
   3.522                                     else let l = bitlen (mantissa x) - 1 in
   3.523                                          Some (ub_ln2 prec * (Float (exponent x + l) 0) + horner (Float (mantissa x) (- l) - 1)))" |
   3.524  "lb_ln prec x = (if x \<le> 0          then None
   3.525              else if x < 1          then Some (- the (ub_ln prec (float_divr prec 1 x)))
   3.526              else let horner = \<lambda>x. x * lb_ln_horner prec (get_even prec) 1 x in
   3.527 -                 if x \<le> Float 3 -1 then Some (horner (x - 1))
   3.528 -            else if x < Float 1 1  then Some (horner (Float 1 -1) +
   3.529 +                 if x \<le> Float 3 (- 1) then Some (horner (x - 1))
   3.530 +            else if x < Float 1 1  then Some (horner (Float 1 (- 1)) +
   3.531                                                horner (max (x * lapprox_rat prec 2 3 - 1) 0))
   3.532                                     else let l = bitlen (mantissa x) - 1 in
   3.533                                          Some (lb_ln2 prec * (Float (exponent x + l) 0) + horner (Float (mantissa x) (- l) - 1)))"
   3.534 @@ -1761,16 +1761,16 @@
   3.535    shows "ub_ln prec x = (if x \<le> 0          then None
   3.536                else if x < 1          then Some (- the (lb_ln prec (float_divl (max prec 1) 1 x)))
   3.537              else let horner = \<lambda>x. x * ub_ln_horner prec (get_odd prec) 1 x in
   3.538 -                 if x \<le> Float 3 -1 then Some (horner (x - 1))
   3.539 -            else if x < Float 1 1  then Some (horner (Float 1 -1) + horner (x * rapprox_rat prec 2 3 - 1))
   3.540 +                 if x \<le> Float 3 (- 1) then Some (horner (x - 1))
   3.541 +            else if x < Float 1 1  then Some (horner (Float 1 (- 1)) + horner (x * rapprox_rat prec 2 3 - 1))
   3.542                                     else let l = bitlen m - 1 in
   3.543                                          Some (ub_ln2 prec * (Float (e + l) 0) + horner (Float m (- l) - 1)))"
   3.544      (is ?th1)
   3.545    and "lb_ln prec x = (if x \<le> 0          then None
   3.546              else if x < 1          then Some (- the (ub_ln prec (float_divr prec 1 x)))
   3.547              else let horner = \<lambda>x. x * lb_ln_horner prec (get_even prec) 1 x in
   3.548 -                 if x \<le> Float 3 -1 then Some (horner (x - 1))
   3.549 -            else if x < Float 1 1  then Some (horner (Float 1 -1) +
   3.550 +                 if x \<le> Float 3 (- 1) then Some (horner (x - 1))
   3.551 +            else if x < Float 1 1  then Some (horner (Float 1 (- 1)) +
   3.552                                                horner (max (x * lapprox_rat prec 2 3 - 1) 0))
   3.553                                     else let l = bitlen m - 1 in
   3.554                                          Some (lb_ln2 prec * (Float (e + l) 0) + horner (Float m (- l) - 1)))"
   3.555 @@ -1816,10 +1816,10 @@
   3.556    have "\<not> x \<le> 0" and "\<not> x < 1" using `1 \<le> x` by auto
   3.557    hence "0 \<le> real (x - 1)" using `1 \<le> x` by auto
   3.558  
   3.559 -  have [simp]: "(Float 3 -1) = 3 / 2" by simp
   3.560 +  have [simp]: "(Float 3 (- 1)) = 3 / 2" by simp
   3.561  
   3.562    show ?thesis
   3.563 -  proof (cases "x \<le> Float 3 -1")
   3.564 +  proof (cases "x \<le> Float 3 (- 1)")
   3.565      case True
   3.566      show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
   3.567        using ln_float_bounds[OF `0 \<le> real (x - 1)` `real (x - 1) < 1`, of prec] `\<not> x \<le> 0` `\<not> x < 1` True
   3.568 @@ -1856,9 +1856,9 @@
   3.569          show "0 \<le> real (x * rapprox_rat prec 2 3 - 1)" using pos by auto
   3.570        qed
   3.571        finally have "ln x
   3.572 -        \<le> ?ub_horner (Float 1 -1)
   3.573 +        \<le> ?ub_horner (Float 1 (- 1))
   3.574            + ?ub_horner (x * rapprox_rat prec 2 3 - 1)"
   3.575 -        using ln_float_bounds(2)[of "Float 1 -1" prec prec] add by auto }
   3.576 +        using ln_float_bounds(2)[of "Float 1 (- 1)" prec prec] add by auto }
   3.577      moreover
   3.578      { let ?max = "max (x * lapprox_rat prec 2 3 - 1) 0"
   3.579  
   3.580 @@ -1884,16 +1884,16 @@
   3.581            by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
   3.582                auto simp add: max_def)
   3.583        qed
   3.584 -      finally have "?lb_horner (Float 1 -1) + ?lb_horner ?max
   3.585 +      finally have "?lb_horner (Float 1 (- 1)) + ?lb_horner ?max
   3.586          \<le> ln x"
   3.587 -        using ln_float_bounds(1)[of "Float 1 -1" prec prec] add by auto }
   3.588 +        using ln_float_bounds(1)[of "Float 1 (- 1)" prec prec] add by auto }
   3.589      ultimately
   3.590      show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
   3.591        using `\<not> x \<le> 0` `\<not> x < 1` True False by auto
   3.592    qed
   3.593  next
   3.594    case False
   3.595 -  hence "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" "\<not> x \<le> Float 3 -1"
   3.596 +  hence "\<not> x \<le> 0" and "\<not> x < 1" "0 < x" "\<not> x \<le> Float 3 (- 1)"
   3.597      using `1 \<le> x` by auto
   3.598    show ?thesis
   3.599    proof -
   3.600 @@ -1946,7 +1946,7 @@
   3.601          unfolding Float ln_shifted_float[OF `0 < m`, of e] by auto
   3.602      }
   3.603      ultimately show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps
   3.604 -      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
   3.605 +      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
   3.606        unfolding plus_float.rep_eq e_def[symmetric] m_def[symmetric] by simp
   3.607    qed
   3.608  qed
   3.609 @@ -2079,14 +2079,14 @@
   3.610  lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
   3.611    unfolding interpret_floatarith.simps by simp
   3.612  
   3.613 -lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
   3.614 +lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) vs =
   3.615    sin (interpret_floatarith a vs)"
   3.616    unfolding sin_cos_eq interpret_floatarith.simps
   3.617              interpret_floatarith_divide interpret_floatarith_diff
   3.618    by auto
   3.619  
   3.620  lemma interpret_floatarith_tan:
   3.621 -  "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (Inverse (Cos a))) vs =
   3.622 +  "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) (Inverse (Cos a))) vs =
   3.623     tan (interpret_floatarith a vs)"
   3.624    unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse
   3.625    by auto
   3.626 @@ -2472,7 +2472,7 @@
   3.627  fun approx_form' and approx_form :: "nat \<Rightarrow> form \<Rightarrow> (float * float) option list \<Rightarrow> nat list \<Rightarrow> bool" where
   3.628  "approx_form' prec f 0 n l u bs ss = approx_form prec f (bs[n := Some (l, u)]) ss" |
   3.629  "approx_form' prec f (Suc s) n l u bs ss =
   3.630 -  (let m = (l + u) * Float 1 -1
   3.631 +  (let m = (l + u) * Float 1 (- 1)
   3.632     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))" |
   3.633  "approx_form prec (Bound (Var n) a b f) bs ss =
   3.634     (case (approx prec a bs, approx prec b bs)
   3.635 @@ -2509,7 +2509,7 @@
   3.636  next
   3.637    case (Suc s)
   3.638  
   3.639 -  let ?m = "(l + u) * Float 1 -1"
   3.640 +  let ?m = "(l + u) * Float 1 (- 1)"
   3.641    have "real l \<le> ?m" and "?m \<le> real u"
   3.642      unfolding less_eq_float_def using Suc.prems by auto
   3.643  
   3.644 @@ -2644,7 +2644,7 @@
   3.645  "DERIV_floatarith x (Mult a b)        = Add (Mult a (DERIV_floatarith x b)) (Mult (DERIV_floatarith x a) b)" |
   3.646  "DERIV_floatarith x (Minus a)         = Minus (DERIV_floatarith x a)" |
   3.647  "DERIV_floatarith x (Inverse a)       = Minus (Mult (DERIV_floatarith x a) (Inverse (Power a 2)))" |
   3.648 -"DERIV_floatarith x (Cos a)           = Minus (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (DERIV_floatarith x a))" |
   3.649 +"DERIV_floatarith x (Cos a)           = Minus (Mult (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) (DERIV_floatarith x a))" |
   3.650  "DERIV_floatarith x (Arctan a)        = Mult (Inverse (Add (Num 1) (Power a 2))) (DERIV_floatarith x a)" |
   3.651  "DERIV_floatarith x (Min a b)         = Num 0" |
   3.652  "DERIV_floatarith x (Max a b)         = Num 0" |
   3.653 @@ -3040,10 +3040,10 @@
   3.654  
   3.655  fun approx_tse_form' where
   3.656  "approx_tse_form' prec t f 0 l u cmp =
   3.657 -  (case approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)]
   3.658 +  (case approx_tse prec 0 t ((l + u) * Float 1 (- 1)) 1 f [Some (l, u)]
   3.659       of Some (l, u) \<Rightarrow> cmp l u | None \<Rightarrow> False)" |
   3.660  "approx_tse_form' prec t f (Suc s) l u cmp =
   3.661 -  (let m = (l + u) * Float 1 -1
   3.662 +  (let m = (l + u) * Float 1 (- 1)
   3.663     in (if approx_tse_form' prec t f s l m cmp then
   3.664        approx_tse_form' prec t f s m u cmp else False))"
   3.665  
   3.666 @@ -3051,16 +3051,16 @@
   3.667    fixes x :: real
   3.668    assumes "approx_tse_form' prec t f s l u cmp" and "x \<in> {l .. u}"
   3.669    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>
   3.670 -                  approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)"
   3.671 +                  approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 f [Some (l', u')] = Some (ly, uy)"
   3.672  using assms proof (induct s arbitrary: l u)
   3.673    case 0
   3.674    then obtain ly uy
   3.675 -    where *: "approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)] = Some (ly, uy)"
   3.676 +    where *: "approx_tse prec 0 t ((l + u) * Float 1 (- 1)) 1 f [Some (l, u)] = Some (ly, uy)"
   3.677      and **: "cmp ly uy" by (auto elim!: case_optionE)
   3.678    with 0 show ?case by auto
   3.679  next
   3.680    case (Suc s)
   3.681 -  let ?m = "(l + u) * Float 1 -1"
   3.682 +  let ?m = "(l + u) * Float 1 (- 1)"
   3.683    from Suc.prems
   3.684    have l: "approx_tse_form' prec t f s l ?m cmp"
   3.685      and u: "approx_tse_form' prec t f s ?m u cmp"
   3.686 @@ -3077,14 +3077,14 @@
   3.687      from Suc.hyps[OF l this]
   3.688      obtain l' u' ly uy
   3.689        where "x \<in> { l' .. u' } \<and> real l \<le> l' \<and> real u' \<le> ?m \<and> cmp ly uy \<and>
   3.690 -                  approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)" by blast
   3.691 +                  approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 f [Some (l', u')] = Some (ly, uy)" by blast
   3.692      with m_u show ?thesis by (auto intro!: exI)
   3.693    next
   3.694      assume "x \<in> { ?m .. u }"
   3.695      from Suc.hyps[OF u this]
   3.696      obtain l' u' ly uy
   3.697        where "x \<in> { l' .. u' } \<and> ?m \<le> real l' \<and> u' \<le> real u \<and> cmp ly uy \<and>
   3.698 -                  approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)" by blast
   3.699 +                  approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 f [Some (l', u')] = Some (ly, uy)" by blast
   3.700      with m_u show ?thesis by (auto intro!: exI)
   3.701    qed
   3.702  qed
   3.703 @@ -3099,7 +3099,7 @@
   3.704    obtain l' u' ly uy
   3.705      where x': "x \<in> { l' .. u' }" and "l \<le> real l'"
   3.706      and "real u' \<le> u" and "0 < ly"
   3.707 -    and tse: "approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
   3.708 +    and tse: "approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
   3.709      by blast
   3.710  
   3.711    hence "bounded_by [x] [Some (l', u')]" by (auto simp add: bounded_by_def)
   3.712 @@ -3121,7 +3121,7 @@
   3.713    obtain l' u' ly uy
   3.714      where x': "x \<in> { l' .. u' }" and "l \<le> real l'"
   3.715      and "real u' \<le> u" and "0 \<le> ly"
   3.716 -    and tse: "approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
   3.717 +    and tse: "approx_tse prec 0 t ((l' + u') * Float 1 (- 1)) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
   3.718      by blast
   3.719  
   3.720    hence "bounded_by [x] [Some (l', u')]" by (auto simp add: bounded_by_def)
     4.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sun Sep 21 16:56:06 2014 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Sep 21 16:56:11 2014 +0200
     4.3 @@ -1458,22 +1458,22 @@
     4.4  recdef \<beta> "measure size"
     4.5    "\<beta> (And p q) = (\<beta> p @ \<beta> q)"
     4.6    "\<beta> (Or p q) = (\<beta> p @ \<beta> q)"
     4.7 -  "\<beta> (Eq  (CN 0 c e)) = [Sub (C -1) e]"
     4.8 +  "\<beta> (Eq  (CN 0 c e)) = [Sub (C (- 1)) e]"
     4.9    "\<beta> (NEq (CN 0 c e)) = [Neg e]"
    4.10    "\<beta> (Lt  (CN 0 c e)) = []"
    4.11    "\<beta> (Le  (CN 0 c e)) = []"
    4.12    "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
    4.13 -  "\<beta> (Ge  (CN 0 c e)) = [Sub (C -1) e]"
    4.14 +  "\<beta> (Ge  (CN 0 c e)) = [Sub (C (- 1)) e]"
    4.15    "\<beta> p = []"
    4.16  
    4.17  consts \<alpha> :: "fm \<Rightarrow> num list"
    4.18  recdef \<alpha> "measure size"
    4.19    "\<alpha> (And p q) = \<alpha> p @ \<alpha> q"
    4.20    "\<alpha> (Or p q) = \<alpha> p @ \<alpha> q"
    4.21 -  "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"
    4.22 +  "\<alpha> (Eq  (CN 0 c e)) = [Add (C (- 1)) e]"
    4.23    "\<alpha> (NEq (CN 0 c e)) = [e]"
    4.24    "\<alpha> (Lt  (CN 0 c e)) = [e]"
    4.25 -  "\<alpha> (Le  (CN 0 c e)) = [Add (C -1) e]"
    4.26 +  "\<alpha> (Le  (CN 0 c e)) = [Add (C (- 1)) e]"
    4.27    "\<alpha> (Gt  (CN 0 c e)) = []"
    4.28    "\<alpha> (Ge  (CN 0 c e)) = []"
    4.29    "\<alpha> p = []"
    4.30 @@ -2082,7 +2082,7 @@
    4.31    moreover
    4.32    {
    4.33      assume H: "\<not> (x - d) + ?e \<ge> 0"
    4.34 -    let ?v = "Sub (C -1) e"
    4.35 +    let ?v = "Sub (C (- 1)) e"
    4.36      have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))"
    4.37        by simp
    4.38      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"]]
    4.39 @@ -2109,7 +2109,7 @@
    4.40      and bn: "numbound0 e"
    4.41      by simp_all
    4.42    let ?e = "Inum (x # bs) e"
    4.43 -  let ?v="(Sub (C -1) e)"
    4.44 +  let ?v="(Sub (C (- 1)) e)"
    4.45    have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))"
    4.46      by simp
    4.47    from p have "x= - ?e"
     5.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun Sep 21 16:56:06 2014 +0200
     5.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun Sep 21 16:56:11 2014 +0200
     5.3 @@ -2304,21 +2304,21 @@
     5.4  recdef \<beta> "measure size"
     5.5    "\<beta> (And p q) = (\<beta> p @ \<beta> q)" 
     5.6    "\<beta> (Or p q) = (\<beta> p @ \<beta> q)" 
     5.7 -  "\<beta> (Eq  (CN 0 c e)) = [Sub (C -1) e]"
     5.8 +  "\<beta> (Eq  (CN 0 c e)) = [Sub (C (- 1)) e]"
     5.9    "\<beta> (NEq (CN 0 c e)) = [Neg e]"
    5.10    "\<beta> (Lt  (CN 0 c e)) = []"
    5.11    "\<beta> (Le  (CN 0 c e)) = []"
    5.12    "\<beta> (Gt  (CN 0 c e)) = [Neg e]"
    5.13 -  "\<beta> (Ge  (CN 0 c e)) = [Sub (C -1) e]"
    5.14 +  "\<beta> (Ge  (CN 0 c e)) = [Sub (C (- 1)) e]"
    5.15    "\<beta> p = []"
    5.16  
    5.17  recdef \<alpha> "measure size"
    5.18    "\<alpha> (And p q) = (\<alpha> p @ \<alpha> q)" 
    5.19    "\<alpha> (Or p q) = (\<alpha> p @ \<alpha> q)" 
    5.20 -  "\<alpha> (Eq  (CN 0 c e)) = [Add (C -1) e]"
    5.21 +  "\<alpha> (Eq  (CN 0 c e)) = [Add (C (- 1)) e]"
    5.22    "\<alpha> (NEq (CN 0 c e)) = [e]"
    5.23    "\<alpha> (Lt  (CN 0 c e)) = [e]"
    5.24 -  "\<alpha> (Le  (CN 0 c e)) = [Add (C -1) e]"
    5.25 +  "\<alpha> (Le  (CN 0 c e)) = [Add (C (- 1)) e]"
    5.26    "\<alpha> (Gt  (CN 0 c e)) = []"
    5.27    "\<alpha> (Ge  (CN 0 c e)) = []"
    5.28    "\<alpha> p = []"
    5.29 @@ -2636,7 +2636,7 @@
    5.30          by (simp del: real_of_int_minus)}
    5.31      moreover
    5.32      {assume H: "\<not> real (x-d) + ?e \<ge> 0" 
    5.33 -      let ?v="Sub (C -1) e"
    5.34 +      let ?v="Sub (C (- 1)) e"
    5.35        have vb: "?v \<in> set (\<beta> (Ge (CN 0 c e)))" by simp
    5.36        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"]] 
    5.37        have nob: "\<not> (\<exists> j\<in> {1 ..d}. real x =  - ?e - 1 + real j)" by auto 
    5.38 @@ -2656,7 +2656,7 @@
    5.39    case (3 c e) hence p: "Ifm (real x #bs) (Eq (CN 0 c e))" (is "?p x") and c1: "c=1" 
    5.40      and bn:"numbound0 e" and ie1: "isint e (a #bs)" using dvd1_eq1[where x="c"] by simp+
    5.41      let ?e = "Inum (real x # bs) e"
    5.42 -    let ?v="(Sub (C -1) e)"
    5.43 +    let ?v="(Sub (C (- 1)) e)"
    5.44      have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))" by simp
    5.45      from p have "real x= - ?e" by (simp add: c1) with 3(5) show ?case using dp
    5.46        by simp (erule ballE[where x="1"],
    5.47 @@ -2796,7 +2796,7 @@
    5.48  recdef \<rho> "measure size"
    5.49    "\<rho> (And p q) = (\<rho> p @ \<rho> q)" 
    5.50    "\<rho> (Or p q) = (\<rho> p @ \<rho> q)" 
    5.51 -  "\<rho> (Eq  (CN 0 c e)) = [(Sub (C -1) e,c)]"
    5.52 +  "\<rho> (Eq  (CN 0 c e)) = [(Sub (C (- 1)) e,c)]"
    5.53    "\<rho> (NEq (CN 0 c e)) = [(Neg e,c)]"
    5.54    "\<rho> (Lt  (CN 0 c e)) = []"
    5.55    "\<rho> (Le  (CN 0 c e)) = []"
    5.56 @@ -2828,10 +2828,10 @@
    5.57  recdef \<alpha>_\<rho> "measure size"
    5.58    "\<alpha>_\<rho> (And p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)" 
    5.59    "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)" 
    5.60 -  "\<alpha>_\<rho> (Eq  (CN 0 c e)) = [(Add (C -1) e,c)]"
    5.61 +  "\<alpha>_\<rho> (Eq  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
    5.62    "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
    5.63    "\<alpha>_\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
    5.64 -  "\<alpha>_\<rho> (Le  (CN 0 c e)) = [(Add (C -1) e,c)]"
    5.65 +  "\<alpha>_\<rho> (Le  (CN 0 c e)) = [(Add (C (- 1)) e,c)]"
    5.66    "\<alpha>_\<rho> p = []"
    5.67  
    5.68      (* Simulates normal substituion by modifying the formula see correctness theorem *)
    5.69 @@ -4856,9 +4856,9 @@
    5.70    let ?P = "?I x (plusinf ?rq)"
    5.71    have MF: "?M = False"
    5.72      apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
    5.73 -    by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
    5.74 +    by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))", simp_all)
    5.75    have PF: "?P = False" apply (simp add: Let_def reducecoeff_def numgcd_def rsplit_def ge_def lt_def conj_def disj_def)
    5.76 -    by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C -1)))", simp_all)
    5.77 +    by (cases "rlfm p = And (Ge (CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))", simp_all)
    5.78    have "(\<exists> x. ?I x ?q ) = 
    5.79      ((?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))))"
    5.80      (is "(\<exists> x. ?I x ?q) = (?M \<or> ?P \<or> ?F)" is "?E = ?D")
     6.1 --- a/src/HOL/Divides.thy	Sun Sep 21 16:56:06 2014 +0200
     6.2 +++ b/src/HOL/Divides.thy	Sun Sep 21 16:56:11 2014 +0200
     6.3 @@ -1664,7 +1664,7 @@
     6.4  lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)"
     6.5  by (subst posDivAlg.simps, auto)
     6.6  
     6.7 -lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)"
     6.8 +lemma negDivAlg_minus1 [simp]: "negDivAlg (- 1) b = (- 1, b - 1)"
     6.9  by (subst negDivAlg.simps, auto)
    6.10  
    6.11  lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"
     7.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Sun Sep 21 16:56:06 2014 +0200
     7.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Sun Sep 21 16:56:11 2014 +0200
     7.3 @@ -252,7 +252,7 @@
     7.4  definition "test3_ivl =
     7.5   ''x'' ::= N 0;; ''y'' ::= N 100;; ''z'' ::= Plus (V ''x'') (V ''y'');;
     7.6   WHILE Less (V ''x'') (N 11)
     7.7 - DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N -1))"
     7.8 + DO (''x'' ::= Plus (V ''x'') (N 1);; ''y'' ::= Plus (V ''y'') (N (- 1)))"
     7.9  value "list_up(AI_ivl test3_ivl Top)"
    7.10  
    7.11  definition "test4_ivl =
    7.12 @@ -264,7 +264,7 @@
    7.13  text{* Nontermination not detected: *}
    7.14  definition "test5_ivl =
    7.15   ''x'' ::= N 0;;
    7.16 - WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
    7.17 + WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N (- 1))"
    7.18  value "list_up(AI_ivl test5_ivl Top)"
    7.19  
    7.20  end
     8.1 --- a/src/HOL/IMP/Abs_Int_Tests.thy	Sun Sep 21 16:56:06 2014 +0200
     8.2 +++ b/src/HOL/IMP/Abs_Int_Tests.thy	Sun Sep 21 16:56:11 2014 +0200
     8.3 @@ -63,6 +63,6 @@
     8.4  
     8.5  definition "test6_ivl =
     8.6   ''x'' ::= N 0;;
     8.7 - WHILE Less (N -1) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
     8.8 + WHILE Less (N (- 1)) (V ''x'') DO ''x'' ::= Plus (V ''x'') (N 1)"
     8.9  
    8.10  end
     9.1 --- a/src/HOL/IMP/Hoare_Examples.thy	Sun Sep 21 16:56:06 2014 +0200
     9.2 +++ b/src/HOL/IMP/Hoare_Examples.thy	Sun Sep 21 16:56:11 2014 +0200
     9.3 @@ -17,7 +17,7 @@
     9.4  abbreviation "wsum ==
     9.5    WHILE Less (N 0) (V ''x'')
     9.6    DO (''y'' ::= Plus (V ''y'') (V ''x'');;
     9.7 -      ''x'' ::= Plus (V ''x'') (N -1))"
     9.8 +      ''x'' ::= Plus (V ''x'') (N (- 1)))"
     9.9  
    9.10  
    9.11  subsubsection{* Proof by Operational Semantics *}
    10.1 --- a/src/HOL/Library/Float.thy	Sun Sep 21 16:56:06 2014 +0200
    10.2 +++ b/src/HOL/Library/Float.thy	Sun Sep 21 16:56:11 2014 +0200
    10.3 @@ -205,7 +205,7 @@
    10.4      done
    10.5    assume "a < b"
    10.6    then show "\<exists>c. a < c \<and> c < b"
    10.7 -    apply (intro exI[of _ "(a + b) * Float 1 -1"])
    10.8 +    apply (intro exI[of _ "(a + b) * Float 1 (- 1)"])
    10.9      apply transfer
   10.10      apply (simp add: powr_minus)
   10.11      done
   10.12 @@ -1085,8 +1085,8 @@
   10.13  
   10.14  lemma Float_num[simp]: shows
   10.15     "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
   10.16 -   "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and
   10.17 -   "real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
   10.18 +   "real (Float 1 (- 1)) = 1/2" and "real (Float 1 (- 2)) = 1/4" and "real (Float 1 (- 3)) = 1/8" and
   10.19 +   "real (Float (- 1) 0) = -1" and "real (Float (number_of n) 0) = number_of n"
   10.20  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"]
   10.21  using powr_realpow[of 2 2] powr_realpow[of 2 3]
   10.22  using powr_minus[of 2 1] powr_minus[of 2 2] powr_minus[of 2 3]
    11.1 --- a/src/HOL/MacLaurin.thy	Sun Sep 21 16:56:06 2014 +0200
    11.2 +++ b/src/HOL/MacLaurin.thy	Sun Sep 21 16:56:11 2014 +0200
    11.3 @@ -221,10 +221,10 @@
    11.4      by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
    11.5    then guess t ..
    11.6    moreover
    11.7 -  have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
    11.8 +  have "(- 1) ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
    11.9      by (auto simp add: power_mult_distrib[symmetric])
   11.10    moreover
   11.11 -  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))"
   11.12 +  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))"
   11.13      by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
   11.14    ultimately have " h < - t \<and>
   11.15      - t < 0 \<and>
   11.16 @@ -561,7 +561,7 @@
   11.17        ?diff n t / real (fact n) * x ^ n" by fast
   11.18    have diff_m_0:
   11.19      "\<And>m. ?diff m 0 = (if even m then 0
   11.20 -         else -1 ^ ((m - Suc 0) div 2))"
   11.21 +         else (- 1) ^ ((m - Suc 0) div 2))"
   11.22      apply (subst even_even_mod_4_iff)
   11.23      apply (cut_tac m=m in mod_exhaust_less_4)
   11.24      apply (elim disjE, simp_all)
    12.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 21 16:56:06 2014 +0200
    12.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 21 16:56:11 2014 +0200
    12.3 @@ -146,7 +146,7 @@
    12.4      using UNIV_2 by auto
    12.5    have 1: "box (- 1) (1::real^2) \<noteq> {}"
    12.6      unfolding interval_eq_empty_cart by auto
    12.7 -  have 2: "continuous_on (cbox -1 1) (negatex \<circ> sqprojection \<circ> ?F)"
    12.8 +  have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
    12.9      apply (intro continuous_intros continuous_on_component)
   12.10      unfolding *
   12.11      apply (rule assms)+
   12.12 @@ -179,7 +179,7 @@
   12.13    proof -
   12.14      case goal1
   12.15      then obtain y :: "real^2" where y:
   12.16 -        "y \<in> cbox -1 1"
   12.17 +        "y \<in> cbox (- 1) 1"
   12.18          "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y"
   12.19        unfolding image_iff ..
   12.20      have "?F y \<noteq> 0"
   12.21 @@ -208,9 +208,9 @@
   12.22      qed
   12.23    qed
   12.24    obtain x :: "real^2" where x:
   12.25 -      "x \<in> cbox -1 1"
   12.26 +      "x \<in> cbox (- 1) 1"
   12.27        "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
   12.28 -    apply (rule brouwer_weak[of "cbox -1 (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
   12.29 +    apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
   12.30      apply (rule compact_cbox convex_box)+
   12.31      unfolding interior_cbox
   12.32      apply (rule 1 2 3)+
   12.33 @@ -362,7 +362,7 @@
   12.34      unfolding iscale_def by auto
   12.35    have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
   12.36    proof (rule fashoda_unit)
   12.37 -    show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox -1 1"
   12.38 +    show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1"
   12.39        using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
   12.40      have *: "continuous_on {- 1..1} iscale"
   12.41        unfolding iscale_def by (rule continuous_intros)+
   12.42 @@ -506,7 +506,7 @@
   12.43          "y \<in> {0..1}"
   12.44          "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
   12.45        unfolding image_iff ..
   12.46 -    show "x \<in> cbox -1 1"
   12.47 +    show "x \<in> cbox (- 1) 1"
   12.48        unfolding y o_def
   12.49        apply (rule in_interval_interval_bij)
   12.50        using y(1)
   12.51 @@ -520,7 +520,7 @@
   12.52          "y \<in> {0..1}"
   12.53          "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
   12.54        unfolding image_iff ..
   12.55 -    show "x \<in> cbox -1 1"
   12.56 +    show "x \<in> cbox (- 1) 1"
   12.57        unfolding y o_def
   12.58        apply (rule in_interval_interval_bij)
   12.59        using y(1)
    13.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Sep 21 16:56:06 2014 +0200
    13.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Sep 21 16:56:11 2014 +0200
    13.3 @@ -11000,7 +11000,7 @@
    13.4    shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
    13.5  proof -
    13.6    note assm = assms[rule_format]
    13.7 -  have *: "{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R -1 ` {integral s (f k)| k. True}"
    13.8 +  have *: "{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R (- 1) ` {integral s (f k)| k. True}"
    13.9      apply safe
   13.10      unfolding image_iff
   13.11      apply (rule_tac x="integral s (f k)" in bexI)
    14.1 --- a/src/HOL/NSA/HyperDef.thy	Sun Sep 21 16:56:06 2014 +0200
    14.2 +++ b/src/HOL/NSA/HyperDef.thy	Sun Sep 21 16:56:11 2014 +0200
    14.3 @@ -523,7 +523,7 @@
    14.4  done
    14.5  
    14.6  lemma hyperpow_minus_one2 [simp]:
    14.7 -     "\<And>n. -1 pow (2*n) = (1::hypreal)"
    14.8 +     "\<And>n. (- 1) pow (2*n) = (1::hypreal)"
    14.9  by transfer (rule power_minus1_even)
   14.10  
   14.11  lemma hyperpow_less_le:
    15.1 --- a/src/HOL/Num.thy	Sun Sep 21 16:56:06 2014 +0200
    15.2 +++ b/src/HOL/Num.thy	Sun Sep 21 16:56:11 2014 +0200
    15.3 @@ -280,31 +280,14 @@
    15.4  syntax
    15.5    "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
    15.6  
    15.7 +ML_file "Tools/numeral.ML"
    15.8 +
    15.9  parse_translation {*
   15.10    let
   15.11 -    fun num_of_int n =
   15.12 -      if n > 0 then
   15.13 -        (case IntInf.quotRem (n, 2) of
   15.14 -          (0, 1) => Syntax.const @{const_syntax One}
   15.15 -        | (n, 0) => Syntax.const @{const_syntax Bit0} $ num_of_int n
   15.16 -        | (n, 1) => Syntax.const @{const_syntax Bit1} $ num_of_int n)
   15.17 -      else raise Match
   15.18 -    val numeral = Syntax.const @{const_syntax numeral}
   15.19 -    val uminus = Syntax.const @{const_syntax uminus}
   15.20 -    val one = Syntax.const @{const_syntax Groups.one}
   15.21 -    val zero = Syntax.const @{const_syntax Groups.zero}
   15.22      fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
   15.23            c $ numeral_tr [t] $ u
   15.24        | numeral_tr [Const (num, _)] =
   15.25 -          let
   15.26 -            val {value, ...} = Lexicon.read_xnum num;
   15.27 -          in
   15.28 -            if value = 0 then zero else
   15.29 -            if value > 0
   15.30 -            then numeral $ num_of_int value
   15.31 -            else if value = ~1 then uminus $ one
   15.32 -            else uminus $ (numeral $ num_of_int (~ value))
   15.33 -          end
   15.34 +          (Numeral.mk_number_syntax o #value o Lexicon.read_xnum) num
   15.35        | numeral_tr ts = raise TERM ("numeral_tr", ts);
   15.36    in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
   15.37  *}
   15.38 @@ -334,8 +317,6 @@
   15.39    end
   15.40  *}
   15.41  
   15.42 -ML_file "Tools/numeral.ML"
   15.43 -
   15.44  
   15.45  subsection {* Class-specific numeral rules *}
   15.46  
    16.1 --- a/src/HOL/Number_Theory/Binomial.thy	Sun Sep 21 16:56:06 2014 +0200
    16.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Sun Sep 21 16:56:11 2014 +0200
    16.3 @@ -695,19 +695,19 @@
    16.4  
    16.5  lemma card_UNION:
    16.6    assumes "finite A" and "\<forall>k \<in> A. finite k"
    16.7 -  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * int (card (\<Inter>I)))"
    16.8 +  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
    16.9    (is "?lhs = ?rhs")
   16.10  proof -
   16.11 -  have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. -1 ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
   16.12 -  also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. -1 ^ (card I + 1)))" (is "_ = nat ?rhs")
   16.13 +  have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
   16.14 +  also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))" (is "_ = nat ?rhs")
   16.15      by(subst setsum_right_distrib) simp
   16.16 -  also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. -1 ^ (card I + 1))"
   16.17 +  also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
   16.18      using assms by(subst setsum.Sigma)(auto)
   16.19 -  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))"
   16.20 +  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))"
   16.21      by (rule setsum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta)
   16.22 -  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))"
   16.23 +  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))"
   16.24      using assms by(auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
   16.25 -  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)))" 
   16.26 +  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)))" 
   16.27      using assms by(subst setsum.Sigma) auto
   16.28    also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "setsum ?lhs _ = _")
   16.29    proof(rule setsum.cong[OF refl])
   16.30 @@ -722,13 +722,13 @@
   16.31        using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a]
   16.32          simp add: card_gt_0_iff[folded Suc_le_eq]
   16.33          dest: finite_subset intro: card_mono)
   16.34 -    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). -1 ^ (i + 1))"
   16.35 +    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
   16.36        by (rule setsum.reindex_cong [where l = snd]) fastforce
   16.37 -    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)))"
   16.38 +    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)))"
   16.39        using assms by(subst setsum.Sigma) auto
   16.40 -    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))"
   16.41 +    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))"
   16.42        by(subst setsum_right_distrib) simp
   16.43 -    also have "\<dots> = (\<Sum>i=1..card K. -1 ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
   16.44 +    also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
   16.45      proof(rule setsum.mono_neutral_cong_right[rule_format])
   16.46        show "{1..card K} \<subseteq> {1..card A}" using `finite A`
   16.47          by(auto simp add: K_def intro: card_mono)
   16.48 @@ -740,22 +740,22 @@
   16.49          by(auto simp add: K_def)
   16.50        also have "\<dots> = {}" using `finite A` i
   16.51          by(auto simp add: K_def dest: card_mono[rotated 1])
   16.52 -      finally show "-1 ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
   16.53 +      finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
   16.54          by(simp only:) simp
   16.55      next
   16.56        fix i
   16.57        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)"
   16.58          (is "?lhs = ?rhs")
   16.59          by(rule setsum.cong)(auto simp add: K_def)
   16.60 -      thus "-1 ^ (i + 1) * ?lhs = -1 ^ (i + 1) * ?rhs" by simp
   16.61 +      thus "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs" by simp
   16.62      qed simp
   16.63      also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" using assms
   16.64        by(auto simp add: card_eq_0_iff K_def dest: finite_subset)
   16.65 -    hence "?rhs = (\<Sum>i = 0..card K. -1 ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
   16.66 +    hence "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
   16.67        by(subst (2) setsum_head_Suc)(simp_all )
   16.68 -    also have "\<dots> = (\<Sum>i = 0..card K. -1 * (-1 ^ i * int (card K choose i))) + 1"
   16.69 +    also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
   16.70        using K by(subst n_subsets[symmetric]) simp_all
   16.71 -    also have "\<dots> = - (\<Sum>i = 0..card K. -1 ^ i * int (card K choose i)) + 1"
   16.72 +    also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
   16.73        by(subst setsum_right_distrib[symmetric]) simp
   16.74      also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
   16.75        by(subst binomial_ring)(simp add: ac_simps)
    17.1 --- a/src/HOL/Number_Theory/Gauss.thy	Sun Sep 21 16:56:06 2014 +0200
    17.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sun Sep 21 16:56:11 2014 +0200
    17.3 @@ -318,7 +318,7 @@
    17.4  
    17.5  subsection {* Gauss' Lemma *}
    17.6  
    17.7 -lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
    17.8 +lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
    17.9  by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
   17.10  
   17.11  theorem pre_gauss_lemma:
   17.12 @@ -363,7 +363,7 @@
   17.13      apply (rule cong_trans_int)
   17.14      apply (simp add: aux cong del:setprod.cong)
   17.15      done
   17.16 -  with A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
   17.17 +  with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
   17.18      by (metis cong_mult_lcancel_int)
   17.19    then show ?thesis
   17.20      by (simp add: A_card_eq cong_sym_int)
    18.1 --- a/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Sep 21 16:56:06 2014 +0200
    18.2 +++ b/src/HOL/Old_Number_Theory/EvenOdd.thy	Sun Sep 21 16:56:11 2014 +0200
    18.3 @@ -240,8 +240,8 @@
    18.4  (* Powers of -1 and parity *)
    18.5  
    18.6  lemma neg_one_special: "finite A ==>
    18.7 -    ((-1 :: int) ^ card A) * (-1 ^ card A) = 1"
    18.8 -  by (induct set: finite) auto
    18.9 +  ((- 1) ^ card A) * ((- 1) ^ card A) = (1 :: int)"
   18.10 +  unfolding power_add [symmetric] by simp
   18.11  
   18.12  lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1"
   18.13    by (induct n) auto
    19.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy	Sun Sep 21 16:56:06 2014 +0200
    19.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sun Sep 21 16:56:11 2014 +0200
    19.3 @@ -436,7 +436,7 @@
    19.4  
    19.5  subsection {* Gauss' Lemma *}
    19.6  
    19.7 -lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
    19.8 +lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
    19.9    by (auto simp add: finite_E neg_one_special)
   19.10  
   19.11  theorem pre_gauss_lemma:
   19.12 @@ -488,8 +488,8 @@
   19.13      apply (rule zcong_trans)
   19.14      apply (simp add: aux cong del:setprod.cong)
   19.15      done
   19.16 -  with this zcong_cancel2 [of p "setprod id A" "-1 ^ card E" "a ^ card A"]
   19.17 -      p_g_0 A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
   19.18 +  with this zcong_cancel2 [of p "setprod id A" "(- 1) ^ card E" "a ^ card A"]
   19.19 +      p_g_0 A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
   19.20      by (simp add: order_less_imp_le)
   19.21    from this show ?thesis
   19.22      by (simp add: A_card_eq zcong_sym)
    20.1 --- a/src/HOL/Power.thy	Sun Sep 21 16:56:06 2014 +0200
    20.2 +++ b/src/HOL/Power.thy	Sun Sep 21 16:56:11 2014 +0200
    20.3 @@ -214,7 +214,7 @@
    20.4    by (rule power_minus_Bit0)
    20.5  
    20.6  lemma power_minus1_even [simp]:
    20.7 -  "-1 ^ (2*n) = 1"
    20.8 +  "(- 1) ^ (2*n) = 1"
    20.9  proof (induct n)
   20.10    case 0 show ?case by simp
   20.11  next
   20.12 @@ -222,7 +222,7 @@
   20.13  qed
   20.14  
   20.15  lemma power_minus1_odd:
   20.16 -  "-1 ^ Suc (2*n) = -1"
   20.17 +  "(- 1) ^ Suc (2*n) = -1"
   20.18    by simp
   20.19  
   20.20  lemma power_minus_even [simp]:
    21.1 --- a/src/HOL/Rat.thy	Sun Sep 21 16:56:06 2014 +0200
    21.2 +++ b/src/HOL/Rat.thy	Sun Sep 21 16:56:11 2014 +0200
    21.3 @@ -1151,29 +1151,13 @@
    21.4  
    21.5  parse_translation {*
    21.6    let
    21.7 -    fun mk_number i =
    21.8 -      let
    21.9 -        fun mk 1 = Syntax.const @{const_syntax Num.One}
   21.10 -          | mk i =
   21.11 -              let
   21.12 -                val (q, r) = Integer.div_mod i 2;
   21.13 -                val bit = if r = 0 then @{const_syntax Num.Bit0} else @{const_syntax Num.Bit1};
   21.14 -              in Syntax.const bit $ (mk q) end;
   21.15 -      in
   21.16 -        if i = 0 then Syntax.const @{const_syntax Groups.zero}
   21.17 -        else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
   21.18 -        else
   21.19 -          Syntax.const @{const_syntax Groups.uminus} $
   21.20 -            (Syntax.const @{const_syntax Num.numeral} $ mk (~ i))
   21.21 -      end;
   21.22 -
   21.23      fun mk_frac str =
   21.24        let
   21.25          val {mant = i, exp = n} = Lexicon.read_float str;
   21.26          val exp = Syntax.const @{const_syntax Power.power};
   21.27 -        val ten = mk_number 10;
   21.28 -        val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
   21.29 -      in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
   21.30 +        val ten = Numeral.mk_number_syntax 10;
   21.31 +        val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n;;
   21.32 +      in Syntax.const @{const_syntax divide} $ Numeral.mk_number_syntax i $ exp10 end;
   21.33  
   21.34      fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
   21.35        | float_tr [t as Const (str, _)] = mk_frac str
    22.1 --- a/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Sun Sep 21 16:56:06 2014 +0200
    22.2 +++ b/src/HOL/SMT_Examples/SMT_Word_Examples.thy	Sun Sep 21 16:56:11 2014 +0200
    22.3 @@ -27,7 +27,7 @@
    22.4  lemma "27 + 11 = (6::5 word)" by smt
    22.5  lemma "7 * 3 = (21::8 word)" by smt
    22.6  lemma "11 - 27 = (-16::8 word)" by smt
    22.7 -lemma "- -11 = (11::5 word)" by smt
    22.8 +lemma "- (- 11) = (11::5 word)" by smt
    22.9  lemma "-40 + 1 = (-39::7 word)" by smt
   22.10  lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by smt
   22.11  lemma "x = (5 :: 4 word) \<Longrightarrow> 4 * x = 4" by smt
    23.1 --- a/src/HOL/Tools/numeral.ML	Sun Sep 21 16:56:06 2014 +0200
    23.2 +++ b/src/HOL/Tools/numeral.ML	Sun Sep 21 16:56:11 2014 +0200
    23.3 @@ -8,6 +8,7 @@
    23.4  sig
    23.5    val mk_cnumeral: int -> cterm
    23.6    val mk_cnumber: ctyp -> int -> cterm
    23.7 +  val mk_number_syntax: int -> term
    23.8    val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
    23.9  end;
   23.10  
   23.11 @@ -60,6 +61,19 @@
   23.12  
   23.13  end;
   23.14  
   23.15 +fun mk_num_syntax n =
   23.16 +  if n > 0 then
   23.17 +    (case IntInf.quotRem (n, 2) of
   23.18 +      (0, 1) => Syntax.const @{const_syntax One}
   23.19 +    | (n, 0) => Syntax.const @{const_syntax Bit0} $ mk_num_syntax n
   23.20 +    | (n, 1) => Syntax.const @{const_syntax Bit1} $ mk_num_syntax n)
   23.21 +  else raise Match
   23.22 +
   23.23 +fun mk_number_syntax n =
   23.24 +  if n = 0 then Syntax.const @{const_syntax Groups.zero}
   23.25 +  else if n = 1 then Syntax.const @{const_syntax Groups.one}
   23.26 +  else Syntax.const @{const_syntax numeral} $ mk_num_syntax n;
   23.27 +
   23.28  
   23.29  (* code generator *)
   23.30  
    24.1 --- a/src/HOL/Transcendental.thy	Sun Sep 21 16:56:06 2014 +0200
    24.2 +++ b/src/HOL/Transcendental.thy	Sun Sep 21 16:56:11 2014 +0200
    24.3 @@ -247,8 +247,8 @@
    24.4  lemma sums_alternating_upper_lower:
    24.5    fixes a :: "nat \<Rightarrow> real"
    24.6    assumes mono: "\<And>n. a (Suc n) \<le> a n" and a_pos: "\<And>n. 0 \<le> a n" and "a ----> 0"
    24.7 -  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>
    24.8 -             ((\<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)"
    24.9 +  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>
   24.10 +             ((\<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)"
   24.11    (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
   24.12  proof (rule nested_sequence_unique)
   24.13    have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
   24.14 @@ -367,11 +367,11 @@
   24.15    assumes a_zero: "a ----> 0" and "monoseq a"
   24.16    shows "summable (\<lambda> n. (-1)^n * a n)" (is "?summable")
   24.17      and "0 < a 0 \<longrightarrow>
   24.18 -      (\<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")
   24.19 +      (\<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")
   24.20      and "a 0 < 0 \<longrightarrow>
   24.21 -      (\<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")
   24.22 -    and "(\<lambda>n. \<Sum>i<2*n. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?f")
   24.23 -    and "(\<lambda>n. \<Sum>i<2*n+1. -1^i*a i) ----> (\<Sum>i. -1^i*a i)" (is "?g")
   24.24 +      (\<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")
   24.25 +    and "(\<lambda>n. \<Sum>i<2*n. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?f")
   24.26 +    and "(\<lambda>n. \<Sum>i<2*n+1. (- 1)^i*a i) ----> (\<Sum>i. (- 1)^i*a i)" (is "?g")
   24.27  proof -
   24.28    have "?summable \<and> ?pos \<and> ?neg \<and> ?f \<and> ?g"
   24.29    proof (cases "(\<forall> n. 0 \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)")
   24.30 @@ -413,7 +413,7 @@
   24.31        unfolding minus_diff_minus by auto
   24.32  
   24.33      from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus]
   24.34 -    have move_minus: "(\<Sum>n. - (-1 ^ n * a n)) = - (\<Sum>n. -1 ^ n * a n)"
   24.35 +    have move_minus: "(\<Sum>n. - ((- 1) ^ n * a n)) = - (\<Sum>n. (- 1) ^ n * a n)"
   24.36        by auto
   24.37  
   24.38      have ?pos using `0 \<le> ?a 0` by auto
   24.39 @@ -1383,7 +1383,7 @@
   24.40        fix x :: real
   24.41        assume "x \<in> {- 1<..<1}"
   24.42        hence "norm (-x) < 1" by auto
   24.43 -      show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
   24.44 +      show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
   24.45          unfolding One_nat_def
   24.46          by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
   24.47      qed
   24.48 @@ -2216,10 +2216,10 @@
   24.49  subsection {* Sine and Cosine *}
   24.50  
   24.51  definition sin_coeff :: "nat \<Rightarrow> real" where
   24.52 -  "sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))"
   24.53 +  "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
   24.54  
   24.55  definition cos_coeff :: "nat \<Rightarrow> real" where
   24.56 -  "cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
   24.57 +  "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
   24.58  
   24.59  definition sin :: "real \<Rightarrow> real"
   24.60    where "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
   24.61 @@ -2472,7 +2472,7 @@
   24.62     hence define pi.*}
   24.63  
   24.64  lemma sin_paired:
   24.65 -  "(\<lambda>n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
   24.66 +  "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
   24.67  proof -
   24.68    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
   24.69      by (rule sin_converges [THEN sums_group], simp)
   24.70 @@ -2483,7 +2483,7 @@
   24.71    assumes "0 < x" and "x < 2"
   24.72    shows "0 < sin x"
   24.73  proof -
   24.74 -  let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. -1 ^ k / real (fact (2*k+1)) * x^(2*k+1)"
   24.75 +  let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
   24.76    have pos: "\<forall>n. 0 < ?f n"
   24.77    proof
   24.78      fix n :: nat
   24.79 @@ -2508,7 +2508,7 @@
   24.80  lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
   24.81    using sin_gt_zero [where x = x] by (auto simp add: cos_squared_eq cos_double)
   24.82  
   24.83 -lemma cos_paired: "(\<lambda>n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
   24.84 +lemma cos_paired: "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
   24.85  proof -
   24.86    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
   24.87      by (rule cos_converges [THEN sums_group], simp)
   24.88 @@ -2541,16 +2541,16 @@
   24.89  proof -
   24.90    note fact_Suc [simp del]
   24.91    from cos_paired
   24.92 -  have "(\<lambda>n. - (-1 ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
   24.93 +  have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
   24.94      by (rule sums_minus)
   24.95 -  then have *: "(\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
   24.96 +  then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
   24.97      by simp
   24.98 -  then have **: "summable (\<lambda>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
   24.99 +  then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  24.100      by (rule sums_summable)
  24.101 -  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  24.102 +  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  24.103      by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
  24.104 -  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - (-1 ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
  24.105 -    < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  24.106 +  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
  24.107 +    < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  24.108    proof -
  24.109      { fix d
  24.110        have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  24.111 @@ -2569,9 +2569,9 @@
  24.112      from ** show ?thesis by (rule sumr_pos_lt_pair)
  24.113        (simp add: divide_inverse mult.assoc [symmetric] ***)
  24.114    qed
  24.115 -  ultimately have "0 < (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  24.116 +  ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  24.117      by (rule order_less_trans)
  24.118 -  moreover from * have "- cos 2 = (\<Sum>n. - (-1 ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  24.119 +  moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  24.120      by (rule sums_unique)
  24.121    ultimately have "0 < - cos 2" by simp
  24.122    then show ?thesis by simp
  24.123 @@ -2677,10 +2677,10 @@
  24.124  lemma cos_periodic [simp]: "cos (x + 2*pi) = cos x"
  24.125    by (simp add: cos_add cos_double)
  24.126  
  24.127 -lemma cos_npi [simp]: "cos (real n * pi) = -1 ^ n"
  24.128 +lemma cos_npi [simp]: "cos (real n * pi) = (- 1) ^ n"
  24.129    by (induct n) (auto simp add: real_of_nat_Suc distrib_right)
  24.130  
  24.131 -lemma cos_npi2 [simp]: "cos (pi * real n) = -1 ^ n"
  24.132 +lemma cos_npi2 [simp]: "cos (pi * real n) = (- 1) ^ n"
  24.133    by (metis cos_npi mult.commute)
  24.134  
  24.135  lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
  24.136 @@ -3754,9 +3754,9 @@
  24.137      fix x :: real
  24.138      assume "\<bar>x\<bar> < 1"
  24.139      hence "x\<^sup>2 < 1" by (rule less_one_imp_sqr_less_one)
  24.140 -    have "summable (\<lambda> n. -1 ^ n * (x\<^sup>2) ^n)"
  24.141 +    have "summable (\<lambda> n. (- 1) ^ n * (x\<^sup>2) ^n)"
  24.142        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`])
  24.143 -    hence "summable (\<lambda> n. -1 ^ n * x^(2*n))" unfolding power_mult .
  24.144 +    hence "summable (\<lambda> n. (- 1) ^ n * x^(2*n))" unfolding power_mult .
  24.145    } note summable_Integral = this
  24.146  
  24.147    {
  24.148 @@ -3778,17 +3778,17 @@
  24.149    } note sums_even = this
  24.150  
  24.151    have Int_eq: "(\<Sum>n. ?f n * real (Suc n) * x^n) = ?Int"
  24.152 -    unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. -1 ^ n * x ^ (2 * n)", symmetric]
  24.153 +    unfolding if_eq mult.commute[of _ 2] suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * x ^ (2 * n)", symmetric]
  24.154      by auto
  24.155  
  24.156    {
  24.157      fix x :: real
  24.158 -    have if_eq': "\<And>n. (if even n then -1 ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
  24.159 -      (if even n then -1 ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
  24.160 +    have if_eq': "\<And>n. (if even n then (- 1) ^ (n div 2) * 1 / real (Suc n) else 0) * x ^ Suc n =
  24.161 +      (if even n then (- 1) ^ (n div 2) * (1 / real (Suc (2 * (n div 2))) * x ^ Suc (2 * (n div 2))) else 0)"
  24.162        using n_even by auto
  24.163      have idx_eq: "\<And>n. n * 2 + 1 = Suc (2 * n)" by auto
  24.164      have "(\<Sum>n. ?f n * x^(Suc n)) = ?arctan x"
  24.165 -      unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. -1 ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
  24.166 +      unfolding if_eq' idx_eq suminf_def sums_even[of "\<lambda> n. (- 1) ^ n * (1 / real (Suc (2 * n)) * x ^ Suc (2 * n))", symmetric]
  24.167        by auto
  24.168    } note arctan_eq = this
  24.169  
  24.170 @@ -3798,11 +3798,18 @@
  24.171      {
  24.172        fix x' :: real
  24.173        assume x'_bounds: "x' \<in> {- 1 <..< 1}"
  24.174 -      hence "\<bar>x'\<bar> < 1" by auto
  24.175 -
  24.176 +      then have "\<bar>x'\<bar> < 1" by auto
  24.177 +      then
  24.178 +        have *: "summable (\<lambda>n. (- 1) ^ n * x' ^ (2 * n))"
  24.179 +        by (rule summable_Integral)
  24.180        let ?S = "\<Sum> n. (-1)^n * x'^(2 * n)"
  24.181        show "summable (\<lambda> n. ?f n * real (Suc n) * x'^n)" unfolding if_eq
  24.182 -        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`])
  24.183 +        apply (rule sums_summable [where l="0 + ?S"])
  24.184 +        apply (rule sums_if)
  24.185 +        apply (rule sums_zero)
  24.186 +        apply (rule summable_sums)
  24.187 +        apply (rule *)
  24.188 +        done
  24.189      }
  24.190    qed auto
  24.191    thus ?thesis unfolding Int_eq arctan_eq .
    25.1 --- a/src/HOL/Word/Bit_Representation.thy	Sun Sep 21 16:56:06 2014 +0200
    25.2 +++ b/src/HOL/Word/Bit_Representation.thy	Sun Sep 21 16:56:11 2014 +0200
    25.3 @@ -98,7 +98,7 @@
    25.4  lemma bin_last_numeral_simps [simp]:
    25.5    "\<not> bin_last 0"
    25.6    "bin_last 1"
    25.7 -  "bin_last -1"
    25.8 +  "bin_last (- 1)"
    25.9    "bin_last Numeral1"
   25.10    "\<not> bin_last (numeral (Num.Bit0 w))"
   25.11    "bin_last (numeral (Num.Bit1 w))"
   25.12 @@ -109,7 +109,7 @@
   25.13  lemma bin_rest_numeral_simps [simp]:
   25.14    "bin_rest 0 = 0"
   25.15    "bin_rest 1 = 0"
   25.16 -  "bin_rest -1 = -1"
   25.17 +  "bin_rest (- 1) = - 1"
   25.18    "bin_rest Numeral1 = 0"
   25.19    "bin_rest (numeral (Num.Bit0 w)) = numeral w"
   25.20    "bin_rest (numeral (Num.Bit1 w)) = numeral w"
   25.21 @@ -182,7 +182,7 @@
   25.22  
   25.23  lemma bin_induct:
   25.24    assumes PPls: "P 0"
   25.25 -    and PMin: "P -1"
   25.26 +    and PMin: "P (- 1)"
   25.27      and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
   25.28    shows "P bin"
   25.29    apply (rule_tac P=P and a=bin and f1="nat o abs" 
   25.30 @@ -242,7 +242,7 @@
   25.31  lemma bin_nth_1 [simp]: "bin_nth 1 n \<longleftrightarrow> n = 0"
   25.32    by (cases n) simp_all
   25.33  
   25.34 -lemma bin_nth_minus1 [simp]: "bin_nth -1 n"
   25.35 +lemma bin_nth_minus1 [simp]: "bin_nth (- 1) n"
   25.36    by (induct n) auto
   25.37  
   25.38  lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 \<longleftrightarrow> b"
   25.39 @@ -328,12 +328,12 @@
   25.40  lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
   25.41    by (induct n) auto
   25.42  
   25.43 -lemma sbintrunc_n_minus1 [simp]: "sbintrunc n -1 = -1"
   25.44 +lemma sbintrunc_n_minus1 [simp]: "sbintrunc n (- 1) = -1"
   25.45    by (induct n) auto
   25.46  
   25.47  lemma bintrunc_Suc_numeral:
   25.48    "bintrunc (Suc n) 1 = 1"
   25.49 -  "bintrunc (Suc n) -1 = bintrunc n -1 BIT True"
   25.50 +  "bintrunc (Suc n) (- 1) = bintrunc n (- 1) BIT True"
   25.51    "bintrunc (Suc n) (numeral (Num.Bit0 w)) = bintrunc n (numeral w) BIT False"
   25.52    "bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT True"
   25.53    "bintrunc (Suc n) (- numeral (Num.Bit0 w)) =
   25.54 @@ -678,7 +678,7 @@
   25.55  lemma bintr_lt2p: "bintrunc n w < 2 ^ n"
   25.56    by (simp add: bintrunc_mod2p)
   25.57  
   25.58 -lemma bintr_Min: "bintrunc n -1 = 2 ^ n - 1"
   25.59 +lemma bintr_Min: "bintrunc n (- 1) = 2 ^ n - 1"
   25.60    by (simp add: bintrunc_mod2p m1mod2k)
   25.61  
   25.62  lemma sbintr_ge: "- (2 ^ n) \<le> sbintrunc n w"
    26.1 --- a/src/HOL/Word/Bits_Int.thy	Sun Sep 21 16:56:06 2014 +0200
    26.2 +++ b/src/HOL/Word/Bits_Int.thy	Sun Sep 21 16:56:11 2014 +0200
    26.3 @@ -462,7 +462,7 @@
    26.4  lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
    26.5    by (induct n) auto
    26.6  
    26.7 -lemma bin_sc_TM [simp]: "bin_sc n True -1 = -1"
    26.8 +lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1"
    26.9    by (induct n) auto
   26.10    
   26.11  lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
   26.12 @@ -583,7 +583,7 @@
   26.13    by (induct n) auto
   26.14  
   26.15  lemma bin_split_minus1 [simp]:
   26.16 -  "bin_split n -1 = (-1, bintrunc n -1)"
   26.17 +  "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
   26.18    by (induct n) auto
   26.19  
   26.20  lemma bin_split_trunc:
    27.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Sun Sep 21 16:56:06 2014 +0200
    27.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Sun Sep 21 16:56:11 2014 +0200
    27.3 @@ -105,8 +105,8 @@
    27.4    by (cases n) auto
    27.5  
    27.6  lemma bin_to_bl_aux_minus1_minus_simp [simp]:
    27.7 -  "0 < n ==> bin_to_bl_aux n -1 bl = 
    27.8 -    bin_to_bl_aux (n - 1) -1 (True # bl)"
    27.9 +  "0 < n ==> bin_to_bl_aux n (- 1) bl = 
   27.10 +    bin_to_bl_aux (n - 1) (- 1) (True # bl)"
   27.11    by (cases n) auto
   27.12  
   27.13  lemma bin_to_bl_aux_one_minus_simp [simp]:
   27.14 @@ -206,10 +206,10 @@
   27.15    unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux)
   27.16  
   27.17  lemma bin_to_bl_minus1_aux:
   27.18 -  "bin_to_bl_aux n -1 bl = replicate n True @ bl"
   27.19 +  "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
   27.20    by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
   27.21  
   27.22 -lemma bin_to_bl_minus1: "bin_to_bl n -1 = replicate n True"
   27.23 +lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
   27.24    unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux)
   27.25  
   27.26  lemma bl_to_bin_rep_F: 
    28.1 --- a/src/HOL/Word/Examples/WordExamples.thy	Sun Sep 21 16:56:06 2014 +0200
    28.2 +++ b/src/HOL/Word/Examples/WordExamples.thy	Sun Sep 21 16:56:11 2014 +0200
    28.3 @@ -33,13 +33,13 @@
    28.4    "27 + 11 = (6::5 word)"
    28.5    "7 * 3 = (21::'a::len word)"
    28.6    "11 - 27 = (-16::'a::len word)"
    28.7 -  "- -11 = (11::'a::len word)"
    28.8 +  "- (- 11) = (11::'a::len word)"
    28.9    "-40 + 1 = (-39::'a::len word)"
   28.10    by simp_all
   28.11  
   28.12  lemma "word_pred 2 = 1" by simp
   28.13  
   28.14 -lemma "word_succ -3 = -2" by simp
   28.15 +lemma "word_succ (- 3) = -2" by simp
   28.16    
   28.17  lemma "23 < (27::8 word)" by simp
   28.18  lemma "23 \<le> (27::8 word)" by simp
   28.19 @@ -147,11 +147,11 @@
   28.20  lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp
   28.21  lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp
   28.22  lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp
   28.23 -lemma "word_roti -2 0b0110 = (0b1001::4 word)" by simp
   28.24 +lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)" by simp
   28.25  lemma "word_rotr 2 0 = (0::4 word)" by simp
   28.26  lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops
   28.27  lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops
   28.28 -lemma "word_roti -2 1 = (0b0100::4 word)" apply simp? oops
   28.29 +lemma "word_roti (- 2) 1 = (0b0100::4 word)" apply simp? oops
   28.30  
   28.31  lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
   28.32  proof -
    29.1 --- a/src/HOL/Word/Word.thy	Sun Sep 21 16:56:06 2014 +0200
    29.2 +++ b/src/HOL/Word/Word.thy	Sun Sep 21 16:56:11 2014 +0200
    29.3 @@ -1275,7 +1275,7 @@
    29.4  lemma scast_0 [simp]: "scast 0 = 0"
    29.5    unfolding scast_def by simp
    29.6  
    29.7 -lemma sint_n1 [simp] : "sint -1 = -1"
    29.8 +lemma sint_n1 [simp] : "sint (- 1) = - 1"
    29.9    unfolding word_m1_wi word_sbin.eq_norm by simp
   29.10  
   29.11  lemma scast_n1 [simp]: "scast (- 1) = - 1"
   29.12 @@ -1349,7 +1349,7 @@
   29.13  lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
   29.14  lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
   29.15  
   29.16 -lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
   29.17 +lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)"
   29.18    unfolding word_pred_m1 by simp
   29.19  
   29.20  lemma succ_pred_no [simp]:
   29.21 @@ -1360,7 +1360,7 @@
   29.22    unfolding word_succ_p1 word_pred_m1 by simp_all
   29.23  
   29.24  lemma word_sp_01 [simp] : 
   29.25 -  "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
   29.26 +  "word_succ (- 1) = 0 & word_succ 0 = 1 & word_pred 0 = - 1 & word_pred 1 = 0"
   29.27    unfolding word_succ_p1 word_pred_m1 by simp_all
   29.28  
   29.29  (* alternative approach to lifting arithmetic equalities *)
   29.30 @@ -2803,7 +2803,7 @@
   29.31  lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
   29.32    unfolding sshiftr1_def by simp
   29.33  
   29.34 -lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
   29.35 +lemma sshiftr1_n1 [simp] : "sshiftr1 (- 1) = - 1"
   29.36    unfolding sshiftr1_def by simp
   29.37  
   29.38  lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
   29.39 @@ -3243,7 +3243,7 @@
   29.40  lemma mask_bl: "mask n = of_bl (replicate n True)"
   29.41    by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
   29.42  
   29.43 -lemma mask_bin: "mask n = word_of_int (bintrunc n -1)"
   29.44 +lemma mask_bin: "mask n = word_of_int (bintrunc n (- 1))"
   29.45    by (auto simp add: nth_bintr word_size intro: word_eqI)
   29.46  
   29.47  lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
   29.48 @@ -4729,7 +4729,7 @@
   29.49  done
   29.50  
   29.51  lemma word_rec_max: 
   29.52 -  "\<forall>m\<ge>n. m \<noteq> -1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f -1 = word_rec z f n"
   29.53 +  "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
   29.54  apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
   29.55   apply simp
   29.56  apply simp
    30.1 --- a/src/HOL/ex/BinEx.thy	Sun Sep 21 16:56:06 2014 +0200
    30.2 +++ b/src/HOL/ex/BinEx.thy	Sun Sep 21 16:56:11 2014 +0200
    30.3 @@ -98,7 +98,7 @@
    30.4  lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"
    30.5  by arith
    30.6  
    30.7 -lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - -1 < j+j - 3"
    30.8 +lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - (- 1) < j+j - 3"
    30.9  by arith
   30.10  
   30.11  lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"
   30.12 @@ -262,7 +262,7 @@
   30.13  lemma "2 ^ 10 = (1024::int)"
   30.14    by simp
   30.15  
   30.16 -lemma "-3 ^ 7 = (-2187::int)"
   30.17 +lemma "(- 3) ^ 7 = (-2187::int)"
   30.18    by simp
   30.19  
   30.20  lemma "13 ^ 7 = (62748517::int)"
   30.21 @@ -271,7 +271,7 @@
   30.22  lemma "3 ^ 15 = (14348907::int)"
   30.23    by simp
   30.24  
   30.25 -lemma "-5 ^ 11 = (-48828125::int)"
   30.26 +lemma "(- 5) ^ 11 = (-48828125::int)"
   30.27    by simp
   30.28  
   30.29  
   30.30 @@ -446,7 +446,7 @@
   30.31  lemma "2 ^ 15 = (32768::real)"
   30.32  by simp
   30.33  
   30.34 -lemma "-3 ^ 7 = (-2187::real)"
   30.35 +lemma "(- 3) ^ 7 = (-2187::real)"
   30.36  by simp
   30.37  
   30.38  lemma "13 ^ 7 = (62748517::real)"
   30.39 @@ -455,7 +455,7 @@
   30.40  lemma "3 ^ 15 = (14348907::real)"
   30.41  by simp
   30.42  
   30.43 -lemma "-5 ^ 11 = (-48828125::real)"
   30.44 +lemma "(- 5) ^ 11 = (-48828125::real)"
   30.45  by simp
   30.46  
   30.47  
    31.1 --- a/src/Pure/Syntax/lexicon.ML	Sun Sep 21 16:56:06 2014 +0200
    31.2 +++ b/src/Pure/Syntax/lexicon.ML	Sun Sep 21 16:56:11 2014 +0200
    31.3 @@ -98,9 +98,8 @@
    31.4  val scan_tid = $$$ "'" @@@ scan_id;
    31.5  
    31.6  val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
    31.7 +val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat;
    31.8  val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
    31.9 -val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat;
   31.10 -val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot;
   31.11  val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
   31.12  val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
   31.13  
   31.14 @@ -264,15 +263,16 @@
   31.15        (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) ||
   31.16        $$$ "_" @@@ $$$ "_";
   31.17  
   31.18 -    val scan_num = scan_hex || scan_bin || scan_int;
   31.19 +    val scan_num_unsigned = scan_hex || scan_bin || scan_nat;
   31.20 +    val scan_num_signed = scan_hex || scan_bin || scan_int;
   31.21  
   31.22      val scan_val =
   31.23        scan_tvar >> token TVarSy ||
   31.24        scan_var >> token VarSy ||
   31.25        scan_tid >> token TFreeSy ||
   31.26        scan_float >> token FloatSy ||
   31.27 -      scan_num >> token NumSy ||
   31.28 -      $$$ "#" @@@ scan_num >> token XNumSy ||
   31.29 +      scan_num_unsigned >> token NumSy ||
   31.30 +      $$$ "#" @@@ scan_num_signed >> token XNumSy ||
   31.31        scan_longid >> token LongIdentSy ||
   31.32        scan_xid >> token IdentSy;
   31.33