src/HOL/Int.thy
changeset 54489 03ff4d1e6784
parent 54249 ce00f2fef556
child 54863 82acc20ded73
     1.1 --- a/src/HOL/Int.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Int.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -232,9 +232,8 @@
     1.4  lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
     1.5    by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
     1.6  
     1.7 -lemma of_int_neg_numeral [simp, code_post]: "of_int (neg_numeral k) = neg_numeral k"
     1.8 -  unfolding neg_numeral_def neg_numeral_class.neg_numeral_def
     1.9 -  by (simp only: of_int_minus of_int_numeral)
    1.10 +lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
    1.11 +  by simp
    1.12  
    1.13  lemma of_int_power:
    1.14    "of_int (z ^ n) = of_int z ^ n"
    1.15 @@ -370,7 +369,7 @@
    1.16    by (simp add: nat_eq_iff)
    1.17  
    1.18  lemma nat_neg_numeral [simp]:
    1.19 -  "nat (neg_numeral k) = 0"
    1.20 +  "nat (- numeral k) = 0"
    1.21    by simp
    1.22  
    1.23  lemma nat_2: "nat 2 = Suc (Suc 0)"
    1.24 @@ -511,13 +510,13 @@
    1.25  
    1.26  lemma nonneg_int_cases:
    1.27    assumes "0 \<le> k" obtains n where "k = int n"
    1.28 -  using assms by (cases k, simp, simp del: of_nat_Suc)
    1.29 +  using assms by (rule nonneg_eq_int)
    1.30  
    1.31  lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
    1.32    -- {* Unfold all @{text let}s involving constants *}
    1.33    unfolding Let_def ..
    1.34  
    1.35 -lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
    1.36 +lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
    1.37    -- {* Unfold all @{text let}s involving constants *}
    1.38    unfolding Let_def ..
    1.39  
    1.40 @@ -525,15 +524,15 @@
    1.41  
    1.42  lemmas max_number_of [simp] =
    1.43    max_def [of "numeral u" "numeral v"]
    1.44 -  max_def [of "numeral u" "neg_numeral v"]
    1.45 -  max_def [of "neg_numeral u" "numeral v"]
    1.46 -  max_def [of "neg_numeral u" "neg_numeral v"] for u v
    1.47 +  max_def [of "numeral u" "- numeral v"]
    1.48 +  max_def [of "- numeral u" "numeral v"]
    1.49 +  max_def [of "- numeral u" "- numeral v"] for u v
    1.50  
    1.51  lemmas min_number_of [simp] =
    1.52    min_def [of "numeral u" "numeral v"]
    1.53 -  min_def [of "numeral u" "neg_numeral v"]
    1.54 -  min_def [of "neg_numeral u" "numeral v"]
    1.55 -  min_def [of "neg_numeral u" "neg_numeral v"] for u v
    1.56 +  min_def [of "numeral u" "- numeral v"]
    1.57 +  min_def [of "- numeral u" "numeral v"]
    1.58 +  min_def [of "- numeral u" "- numeral v"] for u v
    1.59  
    1.60  
    1.61  subsubsection {* Binary comparisons *}
    1.62 @@ -1070,8 +1069,6 @@
    1.63      by auto
    1.64  qed
    1.65  
    1.66 -ML_val {* @{const_name neg_numeral} *}
    1.67 -
    1.68  lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
    1.69  by (insert abs_zmult_eq_1 [of m n], arith)
    1.70  
    1.71 @@ -1127,62 +1124,30 @@
    1.72    inverse_eq_divide [of "numeral w"] for w
    1.73  
    1.74  lemmas inverse_eq_divide_neg_numeral [simp] =
    1.75 -  inverse_eq_divide [of "neg_numeral w"] for w
    1.76 +  inverse_eq_divide [of "- numeral w"] for w
    1.77  
    1.78  text {*These laws simplify inequalities, moving unary minus from a term
    1.79  into the literal.*}
    1.80  
    1.81 -lemmas le_minus_iff_numeral [simp, no_atp] =
    1.82 -  le_minus_iff [of "numeral v"]
    1.83 -  le_minus_iff [of "neg_numeral v"] for v
    1.84 -
    1.85 -lemmas equation_minus_iff_numeral [simp, no_atp] =
    1.86 -  equation_minus_iff [of "numeral v"]
    1.87 -  equation_minus_iff [of "neg_numeral v"] for v
    1.88 +lemmas equation_minus_iff_numeral [no_atp] =
    1.89 +  equation_minus_iff [of "numeral v"] for v
    1.90  
    1.91 -lemmas minus_less_iff_numeral [simp, no_atp] =
    1.92 -  minus_less_iff [of _ "numeral v"]
    1.93 -  minus_less_iff [of _ "neg_numeral v"] for v
    1.94 +lemmas minus_equation_iff_numeral [no_atp] =
    1.95 +  minus_equation_iff [of _ "numeral v"] for v
    1.96  
    1.97 -lemmas minus_le_iff_numeral [simp, no_atp] =
    1.98 -  minus_le_iff [of _ "numeral v"]
    1.99 -  minus_le_iff [of _ "neg_numeral v"] for v
   1.100 -
   1.101 -lemmas minus_equation_iff_numeral [simp, no_atp] =
   1.102 -  minus_equation_iff [of _ "numeral v"]
   1.103 -  minus_equation_iff [of _ "neg_numeral v"] for v
   1.104 -
   1.105 -text{*To Simplify Inequalities Where One Side is the Constant 1*}
   1.106 +lemmas le_minus_iff_numeral [no_atp] =
   1.107 +  le_minus_iff [of "numeral v"] for v
   1.108  
   1.109 -lemma less_minus_iff_1 [simp]:
   1.110 -  fixes b::"'b::linordered_idom"
   1.111 -  shows "(1 < - b) = (b < -1)"
   1.112 -by auto
   1.113 -
   1.114 -lemma le_minus_iff_1 [simp]:
   1.115 -  fixes b::"'b::linordered_idom"
   1.116 -  shows "(1 \<le> - b) = (b \<le> -1)"
   1.117 -by auto
   1.118 -
   1.119 -lemma equation_minus_iff_1 [simp]:
   1.120 -  fixes b::"'b::ring_1"
   1.121 -  shows "(1 = - b) = (b = -1)"
   1.122 -by (subst equation_minus_iff, auto)
   1.123 +lemmas minus_le_iff_numeral [no_atp] =
   1.124 +  minus_le_iff [of _ "numeral v"] for v
   1.125  
   1.126 -lemma minus_less_iff_1 [simp]:
   1.127 -  fixes a::"'b::linordered_idom"
   1.128 -  shows "(- a < 1) = (-1 < a)"
   1.129 -by auto
   1.130 +lemmas less_minus_iff_numeral [no_atp] =
   1.131 +  less_minus_iff [of "numeral v"] for v
   1.132  
   1.133 -lemma minus_le_iff_1 [simp]:
   1.134 -  fixes a::"'b::linordered_idom"
   1.135 -  shows "(- a \<le> 1) = (-1 \<le> a)"
   1.136 -by auto
   1.137 +lemmas minus_less_iff_numeral [no_atp] =
   1.138 +  minus_less_iff [of _ "numeral v"] for v
   1.139  
   1.140 -lemma minus_equation_iff_1 [simp]:
   1.141 -  fixes a::"'b::ring_1"
   1.142 -  shows "(- a = 1) = (a = -1)"
   1.143 -by (subst minus_equation_iff, auto)
   1.144 +-- {* FIXME maybe simproc *}
   1.145  
   1.146  
   1.147  text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
   1.148 @@ -1197,27 +1162,28 @@
   1.149  
   1.150  lemmas le_divide_eq_numeral1 [simp] =
   1.151    pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
   1.152 -  neg_le_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
   1.153 +  neg_le_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
   1.154  
   1.155  lemmas divide_le_eq_numeral1 [simp] =
   1.156    pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
   1.157 -  neg_divide_le_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
   1.158 +  neg_divide_le_eq [of "- numeral w", OF neg_numeral_less_zero] for w
   1.159  
   1.160  lemmas less_divide_eq_numeral1 [simp] =
   1.161    pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
   1.162 -  neg_less_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
   1.163 +  neg_less_divide_eq [of "- numeral w", OF neg_numeral_less_zero] for w
   1.164  
   1.165  lemmas divide_less_eq_numeral1 [simp] =
   1.166    pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
   1.167 -  neg_divide_less_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
   1.168 +  neg_divide_less_eq [of "- numeral w", OF neg_numeral_less_zero] for w
   1.169  
   1.170  lemmas eq_divide_eq_numeral1 [simp] =
   1.171    eq_divide_eq [of _ _ "numeral w"]
   1.172 -  eq_divide_eq [of _ _ "neg_numeral w"] for w
   1.173 +  eq_divide_eq [of _ _ "- numeral w"] for w
   1.174  
   1.175  lemmas divide_eq_eq_numeral1 [simp] =
   1.176    divide_eq_eq [of _ "numeral w"]
   1.177 -  divide_eq_eq [of _ "neg_numeral w"] for w
   1.178 +  divide_eq_eq [of _ "- numeral w"] for w
   1.179 +
   1.180  
   1.181  subsubsection{*Optional Simplification Rules Involving Constants*}
   1.182  
   1.183 @@ -1225,27 +1191,27 @@
   1.184  
   1.185  lemmas le_divide_eq_numeral =
   1.186    le_divide_eq [of "numeral w"]
   1.187 -  le_divide_eq [of "neg_numeral w"] for w
   1.188 +  le_divide_eq [of "- numeral w"] for w
   1.189  
   1.190  lemmas divide_le_eq_numeral =
   1.191    divide_le_eq [of _ _ "numeral w"]
   1.192 -  divide_le_eq [of _ _ "neg_numeral w"] for w
   1.193 +  divide_le_eq [of _ _ "- numeral w"] for w
   1.194  
   1.195  lemmas less_divide_eq_numeral =
   1.196    less_divide_eq [of "numeral w"]
   1.197 -  less_divide_eq [of "neg_numeral w"] for w
   1.198 +  less_divide_eq [of "- numeral w"] for w
   1.199  
   1.200  lemmas divide_less_eq_numeral =
   1.201    divide_less_eq [of _ _ "numeral w"]
   1.202 -  divide_less_eq [of _ _ "neg_numeral w"] for w
   1.203 +  divide_less_eq [of _ _ "- numeral w"] for w
   1.204  
   1.205  lemmas eq_divide_eq_numeral =
   1.206    eq_divide_eq [of "numeral w"]
   1.207 -  eq_divide_eq [of "neg_numeral w"] for w
   1.208 +  eq_divide_eq [of "- numeral w"] for w
   1.209  
   1.210  lemmas divide_eq_eq_numeral =
   1.211    divide_eq_eq [of _ _ "numeral w"]
   1.212 -  divide_eq_eq [of _ _ "neg_numeral w"] for w
   1.213 +  divide_eq_eq [of _ _ "- numeral w"] for w
   1.214  
   1.215  
   1.216  text{*Not good as automatic simprules because they cause case splits.*}
   1.217 @@ -1257,21 +1223,20 @@
   1.218  text{*Division By @{text "-1"}*}
   1.219  
   1.220  lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x"
   1.221 -  unfolding minus_one [symmetric]
   1.222    unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
   1.223    by simp
   1.224  
   1.225  lemma minus1_divide [simp]: "-1 / (x::'a::field) = - (1 / x)"
   1.226 -  unfolding minus_one [symmetric] by (rule divide_minus_left)
   1.227 +  by (fact divide_minus_left)
   1.228  
   1.229  lemma half_gt_zero_iff:
   1.230 -     "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
   1.231 -by auto
   1.232 +  "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
   1.233 +  by auto
   1.234  
   1.235  lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
   1.236  
   1.237  lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x"
   1.238 -  by simp
   1.239 +  by (fact divide_numeral_1)
   1.240  
   1.241  
   1.242  subsection {* The divides relation *}
   1.243 @@ -1475,7 +1440,7 @@
   1.244    [simp, code_abbrev]: "Pos = numeral"
   1.245  
   1.246  definition Neg :: "num \<Rightarrow> int" where
   1.247 -  [simp, code_abbrev]: "Neg = neg_numeral"
   1.248 +  [simp, code_abbrev]: "Neg n = - (Pos n)"
   1.249  
   1.250  code_datatype "0::int" Pos Neg
   1.251  
   1.252 @@ -1489,7 +1454,7 @@
   1.253    "dup 0 = 0"
   1.254    "dup (Pos n) = Pos (Num.Bit0 n)"
   1.255    "dup (Neg n) = Neg (Num.Bit0 n)"
   1.256 -  unfolding Pos_def Neg_def neg_numeral_def
   1.257 +  unfolding Pos_def Neg_def
   1.258    by (simp_all add: numeral_Bit0)
   1.259  
   1.260  definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
   1.261 @@ -1505,12 +1470,10 @@
   1.262    "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
   1.263    "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   1.264    "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
   1.265 -  apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def
   1.266 -    neg_numeral_def numeral_BitM)
   1.267 +  apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
   1.268    apply (simp_all only: algebra_simps minus_diff_eq)
   1.269    apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
   1.270    apply (simp_all only: minus_add add.assoc left_minus)
   1.271 -  apply (simp_all only: algebra_simps right_minus)
   1.272    done
   1.273  
   1.274  text {* Implementations *}
   1.275 @@ -1606,10 +1569,10 @@
   1.276    "nat (Int.Neg k) = 0"
   1.277    "nat 0 = 0"
   1.278    "nat (Int.Pos k) = nat_of_num k"
   1.279 -  by (simp_all add: nat_of_num_numeral nat_numeral)
   1.280 +  by (simp_all add: nat_of_num_numeral)
   1.281  
   1.282  lemma (in ring_1) of_int_code [code]:
   1.283 -  "of_int (Int.Neg k) = neg_numeral k"
   1.284 +  "of_int (Int.Neg k) = - numeral k"
   1.285    "of_int 0 = 0"
   1.286    "of_int (Int.Pos k) = numeral k"
   1.287    by simp_all
   1.288 @@ -1653,7 +1616,7 @@
   1.289  
   1.290  lemma int_power:
   1.291    "int (m ^ n) = int m ^ n"
   1.292 -  by (rule of_nat_power)
   1.293 +  by (fact of_nat_power)
   1.294  
   1.295  lemmas zpower_int = int_power [symmetric]
   1.296