src/HOL/Int.thy
 author nipkow Mon Mar 02 16:53:55 2009 +0100 (2009-03-02) changeset 30198 922f944f03b2 parent 30079 293b896b9c25 child 30242 aea5d7fa7ef5 permissions -rw-r--r--
name changes
 haftmann@25919 1 (* Title: Int.thy haftmann@25919 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory haftmann@25919 3 Tobias Nipkow, Florian Haftmann, TU Muenchen haftmann@25919 4 Copyright 1994 University of Cambridge haftmann@25919 5 haftmann@25919 6 *) haftmann@25919 7 haftmann@25919 8 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} haftmann@25919 9 haftmann@25919 10 theory Int krauss@26748 11 imports Equiv_Relations Nat Wellfounded haftmann@25919 12 uses haftmann@25919 13 ("Tools/numeral.ML") haftmann@25919 14 ("Tools/numeral_syntax.ML") haftmann@25919 15 ("~~/src/Provers/Arith/assoc_fold.ML") haftmann@25919 16 "~~/src/Provers/Arith/cancel_numerals.ML" haftmann@25919 17 "~~/src/Provers/Arith/combine_numerals.ML" haftmann@28952 18 ("Tools/int_arith.ML") haftmann@25919 19 begin haftmann@25919 20 haftmann@25919 21 subsection {* The equivalence relation underlying the integers *} haftmann@25919 22 haftmann@28661 23 definition intrel :: "((nat \ nat) \ (nat \ nat)) set" where haftmann@28562 24 [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }" haftmann@25919 25 haftmann@25919 26 typedef (Integ) haftmann@25919 27 int = "UNIV//intrel" haftmann@25919 28 by (auto simp add: quotient_def) haftmann@25919 29 haftmann@25919 30 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" haftmann@25919 31 begin haftmann@25919 32 haftmann@25919 33 definition haftmann@28562 34 Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})" haftmann@25919 35 haftmann@25919 36 definition haftmann@28562 37 One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})" haftmann@25919 38 haftmann@25919 39 definition haftmann@28562 40 add_int_def [code del]: "z + w = Abs_Integ haftmann@25919 41 (\(x, y) \ Rep_Integ z. \(u, v) \ Rep_Integ w. haftmann@25919 42 intrel `` {(x + u, y + v)})" haftmann@25919 43 haftmann@25919 44 definition haftmann@28562 45 minus_int_def [code del]: haftmann@25919 46 "- z = Abs_Integ (\(x, y) \ Rep_Integ z. intrel `` {(y, x)})" haftmann@25919 47 haftmann@25919 48 definition haftmann@28562 49 diff_int_def [code del]: "z - w = z + (-w \ int)" haftmann@25919 50 haftmann@25919 51 definition haftmann@28562 52 mult_int_def [code del]: "z * w = Abs_Integ haftmann@25919 53 (\(x, y) \ Rep_Integ z. \(u,v ) \ Rep_Integ w. haftmann@25919 54 intrel `` {(x*u + y*v, x*v + y*u)})" haftmann@25919 55 haftmann@25919 56 definition haftmann@28562 57 le_int_def [code del]: haftmann@25919 58 "z \ w \ (\x y u v. x+v \ u+y \ (x, y) \ Rep_Integ z \ (u, v) \ Rep_Integ w)" haftmann@25919 59 haftmann@25919 60 definition haftmann@28562 61 less_int_def [code del]: "(z\int) < w \ z \ w \ z \ w" haftmann@25919 62 haftmann@25919 63 definition haftmann@25919 64 zabs_def: "\i\int\ = (if i < 0 then - i else i)" haftmann@25919 65 haftmann@25919 66 definition haftmann@25919 67 zsgn_def: "sgn (i\int) = (if i=0 then 0 else if 0 intrel) = (x+v = u+y)" haftmann@25919 77 by (simp add: intrel_def) haftmann@25919 78 haftmann@25919 79 lemma equiv_intrel: "equiv UNIV intrel" nipkow@30198 80 by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def) haftmann@25919 81 haftmann@25919 82 text{*Reduces equality of equivalence classes to the @{term intrel} relation: haftmann@25919 83 @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \ intrel)"} *} haftmann@25919 84 lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I] haftmann@25919 85 haftmann@25919 86 text{*All equivalence classes belong to set of representatives*} haftmann@25919 87 lemma [simp]: "intrel``{(x,y)} \ Integ" haftmann@25919 88 by (auto simp add: Integ_def intrel_def quotient_def) haftmann@25919 89 haftmann@25919 90 text{*Reduces equality on abstractions to equality on representatives: haftmann@25919 91 @{prop "\x \ Integ; y \ Integ\ \ (Abs_Integ x = Abs_Integ y) = (x=y)"} *} haftmann@25919 92 declare Abs_Integ_inject [simp,noatp] Abs_Integ_inverse [simp,noatp] haftmann@25919 93 haftmann@25919 94 text{*Case analysis on the representation of an integer as an equivalence haftmann@25919 95 class of pairs of naturals.*} haftmann@25919 96 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: haftmann@25919 97 "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P" haftmann@25919 98 apply (rule Abs_Integ_cases [of z]) haftmann@25919 99 apply (auto simp add: Integ_def quotient_def) haftmann@25919 100 done haftmann@25919 101 haftmann@25919 102 haftmann@25919 103 subsection {* Arithmetic Operations *} haftmann@25919 104 haftmann@25919 105 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})" haftmann@25919 106 proof - haftmann@25919 107 have "(\(x,y). intrel``{(y,x)}) respects intrel" haftmann@25919 108 by (simp add: congruent_def) haftmann@25919 109 thus ?thesis haftmann@25919 110 by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel]) haftmann@25919 111 qed haftmann@25919 112 haftmann@25919 113 lemma add: haftmann@25919 114 "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) = haftmann@25919 115 Abs_Integ (intrel``{(x+u, y+v)})" haftmann@25919 116 proof - haftmann@25919 117 have "(\z w. (\(x,y). (\(u,v). intrel `` {(x+u, y+v)}) w) z) haftmann@25919 118 respects2 intrel" haftmann@25919 119 by (simp add: congruent2_def) haftmann@25919 120 thus ?thesis haftmann@25919 121 by (simp add: add_int_def UN_UN_split_split_eq haftmann@25919 122 UN_equiv_class2 [OF equiv_intrel equiv_intrel]) haftmann@25919 123 qed haftmann@25919 124 haftmann@25919 125 text{*Congruence property for multiplication*} haftmann@25919 126 lemma mult_congruent2: haftmann@25919 127 "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1) haftmann@25919 128 respects2 intrel" haftmann@25919 129 apply (rule equiv_intrel [THEN congruent2_commuteI]) haftmann@25919 130 apply (force simp add: mult_ac, clarify) haftmann@25919 131 apply (simp add: congruent_def mult_ac) haftmann@25919 132 apply (rename_tac u v w x y z) haftmann@25919 133 apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z") haftmann@25919 134 apply (simp add: mult_ac) haftmann@25919 135 apply (simp add: add_mult_distrib [symmetric]) haftmann@25919 136 done haftmann@25919 137 haftmann@25919 138 lemma mult: haftmann@25919 139 "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) = haftmann@25919 140 Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})" haftmann@25919 141 by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2 haftmann@25919 142 UN_equiv_class2 [OF equiv_intrel equiv_intrel]) haftmann@25919 143 haftmann@25919 144 text{*The integers form a @{text comm_ring_1}*} haftmann@25919 145 instance int :: comm_ring_1 haftmann@25919 146 proof haftmann@25919 147 fix i j k :: int haftmann@25919 148 show "(i + j) + k = i + (j + k)" haftmann@25919 149 by (cases i, cases j, cases k) (simp add: add add_assoc) haftmann@25919 150 show "i + j = j + i" haftmann@25919 151 by (cases i, cases j) (simp add: add_ac add) haftmann@25919 152 show "0 + i = i" haftmann@25919 153 by (cases i) (simp add: Zero_int_def add) haftmann@25919 154 show "- i + i = 0" haftmann@25919 155 by (cases i) (simp add: Zero_int_def minus add) haftmann@25919 156 show "i - j = i + - j" haftmann@25919 157 by (simp add: diff_int_def) haftmann@25919 158 show "(i * j) * k = i * (j * k)" nipkow@29667 159 by (cases i, cases j, cases k) (simp add: mult algebra_simps) haftmann@25919 160 show "i * j = j * i" nipkow@29667 161 by (cases i, cases j) (simp add: mult algebra_simps) haftmann@25919 162 show "1 * i = i" haftmann@25919 163 by (cases i) (simp add: One_int_def mult) haftmann@25919 164 show "(i + j) * k = i * k + j * k" nipkow@29667 165 by (cases i, cases j, cases k) (simp add: add mult algebra_simps) haftmann@25919 166 show "0 \ (1::int)" haftmann@25919 167 by (simp add: Zero_int_def One_int_def) haftmann@25919 168 qed haftmann@25919 169 haftmann@25919 170 lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})" haftmann@25919 171 by (induct m, simp_all add: Zero_int_def One_int_def add) haftmann@25919 172 haftmann@25919 173 haftmann@25919 174 subsection {* The @{text "\"} Ordering *} haftmann@25919 175 haftmann@25919 176 lemma le: haftmann@25919 177 "(Abs_Integ(intrel``{(x,y)}) \ Abs_Integ(intrel``{(u,v)})) = (x+v \ u+y)" haftmann@25919 178 by (force simp add: le_int_def) haftmann@25919 179 haftmann@25919 180 lemma less: haftmann@25919 181 "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)" haftmann@25919 182 by (simp add: less_int_def le order_less_le) haftmann@25919 183 haftmann@25919 184 instance int :: linorder haftmann@25919 185 proof haftmann@25919 186 fix i j k :: int haftmann@27682 187 show antisym: "i \ j \ j \ i \ i = j" haftmann@27682 188 by (cases i, cases j) (simp add: le) haftmann@27682 189 show "(i < j) = (i \ j \ \ j \ i)" haftmann@27682 190 by (auto simp add: less_int_def dest: antisym) haftmann@25919 191 show "i \ i" haftmann@25919 192 by (cases i) (simp add: le) haftmann@25919 193 show "i \ j \ j \ k \ i \ k" haftmann@25919 194 by (cases i, cases j, cases k) (simp add: le) haftmann@25919 195 show "i \ j \ j \ i" haftmann@25919 196 by (cases i, cases j) (simp add: le linorder_linear) haftmann@25919 197 qed haftmann@25919 198 haftmann@25919 199 instantiation int :: distrib_lattice haftmann@25919 200 begin haftmann@25919 201 haftmann@25919 202 definition haftmann@25919 203 "(inf \ int \ int \ int) = min" haftmann@25919 204 haftmann@25919 205 definition haftmann@25919 206 "(sup \ int \ int \ int) = max" haftmann@25919 207 haftmann@25919 208 instance haftmann@25919 209 by intro_classes haftmann@25919 210 (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) haftmann@25919 211 haftmann@25919 212 end haftmann@25919 213 haftmann@25919 214 instance int :: pordered_cancel_ab_semigroup_add haftmann@25919 215 proof haftmann@25919 216 fix i j k :: int haftmann@25919 217 show "i \ j \ k + i \ k + j" haftmann@25919 218 by (cases i, cases j, cases k) (simp add: le add) haftmann@25919 219 qed haftmann@25919 220 haftmann@25961 221 haftmann@25919 222 text{*Strict Monotonicity of Multiplication*} haftmann@25919 223 haftmann@25919 224 text{*strict, in 1st argument; proof is by induction on k>0*} haftmann@25919 225 lemma zmult_zless_mono2_lemma: haftmann@25919 226 "(i::int) 0 of_nat k * i < of_nat k * j" haftmann@25919 227 apply (induct "k", simp) haftmann@25919 228 apply (simp add: left_distrib) haftmann@25919 229 apply (case_tac "k=0") haftmann@25919 230 apply (simp_all add: add_strict_mono) haftmann@25919 231 done haftmann@25919 232 haftmann@25919 233 lemma zero_le_imp_eq_int: "(0::int) \ k ==> \n. k = of_nat n" haftmann@25919 234 apply (cases k) haftmann@25919 235 apply (auto simp add: le add int_def Zero_int_def) haftmann@25919 236 apply (rule_tac x="x-y" in exI, simp) haftmann@25919 237 done haftmann@25919 238 haftmann@25919 239 lemma zero_less_imp_eq_int: "(0::int) < k ==> \n>0. k = of_nat n" haftmann@25919 240 apply (cases k) haftmann@25919 241 apply (simp add: less int_def Zero_int_def) haftmann@25919 242 apply (rule_tac x="x-y" in exI, simp) haftmann@25919 243 done haftmann@25919 244 haftmann@25919 245 lemma zmult_zless_mono2: "[| i k*i < k*j" haftmann@25919 246 apply (drule zero_less_imp_eq_int) haftmann@25919 247 apply (auto simp add: zmult_zless_mono2_lemma) haftmann@25919 248 done haftmann@25919 249 haftmann@25919 250 text{*The integers form an ordered integral domain*} haftmann@25919 251 instance int :: ordered_idom haftmann@25919 252 proof haftmann@25919 253 fix i j k :: int haftmann@25919 254 show "i < j \ 0 < k \ k * i < k * j" haftmann@25919 255 by (rule zmult_zless_mono2) haftmann@25919 256 show "\i\ = (if i < 0 then -i else i)" haftmann@25919 257 by (simp only: zabs_def) haftmann@25919 258 show "sgn (i\int) = (if i=0 then 0 else if 0 w + (1\int) \ z" haftmann@25919 270 apply (cases w, cases z) haftmann@25919 271 apply (simp add: less le add One_int_def) haftmann@25919 272 done haftmann@25919 273 haftmann@25919 274 lemma zless_iff_Suc_zadd: haftmann@25919 275 "(w \ int) < z \ (\n. z = w + of_nat (Suc n))" haftmann@25919 276 apply (cases z, cases w) haftmann@25919 277 apply (auto simp add: less add int_def) haftmann@25919 278 apply (rename_tac a b c d) haftmann@25919 279 apply (rule_tac x="a+d - Suc(c+b)" in exI) haftmann@25919 280 apply arith haftmann@25919 281 done haftmann@25919 282 haftmann@25919 283 lemmas int_distrib = haftmann@25919 284 left_distrib [of "z1::int" "z2" "w", standard] haftmann@25919 285 right_distrib [of "w::int" "z1" "z2", standard] haftmann@25919 286 left_diff_distrib [of "z1::int" "z2" "w", standard] haftmann@25919 287 right_diff_distrib [of "w::int" "z1" "z2", standard] haftmann@25919 288 haftmann@25919 289 haftmann@25919 290 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*} haftmann@25919 291 haftmann@25919 292 context ring_1 haftmann@25919 293 begin haftmann@25919 294 haftmann@25919 295 definition haftmann@25919 296 of_int :: "int \ 'a" haftmann@25919 297 where haftmann@28562 298 [code del]: "of_int z = contents (\(i, j) \ Rep_Integ z. { of_nat i - of_nat j })" haftmann@25919 299 haftmann@25919 300 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j" haftmann@25919 301 proof - haftmann@25919 302 have "(\(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel" nipkow@29667 303 by (simp add: congruent_def algebra_simps of_nat_add [symmetric] haftmann@25919 304 del: of_nat_add) haftmann@25919 305 thus ?thesis haftmann@25919 306 by (simp add: of_int_def UN_equiv_class [OF equiv_intrel]) haftmann@25919 307 qed haftmann@25919 308 haftmann@25919 309 lemma of_int_0 [simp]: "of_int 0 = 0" nipkow@29667 310 by (simp add: of_int Zero_int_def) haftmann@25919 311 haftmann@25919 312 lemma of_int_1 [simp]: "of_int 1 = 1" nipkow@29667 313 by (simp add: of_int One_int_def) haftmann@25919 314 haftmann@25919 315 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" nipkow@29667 316 by (cases w, cases z, simp add: algebra_simps of_int add) haftmann@25919 317 haftmann@25919 318 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)" nipkow@29667 319 by (cases z, simp add: algebra_simps of_int minus) haftmann@25919 320 haftmann@25919 321 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z" nipkow@29667 322 by (simp add: OrderedGroup.diff_minus diff_minus) haftmann@25919 323 haftmann@25919 324 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" haftmann@25919 325 apply (cases w, cases z) nipkow@29667 326 apply (simp add: algebra_simps of_int mult of_nat_mult) haftmann@25919 327 done haftmann@25919 328 haftmann@25919 329 text{*Collapse nested embeddings*} haftmann@25919 330 lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n" nipkow@29667 331 by (induct n) auto haftmann@25919 332 haftmann@25919 333 end haftmann@25919 334 haftmann@25919 335 context ordered_idom haftmann@25919 336 begin haftmann@25919 337 haftmann@25919 338 lemma of_int_le_iff [simp]: haftmann@25919 339 "of_int w \ of_int z \ w \ z" nipkow@29667 340 by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add) haftmann@25919 341 haftmann@25919 342 text{*Special cases where either operand is zero*} haftmann@25919 343 lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified] haftmann@25919 344 lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified] haftmann@25919 345 haftmann@25919 346 lemma of_int_less_iff [simp]: haftmann@25919 347 "of_int w < of_int z \ w < z" haftmann@25919 348 by (simp add: not_le [symmetric] linorder_not_le [symmetric]) haftmann@25919 349 haftmann@25919 350 text{*Special cases where either operand is zero*} haftmann@25919 351 lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified] haftmann@25919 352 lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified] haftmann@25919 353 haftmann@25919 354 end haftmann@25919 355 haftmann@25919 356 text{*Class for unital rings with characteristic zero. haftmann@25919 357 Includes non-ordered rings like the complex numbers.*} haftmann@25919 358 class ring_char_0 = ring_1 + semiring_char_0 haftmann@25919 359 begin haftmann@25919 360 haftmann@25919 361 lemma of_int_eq_iff [simp]: haftmann@25919 362 "of_int w = of_int z \ w = z" haftmann@25919 363 apply (cases w, cases z, simp add: of_int) haftmann@25919 364 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq) haftmann@25919 365 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff) haftmann@25919 366 done haftmann@25919 367 haftmann@25919 368 text{*Special cases where either operand is zero*} haftmann@25919 369 lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified] haftmann@25919 370 lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified] haftmann@25919 371 haftmann@25919 372 end haftmann@25919 373 haftmann@25919 374 text{*Every @{text ordered_idom} has characteristic zero.*} haftmann@25919 375 subclass (in ordered_idom) ring_char_0 by intro_locales haftmann@25919 376 haftmann@25919 377 lemma of_int_eq_id [simp]: "of_int = id" haftmann@25919 378 proof haftmann@25919 379 fix z show "of_int z = id z" haftmann@25919 380 by (cases z) (simp add: of_int add minus int_def diff_minus) haftmann@25919 381 qed haftmann@25919 382 haftmann@25919 383 haftmann@25919 384 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *} haftmann@25919 385 haftmann@25919 386 definition haftmann@25919 387 nat :: "int \ nat" haftmann@25919 388 where haftmann@28562 389 [code del]: "nat z = contents (\(x, y) \ Rep_Integ z. {x-y})" haftmann@25919 390 haftmann@25919 391 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y" haftmann@25919 392 proof - haftmann@25919 393 have "(\(x,y). {x-y}) respects intrel" haftmann@25919 394 by (simp add: congruent_def) arith haftmann@25919 395 thus ?thesis haftmann@25919 396 by (simp add: nat_def UN_equiv_class [OF equiv_intrel]) haftmann@25919 397 qed haftmann@25919 398 haftmann@25919 399 lemma nat_int [simp]: "nat (of_nat n) = n" haftmann@25919 400 by (simp add: nat int_def) haftmann@25919 401 haftmann@25919 402 lemma nat_zero [simp]: "nat 0 = 0" haftmann@25919 403 by (simp add: Zero_int_def nat) haftmann@25919 404 haftmann@25919 405 lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \ z then z else 0)" haftmann@25919 406 by (cases z, simp add: nat le int_def Zero_int_def) haftmann@25919 407 haftmann@25919 408 corollary nat_0_le: "0 \ z ==> of_nat (nat z) = z" haftmann@25919 409 by simp haftmann@25919 410 haftmann@25919 411 lemma nat_le_0 [simp]: "z \ 0 ==> nat z = 0" haftmann@25919 412 by (cases z, simp add: nat le Zero_int_def) haftmann@25919 413 haftmann@25919 414 lemma nat_le_eq_zle: "0 < w | 0 \ z ==> (nat w \ nat z) = (w\z)" haftmann@25919 415 apply (cases w, cases z) haftmann@25919 416 apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith) haftmann@25919 417 done haftmann@25919 418 haftmann@25919 419 text{*An alternative condition is @{term "0 \ w"} *} haftmann@25919 420 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" haftmann@25919 421 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) haftmann@25919 422 haftmann@25919 423 corollary nat_less_eq_zless: "0 \ w ==> (nat w < nat z) = (w z" and "\m. z = of_nat m \ P" haftmann@25919 434 shows P haftmann@25919 435 using assms by (blast dest: nat_0_le sym) haftmann@25919 436 haftmann@25919 437 lemma nat_eq_iff: "(nat w = m) = (if 0 \ w then w = of_nat m else m=0)" haftmann@25919 438 by (cases w, simp add: nat le int_def Zero_int_def, arith) haftmann@25919 439 haftmann@25919 440 corollary nat_eq_iff2: "(m = nat w) = (if 0 \ w then w = of_nat m else m=0)" haftmann@25919 441 by (simp only: eq_commute [of m] nat_eq_iff) haftmann@25919 442 haftmann@25919 443 lemma nat_less_iff: "0 \ w ==> (nat w < m) = (w < of_nat m)" haftmann@25919 444 apply (cases w) nipkow@29700 445 apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith) haftmann@25919 446 done haftmann@25919 447 nipkow@29700 448 lemma nat_0_iff[simp]: "nat(i::int) = 0 \ i\0" nipkow@29700 449 by(simp add: nat_eq_iff) arith nipkow@29700 450 haftmann@25919 451 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \ z)" haftmann@25919 452 by (auto simp add: nat_eq_iff2) haftmann@25919 453 haftmann@25919 454 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" haftmann@25919 455 by (insert zless_nat_conj [of 0], auto) haftmann@25919 456 haftmann@25919 457 lemma nat_add_distrib: haftmann@25919 458 "[| (0::int) \ z; 0 \ z' |] ==> nat (z+z') = nat z + nat z'" haftmann@25919 459 by (cases z, cases z', simp add: nat add le Zero_int_def) haftmann@25919 460 haftmann@25919 461 lemma nat_diff_distrib: haftmann@25919 462 "[| (0::int) \ z'; z' \ z |] ==> nat (z-z') = nat z - nat z'" haftmann@25919 463 by (cases z, cases z', haftmann@25919 464 simp add: nat add minus diff_minus le Zero_int_def) haftmann@25919 465 haftmann@25919 466 lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0" haftmann@25919 467 by (simp add: int_def minus nat Zero_int_def) haftmann@25919 468 haftmann@25919 469 lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)" haftmann@25919 470 by (cases z, simp add: nat less int_def, arith) haftmann@25919 471 haftmann@25919 472 context ring_1 haftmann@25919 473 begin haftmann@25919 474 haftmann@25919 475 lemma of_nat_nat: "0 \ z \ of_nat (nat z) = of_int z" haftmann@25919 476 by (cases z rule: eq_Abs_Integ) haftmann@25919 477 (simp add: nat le of_int Zero_int_def of_nat_diff) haftmann@25919 478 haftmann@25919 479 end haftmann@25919 480 krauss@29779 481 text {* For termination proofs: *} krauss@29779 482 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. krauss@29779 483 haftmann@25919 484 haftmann@25919 485 subsection{*Lemmas about the Function @{term of_nat} and Orderings*} haftmann@25919 486 haftmann@25919 487 lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \ int)" haftmann@25919 488 by (simp add: order_less_le del: of_nat_Suc) haftmann@25919 489 haftmann@25919 490 lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \ int)" haftmann@25919 491 by (rule negative_zless_0 [THEN order_less_le_trans], simp) haftmann@25919 492 haftmann@25919 493 lemma negative_zle_0: "- of_nat n \ (0 \ int)" haftmann@25919 494 by (simp add: minus_le_iff) haftmann@25919 495 haftmann@25919 496 lemma negative_zle [iff]: "- of_nat n \ (of_nat m \ int)" haftmann@25919 497 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff]) haftmann@25919 498 haftmann@25919 499 lemma not_zle_0_negative [simp]: "~ (0 \ - (of_nat (Suc n) \ int))" haftmann@25919 500 by (subst le_minus_iff, simp del: of_nat_Suc) haftmann@25919 501 haftmann@25919 502 lemma int_zle_neg: "((of_nat n \ int) \ - of_nat m) = (n = 0 & m = 0)" haftmann@25919 503 by (simp add: int_def le minus Zero_int_def) haftmann@25919 504 haftmann@25919 505 lemma not_int_zless_negative [simp]: "~ ((of_nat n \ int) < - of_nat m)" haftmann@25919 506 by (simp add: linorder_not_less) haftmann@25919 507 haftmann@25919 508 lemma negative_eq_positive [simp]: "((- of_nat n \ int) = of_nat m) = (n = 0 & m = 0)" haftmann@25919 509 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg) haftmann@25919 510 haftmann@25919 511 lemma zle_iff_zadd: "(w\int) \ z \ (\n. z = w + of_nat n)" haftmann@25919 512 proof - haftmann@25919 513 have "(w \ z) = (0 \ z - w)" haftmann@25919 514 by (simp only: le_diff_eq add_0_left) haftmann@25919 515 also have "\ = (\n. z - w = of_nat n)" haftmann@25919 516 by (auto elim: zero_le_imp_eq_int) haftmann@25919 517 also have "\ = (\n. z = w + of_nat n)" nipkow@29667 518 by (simp only: algebra_simps) haftmann@25919 519 finally show ?thesis . haftmann@25919 520 qed haftmann@25919 521 haftmann@25919 522 lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\int)" haftmann@25919 523 by simp haftmann@25919 524 haftmann@25919 525 lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\int)" haftmann@25919 526 by simp haftmann@25919 527 haftmann@25919 528 text{*This version is proved for all ordered rings, not just integers! haftmann@25919 529 It is proved here because attribute @{text arith_split} is not available haftmann@25919 530 in theory @{text Ring_and_Field}. haftmann@25919 531 But is it really better than just rewriting with @{text abs_if}?*} haftmann@25919 532 lemma abs_split [arith_split,noatp]: haftmann@25919 533 "P(abs(a::'a::ordered_idom)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" haftmann@25919 534 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) haftmann@25919 535 haftmann@25919 536 lemma negD: "(x \ int) < 0 \ \n. x = - (of_nat (Suc n))" haftmann@25919 537 apply (cases x) haftmann@25919 538 apply (auto simp add: le minus Zero_int_def int_def order_less_le) haftmann@25919 539 apply (rule_tac x="y - Suc x" in exI, arith) haftmann@25919 540 done haftmann@25919 541 haftmann@25919 542 haftmann@25919 543 subsection {* Cases and induction *} haftmann@25919 544 haftmann@25919 545 text{*Now we replace the case analysis rule by a more conventional one: haftmann@25919 546 whether an integer is negative or not.*} haftmann@25919 547 haftmann@25919 548 theorem int_cases [cases type: int, case_names nonneg neg]: haftmann@25919 549 "[|!! n. (z \ int) = of_nat n ==> P; !! n. z = - (of_nat (Suc n)) ==> P |] ==> P" haftmann@25919 550 apply (cases "z < 0", blast dest!: negD) haftmann@25919 551 apply (simp add: linorder_not_less del: of_nat_Suc) haftmann@25919 552 apply auto haftmann@25919 553 apply (blast dest: nat_0_le [THEN sym]) haftmann@25919 554 done haftmann@25919 555 haftmann@25919 556 theorem int_induct [induct type: int, case_names nonneg neg]: haftmann@25919 557 "[|!! n. P (of_nat n \ int); !!n. P (- (of_nat (Suc n))) |] ==> P z" haftmann@25919 558 by (cases z rule: int_cases) auto haftmann@25919 559 haftmann@25919 560 text{*Contributed by Brian Huffman*} haftmann@25919 561 theorem int_diff_cases: haftmann@25919 562 obtains (diff) m n where "(z\int) = of_nat m - of_nat n" haftmann@25919 563 apply (cases z rule: eq_Abs_Integ) haftmann@25919 564 apply (rule_tac m=x and n=y in diff) haftmann@25919 565 apply (simp add: int_def diff_def minus add) haftmann@25919 566 done haftmann@25919 567 haftmann@25919 568 haftmann@25919 569 subsection {* Binary representation *} haftmann@25919 570 haftmann@25919 571 text {* haftmann@25919 572 This formalization defines binary arithmetic in terms of the integers haftmann@25919 573 rather than using a datatype. This avoids multiple representations (leading haftmann@25919 574 zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text haftmann@25919 575 int_of_binary}, for the numerical interpretation. haftmann@25919 576 haftmann@25919 577 The representation expects that @{text "(m mod 2)"} is 0 or 1, haftmann@25919 578 even if m is negative; haftmann@25919 579 For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus haftmann@25919 580 @{text "-5 = (-3)*2 + 1"}. haftmann@25919 581 haftmann@25919 582 This two's complement binary representation derives from the paper haftmann@25919 583 "An Efficient Representation of Arithmetic for Term Rewriting" by haftmann@25919 584 Dave Cohen and Phil Watson, Rewriting Techniques and Applications, haftmann@25919 585 Springer LNCS 488 (240-251), 1991. haftmann@25919 586 *} haftmann@25919 587 huffman@28958 588 subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *} huffman@28958 589 haftmann@25919 590 definition haftmann@25919 591 Pls :: int where haftmann@28562 592 [code del]: "Pls = 0" haftmann@25919 593 haftmann@25919 594 definition haftmann@25919 595 Min :: int where haftmann@28562 596 [code del]: "Min = - 1" haftmann@25919 597 haftmann@25919 598 definition huffman@26086 599 Bit0 :: "int \ int" where haftmann@28562 600 [code del]: "Bit0 k = k + k" huffman@26086 601 huffman@26086 602 definition huffman@26086 603 Bit1 :: "int \ int" where haftmann@28562 604 [code del]: "Bit1 k = 1 + k + k" haftmann@25919 605 haftmann@29608 606 class number = -- {* for numeric types: nat, int, real, \dots *} haftmann@25919 607 fixes number_of :: "int \ 'a" haftmann@25919 608 haftmann@25919 609 use "Tools/numeral.ML" haftmann@25919 610 haftmann@25919 611 syntax haftmann@25919 612 "_Numeral" :: "num_const \ 'a" ("_") haftmann@25919 613 haftmann@25919 614 use "Tools/numeral_syntax.ML" haftmann@25919 615 setup NumeralSyntax.setup haftmann@25919 616 haftmann@25919 617 abbreviation haftmann@25919 618 "Numeral0 \ number_of Pls" haftmann@25919 619 haftmann@25919 620 abbreviation huffman@26086 621 "Numeral1 \ number_of (Bit1 Pls)" haftmann@25919 622 haftmann@25919 623 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)" haftmann@25919 624 -- {* Unfold all @{text let}s involving constants *} haftmann@25919 625 unfolding Let_def .. haftmann@25919 626 haftmann@25919 627 definition haftmann@25919 628 succ :: "int \ int" where haftmann@28562 629 [code del]: "succ k = k + 1" haftmann@25919 630 haftmann@25919 631 definition haftmann@25919 632 pred :: "int \ int" where haftmann@28562 633 [code del]: "pred k = k - 1" haftmann@25919 634 haftmann@25919 635 lemmas haftmann@25919 636 max_number_of [simp] = max_def haftmann@25919 637 [of "number_of u" "number_of v", standard, simp] haftmann@25919 638 and haftmann@25919 639 min_number_of [simp] = min_def haftmann@25919 640 [of "number_of u" "number_of v", standard, simp] haftmann@25919 641 -- {* unfolding @{text minx} and @{text max} on numerals *} haftmann@25919 642 haftmann@25919 643 lemmas numeral_simps = huffman@26086 644 succ_def pred_def Pls_def Min_def Bit0_def Bit1_def haftmann@25919 645 haftmann@25919 646 text {* Removal of leading zeroes *} haftmann@25919 647 huffman@26086 648 lemma Bit0_Pls [simp, code post]: huffman@26086 649 "Bit0 Pls = Pls" haftmann@25919 650 unfolding numeral_simps by simp haftmann@25919 651 huffman@26086 652 lemma Bit1_Min [simp, code post]: huffman@26086 653 "Bit1 Min = Min" haftmann@25919 654 unfolding numeral_simps by simp haftmann@25919 655 huffman@26075 656 lemmas normalize_bin_simps = huffman@26086 657 Bit0_Pls Bit1_Min huffman@26075 658 haftmann@25919 659 huffman@28958 660 subsubsection {* Successor and predecessor functions *} huffman@28958 661 huffman@28958 662 text {* Successor *} huffman@28958 663 huffman@28958 664 lemma succ_Pls: huffman@26086 665 "succ Pls = Bit1 Pls" haftmann@25919 666 unfolding numeral_simps by simp haftmann@25919 667 huffman@28958 668 lemma succ_Min: haftmann@25919 669 "succ Min = Pls" haftmann@25919 670 unfolding numeral_simps by simp haftmann@25919 671 huffman@28958 672 lemma succ_Bit0: huffman@26086 673 "succ (Bit0 k) = Bit1 k" haftmann@25919 674 unfolding numeral_simps by simp haftmann@25919 675 huffman@28958 676 lemma succ_Bit1: huffman@26086 677 "succ (Bit1 k) = Bit0 (succ k)" haftmann@25919 678 unfolding numeral_simps by simp haftmann@25919 679 huffman@28958 680 lemmas succ_bin_simps [simp] = huffman@26086 681 succ_Pls succ_Min succ_Bit0 succ_Bit1 huffman@26075 682 huffman@28958 683 text {* Predecessor *} huffman@28958 684 huffman@28958 685 lemma pred_Pls: haftmann@25919 686 "pred Pls = Min" haftmann@25919 687 unfolding numeral_simps by simp haftmann@25919 688 huffman@28958 689 lemma pred_Min: huffman@26086 690 "pred Min = Bit0 Min" haftmann@25919 691 unfolding numeral_simps by simp haftmann@25919 692 huffman@28958 693 lemma pred_Bit0: huffman@26086 694 "pred (Bit0 k) = Bit1 (pred k)" haftmann@25919 695 unfolding numeral_simps by simp haftmann@25919 696 huffman@28958 697 lemma pred_Bit1: huffman@26086 698 "pred (Bit1 k) = Bit0 k" huffman@26086 699 unfolding numeral_simps by simp huffman@26086 700 huffman@28958 701 lemmas pred_bin_simps [simp] = huffman@26086 702 pred_Pls pred_Min pred_Bit0 pred_Bit1 huffman@26075 703 huffman@28958 704 huffman@28958 705 subsubsection {* Binary arithmetic *} huffman@28958 706 huffman@28958 707 text {* Addition *} huffman@28958 708 huffman@28958 709 lemma add_Pls: huffman@28958 710 "Pls + k = k" huffman@28958 711 unfolding numeral_simps by simp huffman@28958 712 huffman@28958 713 lemma add_Min: huffman@28958 714 "Min + k = pred k" huffman@28958 715 unfolding numeral_simps by simp huffman@28958 716 huffman@28958 717 lemma add_Bit0_Bit0: huffman@28958 718 "(Bit0 k) + (Bit0 l) = Bit0 (k + l)" huffman@28958 719 unfolding numeral_simps by simp huffman@28958 720 huffman@28958 721 lemma add_Bit0_Bit1: huffman@28958 722 "(Bit0 k) + (Bit1 l) = Bit1 (k + l)" huffman@28958 723 unfolding numeral_simps by simp huffman@28958 724 huffman@28958 725 lemma add_Bit1_Bit0: huffman@28958 726 "(Bit1 k) + (Bit0 l) = Bit1 (k + l)" huffman@28958 727 unfolding numeral_simps by simp huffman@28958 728 huffman@28958 729 lemma add_Bit1_Bit1: huffman@28958 730 "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)" huffman@28958 731 unfolding numeral_simps by simp huffman@28958 732 huffman@28958 733 lemma add_Pls_right: huffman@28958 734 "k + Pls = k" huffman@28958 735 unfolding numeral_simps by simp huffman@28958 736 huffman@28958 737 lemma add_Min_right: huffman@28958 738 "k + Min = pred k" huffman@28958 739 unfolding numeral_simps by simp huffman@28958 740 huffman@28958 741 lemmas add_bin_simps [simp] = huffman@28958 742 add_Pls add_Min add_Pls_right add_Min_right huffman@28958 743 add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1 huffman@28958 744 huffman@28958 745 text {* Negation *} huffman@28958 746 huffman@28958 747 lemma minus_Pls: haftmann@25919 748 "- Pls = Pls" huffman@28958 749 unfolding numeral_simps by simp huffman@28958 750 huffman@28958 751 lemma minus_Min: huffman@26086 752 "- Min = Bit1 Pls" huffman@28958 753 unfolding numeral_simps by simp huffman@28958 754 huffman@28958 755 lemma minus_Bit0: huffman@26086 756 "- (Bit0 k) = Bit0 (- k)" huffman@28958 757 unfolding numeral_simps by simp huffman@28958 758 huffman@28958 759 lemma minus_Bit1: huffman@26086 760 "- (Bit1 k) = Bit1 (pred (- k))" huffman@26086 761 unfolding numeral_simps by simp haftmann@25919 762 huffman@28958 763 lemmas minus_bin_simps [simp] = huffman@26086 764 minus_Pls minus_Min minus_Bit0 minus_Bit1 huffman@26075 765 huffman@28958 766 text {* Subtraction *} huffman@28958 767 huffman@29046 768 lemma diff_bin_simps [simp]: huffman@29046 769 "k - Pls = k" huffman@29046 770 "k - Min = succ k" huffman@29046 771 "Pls - (Bit0 l) = Bit0 (Pls - l)" huffman@29046 772 "Pls - (Bit1 l) = Bit1 (Min - l)" huffman@29046 773 "Min - (Bit0 l) = Bit1 (Min - l)" huffman@29046 774 "Min - (Bit1 l) = Bit0 (Min - l)" huffman@28958 775 "(Bit0 k) - (Bit0 l) = Bit0 (k - l)" huffman@28958 776 "(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)" huffman@28958 777 "(Bit1 k) - (Bit0 l) = Bit1 (k - l)" huffman@28958 778 "(Bit1 k) - (Bit1 l) = Bit0 (k - l)" huffman@29046 779 unfolding numeral_simps by simp_all huffman@28958 780 huffman@28958 781 text {* Multiplication *} huffman@28958 782 huffman@28958 783 lemma mult_Pls: huffman@28958 784 "Pls * w = Pls" huffman@26086 785 unfolding numeral_simps by simp haftmann@25919 786 huffman@28958 787 lemma mult_Min: haftmann@25919 788 "Min * k = - k" haftmann@25919 789 unfolding numeral_simps by simp haftmann@25919 790 huffman@28958 791 lemma mult_Bit0: huffman@26086 792 "(Bit0 k) * l = Bit0 (k * l)" huffman@26086 793 unfolding numeral_simps int_distrib by simp haftmann@25919 794 huffman@28958 795 lemma mult_Bit1: huffman@26086 796 "(Bit1 k) * l = (Bit0 (k * l)) + l" huffman@28958 797 unfolding numeral_simps int_distrib by simp huffman@28958 798 huffman@28958 799 lemmas mult_bin_simps [simp] = huffman@26086 800 mult_Pls mult_Min mult_Bit0 mult_Bit1 huffman@26075 801 haftmann@25919 802 huffman@28958 803 subsubsection {* Binary comparisons *} huffman@28958 804 huffman@28958 805 text {* Preliminaries *} huffman@28958 806 huffman@28958 807 lemma even_less_0_iff: huffman@28958 808 "a + a < 0 \ a < (0::'a::ordered_idom)" huffman@28958 809 proof - huffman@28958 810 have "a + a < 0 \ (1+1)*a < 0" by (simp add: left_distrib) huffman@28958 811 also have "(1+1)*a < 0 \ a < 0" huffman@28958 812 by (simp add: mult_less_0_iff zero_less_two huffman@28958 813 order_less_not_sym [OF zero_less_two]) huffman@28958 814 finally show ?thesis . huffman@28958 815 qed huffman@28958 816 huffman@28958 817 lemma le_imp_0_less: huffman@28958 818 assumes le: "0 \ z" huffman@28958 819 shows "(0::int) < 1 + z" huffman@28958 820 proof - huffman@28958 821 have "0 \ z" by fact huffman@28958 822 also have "... < z + 1" by (rule less_add_one) huffman@28958 823 also have "... = 1 + z" by (simp add: add_ac) huffman@28958 824 finally show "0 < 1 + z" . huffman@28958 825 qed huffman@28958 826 huffman@28958 827 lemma odd_less_0_iff: huffman@28958 828 "(1 + z + z < 0) = (z < (0::int))" huffman@28958 829 proof (cases z rule: int_cases) huffman@28958 830 case (nonneg n) huffman@28958 831 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing huffman@28958 832 le_imp_0_less [THEN order_less_imp_le]) huffman@28958 833 next huffman@28958 834 case (neg n) huffman@30079 835 thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 huffman@30079 836 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) huffman@28958 837 qed huffman@28958 838 huffman@28985 839 lemma bin_less_0_simps: huffman@28958 840 "Pls < 0 \ False" huffman@28958 841 "Min < 0 \ True" huffman@28958 842 "Bit0 w < 0 \ w < 0" huffman@28958 843 "Bit1 w < 0 \ w < 0" huffman@28958 844 unfolding numeral_simps huffman@28958 845 by (simp_all add: even_less_0_iff odd_less_0_iff) huffman@28958 846 huffman@28958 847 lemma less_bin_lemma: "k < l \ k - l < (0::int)" huffman@28958 848 by simp huffman@28958 849 huffman@28958 850 lemma le_iff_pred_less: "k \ l \ pred k < l" huffman@28958 851 unfolding numeral_simps huffman@28958 852 proof huffman@28958 853 have "k - 1 < k" by simp huffman@28958 854 also assume "k \ l" huffman@28958 855 finally show "k - 1 < l" . huffman@28958 856 next huffman@28958 857 assume "k - 1 < l" huffman@28958 858 hence "(k - 1) + 1 \ l" by (rule zless_imp_add1_zle) huffman@28958 859 thus "k \ l" by simp huffman@28958 860 qed huffman@28958 861 huffman@28958 862 lemma succ_pred: "succ (pred x) = x" huffman@28958 863 unfolding numeral_simps by simp huffman@28958 864 huffman@28958 865 text {* Less-than *} huffman@28958 866 huffman@28958 867 lemma less_bin_simps [simp]: huffman@28958 868 "Pls < Pls \ False" huffman@28958 869 "Pls < Min \ False" huffman@28958 870 "Pls < Bit0 k \ Pls < k" huffman@28958 871 "Pls < Bit1 k \ Pls \ k" huffman@28958 872 "Min < Pls \ True" huffman@28958 873 "Min < Min \ False" huffman@28958 874 "Min < Bit0 k \ Min < k" huffman@28958 875 "Min < Bit1 k \ Min < k" huffman@28958 876 "Bit0 k < Pls \ k < Pls" huffman@28958 877 "Bit0 k < Min \ k \ Min" huffman@28958 878 "Bit1 k < Pls \ k < Pls" huffman@28958 879 "Bit1 k < Min \ k < Min" huffman@28958 880 "Bit0 k < Bit0 l \ k < l" huffman@28958 881 "Bit0 k < Bit1 l \ k \ l" huffman@28958 882 "Bit1 k < Bit0 l \ k < l" huffman@28958 883 "Bit1 k < Bit1 l \ k < l" huffman@28958 884 unfolding le_iff_pred_less huffman@28958 885 less_bin_lemma [of Pls] huffman@28958 886 less_bin_lemma [of Min] huffman@28958 887 less_bin_lemma [of "k"] huffman@28958 888 less_bin_lemma [of "Bit0 k"] huffman@28958 889 less_bin_lemma [of "Bit1 k"] huffman@28958 890 less_bin_lemma [of "pred Pls"] huffman@28958 891 less_bin_lemma [of "pred k"] huffman@28985 892 by (simp_all add: bin_less_0_simps succ_pred) huffman@28958 893 huffman@28958 894 text {* Less-than-or-equal *} huffman@28958 895 huffman@28958 896 lemma le_bin_simps [simp]: huffman@28958 897 "Pls \ Pls \ True" huffman@28958 898 "Pls \ Min \ False" huffman@28958 899 "Pls \ Bit0 k \ Pls \ k" huffman@28958 900 "Pls \ Bit1 k \ Pls \ k" huffman@28958 901 "Min \ Pls \ True" huffman@28958 902 "Min \ Min \ True" huffman@28958 903 "Min \ Bit0 k \ Min < k" huffman@28958 904 "Min \ Bit1 k \ Min \ k" huffman@28958 905 "Bit0 k \ Pls \ k \ Pls" huffman@28958 906 "Bit0 k \ Min \ k \ Min" huffman@28958 907 "Bit1 k \ Pls \ k < Pls" huffman@28958 908 "Bit1 k \ Min \ k \ Min" huffman@28958 909 "Bit0 k \ Bit0 l \ k \ l" huffman@28958 910 "Bit0 k \ Bit1 l \ k \ l" huffman@28958 911 "Bit1 k \ Bit0 l \ k < l" huffman@28958 912 "Bit1 k \ Bit1 l \ k \ l" huffman@28958 913 unfolding not_less [symmetric] huffman@28958 914 by (simp_all add: not_le) huffman@28958 915 huffman@28958 916 text {* Equality *} huffman@28958 917 huffman@28958 918 lemma eq_bin_simps [simp]: huffman@28958 919 "Pls = Pls \ True" huffman@28958 920 "Pls = Min \ False" huffman@28958 921 "Pls = Bit0 l \ Pls = l" huffman@28958 922 "Pls = Bit1 l \ False" huffman@28958 923 "Min = Pls \ False" huffman@28958 924 "Min = Min \ True" huffman@28958 925 "Min = Bit0 l \ False" huffman@28958 926 "Min = Bit1 l \ Min = l" huffman@28958 927 "Bit0 k = Pls \ k = Pls" huffman@28958 928 "Bit0 k = Min \ False" huffman@28958 929 "Bit1 k = Pls \ False" huffman@28958 930 "Bit1 k = Min \ k = Min" huffman@28958 931 "Bit0 k = Bit0 l \ k = l" huffman@28958 932 "Bit0 k = Bit1 l \ False" huffman@28958 933 "Bit1 k = Bit0 l \ False" huffman@28958 934 "Bit1 k = Bit1 l \ k = l" huffman@28958 935 unfolding order_eq_iff [where 'a=int] huffman@28958 936 by (simp_all add: not_less) huffman@28958 937 huffman@28958 938 haftmann@25919 939 subsection {* Converting Numerals to Rings: @{term number_of} *} haftmann@25919 940 haftmann@25919 941 class number_ring = number + comm_ring_1 + haftmann@25919 942 assumes number_of_eq: "number_of k = of_int k" haftmann@25919 943 haftmann@25919 944 text {* self-embedding of the integers *} haftmann@25919 945 haftmann@25919 946 instantiation int :: number_ring haftmann@25919 947 begin haftmann@25919 948 haftmann@28724 949 definition int_number_of_def [code del]: haftmann@28724 950 "number_of w = (of_int w \ int)" haftmann@25919 951 haftmann@28724 952 instance proof haftmann@28724 953 qed (simp only: int_number_of_def) haftmann@25919 954 haftmann@25919 955 end haftmann@25919 956 haftmann@25919 957 lemma number_of_is_id: haftmann@25919 958 "number_of (k::int) = k" haftmann@25919 959 unfolding int_number_of_def by simp haftmann@25919 960 haftmann@25919 961 lemma number_of_succ: haftmann@25919 962 "number_of (succ k) = (1 + number_of k ::'a::number_ring)" haftmann@25919 963 unfolding number_of_eq numeral_simps by simp haftmann@25919 964 haftmann@25919 965 lemma number_of_pred: haftmann@25919 966 "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)" haftmann@25919 967 unfolding number_of_eq numeral_simps by simp haftmann@25919 968 haftmann@25919 969 lemma number_of_minus: haftmann@25919 970 "number_of (uminus w) = (- (number_of w)::'a::number_ring)" huffman@28958 971 unfolding number_of_eq by (rule of_int_minus) haftmann@25919 972 haftmann@25919 973 lemma number_of_add: haftmann@25919 974 "number_of (v + w) = (number_of v + number_of w::'a::number_ring)" huffman@28958 975 unfolding number_of_eq by (rule of_int_add) huffman@28958 976 huffman@28958 977 lemma number_of_diff: huffman@28958 978 "number_of (v - w) = (number_of v - number_of w::'a::number_ring)" huffman@28958 979 unfolding number_of_eq by (rule of_int_diff) haftmann@25919 980 haftmann@25919 981 lemma number_of_mult: haftmann@25919 982 "number_of (v * w) = (number_of v * number_of w::'a::number_ring)" huffman@28958 983 unfolding number_of_eq by (rule of_int_mult) haftmann@25919 984 haftmann@25919 985 text {* haftmann@25919 986 The correctness of shifting. haftmann@25919 987 But it doesn't seem to give a measurable speed-up. haftmann@25919 988 *} haftmann@25919 989 huffman@26086 990 lemma double_number_of_Bit0: huffman@26086 991 "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)" haftmann@25919 992 unfolding number_of_eq numeral_simps left_distrib by simp haftmann@25919 993 haftmann@25919 994 text {* haftmann@25919 995 Converting numerals 0 and 1 to their abstract versions. haftmann@25919 996 *} haftmann@25919 997 haftmann@25919 998 lemma numeral_0_eq_0 [simp]: haftmann@25919 999 "Numeral0 = (0::'a::number_ring)" haftmann@25919 1000 unfolding number_of_eq numeral_simps by simp haftmann@25919 1001 haftmann@25919 1002 lemma numeral_1_eq_1 [simp]: haftmann@25919 1003 "Numeral1 = (1::'a::number_ring)" haftmann@25919 1004 unfolding number_of_eq numeral_simps by simp haftmann@25919 1005 haftmann@25919 1006 text {* haftmann@25919 1007 Special-case simplification for small constants. haftmann@25919 1008 *} haftmann@25919 1009 haftmann@25919 1010 text{* haftmann@25919 1011 Unary minus for the abstract constant 1. Cannot be inserted haftmann@25919 1012 as a simprule until later: it is @{text number_of_Min} re-oriented! haftmann@25919 1013 *} haftmann@25919 1014 haftmann@25919 1015 lemma numeral_m1_eq_minus_1: haftmann@25919 1016 "(-1::'a::number_ring) = - 1" haftmann@25919 1017 unfolding number_of_eq numeral_simps by simp haftmann@25919 1018 haftmann@25919 1019 lemma mult_minus1 [simp]: haftmann@25919 1020 "-1 * z = -(z::'a::number_ring)" haftmann@25919 1021 unfolding number_of_eq numeral_simps by simp haftmann@25919 1022 haftmann@25919 1023 lemma mult_minus1_right [simp]: haftmann@25919 1024 "z * -1 = -(z::'a::number_ring)" haftmann@25919 1025 unfolding number_of_eq numeral_simps by simp haftmann@25919 1026 haftmann@25919 1027 (*Negation of a coefficient*) haftmann@25919 1028 lemma minus_number_of_mult [simp]: haftmann@25919 1029 "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)" haftmann@25919 1030 unfolding number_of_eq by simp haftmann@25919 1031 haftmann@25919 1032 text {* Subtraction *} haftmann@25919 1033 haftmann@25919 1034 lemma diff_number_of_eq: haftmann@25919 1035 "number_of v - number_of w = haftmann@25919 1036 (number_of (v + uminus w)::'a::number_ring)" haftmann@25919 1037 unfolding number_of_eq by simp haftmann@25919 1038 haftmann@25919 1039 lemma number_of_Pls: haftmann@25919 1040 "number_of Pls = (0::'a::number_ring)" haftmann@25919 1041 unfolding number_of_eq numeral_simps by simp haftmann@25919 1042 haftmann@25919 1043 lemma number_of_Min: haftmann@25919 1044 "number_of Min = (- 1::'a::number_ring)" haftmann@25919 1045 unfolding number_of_eq numeral_simps by simp haftmann@25919 1046 huffman@26086 1047 lemma number_of_Bit0: huffman@26086 1048 "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)" huffman@26086 1049 unfolding number_of_eq numeral_simps by simp huffman@26086 1050 huffman@26086 1051 lemma number_of_Bit1: huffman@26086 1052 "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)" huffman@26086 1053 unfolding number_of_eq numeral_simps by simp haftmann@25919 1054 haftmann@25919 1055 huffman@28958 1056 subsubsection {* Equality of Binary Numbers *} haftmann@25919 1057 haftmann@25919 1058 text {* First version by Norbert Voelker *} haftmann@25919 1059 haftmann@25919 1060 definition (*for simplifying equalities*) haftmann@25919 1061 iszero :: "'a\semiring_1 \ bool" haftmann@25919 1062 where haftmann@25919 1063 "iszero z \ z = 0" haftmann@25919 1064 haftmann@25919 1065 lemma iszero_0: "iszero 0" haftmann@25919 1066 by (simp add: iszero_def) haftmann@25919 1067 haftmann@25919 1068 lemma not_iszero_1: "~ iszero 1" haftmann@25919 1069 by (simp add: iszero_def eq_commute) haftmann@25919 1070 haftmann@25919 1071 lemma eq_number_of_eq: haftmann@25919 1072 "((number_of x::'a::number_ring) = number_of y) = haftmann@25919 1073 iszero (number_of (x + uminus y) :: 'a)" nipkow@29667 1074 unfolding iszero_def number_of_add number_of_minus nipkow@29667 1075 by (simp add: algebra_simps) haftmann@25919 1076 haftmann@25919 1077 lemma iszero_number_of_Pls: haftmann@25919 1078 "iszero ((number_of Pls)::'a::number_ring)" nipkow@29667 1079 unfolding iszero_def numeral_0_eq_0 .. haftmann@25919 1080 haftmann@25919 1081 lemma nonzero_number_of_Min: haftmann@25919 1082 "~ iszero ((number_of Min)::'a::number_ring)" nipkow@29667 1083 unfolding iszero_def numeral_m1_eq_minus_1 by simp haftmann@25919 1084 haftmann@25919 1085 huffman@28958 1086 subsubsection {* Comparisons, for Ordered Rings *} haftmann@25919 1087 haftmann@25919 1088 lemmas double_eq_0_iff = double_zero haftmann@25919 1089 haftmann@25919 1090 lemma odd_nonzero: haftmann@25919 1091 "1 + z + z \ (0::int)"; haftmann@25919 1092 proof (cases z rule: int_cases) haftmann@25919 1093 case (nonneg n) haftmann@25919 1094 have le: "0 \ z+z" by (simp add: nonneg add_increasing) haftmann@25919 1095 thus ?thesis using le_imp_0_less [OF le] haftmann@25919 1096 by (auto simp add: add_assoc) haftmann@25919 1097 next haftmann@25919 1098 case (neg n) haftmann@25919 1099 show ?thesis haftmann@25919 1100 proof haftmann@25919 1101 assume eq: "1 + z + z = 0" haftmann@25919 1102 have "(0::int) < 1 + (of_nat n + of_nat n)" haftmann@25919 1103 by (simp add: le_imp_0_less add_increasing) haftmann@25919 1104 also have "... = - (1 + z + z)" haftmann@25919 1105 by (simp add: neg add_assoc [symmetric]) haftmann@25919 1106 also have "... = 0" by (simp add: eq) haftmann@25919 1107 finally have "0<0" .. haftmann@25919 1108 thus False by blast haftmann@25919 1109 qed haftmann@25919 1110 qed haftmann@25919 1111 huffman@26086 1112 lemma iszero_number_of_Bit0: huffman@26086 1113 "iszero (number_of (Bit0 w)::'a) = huffman@26086 1114 iszero (number_of w::'a::{ring_char_0,number_ring})" haftmann@25919 1115 proof - haftmann@25919 1116 have "(of_int w + of_int w = (0::'a)) \ (w = 0)" haftmann@25919 1117 proof - haftmann@25919 1118 assume eq: "of_int w + of_int w = (0::'a)" haftmann@25919 1119 then have "of_int (w + w) = (of_int 0 :: 'a)" by simp haftmann@25919 1120 then have "w + w = 0" by (simp only: of_int_eq_iff) haftmann@25919 1121 then show "w = 0" by (simp only: double_eq_0_iff) haftmann@25919 1122 qed huffman@26086 1123 thus ?thesis huffman@26086 1124 by (auto simp add: iszero_def number_of_eq numeral_simps) huffman@26086 1125 qed huffman@26086 1126 huffman@26086 1127 lemma iszero_number_of_Bit1: huffman@26086 1128 "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})" huffman@26086 1129 proof - huffman@26086 1130 have "1 + of_int w + of_int w \ (0::'a)" haftmann@25919 1131 proof haftmann@25919 1132 assume eq: "1 + of_int w + of_int w = (0::'a)" haftmann@25919 1133 hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp haftmann@25919 1134 hence "1 + w + w = 0" by (simp only: of_int_eq_iff) haftmann@25919 1135 with odd_nonzero show False by blast haftmann@25919 1136 qed huffman@26086 1137 thus ?thesis huffman@26086 1138 by (auto simp add: iszero_def number_of_eq numeral_simps) haftmann@25919 1139 qed haftmann@25919 1140 huffman@28985 1141 lemmas iszero_simps = huffman@28985 1142 iszero_0 not_iszero_1 huffman@28985 1143 iszero_number_of_Pls nonzero_number_of_Min huffman@28985 1144 iszero_number_of_Bit0 iszero_number_of_Bit1 huffman@28985 1145 (* iszero_number_of_Pls would never normally be used huffman@28985 1146 because its lhs simplifies to "iszero 0" *) haftmann@25919 1147 huffman@28958 1148 subsubsection {* The Less-Than Relation *} haftmann@25919 1149 haftmann@25919 1150 lemma double_less_0_iff: haftmann@25919 1151 "(a + a < 0) = (a < (0::'a::ordered_idom))" haftmann@25919 1152 proof - haftmann@25919 1153 have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib) haftmann@25919 1154 also have "... = (a < 0)" haftmann@25919 1155 by (simp add: mult_less_0_iff zero_less_two haftmann@25919 1156 order_less_not_sym [OF zero_less_two]) haftmann@25919 1157 finally show ?thesis . haftmann@25919 1158 qed haftmann@25919 1159 haftmann@25919 1160 lemma odd_less_0: haftmann@25919 1161 "(1 + z + z < 0) = (z < (0::int))"; haftmann@25919 1162 proof (cases z rule: int_cases) haftmann@25919 1163 case (nonneg n) haftmann@25919 1164 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing haftmann@25919 1165 le_imp_0_less [THEN order_less_imp_le]) haftmann@25919 1166 next haftmann@25919 1167 case (neg n) huffman@30079 1168 thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 huffman@30079 1169 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) haftmann@25919 1170 qed haftmann@25919 1171 haftmann@25919 1172 text {* Less-Than or Equals *} haftmann@25919 1173 haftmann@25919 1174 text {* Reduces @{term "a\b"} to @{term "~ (b x < y" huffman@28962 1219 unfolding number_of_eq by (rule of_int_less_iff) huffman@28962 1220 huffman@28962 1221 lemma le_number_of [simp]: huffman@28962 1222 "(number_of x::'a::{ordered_idom,number_ring}) \ number_of y \ x \ y" huffman@28962 1223 unfolding number_of_eq by (rule of_int_le_iff) huffman@28962 1224 huffman@28967 1225 lemma eq_number_of [simp]: huffman@28967 1226 "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \ x = y" huffman@28967 1227 unfolding number_of_eq by (rule of_int_eq_iff) huffman@28967 1228 haftmann@25919 1229 lemmas rel_simps [simp] = huffman@28962 1230 less_number_of less_bin_simps huffman@28962 1231 le_number_of le_bin_simps huffman@28988 1232 eq_number_of_eq eq_bin_simps huffman@29039 1233 iszero_simps haftmann@25919 1234 haftmann@25919 1235 huffman@28958 1236 subsubsection {* Simplification of arithmetic when nested to the right. *} haftmann@25919 1237 haftmann@25919 1238 lemma add_number_of_left [simp]: haftmann@25919 1239 "number_of v + (number_of w + z) = haftmann@25919 1240 (number_of(v + w) + z::'a::number_ring)" haftmann@25919 1241 by (simp add: add_assoc [symmetric]) haftmann@25919 1242 haftmann@25919 1243 lemma mult_number_of_left [simp]: haftmann@25919 1244 "number_of v * (number_of w * z) = haftmann@25919 1245 (number_of(v * w) * z::'a::number_ring)" haftmann@25919 1246 by (simp add: mult_assoc [symmetric]) haftmann@25919 1247 haftmann@25919 1248 lemma add_number_of_diff1: haftmann@25919 1249 "number_of v + (number_of w - c) = haftmann@25919 1250 number_of(v + w) - (c::'a::number_ring)" haftmann@25919 1251 by (simp add: diff_minus add_number_of_left) haftmann@25919 1252 haftmann@25919 1253 lemma add_number_of_diff2 [simp]: haftmann@25919 1254 "number_of v + (c - number_of w) = haftmann@25919 1255 number_of (v + uminus w) + (c::'a::number_ring)" nipkow@29667 1256 by (simp add: algebra_simps diff_number_of_eq [symmetric]) haftmann@25919 1257 haftmann@25919 1258 haftmann@25919 1259 subsection {* The Set of Integers *} haftmann@25919 1260 haftmann@25919 1261 context ring_1 haftmann@25919 1262 begin haftmann@25919 1263 haftmann@25919 1264 definition haftmann@25919 1265 Ints :: "'a set" haftmann@25919 1266 where haftmann@28562 1267 [code del]: "Ints = range of_int" haftmann@25919 1268 haftmann@25919 1269 end haftmann@25919 1270 haftmann@25919 1271 notation (xsymbols) haftmann@25919 1272 Ints ("\") haftmann@25919 1273 haftmann@25919 1274 context ring_1 haftmann@25919 1275 begin haftmann@25919 1276 haftmann@25919 1277 lemma Ints_0 [simp]: "0 \ \" haftmann@25919 1278 apply (simp add: Ints_def) haftmann@25919 1279 apply (rule range_eqI) haftmann@25919 1280 apply (rule of_int_0 [symmetric]) haftmann@25919 1281 done haftmann@25919 1282 haftmann@25919 1283 lemma Ints_1 [simp]: "1 \ \" haftmann@25919 1284 apply (simp add: Ints_def) haftmann@25919 1285 apply (rule range_eqI) haftmann@25919 1286 apply (rule of_int_1 [symmetric]) haftmann@25919 1287 done haftmann@25919 1288 haftmann@25919 1289 lemma Ints_add [simp]: "a \ \ \ b \ \ \ a + b \ \" haftmann@25919 1290 apply (auto simp add: Ints_def) haftmann@25919 1291 apply (rule range_eqI) haftmann@25919 1292 apply (rule of_int_add [symmetric]) haftmann@25919 1293 done haftmann@25919 1294 haftmann@25919 1295 lemma Ints_minus [simp]: "a \ \ \ -a \ \" haftmann@25919 1296 apply (auto simp add: Ints_def) haftmann@25919 1297 apply (rule range_eqI) haftmann@25919 1298 apply (rule of_int_minus [symmetric]) haftmann@25919 1299 done haftmann@25919 1300 haftmann@25919 1301 lemma Ints_mult [simp]: "a \ \ \ b \ \ \ a * b \ \" haftmann@25919 1302 apply (auto simp add: Ints_def) haftmann@25919 1303 apply (rule range_eqI) haftmann@25919 1304 apply (rule of_int_mult [symmetric]) haftmann@25919 1305 done haftmann@25919 1306 haftmann@25919 1307 lemma Ints_cases [cases set: Ints]: haftmann@25919 1308 assumes "q \ \" haftmann@25919 1309 obtains (of_int) z where "q = of_int z" haftmann@25919 1310 unfolding Ints_def haftmann@25919 1311 proof - haftmann@25919 1312 from `q \ \` have "q \ range of_int" unfolding Ints_def . haftmann@25919 1313 then obtain z where "q = of_int z" .. haftmann@25919 1314 then show thesis .. haftmann@25919 1315 qed haftmann@25919 1316 haftmann@25919 1317 lemma Ints_induct [case_names of_int, induct set: Ints]: haftmann@25919 1318 "q \ \ \ (\z. P (of_int z)) \ P q" haftmann@25919 1319 by (rule Ints_cases) auto haftmann@25919 1320 haftmann@25919 1321 end haftmann@25919 1322 haftmann@25919 1323 lemma Ints_diff [simp]: "a \ \ \ b \ \ \ a-b \ \" haftmann@25919 1324 apply (auto simp add: Ints_def) haftmann@25919 1325 apply (rule range_eqI) haftmann@25919 1326 apply (rule of_int_diff [symmetric]) haftmann@25919 1327 done haftmann@25919 1328 haftmann@25919 1329 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *} haftmann@25919 1330 haftmann@25919 1331 lemma Ints_double_eq_0_iff: haftmann@25919 1332 assumes in_Ints: "a \ Ints" haftmann@25919 1333 shows "(a + a = 0) = (a = (0::'a::ring_char_0))" haftmann@25919 1334 proof - haftmann@25919 1335 from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . haftmann@25919 1336 then obtain z where a: "a = of_int z" .. haftmann@25919 1337 show ?thesis haftmann@25919 1338 proof haftmann@25919 1339 assume "a = 0" haftmann@25919 1340 thus "a + a = 0" by simp haftmann@25919 1341 next haftmann@25919 1342 assume eq: "a + a = 0" haftmann@25919 1343 hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a) haftmann@25919 1344 hence "z + z = 0" by (simp only: of_int_eq_iff) haftmann@25919 1345 hence "z = 0" by (simp only: double_eq_0_iff) haftmann@25919 1346 thus "a = 0" by (simp add: a) haftmann@25919 1347 qed haftmann@25919 1348 qed haftmann@25919 1349 haftmann@25919 1350 lemma Ints_odd_nonzero: haftmann@25919 1351 assumes in_Ints: "a \ Ints" haftmann@25919 1352 shows "1 + a + a \ (0::'a::ring_char_0)" haftmann@25919 1353 proof - haftmann@25919 1354 from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . haftmann@25919 1355 then obtain z where a: "a = of_int z" .. haftmann@25919 1356 show ?thesis haftmann@25919 1357 proof haftmann@25919 1358 assume eq: "1 + a + a = 0" haftmann@25919 1359 hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a) haftmann@25919 1360 hence "1 + z + z = 0" by (simp only: of_int_eq_iff) haftmann@25919 1361 with odd_nonzero show False by blast haftmann@25919 1362 qed haftmann@25919 1363 qed haftmann@25919 1364 haftmann@25919 1365 lemma Ints_number_of: haftmann@25919 1366 "(number_of w :: 'a::number_ring) \ Ints" haftmann@25919 1367 unfolding number_of_eq Ints_def by simp haftmann@25919 1368 haftmann@25919 1369 lemma Ints_odd_less_0: haftmann@25919 1370 assumes in_Ints: "a \ Ints" haftmann@25919 1371 shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))"; haftmann@25919 1372 proof - haftmann@25919 1373 from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . haftmann@25919 1374 then obtain z where a: "a = of_int z" .. haftmann@25919 1375 hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))" haftmann@25919 1376 by (simp add: a) haftmann@25919 1377 also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0) haftmann@25919 1378 also have "... = (a < 0)" by (simp add: a) haftmann@25919 1379 finally show ?thesis . haftmann@25919 1380 qed haftmann@25919 1381 haftmann@25919 1382 haftmann@25919 1383 subsection {* @{term setsum} and @{term setprod} *} haftmann@25919 1384 haftmann@25919 1385 text {*By Jeremy Avigad*} haftmann@25919 1386 haftmann@25919 1387 lemma of_nat_setsum: "of_nat (setsum f A) = (\x\A. of_nat(f x))" haftmann@25919 1388 apply (cases "finite A") haftmann@25919 1389 apply (erule finite_induct, auto) haftmann@25919 1390 done haftmann@25919 1391 haftmann@25919 1392 lemma of_int_setsum: "of_int (setsum f A) = (\x\A. of_int(f x))" haftmann@25919 1393 apply (cases "finite A") haftmann@25919 1394 apply (erule finite_induct, auto) haftmann@25919 1395 done haftmann@25919 1396 haftmann@25919 1397 lemma of_nat_setprod: "of_nat (setprod f A) = (\x\A. of_nat(f x))" haftmann@25919 1398 apply (cases "finite A") haftmann@25919 1399 apply (erule finite_induct, auto simp add: of_nat_mult) haftmann@25919 1400 done haftmann@25919 1401 haftmann@25919 1402 lemma of_int_setprod: "of_int (setprod f A) = (\x\A. of_int(f x))" haftmann@25919 1403 apply (cases "finite A") haftmann@25919 1404 apply (erule finite_induct, auto) haftmann@25919 1405 done haftmann@25919 1406 haftmann@25919 1407 lemma setprod_nonzero_nat: haftmann@25919 1408 "finite A ==> (\x \ A. f x \ (0::nat)) ==> setprod f A \ 0" haftmann@25919 1409 by (rule setprod_nonzero, auto) haftmann@25919 1410 haftmann@25919 1411 lemma setprod_zero_eq_nat: haftmann@25919 1412 "finite A ==> (setprod f A = (0::nat)) = (\x \ A. f x = 0)" haftmann@25919 1413 by (rule setprod_zero_eq, auto) haftmann@25919 1414 haftmann@25919 1415 lemma setprod_nonzero_int: haftmann@25919 1416 "finite A ==> (\x \ A. f x \ (0::int)) ==> setprod f A \ 0" haftmann@25919 1417 by (rule setprod_nonzero, auto) haftmann@25919 1418 haftmann@25919 1419 lemma setprod_zero_eq_int: haftmann@25919 1420 "finite A ==> (setprod f A = (0::int)) = (\x \ A. f x = 0)" haftmann@25919 1421 by (rule setprod_zero_eq, auto) haftmann@25919 1422 haftmann@25919 1423 lemmas int_setsum = of_nat_setsum [where 'a=int] haftmann@25919 1424 lemmas int_setprod = of_nat_setprod [where 'a=int] haftmann@25919 1425 haftmann@25919 1426 haftmann@25919 1427 subsection{*Inequality Reasoning for the Arithmetic Simproc*} haftmann@25919 1428 haftmann@25919 1429 lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)" haftmann@25919 1430 by simp haftmann@25919 1431 haftmann@25919 1432 lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)" haftmann@25919 1433 by simp haftmann@25919 1434 haftmann@25919 1435 lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)" haftmann@25919 1436 by simp haftmann@25919 1437 haftmann@25919 1438 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)" haftmann@25919 1439 by simp haftmann@25919 1440 haftmann@25919 1441 lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})" haftmann@25919 1442 by simp haftmann@25919 1443 haftmann@25919 1444 lemma inverse_numeral_1: haftmann@25919 1445 "inverse Numeral1 = (Numeral1::'a::{number_ring,field})" haftmann@25919 1446 by simp haftmann@25919 1447 haftmann@25919 1448 text{*Theorem lists for the cancellation simprocs. The use of binary numerals haftmann@25919 1449 for 0 and 1 reduces the number of special cases.*} haftmann@25919 1450 haftmann@25919 1451 lemmas add_0s = add_numeral_0 add_numeral_0_right haftmann@25919 1452 lemmas mult_1s = mult_numeral_1 mult_numeral_1_right haftmann@25919 1453 mult_minus1 mult_minus1_right haftmann@25919 1454 haftmann@25919 1455 haftmann@25919 1456 subsection{*Special Arithmetic Rules for Abstract 0 and 1*} haftmann@25919 1457 haftmann@25919 1458 text{*Arithmetic computations are defined for binary literals, which leaves 0 haftmann@25919 1459 and 1 as special cases. Addition already has rules for 0, but not 1. haftmann@25919 1460 Multiplication and unary minus already have rules for both 0 and 1.*} haftmann@25919 1461 haftmann@25919 1462 haftmann@25919 1463 lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'" haftmann@25919 1464 by simp haftmann@25919 1465 haftmann@25919 1466 haftmann@25919 1467 lemmas add_number_of_eq = number_of_add [symmetric] haftmann@25919 1468 haftmann@25919 1469 text{*Allow 1 on either or both sides*} haftmann@25919 1470 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)" haftmann@25919 1471 by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq) haftmann@25919 1472 haftmann@25919 1473 lemmas add_special = haftmann@25919 1474 one_add_one_is_two haftmann@25919 1475 binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard] haftmann@25919 1476 binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard] haftmann@25919 1477 haftmann@25919 1478 text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*} haftmann@25919 1479 lemmas diff_special = haftmann@25919 1480 binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard] haftmann@25919 1481 binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard] haftmann@25919 1482 haftmann@25919 1483 text{*Allow 0 or 1 on either side with a binary numeral on the other*} haftmann@25919 1484 lemmas eq_special = haftmann@25919 1485 binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard] haftmann@25919 1486 binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard] haftmann@25919 1487 binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard] haftmann@25919 1488 binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard] haftmann@25919 1489 haftmann@25919 1490 text{*Allow 0 or 1 on either side with a binary numeral on the other*} haftmann@25919 1491 lemmas less_special = huffman@28984 1492 binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard] huffman@28984 1493 binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard] huffman@28984 1494 binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard] huffman@28984 1495 binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard] haftmann@25919 1496 haftmann@25919 1497 text{*Allow 0 or 1 on either side with a binary numeral on the other*} haftmann@25919 1498 lemmas le_special = huffman@28984 1499 binop_eq [of "op \", OF le_number_of numeral_0_eq_0 refl, standard] huffman@28984 1500 binop_eq [of "op \", OF le_number_of numeral_1_eq_1 refl, standard] huffman@28984 1501 binop_eq [of "op \", OF le_number_of refl numeral_0_eq_0, standard] huffman@28984 1502 binop_eq [of "op \", OF le_number_of refl numeral_1_eq_1, standard] haftmann@25919 1503 haftmann@25919 1504 lemmas arith_special[simp] = haftmann@25919 1505 add_special diff_special eq_special less_special le_special haftmann@25919 1506 haftmann@25919 1507 haftmann@25919 1508 lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 & haftmann@25919 1509 max (0::int) 1 = 1 & max (1::int) 0 = 1" haftmann@25919 1510 by(simp add:min_def max_def) haftmann@25919 1511 haftmann@25919 1512 lemmas min_max_special[simp] = haftmann@25919 1513 min_max_01 haftmann@25919 1514 max_def[of "0::int" "number_of v", standard, simp] haftmann@25919 1515 min_def[of "0::int" "number_of v", standard, simp] haftmann@25919 1516 max_def[of "number_of u" "0::int", standard, simp] haftmann@25919 1517 min_def[of "number_of u" "0::int", standard, simp] haftmann@25919 1518 max_def[of "1::int" "number_of v", standard, simp] haftmann@25919 1519 min_def[of "1::int" "number_of v", standard, simp] haftmann@25919 1520 max_def[of "number_of u" "1::int", standard, simp] haftmann@25919 1521 min_def[of "number_of u" "1::int", standard, simp] haftmann@25919 1522 haftmann@25919 1523 text {* Legacy theorems *} haftmann@25919 1524 haftmann@25919 1525 lemmas zle_int = of_nat_le_iff [where 'a=int] haftmann@25919 1526 lemmas int_int_eq = of_nat_eq_iff [where 'a=int] haftmann@25919 1527 haftmann@25919 1528 use "~~/src/Provers/Arith/assoc_fold.ML" haftmann@28952 1529 use "Tools/int_arith.ML" haftmann@25919 1530 declaration {* K int_arith_setup *} haftmann@25919 1531 haftmann@25919 1532 haftmann@25919 1533 subsection{*Lemmas About Small Numerals*} haftmann@25919 1534 haftmann@25919 1535 lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)" haftmann@25919 1536 proof - haftmann@25919 1537 have "(of_int -1 :: 'a) = of_int (- 1)" by simp haftmann@25919 1538 also have "... = - of_int 1" by (simp only: of_int_minus) haftmann@25919 1539 also have "... = -1" by simp haftmann@25919 1540 finally show ?thesis . haftmann@25919 1541 qed haftmann@25919 1542 haftmann@25919 1543 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})" haftmann@25919 1544 by (simp add: abs_if) haftmann@25919 1545 haftmann@25919 1546 lemma abs_power_minus_one [simp]: haftmann@25919 1547 "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})" haftmann@25919 1548 by (simp add: power_abs) haftmann@25919 1549 huffman@30000 1550 lemma of_int_number_of_eq [simp]: haftmann@25919 1551 "of_int (number_of v) = (number_of v :: 'a :: number_ring)" haftmann@25919 1552 by (simp add: number_of_eq) haftmann@25919 1553 haftmann@25919 1554 text{*Lemmas for specialist use, NOT as default simprules*} haftmann@25919 1555 lemma mult_2: "2 * z = (z+z::'a::number_ring)" haftmann@25919 1556 proof - haftmann@25919 1557 have "2*z = (1 + 1)*z" by simp haftmann@25919 1558 also have "... = z+z" by (simp add: left_distrib) haftmann@25919 1559 finally show ?thesis . haftmann@25919 1560 qed haftmann@25919 1561 haftmann@25919 1562 lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)" haftmann@25919 1563 by (subst mult_commute, rule mult_2) haftmann@25919 1564 haftmann@25919 1565 haftmann@25919 1566 subsection{*More Inequality Reasoning*} haftmann@25919 1567 haftmann@25919 1568 lemma zless_add1_eq: "(w < z + (1::int)) = (w z) = (w z - (1::int)) = (wz)" haftmann@25919 1578 by arith haftmann@25919 1579 haftmann@25919 1580 lemma int_one_le_iff_zero_less: "((1::int) \ z) = (0 < z)" haftmann@25919 1581 by arith haftmann@25919 1582 haftmann@25919 1583 huffman@28958 1584 subsection{*The functions @{term nat} and @{term int}*} haftmann@25919 1585 haftmann@25919 1586 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and haftmann@25919 1587 @{term "w + - z"}*} haftmann@25919 1588 declare Zero_int_def [symmetric, simp] haftmann@25919 1589 declare One_int_def [symmetric, simp] haftmann@25919 1590 haftmann@25919 1591 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp] haftmann@25919 1592 haftmann@25919 1593 lemma nat_0: "nat 0 = 0" haftmann@25919 1594 by (simp add: nat_eq_iff) haftmann@25919 1595 haftmann@25919 1596 lemma nat_1: "nat 1 = Suc 0" haftmann@25919 1597 by (subst nat_eq_iff, simp) haftmann@25919 1598 haftmann@25919 1599 lemma nat_2: "nat 2 = Suc (Suc 0)" haftmann@25919 1600 by (subst nat_eq_iff, simp) haftmann@25919 1601 haftmann@25919 1602 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)" haftmann@25919 1603 apply (insert zless_nat_conj [of 1 z]) haftmann@25919 1604 apply (auto simp add: nat_1) haftmann@25919 1605 done haftmann@25919 1606 haftmann@25919 1607 text{*This simplifies expressions of the form @{term "int n = z"} where haftmann@25919 1608 z is an integer literal.*} haftmann@25919 1609 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard] haftmann@25919 1610 haftmann@25919 1611 lemma split_nat [arith_split]: haftmann@25919 1612 "P(nat(i::int)) = ((\n. i = of_nat n \ P n) & (i < 0 \ P 0))" haftmann@25919 1613 (is "?P = (?L & ?R)") haftmann@25919 1614 proof (cases "i < 0") haftmann@25919 1615 case True thus ?thesis by auto haftmann@25919 1616 next haftmann@25919 1617 case False haftmann@25919 1618 have "?P = ?L" haftmann@25919 1619 proof haftmann@25919 1620 assume ?P thus ?L using False by clarsimp haftmann@25919 1621 next haftmann@25919 1622 assume ?L thus ?P using False by simp haftmann@25919 1623 qed haftmann@25919 1624 with False show ?thesis by simp haftmann@25919 1625 qed haftmann@25919 1626 haftmann@25919 1627 context ring_1 haftmann@25919 1628 begin haftmann@25919 1629 blanchet@29955 1630 lemma of_int_of_nat [nitpick_const_simp]: haftmann@25919 1631 "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))" haftmann@25919 1632 proof (cases "k < 0") haftmann@25919 1633 case True then have "0 \ - k" by simp haftmann@25919 1634 then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat) haftmann@25919 1635 with True show ?thesis by simp haftmann@25919 1636 next haftmann@25919 1637 case False then show ?thesis by (simp add: not_less of_nat_nat) haftmann@25919 1638 qed haftmann@25919 1639 haftmann@25919 1640 end haftmann@25919 1641 haftmann@25919 1642 lemma nat_mult_distrib: haftmann@25919 1643 fixes z z' :: int haftmann@25919 1644 assumes "0 \ z" haftmann@25919 1645 shows "nat (z * z') = nat z * nat z'" haftmann@25919 1646 proof (cases "0 \ z'") haftmann@25919 1647 case False with assms have "z * z' \ 0" haftmann@25919 1648 by (simp add: not_le mult_le_0_iff) haftmann@25919 1649 then have "nat (z * z') = 0" by simp haftmann@25919 1650 moreover from False have "nat z' = 0" by simp haftmann@25919 1651 ultimately show ?thesis by simp haftmann@25919 1652 next haftmann@25919 1653 case True with assms have ge_0: "z * z' \ 0" by (simp add: zero_le_mult_iff) haftmann@25919 1654 show ?thesis haftmann@25919 1655 by (rule injD [of "of_nat :: nat \ int", OF inj_of_nat]) haftmann@25919 1656 (simp only: of_nat_mult of_nat_nat [OF True] haftmann@25919 1657 of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp) haftmann@25919 1658 qed haftmann@25919 1659 haftmann@25919 1660 lemma nat_mult_distrib_neg: "z \ (0::int) ==> nat(z*z') = nat(-z) * nat(-z')" haftmann@25919 1661 apply (rule trans) haftmann@25919 1662 apply (rule_tac [2] nat_mult_distrib, auto) haftmann@25919 1663 done haftmann@25919 1664 haftmann@25919 1665 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)" haftmann@25919 1666 apply (cases "z=0 | w=0") haftmann@25919 1667 apply (auto simp add: abs_if nat_mult_distrib [symmetric] haftmann@25919 1668 nat_mult_distrib_neg [symmetric] mult_less_0_iff) haftmann@25919 1669 done haftmann@25919 1670 haftmann@25919 1671 haftmann@25919 1672 subsection "Induction principles for int" haftmann@25919 1673 haftmann@25919 1674 text{*Well-founded segments of the integers*} haftmann@25919 1675 haftmann@25919 1676 definition haftmann@25919 1677 int_ge_less_than :: "int => (int * int) set" haftmann@25919 1678 where haftmann@25919 1679 "int_ge_less_than d = {(z',z). d \ z' & z' < z}" haftmann@25919 1680 haftmann@25919 1681 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)" haftmann@25919 1682 proof - haftmann@25919 1683 have "int_ge_less_than d \ measure (%z. nat (z-d))" haftmann@25919 1684 by (auto simp add: int_ge_less_than_def) haftmann@25919 1685 thus ?thesis haftmann@25919 1686 by (rule wf_subset [OF wf_measure]) haftmann@25919 1687 qed haftmann@25919 1688 haftmann@25919 1689 text{*This variant looks odd, but is typical of the relations suggested haftmann@25919 1690 by RankFinder.*} haftmann@25919 1691 haftmann@25919 1692 definition haftmann@25919 1693 int_ge_less_than2 :: "int => (int * int) set" haftmann@25919 1694 where haftmann@25919 1695 "int_ge_less_than2 d = {(z',z). d \ z & z' < z}" haftmann@25919 1696 haftmann@25919 1697 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)" haftmann@25919 1698 proof - haftmann@25919 1699 have "int_ge_less_than2 d \ measure (%z. nat (1+z-d))" haftmann@25919 1700 by (auto simp add: int_ge_less_than2_def) haftmann@25919 1701 thus ?thesis haftmann@25919 1702 by (rule wf_subset [OF wf_measure]) haftmann@25919 1703 qed haftmann@25919 1704 haftmann@25919 1705 abbreviation haftmann@25919 1706 int :: "nat \ int" haftmann@25919 1707 where haftmann@25919 1708 "int \ of_nat" haftmann@25919 1709 haftmann@25919 1710 (* `set:int': dummy construction *) haftmann@25919 1711 theorem int_ge_induct [case_names base step, induct set: int]: haftmann@25919 1712 fixes i :: int haftmann@25919 1713 assumes ge: "k \ i" and haftmann@25919 1714 base: "P k" and haftmann@25919 1715 step: "\i. k \ i \ P i \ P (i + 1)" haftmann@25919 1716 shows "P i" haftmann@25919 1717 proof - haftmann@25919 1718 { fix n have "\i::int. n = nat(i-k) \ k \ i \ P i" haftmann@25919 1719 proof (induct n) haftmann@25919 1720 case 0 haftmann@25919 1721 hence "i = k" by arith haftmann@25919 1722 thus "P i" using base by simp haftmann@25919 1723 next haftmann@25919 1724 case (Suc n) haftmann@25919 1725 then have "n = nat((i - 1) - k)" by arith haftmann@25919 1726 moreover haftmann@25919 1727 have ki1: "k \ i - 1" using Suc.prems by arith haftmann@25919 1728 ultimately haftmann@25919 1729 have "P(i - 1)" by(rule Suc.hyps) haftmann@25919 1730 from step[OF ki1 this] show ?case by simp haftmann@25919 1731 qed haftmann@25919 1732 } haftmann@25919 1733 with ge show ?thesis by fast haftmann@25919 1734 qed haftmann@25919 1735 haftmann@25928 1736 (* `set:int': dummy construction *) haftmann@25928 1737 theorem int_gr_induct [case_names base step, induct set: int]: haftmann@25919 1738 assumes gr: "k < (i::int)" and haftmann@25919 1739 base: "P(k+1)" and haftmann@25919 1740 step: "\i. \k < i; P i\ \ P(i+1)" haftmann@25919 1741 shows "P i" haftmann@25919 1742 apply(rule int_ge_induct[of "k + 1"]) haftmann@25919 1743 using gr apply arith haftmann@25919 1744 apply(rule base) haftmann@25919 1745 apply (rule step, simp+) haftmann@25919 1746 done haftmann@25919 1747 haftmann@25919 1748 theorem int_le_induct[consumes 1,case_names base step]: haftmann@25919 1749 assumes le: "i \ (k::int)" and haftmann@25919 1750 base: "P(k)" and haftmann@25919 1751 step: "\i. \i \ k; P i\ \ P(i - 1)" haftmann@25919 1752 shows "P i" haftmann@25919 1753 proof - haftmann@25919 1754 { fix n have "\i::int. n = nat(k-i) \ i \ k \ P i" haftmann@25919 1755 proof (induct n) haftmann@25919 1756 case 0 haftmann@25919 1757 hence "i = k" by arith haftmann@25919 1758 thus "P i" using base by simp haftmann@25919 1759 next haftmann@25919 1760 case (Suc n) haftmann@25919 1761 hence "n = nat(k - (i+1))" by arith haftmann@25919 1762 moreover haftmann@25919 1763 have ki1: "i + 1 \ k" using Suc.prems by arith haftmann@25919 1764 ultimately haftmann@25919 1765 have "P(i+1)" by(rule Suc.hyps) haftmann@25919 1766 from step[OF ki1 this] show ?case by simp haftmann@25919 1767 qed haftmann@25919 1768 } haftmann@25919 1769 with le show ?thesis by fast haftmann@25919 1770 qed haftmann@25919 1771 haftmann@25919 1772 theorem int_less_induct [consumes 1,case_names base step]: haftmann@25919 1773 assumes less: "(i::int) < k" and haftmann@25919 1774 base: "P(k - 1)" and haftmann@25919 1775 step: "\i. \i < k; P i\ \ P(i - 1)" haftmann@25919 1776 shows "P i" haftmann@25919 1777 apply(rule int_le_induct[of _ "k - 1"]) haftmann@25919 1778 using less apply arith haftmann@25919 1779 apply(rule base) haftmann@25919 1780 apply (rule step, simp+) haftmann@25919 1781 done haftmann@25919 1782 haftmann@25919 1783 subsection{*Intermediate value theorems*} haftmann@25919 1784 haftmann@25919 1785 lemma int_val_lemma: haftmann@25919 1786 "(\i 1) --> haftmann@25919 1787 f 0 \ k --> k \ f n --> (\i \ n. f i = (k::int))" huffman@30079 1788 unfolding One_nat_def haftmann@27106 1789 apply (induct n, simp) haftmann@25919 1790 apply (intro strip) haftmann@25919 1791 apply (erule impE, simp) haftmann@25919 1792 apply (erule_tac x = n in allE, simp) huffman@30079 1793 apply (case_tac "k = f (Suc n)") haftmann@27106 1794 apply force haftmann@25919 1795 apply (erule impE) haftmann@25919 1796 apply (simp add: abs_if split add: split_if_asm) haftmann@25919 1797 apply (blast intro: le_SucI) haftmann@25919 1798 done haftmann@25919 1799 haftmann@25919 1800 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)] haftmann@25919 1801 haftmann@25919 1802 lemma nat_intermed_int_val: haftmann@25919 1803 "[| \i. m \ i & i < n --> abs(f(i + 1::nat) - f i) \ 1; m < n; haftmann@25919 1804 f m \ k; k \ f n |] ==> ? i. m \ i & i \ n & f i = (k::int)" haftmann@25919 1805 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k haftmann@25919 1806 in int_val_lemma) huffman@30079 1807 unfolding One_nat_def haftmann@25919 1808 apply simp haftmann@25919 1809 apply (erule exE) haftmann@25919 1810 apply (rule_tac x = "i+m" in exI, arith) haftmann@25919 1811 done haftmann@25919 1812 haftmann@25919 1813 haftmann@25919 1814 subsection{*Products and 1, by T. M. Rasmussen*} haftmann@25919 1815 haftmann@25919 1816 lemma zabs_less_one_iff [simp]: "(\z\ < 1) = (z = (0::int))" haftmann@25919 1817 by arith haftmann@25919 1818 haftmann@25919 1819 lemma abs_zmult_eq_1: "(\m * n\ = 1) ==> \m\ = (1::int)" haftmann@25919 1820 apply (cases "\n\=1") haftmann@25919 1821 apply (simp add: abs_mult) haftmann@25919 1822 apply (rule ccontr) haftmann@25919 1823 apply (auto simp add: linorder_neq_iff abs_mult) haftmann@25919 1824 apply (subgoal_tac "2 \ \m\ & 2 \ \n\") haftmann@25919 1825 prefer 2 apply arith haftmann@25919 1826 apply (subgoal_tac "2*2 \ \m\ * \n\", simp) haftmann@25919 1827 apply (rule mult_mono, auto) haftmann@25919 1828 done haftmann@25919 1829 haftmann@25919 1830 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1" haftmann@25919 1831 by (insert abs_zmult_eq_1 [of m n], arith) haftmann@25919 1832 haftmann@25919 1833 lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)" haftmann@25919 1834 apply (auto dest: pos_zmult_eq_1_iff_lemma) haftmann@25919 1835 apply (simp add: mult_commute [of m]) haftmann@25919 1836 apply (frule pos_zmult_eq_1_iff_lemma, auto) haftmann@25919 1837 done haftmann@25919 1838 haftmann@25919 1839 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))" haftmann@25919 1840 apply (rule iffI) haftmann@25919 1841 apply (frule pos_zmult_eq_1_iff_lemma) haftmann@25919 1842 apply (simp add: mult_commute [of m]) haftmann@25919 1843 apply (frule pos_zmult_eq_1_iff_lemma, auto) haftmann@25919 1844 done haftmann@25919 1845 haftmann@25919 1846 (* Could be simplified but Presburger only becomes available too late *) haftmann@25919 1847 lemma infinite_UNIV_int: "~finite(UNIV::int set)" haftmann@25919 1848 proof haftmann@25919 1849 assume "finite(UNIV::int set)" haftmann@25919 1850 moreover have "~(EX i::int. 2*i = 1)" haftmann@25919 1851 by (auto simp: pos_zmult_eq_1_iff) haftmann@25919 1852 ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"] haftmann@25919 1853 by (simp add:inj_on_def surj_def) (blast intro:sym) haftmann@25919 1854 qed haftmann@25919 1855 haftmann@25919 1856 haftmann@25961 1857 subsection{*Integer Powers*} haftmann@25961 1858 haftmann@25961 1859 instantiation int :: recpower haftmann@25961 1860 begin haftmann@25961 1861 haftmann@25961 1862 primrec power_int where haftmann@25961 1863 "p ^ 0 = (1\int)" haftmann@25961 1864 | "p ^ (Suc n) = (p\int) * (p ^ n)" haftmann@25961 1865 haftmann@25961 1866 instance proof haftmann@25961 1867 fix z :: int haftmann@25961 1868 fix n :: nat haftmann@25961 1869 show "z ^ 0 = 1" by simp haftmann@25961 1870 show "z ^ Suc n = z * (z ^ n)" by simp haftmann@25961 1871 qed haftmann@25961 1872 haftmann@25961 1873 end haftmann@25961 1874 haftmann@25961 1875 lemma zpower_zadd_distrib: "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)" haftmann@25961 1876 by (rule Power.power_add) haftmann@25961 1877 haftmann@25961 1878 lemma zpower_zpower: "(x ^ y) ^ z = (x ^ (y * z)::int)" haftmann@25961 1879 by (rule Power.power_mult [symmetric]) haftmann@25961 1880 haftmann@25961 1881 lemma zero_less_zpower_abs_iff [simp]: haftmann@25961 1882 "(0 < abs x ^ n) \ (x \ (0::int) | n = 0)" haftmann@25961 1883 by (induct n) (auto simp add: zero_less_mult_iff) haftmann@25961 1884 haftmann@25961 1885 lemma zero_le_zpower_abs [simp]: "(0::int) \ abs x ^ n" haftmann@25961 1886 by (induct n) (auto simp add: zero_le_mult_iff) haftmann@25961 1887 haftmann@25961 1888 lemma of_int_power: haftmann@25961 1889 "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})" haftmann@25961 1890 by (induct n) (simp_all add: power_Suc) haftmann@25961 1891 haftmann@25961 1892 lemma int_power: "int (m^n) = (int m) ^ n" haftmann@25961 1893 by (rule of_nat_power) haftmann@25961 1894 haftmann@25961 1895 lemmas zpower_int = int_power [symmetric] haftmann@25961 1896 haftmann@25919 1897 subsection {* Configuration of the code generator *} haftmann@25919 1898 haftmann@26507 1899 code_datatype Pls Min Bit0 Bit1 "number_of \ int \ int" haftmann@26507 1900 haftmann@28562 1901 lemmas pred_succ_numeral_code [code] = haftmann@26507 1902 pred_bin_simps succ_bin_simps haftmann@26507 1903 haftmann@28562 1904 lemmas plus_numeral_code [code] = haftmann@26507 1905 add_bin_simps haftmann@26507 1906 arith_extra_simps(1) [where 'a = int] haftmann@26507 1907 haftmann@28562 1908 lemmas minus_numeral_code [code] = haftmann@26507 1909 minus_bin_simps haftmann@26507 1910 arith_extra_simps(2) [where 'a = int] haftmann@26507 1911 arith_extra_simps(5) [where 'a = int] haftmann@26507 1912 haftmann@28562 1913 lemmas times_numeral_code [code] = haftmann@26507 1914 mult_bin_simps haftmann@26507 1915 arith_extra_simps(4) [where 'a = int] haftmann@26507 1916 haftmann@26507 1917 instantiation int :: eq haftmann@26507 1918 begin haftmann@26507 1919 haftmann@28562 1920 definition [code del]: "eq_class.eq k l \ k - l = (0\int)" haftmann@26507 1921 haftmann@26507 1922 instance by default (simp add: eq_int_def) haftmann@26507 1923 haftmann@26507 1924 end haftmann@26507 1925 haftmann@28562 1926 lemma eq_number_of_int_code [code]: haftmann@26732 1927 "eq_class.eq (number_of k \ int) (number_of l) \ eq_class.eq k l" haftmann@26507 1928 unfolding eq_int_def number_of_is_id .. haftmann@26507 1929 haftmann@28562 1930 lemma eq_int_code [code]: haftmann@26732 1931 "eq_class.eq Int.Pls Int.Pls \ True" haftmann@26732 1932 "eq_class.eq Int.Pls Int.Min \ False" haftmann@26732 1933 "eq_class.eq Int.Pls (Int.Bit0 k2) \ eq_class.eq Int.Pls k2" haftmann@26732 1934 "eq_class.eq Int.Pls (Int.Bit1 k2) \ False" haftmann@26732 1935 "eq_class.eq Int.Min Int.Pls \ False" haftmann@26732 1936 "eq_class.eq Int.Min Int.Min \ True" haftmann@26732 1937 "eq_class.eq Int.Min (Int.Bit0 k2) \ False" haftmann@26732 1938 "eq_class.eq Int.Min (Int.Bit1 k2) \ eq_class.eq Int.Min k2" huffman@28958 1939 "eq_class.eq (Int.Bit0 k1) Int.Pls \ eq_class.eq k1 Int.Pls" haftmann@26732 1940 "eq_class.eq (Int.Bit1 k1) Int.Pls \ False" haftmann@26732 1941 "eq_class.eq (Int.Bit0 k1) Int.Min \ False" huffman@28958 1942 "eq_class.eq (Int.Bit1 k1) Int.Min \ eq_class.eq k1 Int.Min" haftmann@26732 1943 "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \ eq_class.eq k1 k2" haftmann@26732 1944 "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \ False" haftmann@26732 1945 "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \ False" haftmann@26732 1946 "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \ eq_class.eq k1 k2" huffman@28958 1947 unfolding eq_equals by simp_all haftmann@25919 1948 haftmann@28351 1949 lemma eq_int_refl [code nbe]: haftmann@28351 1950 "eq_class.eq (k::int) k \ True" haftmann@28351 1951 by (rule HOL.eq_refl) haftmann@28351 1952 haftmann@28562 1953 lemma less_eq_number_of_int_code [code]: haftmann@26507 1954 "(number_of k \ int) \ number_of l \ k \ l" haftmann@26507 1955 unfolding number_of_is_id .. haftmann@26507 1956 haftmann@28562 1957 lemma less_eq_int_code [code]: haftmann@26507 1958 "Int.Pls \ Int.Pls \ True" haftmann@26507 1959 "Int.Pls \ Int.Min \ False" haftmann@26507 1960 "Int.Pls \ Int.Bit0 k \ Int.Pls \ k" haftmann@26507 1961 "Int.Pls \ Int.Bit1 k \ Int.Pls \ k" haftmann@26507 1962 "Int.Min \ Int.Pls \ True" haftmann@26507 1963 "Int.Min \ Int.Min \ True" haftmann@26507 1964 "Int.Min \ Int.Bit0 k \ Int.Min < k" haftmann@26507 1965 "Int.Min \ Int.Bit1 k \ Int.Min \ k" haftmann@26507 1966 "Int.Bit0 k \ Int.Pls \ k \ Int.Pls" haftmann@26507 1967 "Int.Bit1 k \ Int.Pls \ k < Int.Pls" haftmann@26507 1968 "Int.Bit0 k \ Int.Min \ k \ Int.Min" haftmann@26507 1969 "Int.Bit1 k \ Int.Min \ k \ Int.Min" haftmann@26507 1970 "Int.Bit0 k1 \ Int.Bit0 k2 \ k1 \ k2" haftmann@26507 1971 "Int.Bit0 k1 \ Int.Bit1 k2 \ k1 \ k2" haftmann@26507 1972 "Int.Bit1 k1 \ Int.Bit0 k2 \ k1 < k2" haftmann@26507 1973 "Int.Bit1 k1 \ Int.Bit1 k2 \ k1 \ k2" huffman@28958 1974 by simp_all haftmann@26507 1975 haftmann@28562 1976 lemma less_number_of_int_code [code]: haftmann@26507 1977 "(number_of k \ int) < number_of l \ k < l" haftmann@26507 1978 unfolding number_of_is_id .. haftmann@26507 1979 haftmann@28562 1980 lemma less_int_code [code]: haftmann@26507 1981 "Int.Pls < Int.Pls \ False" haftmann@26507 1982 "Int.Pls < Int.Min \ False" haftmann@26507 1983 "Int.Pls < Int.Bit0 k \ Int.Pls < k" haftmann@26507 1984 "Int.Pls < Int.Bit1 k \ Int.Pls \ k" haftmann@26507 1985 "Int.Min < Int.Pls \ True" haftmann@26507 1986 "Int.Min < Int.Min \ False" haftmann@26507 1987 "Int.Min < Int.Bit0 k \ Int.Min < k" haftmann@26507 1988 "Int.Min < Int.Bit1 k \ Int.Min < k" haftmann@26507 1989 "Int.Bit0 k < Int.Pls \ k < Int.Pls" haftmann@26507 1990 "Int.Bit1 k < Int.Pls \ k < Int.Pls" haftmann@26507 1991 "Int.Bit0 k < Int.Min \ k \ Int.Min" haftmann@26507 1992 "Int.Bit1 k < Int.Min \ k < Int.Min" haftmann@26507 1993 "Int.Bit0 k1 < Int.Bit0 k2 \ k1 < k2" haftmann@26507 1994 "Int.Bit0 k1 < Int.Bit1 k2 \ k1 \ k2" haftmann@26507 1995 "Int.Bit1 k1 < Int.Bit0 k2 \ k1 < k2" haftmann@26507 1996 "Int.Bit1 k1 < Int.Bit1 k2 \ k1 < k2" huffman@28958 1997 by simp_all haftmann@25919 1998 haftmann@25919 1999 definition haftmann@25919 2000 nat_aux :: "int \ nat \ nat" where haftmann@25919 2001 "nat_aux i n = nat i + n" haftmann@25919 2002 haftmann@25919 2003 lemma [code]: haftmann@25919 2004 "nat_aux i n = (if i \ 0 then n else nat_aux (i - 1) (Suc n))" -- {* tail recursive *} haftmann@25919 2005 by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le haftmann@25919 2006 dest: zless_imp_add1_zle) haftmann@25919 2007 haftmann@25919 2008 lemma [code]: "nat i = nat_aux i 0" haftmann@25919 2009 by (simp add: nat_aux_def) haftmann@25919 2010 haftmann@28514 2011 hide (open) const nat_aux haftmann@25928 2012 haftmann@28562 2013 lemma zero_is_num_zero [code, code inline, symmetric, code post]: haftmann@25919 2014 "(0\int) = Numeral0" haftmann@25919 2015 by simp haftmann@25919 2016 haftmann@28562 2017 lemma one_is_num_one [code, code inline, symmetric, code post]: haftmann@25919 2018 "(1\int) = Numeral1" haftmann@25961 2019 by simp haftmann@25919 2020 haftmann@25919 2021 code_modulename SML haftmann@25928 2022 Int Integer haftmann@25919 2023 haftmann@25919 2024 code_modulename OCaml haftmann@25928 2025 Int Integer haftmann@25919 2026 haftmann@25919 2027 code_modulename Haskell haftmann@25928 2028 Int Integer haftmann@25919 2029 haftmann@25919 2030 types_code haftmann@25919 2031 "int" ("int") haftmann@25919 2032 attach (term_of) {* haftmann@25919 2033 val term_of_int = HOLogic.mk_number HOLogic.intT; haftmann@25919 2034 *} haftmann@25919 2035 attach (test) {* haftmann@25919 2036 fun gen_int i = haftmann@25919 2037 let val j = one_of [~1, 1] * random_range 0 i haftmann@25919 2038 in (j, fn () => term_of_int j) end; haftmann@25919 2039 *} haftmann@25919 2040 haftmann@25919 2041 setup {* haftmann@25919 2042 let haftmann@25919 2043 haftmann@25919 2044 fun strip_number_of (@{term "Int.number_of :: int => int"} \$ t) = t haftmann@25919 2045 | strip_number_of t = t; haftmann@25919 2046 haftmann@28537 2047 fun numeral_codegen thy defs dep module b t gr = haftmann@25919 2048 let val i = HOLogic.dest_numeral (strip_number_of t) haftmann@25919 2049 in haftmann@28537 2050 SOME (Codegen.str (string_of_int i), haftmann@28537 2051 snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr)) haftmann@25919 2052 end handle TERM _ => NONE; haftmann@25919 2053 haftmann@25919 2054 in haftmann@25919 2055 haftmann@25919 2056 Codegen.add_codegen "numeral_codegen" numeral_codegen haftmann@25919 2057 haftmann@25919 2058 end haftmann@25919 2059 *} haftmann@25919 2060 haftmann@25919 2061 consts_code haftmann@25919 2062 "number_of :: int \ int" ("(_)") haftmann@25919 2063 "0 :: int" ("0") haftmann@25919 2064 "1 :: int" ("1") haftmann@25919 2065 "uminus :: int => int" ("~") haftmann@25919 2066 "op + :: int => int => int" ("(_ +/ _)") haftmann@25919 2067 "op * :: int => int => int" ("(_ */ _)") haftmann@25919 2068 "op \ :: int => int => bool" ("(_ <=/ _)") haftmann@25919 2069 "op < :: int => int => bool" ("(_