1(* Title: HOL/Int.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Author: Tobias Nipkow, Florian Haftmann, TU Muenchen 4*) 5 6section \<open>The Integers as Equivalence Classes over Pairs of Natural Numbers\<close> 7 8theory Int 9 imports Equiv_Relations Power Quotient Fun_Def 10begin 11 12subsection \<open>Definition of integers as a quotient type\<close> 13 14definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 15 where "intrel = (\<lambda>(x, y) (u, v). x + v = u + y)" 16 17lemma intrel_iff [simp]: "intrel (x, y) (u, v) \<longleftrightarrow> x + v = u + y" 18 by (simp add: intrel_def) 19 20quotient_type int = "nat \<times> nat" / "intrel" 21 morphisms Rep_Integ Abs_Integ 22proof (rule equivpI) 23 show "reflp intrel" by (auto simp: reflp_def) 24 show "symp intrel" by (auto simp: symp_def) 25 show "transp intrel" by (auto simp: transp_def) 26qed 27 28lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: 29 "(\<And>x y. z = Abs_Integ (x, y) \<Longrightarrow> P) \<Longrightarrow> P" 30 by (induct z) auto 31 32 33subsection \<open>Integers form a commutative ring\<close> 34 35instantiation int :: comm_ring_1 36begin 37 38lift_definition zero_int :: "int" is "(0, 0)" . 39 40lift_definition one_int :: "int" is "(1, 0)" . 41 42lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int" 43 is "\<lambda>(x, y) (u, v). (x + u, y + v)" 44 by clarsimp 45 46lift_definition uminus_int :: "int \<Rightarrow> int" 47 is "\<lambda>(x, y). (y, x)" 48 by clarsimp 49 50lift_definition minus_int :: "int \<Rightarrow> int \<Rightarrow> int" 51 is "\<lambda>(x, y) (u, v). (x + v, y + u)" 52 by clarsimp 53 54lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int" 55 is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)" 56proof (clarsimp) 57 fix s t u v w x y z :: nat 58 assume "s + v = u + t" and "w + z = y + x" 59 then have "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) = 60 (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)" 61 by simp 62 then show "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)" 63 by (simp add: algebra_simps) 64qed 65 66instance 67 by standard (transfer; clarsimp simp: algebra_simps)+ 68 69end 70 71abbreviation int :: "nat \<Rightarrow> int" 72 where "int \<equiv> of_nat" 73 74lemma int_def: "int n = Abs_Integ (n, 0)" 75 by (induct n) (simp add: zero_int.abs_eq, simp add: one_int.abs_eq plus_int.abs_eq) 76 77lemma int_transfer [transfer_rule]: "(rel_fun (=) pcr_int) (\<lambda>n. (n, 0)) int" 78 by (simp add: rel_fun_def int.pcr_cr_eq cr_int_def int_def) 79 80lemma int_diff_cases: obtains (diff) m n where "z = int m - int n" 81 by transfer clarsimp 82 83 84subsection \<open>Integers are totally ordered\<close> 85 86instantiation int :: linorder 87begin 88 89lift_definition less_eq_int :: "int \<Rightarrow> int \<Rightarrow> bool" 90 is "\<lambda>(x, y) (u, v). x + v \<le> u + y" 91 by auto 92 93lift_definition less_int :: "int \<Rightarrow> int \<Rightarrow> bool" 94 is "\<lambda>(x, y) (u, v). x + v < u + y" 95 by auto 96 97instance 98 by standard (transfer, force)+ 99 100end 101 102instantiation int :: distrib_lattice 103begin 104 105definition "(inf :: int \<Rightarrow> int \<Rightarrow> int) = min" 106 107definition "(sup :: int \<Rightarrow> int \<Rightarrow> int) = max" 108 109instance 110 by standard (auto simp add: inf_int_def sup_int_def max_min_distrib2) 111 112end 113 114subsection \<open>Ordering properties of arithmetic operations\<close> 115 116instance int :: ordered_cancel_ab_semigroup_add 117proof 118 fix i j k :: int 119 show "i \<le> j \<Longrightarrow> k + i \<le> k + j" 120 by transfer clarsimp 121qed 122 123text \<open>Strict Monotonicity of Multiplication.\<close> 124 125text \<open>Strict, in 1st argument; proof is by induction on \<open>k > 0\<close>.\<close> 126lemma zmult_zless_mono2_lemma: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> int k * i < int k * j" 127 for i j :: int 128proof (induct k) 129 case 0 130 then show ?case by simp 131next 132 case (Suc k) 133 then show ?case 134 by (cases "k = 0") (simp_all add: distrib_right add_strict_mono) 135qed 136 137lemma zero_le_imp_eq_int: "0 \<le> k \<Longrightarrow> \<exists>n. k = int n" 138 for k :: int 139 apply transfer 140 apply clarsimp 141 apply (rule_tac x="a - b" in exI) 142 apply simp 143 done 144 145lemma zero_less_imp_eq_int: "0 < k \<Longrightarrow> \<exists>n>0. k = int n" 146 for k :: int 147 apply transfer 148 apply clarsimp 149 apply (rule_tac x="a - b" in exI) 150 apply simp 151 done 152 153lemma zmult_zless_mono2: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" 154 for i j k :: int 155 by (drule zero_less_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma) 156 157 158text \<open>The integers form an ordered integral domain.\<close> 159 160instantiation int :: linordered_idom 161begin 162 163definition zabs_def: "\<bar>i::int\<bar> = (if i < 0 then - i else i)" 164 165definition zsgn_def: "sgn (i::int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)" 166 167instance 168proof 169 fix i j k :: int 170 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" 171 by (rule zmult_zless_mono2) 172 show "\<bar>i\<bar> = (if i < 0 then -i else i)" 173 by (simp only: zabs_def) 174 show "sgn (i::int) = (if i=0 then 0 else if 0<i then 1 else - 1)" 175 by (simp only: zsgn_def) 176qed 177 178end 179 180lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + 1 \<le> z" 181 for w z :: int 182 by transfer clarsimp 183 184lemma zless_iff_Suc_zadd: "w < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))" 185 for w z :: int 186 apply transfer 187 apply auto 188 apply (rename_tac a b c d) 189 apply (rule_tac x="c+b - Suc(a+d)" in exI) 190 apply arith 191 done 192 193lemma zabs_less_one_iff [simp]: "\<bar>z\<bar> < 1 \<longleftrightarrow> z = 0" (is "?lhs \<longleftrightarrow> ?rhs") 194 for z :: int 195proof 196 assume ?rhs 197 then show ?lhs by simp 198next 199 assume ?lhs 200 with zless_imp_add1_zle [of "\<bar>z\<bar>" 1] have "\<bar>z\<bar> + 1 \<le> 1" by simp 201 then have "\<bar>z\<bar> \<le> 0" by simp 202 then show ?rhs by simp 203qed 204 205 206subsection \<open>Embedding of the Integers into any \<open>ring_1\<close>: \<open>of_int\<close>\<close> 207 208context ring_1 209begin 210 211lift_definition of_int :: "int \<Rightarrow> 'a" 212 is "\<lambda>(i, j). of_nat i - of_nat j" 213 by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq 214 of_nat_add [symmetric] simp del: of_nat_add) 215 216lemma of_int_0 [simp]: "of_int 0 = 0" 217 by transfer simp 218 219lemma of_int_1 [simp]: "of_int 1 = 1" 220 by transfer simp 221 222lemma of_int_add [simp]: "of_int (w + z) = of_int w + of_int z" 223 by transfer (clarsimp simp add: algebra_simps) 224 225lemma of_int_minus [simp]: "of_int (- z) = - (of_int z)" 226 by (transfer fixing: uminus) clarsimp 227 228lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z" 229 using of_int_add [of w "- z"] by simp 230 231lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" 232 by (transfer fixing: times) (clarsimp simp add: algebra_simps) 233 234lemma mult_of_int_commute: "of_int x * y = y * of_int x" 235 by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute) 236 237text \<open>Collapse nested embeddings.\<close> 238lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n" 239 by (induct n) auto 240 241lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k" 242 by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric]) 243 244lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k" 245 by simp 246 247lemma of_int_power [simp]: "of_int (z ^ n) = of_int z ^ n" 248 by (induct n) simp_all 249 250lemma of_int_of_bool [simp]: 251 "of_int (of_bool P) = of_bool P" 252 by auto 253 254end 255 256context ring_char_0 257begin 258 259lemma of_int_eq_iff [simp]: "of_int w = of_int z \<longleftrightarrow> w = z" 260 by transfer (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add) 261 262text \<open>Special cases where either operand is zero.\<close> 263lemma of_int_eq_0_iff [simp]: "of_int z = 0 \<longleftrightarrow> z = 0" 264 using of_int_eq_iff [of z 0] by simp 265 266lemma of_int_0_eq_iff [simp]: "0 = of_int z \<longleftrightarrow> z = 0" 267 using of_int_eq_iff [of 0 z] by simp 268 269lemma of_int_eq_1_iff [iff]: "of_int z = 1 \<longleftrightarrow> z = 1" 270 using of_int_eq_iff [of z 1] by simp 271 272lemma numeral_power_eq_of_int_cancel_iff [simp]: 273 "numeral x ^ n = of_int y \<longleftrightarrow> numeral x ^ n = y" 274 using of_int_eq_iff[of "numeral x ^ n" y, unfolded of_int_numeral of_int_power] . 275 276lemma of_int_eq_numeral_power_cancel_iff [simp]: 277 "of_int y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n" 278 using numeral_power_eq_of_int_cancel_iff [of x n y] by (metis (mono_tags)) 279 280lemma neg_numeral_power_eq_of_int_cancel_iff [simp]: 281 "(- numeral x) ^ n = of_int y \<longleftrightarrow> (- numeral x) ^ n = y" 282 using of_int_eq_iff[of "(- numeral x) ^ n" y] 283 by simp 284 285lemma of_int_eq_neg_numeral_power_cancel_iff [simp]: 286 "of_int y = (- numeral x) ^ n \<longleftrightarrow> y = (- numeral x) ^ n" 287 using neg_numeral_power_eq_of_int_cancel_iff[of x n y] by (metis (mono_tags)) 288 289lemma of_int_eq_of_int_power_cancel_iff[simp]: "(of_int b) ^ w = of_int x \<longleftrightarrow> b ^ w = x" 290 by (metis of_int_power of_int_eq_iff) 291 292lemma of_int_power_eq_of_int_cancel_iff[simp]: "of_int x = (of_int b) ^ w \<longleftrightarrow> x = b ^ w" 293 by (metis of_int_eq_of_int_power_cancel_iff) 294 295end 296 297context linordered_idom 298begin 299 300text \<open>Every \<open>linordered_idom\<close> has characteristic zero.\<close> 301subclass ring_char_0 .. 302 303lemma of_int_le_iff [simp]: "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z" 304 by (transfer fixing: less_eq) 305 (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add) 306 307lemma of_int_less_iff [simp]: "of_int w < of_int z \<longleftrightarrow> w < z" 308 by (simp add: less_le order_less_le) 309 310lemma of_int_0_le_iff [simp]: "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z" 311 using of_int_le_iff [of 0 z] by simp 312 313lemma of_int_le_0_iff [simp]: "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0" 314 using of_int_le_iff [of z 0] by simp 315 316lemma of_int_0_less_iff [simp]: "0 < of_int z \<longleftrightarrow> 0 < z" 317 using of_int_less_iff [of 0 z] by simp 318 319lemma of_int_less_0_iff [simp]: "of_int z < 0 \<longleftrightarrow> z < 0" 320 using of_int_less_iff [of z 0] by simp 321 322lemma of_int_1_le_iff [simp]: "1 \<le> of_int z \<longleftrightarrow> 1 \<le> z" 323 using of_int_le_iff [of 1 z] by simp 324 325lemma of_int_le_1_iff [simp]: "of_int z \<le> 1 \<longleftrightarrow> z \<le> 1" 326 using of_int_le_iff [of z 1] by simp 327 328lemma of_int_1_less_iff [simp]: "1 < of_int z \<longleftrightarrow> 1 < z" 329 using of_int_less_iff [of 1 z] by simp 330 331lemma of_int_less_1_iff [simp]: "of_int z < 1 \<longleftrightarrow> z < 1" 332 using of_int_less_iff [of z 1] by simp 333 334lemma of_int_pos: "z > 0 \<Longrightarrow> of_int z > 0" 335 by simp 336 337lemma of_int_nonneg: "z \<ge> 0 \<Longrightarrow> of_int z \<ge> 0" 338 by simp 339 340lemma of_int_abs [simp]: "of_int \<bar>x\<bar> = \<bar>of_int x\<bar>" 341 by (auto simp add: abs_if) 342 343lemma of_int_lessD: 344 assumes "\<bar>of_int n\<bar> < x" 345 shows "n = 0 \<or> x > 1" 346proof (cases "n = 0") 347 case True 348 then show ?thesis by simp 349next 350 case False 351 then have "\<bar>n\<bar> \<noteq> 0" by simp 352 then have "\<bar>n\<bar> > 0" by simp 353 then have "\<bar>n\<bar> \<ge> 1" 354 using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp 355 then have "\<bar>of_int n\<bar> \<ge> 1" 356 unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp 357 then have "1 < x" using assms by (rule le_less_trans) 358 then show ?thesis .. 359qed 360 361lemma of_int_leD: 362 assumes "\<bar>of_int n\<bar> \<le> x" 363 shows "n = 0 \<or> 1 \<le> x" 364proof (cases "n = 0") 365 case True 366 then show ?thesis by simp 367next 368 case False 369 then have "\<bar>n\<bar> \<noteq> 0" by simp 370 then have "\<bar>n\<bar> > 0" by simp 371 then have "\<bar>n\<bar> \<ge> 1" 372 using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp 373 then have "\<bar>of_int n\<bar> \<ge> 1" 374 unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp 375 then have "1 \<le> x" using assms by (rule order_trans) 376 then show ?thesis .. 377qed 378 379lemma numeral_power_le_of_int_cancel_iff [simp]: 380 "numeral x ^ n \<le> of_int a \<longleftrightarrow> numeral x ^ n \<le> a" 381 by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_le_iff) 382 383lemma of_int_le_numeral_power_cancel_iff [simp]: 384 "of_int a \<le> numeral x ^ n \<longleftrightarrow> a \<le> numeral x ^ n" 385 by (metis (mono_tags) local.numeral_power_eq_of_int_cancel_iff of_int_le_iff) 386 387lemma numeral_power_less_of_int_cancel_iff [simp]: 388 "numeral x ^ n < of_int a \<longleftrightarrow> numeral x ^ n < a" 389 by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_less_iff) 390 391lemma of_int_less_numeral_power_cancel_iff [simp]: 392 "of_int a < numeral x ^ n \<longleftrightarrow> a < numeral x ^ n" 393 by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_less_iff) 394 395lemma neg_numeral_power_le_of_int_cancel_iff [simp]: 396 "(- numeral x) ^ n \<le> of_int a \<longleftrightarrow> (- numeral x) ^ n \<le> a" 397 by (metis (mono_tags) of_int_le_iff of_int_neg_numeral of_int_power) 398 399lemma of_int_le_neg_numeral_power_cancel_iff [simp]: 400 "of_int a \<le> (- numeral x) ^ n \<longleftrightarrow> a \<le> (- numeral x) ^ n" 401 by (metis (mono_tags) of_int_le_iff of_int_neg_numeral of_int_power) 402 403lemma neg_numeral_power_less_of_int_cancel_iff [simp]: 404 "(- numeral x) ^ n < of_int a \<longleftrightarrow> (- numeral x) ^ n < a" 405 using of_int_less_iff[of "(- numeral x) ^ n" a] 406 by simp 407 408lemma of_int_less_neg_numeral_power_cancel_iff [simp]: 409 "of_int a < (- numeral x) ^ n \<longleftrightarrow> a < (- numeral x::int) ^ n" 410 using of_int_less_iff[of a "(- numeral x) ^ n"] 411 by simp 412 413lemma of_int_le_of_int_power_cancel_iff[simp]: "(of_int b) ^ w \<le> of_int x \<longleftrightarrow> b ^ w \<le> x" 414 by (metis (mono_tags) of_int_le_iff of_int_power) 415 416lemma of_int_power_le_of_int_cancel_iff[simp]: "of_int x \<le> (of_int b) ^ w\<longleftrightarrow> x \<le> b ^ w" 417 by (metis (mono_tags) of_int_le_iff of_int_power) 418 419lemma of_int_less_of_int_power_cancel_iff[simp]: "(of_int b) ^ w < of_int x \<longleftrightarrow> b ^ w < x" 420 by (metis (mono_tags) of_int_less_iff of_int_power) 421 422lemma of_int_power_less_of_int_cancel_iff[simp]: "of_int x < (of_int b) ^ w\<longleftrightarrow> x < b ^ w" 423 by (metis (mono_tags) of_int_less_iff of_int_power) 424 425lemma of_int_max: "of_int (max x y) = max (of_int x) (of_int y)" 426 by (auto simp: max_def) 427 428lemma of_int_min: "of_int (min x y) = min (of_int x) (of_int y)" 429 by (auto simp: min_def) 430 431end 432 433text \<open>Comparisons involving @{term of_int}.\<close> 434 435lemma of_int_eq_numeral_iff [iff]: "of_int z = (numeral n :: 'a::ring_char_0) \<longleftrightarrow> z = numeral n" 436 using of_int_eq_iff by fastforce 437 438lemma of_int_le_numeral_iff [simp]: 439 "of_int z \<le> (numeral n :: 'a::linordered_idom) \<longleftrightarrow> z \<le> numeral n" 440 using of_int_le_iff [of z "numeral n"] by simp 441 442lemma of_int_numeral_le_iff [simp]: 443 "(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z" 444 using of_int_le_iff [of "numeral n"] by simp 445 446lemma of_int_less_numeral_iff [simp]: 447 "of_int z < (numeral n :: 'a::linordered_idom) \<longleftrightarrow> z < numeral n" 448 using of_int_less_iff [of z "numeral n"] by simp 449 450lemma of_int_numeral_less_iff [simp]: 451 "(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z" 452 using of_int_less_iff [of "numeral n" z] by simp 453 454lemma of_nat_less_of_int_iff: "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x" 455 by (metis of_int_of_nat_eq of_int_less_iff) 456 457lemma of_int_eq_id [simp]: "of_int = id" 458proof 459 show "of_int z = id z" for z 460 by (cases z rule: int_diff_cases) simp 461qed 462 463instance int :: no_top 464 apply standard 465 apply (rule_tac x="x + 1" in exI) 466 apply simp 467 done 468 469instance int :: no_bot 470 apply standard 471 apply (rule_tac x="x - 1" in exI) 472 apply simp 473 done 474 475 476subsection \<open>Magnitude of an Integer, as a Natural Number: \<open>nat\<close>\<close> 477 478lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y" 479 by auto 480 481lemma nat_int [simp]: "nat (int n) = n" 482 by transfer simp 483 484lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)" 485 by transfer clarsimp 486 487lemma nat_0_le: "0 \<le> z \<Longrightarrow> int (nat z) = z" 488 by simp 489 490lemma nat_le_0 [simp]: "z \<le> 0 \<Longrightarrow> nat z = 0" 491 by transfer clarsimp 492 493lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> nat w \<le> nat z \<longleftrightarrow> w \<le> z" 494 by transfer (clarsimp, arith) 495 496text \<open>An alternative condition is @{term "0 \<le> w"}.\<close> 497lemma nat_mono_iff: "0 < z \<Longrightarrow> nat w < nat z \<longleftrightarrow> w < z" 498 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 499 500lemma nat_less_eq_zless: "0 \<le> w \<Longrightarrow> nat w < nat z \<longleftrightarrow> w < z" 501 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 502 503lemma zless_nat_conj [simp]: "nat w < nat z \<longleftrightarrow> 0 < z \<and> w < z" 504 by transfer (clarsimp, arith) 505 506lemma nonneg_int_cases: 507 assumes "0 \<le> k" 508 obtains n where "k = int n" 509proof - 510 from assms have "k = int (nat k)" 511 by simp 512 then show thesis 513 by (rule that) 514qed 515 516lemma pos_int_cases: 517 assumes "0 < k" 518 obtains n where "k = int n" and "n > 0" 519proof - 520 from assms have "0 \<le> k" 521 by simp 522 then obtain n where "k = int n" 523 by (rule nonneg_int_cases) 524 moreover have "n > 0" 525 using \<open>k = int n\<close> assms by simp 526 ultimately show thesis 527 by (rule that) 528qed 529 530lemma nonpos_int_cases: 531 assumes "k \<le> 0" 532 obtains n where "k = - int n" 533proof - 534 from assms have "- k \<ge> 0" 535 by simp 536 then obtain n where "- k = int n" 537 by (rule nonneg_int_cases) 538 then have "k = - int n" 539 by simp 540 then show thesis 541 by (rule that) 542qed 543 544lemma neg_int_cases: 545 assumes "k < 0" 546 obtains n where "k = - int n" and "n > 0" 547proof - 548 from assms have "- k > 0" 549 by simp 550 then obtain n where "- k = int n" and "- k > 0" 551 by (blast elim: pos_int_cases) 552 then have "k = - int n" and "n > 0" 553 by simp_all 554 then show thesis 555 by (rule that) 556qed 557 558lemma nat_eq_iff: "nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)" 559 by transfer (clarsimp simp add: le_imp_diff_is_add) 560 561lemma nat_eq_iff2: "m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)" 562 using nat_eq_iff [of w m] by auto 563 564lemma nat_0 [simp]: "nat 0 = 0" 565 by (simp add: nat_eq_iff) 566 567lemma nat_1 [simp]: "nat 1 = Suc 0" 568 by (simp add: nat_eq_iff) 569 570lemma nat_numeral [simp]: "nat (numeral k) = numeral k" 571 by (simp add: nat_eq_iff) 572 573lemma nat_neg_numeral [simp]: "nat (- numeral k) = 0" 574 by simp 575 576lemma nat_2: "nat 2 = Suc (Suc 0)" 577 by simp 578 579lemma nat_less_iff: "0 \<le> w \<Longrightarrow> nat w < m \<longleftrightarrow> w < of_nat m" 580 by transfer (clarsimp, arith) 581 582lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n" 583 by transfer (clarsimp simp add: le_diff_conv) 584 585lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y" 586 by transfer auto 587 588lemma nat_0_iff[simp]: "nat i = 0 \<longleftrightarrow> i \<le> 0" 589 for i :: int 590 by transfer clarsimp 591 592lemma int_eq_iff: "of_nat m = z \<longleftrightarrow> m = nat z \<and> 0 \<le> z" 593 by (auto simp add: nat_eq_iff2) 594 595lemma zero_less_nat_eq [simp]: "0 < nat z \<longleftrightarrow> 0 < z" 596 using zless_nat_conj [of 0] by auto 597 598lemma nat_add_distrib: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat (z + z') = nat z + nat z'" 599 by transfer clarsimp 600 601lemma nat_diff_distrib': "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x - y) = nat x - nat y" 602 by transfer clarsimp 603 604lemma nat_diff_distrib: "0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z - z') = nat z - nat z'" 605 by (rule nat_diff_distrib') auto 606 607lemma nat_zminus_int [simp]: "nat (- int n) = 0" 608 by transfer simp 609 610lemma le_nat_iff: "k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k" 611 by transfer auto 612 613lemma zless_nat_eq_int_zless: "m < nat z \<longleftrightarrow> int m < z" 614 by transfer (clarsimp simp add: less_diff_conv) 615 616lemma (in ring_1) of_nat_nat [simp]: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z" 617 by transfer (clarsimp simp add: of_nat_diff) 618 619lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')" 620 by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral) 621 622lemma nat_abs_triangle_ineq: 623 "nat \<bar>k + l\<bar> \<le> nat \<bar>k\<bar> + nat \<bar>l\<bar>" 624 by (simp add: nat_add_distrib [symmetric] nat_le_eq_zle abs_triangle_ineq) 625 626lemma nat_of_bool [simp]: 627 "nat (of_bool P) = of_bool P" 628 by auto 629 630lemma split_nat [arith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))" 631 (is "?P = (?L \<and> ?R)") 632 for i :: int 633proof (cases "i < 0") 634 case True 635 then show ?thesis 636 by auto 637next 638 case False 639 have "?P = ?L" 640 proof 641 assume ?P 642 then show ?L using False by auto 643 next 644 assume ?L 645 moreover from False have "int (nat i) = i" 646 by (simp add: not_less) 647 ultimately show ?P 648 by simp 649 qed 650 with False show ?thesis by simp 651qed 652 653lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))" 654 by (auto split: split_nat) 655 656lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))" 657proof 658 assume "\<exists>x. P x" 659 then obtain x where "P x" .. 660 then have "int x \<ge> 0 \<and> P (nat (int x))" by simp 661 then show "\<exists>x\<ge>0. P (nat x)" .. 662next 663 assume "\<exists>x\<ge>0. P (nat x)" 664 then show "\<exists>x. P x" by auto 665qed 666 667 668text \<open>For termination proofs:\<close> 669lemma measure_function_int[measure_function]: "is_measure (nat \<circ> abs)" .. 670 671 672subsection \<open>Lemmas about the Function @{term of_nat} and Orderings\<close> 673 674lemma negative_zless_0: "- (int (Suc n)) < (0 :: int)" 675 by (simp add: order_less_le del: of_nat_Suc) 676 677lemma negative_zless [iff]: "- (int (Suc n)) < int m" 678 by (rule negative_zless_0 [THEN order_less_le_trans], simp) 679 680lemma negative_zle_0: "- int n \<le> 0" 681 by (simp add: minus_le_iff) 682 683lemma negative_zle [iff]: "- int n \<le> int m" 684 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff]) 685 686lemma not_zle_0_negative [simp]: "\<not> 0 \<le> - int (Suc n)" 687 by (subst le_minus_iff) (simp del: of_nat_Suc) 688 689lemma int_zle_neg: "int n \<le> - int m \<longleftrightarrow> n = 0 \<and> m = 0" 690 by transfer simp 691 692lemma not_int_zless_negative [simp]: "\<not> int n < - int m" 693 by (simp add: linorder_not_less) 694 695lemma negative_eq_positive [simp]: "- int n = of_nat m \<longleftrightarrow> n = 0 \<and> m = 0" 696 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg) 697 698lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)" 699 (is "?lhs \<longleftrightarrow> ?rhs") 700proof 701 assume ?rhs 702 then show ?lhs by auto 703next 704 assume ?lhs 705 then have "0 \<le> z - w" by simp 706 then obtain n where "z - w = int n" 707 using zero_le_imp_eq_int [of "z - w"] by blast 708 then have "z = w + int n" by simp 709 then show ?rhs .. 710qed 711 712lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z" 713 by simp 714 715text \<open> 716 This version is proved for all ordered rings, not just integers! 717 It is proved here because attribute \<open>arith_split\<close> is not available 718 in theory \<open>Rings\<close>. 719 But is it really better than just rewriting with \<open>abs_if\<close>? 720\<close> 721lemma abs_split [arith_split, no_atp]: "P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))" 722 for a :: "'a::linordered_idom" 723 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) 724 725lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))" 726 apply transfer 727 apply clarsimp 728 apply (rule_tac x="b - Suc a" in exI) 729 apply arith 730 done 731 732 733subsection \<open>Cases and induction\<close> 734 735text \<open> 736 Now we replace the case analysis rule by a more conventional one: 737 whether an integer is negative or not. 738\<close> 739 740text \<open>This version is symmetric in the two subgoals.\<close> 741lemma int_cases2 [case_names nonneg nonpos, cases type: int]: 742 "(\<And>n. z = int n \<Longrightarrow> P) \<Longrightarrow> (\<And>n. z = - (int n) \<Longrightarrow> P) \<Longrightarrow> P" 743 by (cases "z < 0") (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym]) 744 745text \<open>This is the default, with a negative case.\<close> 746lemma int_cases [case_names nonneg neg, cases type: int]: 747 "(\<And>n. z = int n \<Longrightarrow> P) \<Longrightarrow> (\<And>n. z = - (int (Suc n)) \<Longrightarrow> P) \<Longrightarrow> P" 748 apply (cases "z < 0") 749 apply (blast dest!: negD) 750 apply (simp add: linorder_not_less del: of_nat_Suc) 751 apply auto 752 apply (blast dest: nat_0_le [THEN sym]) 753 done 754 755lemma int_cases3 [case_names zero pos neg]: 756 fixes k :: int 757 assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P" 758 and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P" 759 shows "P" 760proof (cases k "0::int" rule: linorder_cases) 761 case equal 762 with assms(1) show P by simp 763next 764 case greater 765 then have *: "nat k > 0" by simp 766 moreover from * have "k = int (nat k)" by auto 767 ultimately show P using assms(2) by blast 768next 769 case less 770 then have *: "nat (- k) > 0" by simp 771 moreover from * have "k = - int (nat (- k))" by auto 772 ultimately show P using assms(3) by blast 773qed 774 775lemma int_of_nat_induct [case_names nonneg neg, induct type: int]: 776 "(\<And>n. P (int n)) \<Longrightarrow> (\<And>n. P (- (int (Suc n)))) \<Longrightarrow> P z" 777 by (cases z) auto 778 779lemma sgn_mult_dvd_iff [simp]: 780 "sgn r * l dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int 781 by (cases r rule: int_cases3) auto 782 783lemma mult_sgn_dvd_iff [simp]: 784 "l * sgn r dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int 785 using sgn_mult_dvd_iff [of r l k] by (simp add: ac_simps) 786 787lemma dvd_sgn_mult_iff [simp]: 788 "l dvd sgn r * k \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int 789 by (cases r rule: int_cases3) simp_all 790 791lemma dvd_mult_sgn_iff [simp]: 792 "l dvd k * sgn r \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int 793 using dvd_sgn_mult_iff [of l r k] by (simp add: ac_simps) 794 795lemma int_sgnE: 796 fixes k :: int 797 obtains n and l where "k = sgn l * int n" 798proof - 799 have "k = sgn k * int (nat \<bar>k\<bar>)" 800 by (simp add: sgn_mult_abs) 801 then show ?thesis .. 802qed 803 804 805subsubsection \<open>Binary comparisons\<close> 806 807text \<open>Preliminaries\<close> 808 809lemma le_imp_0_less: 810 fixes z :: int 811 assumes le: "0 \<le> z" 812 shows "0 < 1 + z" 813proof - 814 have "0 \<le> z" by fact 815 also have "\<dots> < z + 1" by (rule less_add_one) 816 also have "\<dots> = 1 + z" by (simp add: ac_simps) 817 finally show "0 < 1 + z" . 818qed 819 820lemma odd_less_0_iff: "1 + z + z < 0 \<longleftrightarrow> z < 0" 821 for z :: int 822proof (cases z) 823 case (nonneg n) 824 then show ?thesis 825 by (simp add: linorder_not_less add.assoc add_increasing le_imp_0_less [THEN order_less_imp_le]) 826next 827 case (neg n) 828 then show ?thesis 829 by (simp del: of_nat_Suc of_nat_add of_nat_1 830 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) 831qed 832 833 834subsubsection \<open>Comparisons, for Ordered Rings\<close> 835 836lemma odd_nonzero: "1 + z + z \<noteq> 0" 837 for z :: int 838proof (cases z) 839 case (nonneg n) 840 have le: "0 \<le> z + z" 841 by (simp add: nonneg add_increasing) 842 then show ?thesis 843 using le_imp_0_less [OF le] by (auto simp: ac_simps) 844next 845 case (neg n) 846 show ?thesis 847 proof 848 assume eq: "1 + z + z = 0" 849 have "0 < 1 + (int n + int n)" 850 by (simp add: le_imp_0_less add_increasing) 851 also have "\<dots> = - (1 + z + z)" 852 by (simp add: neg add.assoc [symmetric]) 853 also have "\<dots> = 0" by (simp add: eq) 854 finally have "0<0" .. 855 then show False by blast 856 qed 857qed 858 859 860subsection \<open>The Set of Integers\<close> 861 862context ring_1 863begin 864 865definition Ints :: "'a set" ("\<int>") 866 where "\<int> = range of_int" 867 868lemma Ints_of_int [simp]: "of_int z \<in> \<int>" 869 by (simp add: Ints_def) 870 871lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>" 872 using Ints_of_int [of "of_nat n"] by simp 873 874lemma Ints_0 [simp]: "0 \<in> \<int>" 875 using Ints_of_int [of "0"] by simp 876 877lemma Ints_1 [simp]: "1 \<in> \<int>" 878 using Ints_of_int [of "1"] by simp 879 880lemma Ints_numeral [simp]: "numeral n \<in> \<int>" 881 by (subst of_nat_numeral [symmetric], rule Ints_of_nat) 882 883lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>" 884 apply (auto simp add: Ints_def) 885 apply (rule range_eqI) 886 apply (rule of_int_add [symmetric]) 887 done 888 889lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>" 890 apply (auto simp add: Ints_def) 891 apply (rule range_eqI) 892 apply (rule of_int_minus [symmetric]) 893 done 894 895lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>" 896 apply (auto simp add: Ints_def) 897 apply (rule range_eqI) 898 apply (rule of_int_diff [symmetric]) 899 done 900 901lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>" 902 apply (auto simp add: Ints_def) 903 apply (rule range_eqI) 904 apply (rule of_int_mult [symmetric]) 905 done 906 907lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>" 908 by (induct n) simp_all 909 910lemma Ints_cases [cases set: Ints]: 911 assumes "q \<in> \<int>" 912 obtains (of_int) z where "q = of_int z" 913 unfolding Ints_def 914proof - 915 from \<open>q \<in> \<int>\<close> have "q \<in> range of_int" unfolding Ints_def . 916 then obtain z where "q = of_int z" .. 917 then show thesis .. 918qed 919 920lemma Ints_induct [case_names of_int, induct set: Ints]: 921 "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q" 922 by (rule Ints_cases) auto 923 924lemma Nats_subset_Ints: "\<nat> \<subseteq> \<int>" 925 unfolding Nats_def Ints_def 926 by (rule subsetI, elim imageE, hypsubst, subst of_int_of_nat_eq[symmetric], rule imageI) simp_all 927 928lemma Nats_altdef1: "\<nat> = {of_int n |n. n \<ge> 0}" 929proof (intro subsetI equalityI) 930 fix x :: 'a 931 assume "x \<in> {of_int n |n. n \<ge> 0}" 932 then obtain n where "x = of_int n" "n \<ge> 0" 933 by (auto elim!: Ints_cases) 934 then have "x = of_nat (nat n)" 935 by (subst of_nat_nat) simp_all 936 then show "x \<in> \<nat>" 937 by simp 938next 939 fix x :: 'a 940 assume "x \<in> \<nat>" 941 then obtain n where "x = of_nat n" 942 by (auto elim!: Nats_cases) 943 then have "x = of_int (int n)" by simp 944 also have "int n \<ge> 0" by simp 945 then have "of_int (int n) \<in> {of_int n |n. n \<ge> 0}" by blast 946 finally show "x \<in> {of_int n |n. n \<ge> 0}" . 947qed 948 949end 950 951lemma (in linordered_idom) Ints_abs [simp]: 952 shows "a \<in> \<int> \<Longrightarrow> abs a \<in> \<int>" 953 by (auto simp: abs_if) 954 955lemma (in linordered_idom) Nats_altdef2: "\<nat> = {n \<in> \<int>. n \<ge> 0}" 956proof (intro subsetI equalityI) 957 fix x :: 'a 958 assume "x \<in> {n \<in> \<int>. n \<ge> 0}" 959 then obtain n where "x = of_int n" "n \<ge> 0" 960 by (auto elim!: Ints_cases) 961 then have "x = of_nat (nat n)" 962 by (subst of_nat_nat) simp_all 963 then show "x \<in> \<nat>" 964 by simp 965qed (auto elim!: Nats_cases) 966 967lemma (in idom_divide) of_int_divide_in_Ints: 968 "of_int a div of_int b \<in> \<int>" if "b dvd a" 969proof - 970 from that obtain c where "a = b * c" .. 971 then show ?thesis 972 by (cases "of_int b = 0") simp_all 973qed 974 975text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close> 976 977lemma Ints_double_eq_0_iff: 978 fixes a :: "'a::ring_char_0" 979 assumes in_Ints: "a \<in> \<int>" 980 shows "a + a = 0 \<longleftrightarrow> a = 0" 981 (is "?lhs \<longleftrightarrow> ?rhs") 982proof - 983 from in_Ints have "a \<in> range of_int" 984 unfolding Ints_def [symmetric] . 985 then obtain z where a: "a = of_int z" .. 986 show ?thesis 987 proof 988 assume ?rhs 989 then show ?lhs by simp 990 next 991 assume ?lhs 992 with a have "of_int (z + z) = (of_int 0 :: 'a)" by simp 993 then have "z + z = 0" by (simp only: of_int_eq_iff) 994 then have "z = 0" by (simp only: double_zero) 995 with a show ?rhs by simp 996 qed 997qed 998 999lemma Ints_odd_nonzero: 1000 fixes a :: "'a::ring_char_0" 1001 assumes in_Ints: "a \<in> \<int>" 1002 shows "1 + a + a \<noteq> 0" 1003proof - 1004 from in_Ints have "a \<in> range of_int" 1005 unfolding Ints_def [symmetric] . 1006 then obtain z where a: "a = of_int z" .. 1007 show ?thesis 1008 proof 1009 assume "1 + a + a = 0" 1010 with a have "of_int (1 + z + z) = (of_int 0 :: 'a)" by simp 1011 then have "1 + z + z = 0" by (simp only: of_int_eq_iff) 1012 with odd_nonzero show False by blast 1013 qed 1014qed 1015 1016lemma Nats_numeral [simp]: "numeral w \<in> \<nat>" 1017 using of_nat_in_Nats [of "numeral w"] by simp 1018 1019lemma Ints_odd_less_0: 1020 fixes a :: "'a::linordered_idom" 1021 assumes in_Ints: "a \<in> \<int>" 1022 shows "1 + a + a < 0 \<longleftrightarrow> a < 0" 1023proof - 1024 from in_Ints have "a \<in> range of_int" 1025 unfolding Ints_def [symmetric] . 1026 then obtain z where a: "a = of_int z" .. 1027 with a have "1 + a + a < 0 \<longleftrightarrow> of_int (1 + z + z) < (of_int 0 :: 'a)" 1028 by simp 1029 also have "\<dots> \<longleftrightarrow> z < 0" 1030 by (simp only: of_int_less_iff odd_less_0_iff) 1031 also have "\<dots> \<longleftrightarrow> a < 0" 1032 by (simp add: a) 1033 finally show ?thesis . 1034qed 1035 1036 1037subsection \<open>@{term sum} and @{term prod}\<close> 1038 1039lemma of_nat_sum [simp]: "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat(f x))" 1040 by (induct A rule: infinite_finite_induct) auto 1041 1042lemma of_int_sum [simp]: "of_int (sum f A) = (\<Sum>x\<in>A. of_int(f x))" 1043 by (induct A rule: infinite_finite_induct) auto 1044 1045lemma of_nat_prod [simp]: "of_nat (prod f A) = (\<Prod>x\<in>A. of_nat(f x))" 1046 by (induct A rule: infinite_finite_induct) auto 1047 1048lemma of_int_prod [simp]: "of_int (prod f A) = (\<Prod>x\<in>A. of_int(f x))" 1049 by (induct A rule: infinite_finite_induct) auto 1050 1051 1052subsection \<open>Setting up simplification procedures\<close> 1053 1054lemmas of_int_simps = 1055 of_int_0 of_int_1 of_int_add of_int_mult 1056 1057ML_file "Tools/int_arith.ML" 1058declaration \<open>K Int_Arith.setup\<close> 1059 1060simproc_setup fast_arith 1061 ("(m::'a::linordered_idom) < n" | 1062 "(m::'a::linordered_idom) \<le> n" | 1063 "(m::'a::linordered_idom) = n") = 1064 \<open>K Lin_Arith.simproc\<close> 1065 1066 1067subsection\<open>More Inequality Reasoning\<close> 1068 1069lemma zless_add1_eq: "w < z + 1 \<longleftrightarrow> w < z \<or> w = z" 1070 for w z :: int 1071 by arith 1072 1073lemma add1_zle_eq: "w + 1 \<le> z \<longleftrightarrow> w < z" 1074 for w z :: int 1075 by arith 1076 1077lemma zle_diff1_eq [simp]: "w \<le> z - 1 \<longleftrightarrow> w < z" 1078 for w z :: int 1079 by arith 1080 1081lemma zle_add1_eq_le [simp]: "w < z + 1 \<longleftrightarrow> w \<le> z" 1082 for w z :: int 1083 by arith 1084 1085lemma int_one_le_iff_zero_less: "1 \<le> z \<longleftrightarrow> 0 < z" 1086 for z :: int 1087 by arith 1088 1089lemma Ints_nonzero_abs_ge1: 1090 fixes x:: "'a :: linordered_idom" 1091 assumes "x \<in> Ints" "x \<noteq> 0" 1092 shows "1 \<le> abs x" 1093proof (rule Ints_cases [OF \<open>x \<in> Ints\<close>]) 1094 fix z::int 1095 assume "x = of_int z" 1096 with \<open>x \<noteq> 0\<close> 1097 show "1 \<le> \<bar>x\<bar>" 1098 apply (auto simp add: abs_if) 1099 by (metis diff_0 of_int_1 of_int_le_iff of_int_minus zle_diff1_eq) 1100qed 1101 1102lemma Ints_nonzero_abs_less1: 1103 fixes x:: "'a :: linordered_idom" 1104 shows "\<lbrakk>x \<in> Ints; abs x < 1\<rbrakk> \<Longrightarrow> x = 0" 1105 using Ints_nonzero_abs_ge1 [of x] by auto 1106 1107 1108subsection \<open>The functions @{term nat} and @{term int}\<close> 1109 1110text \<open>Simplify the term @{term "w + - z"}.\<close> 1111 1112lemma one_less_nat_eq [simp]: "Suc 0 < nat z \<longleftrightarrow> 1 < z" 1113 using zless_nat_conj [of 1 z] by auto 1114 1115lemma int_eq_iff_numeral [simp]: 1116 "int m = numeral v \<longleftrightarrow> m = numeral v" 1117 by (simp add: int_eq_iff) 1118 1119lemma nat_abs_int_diff: 1120 "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)" 1121 by auto 1122 1123lemma nat_int_add: "nat (int a + int b) = a + b" 1124 by auto 1125 1126context ring_1 1127begin 1128 1129lemma of_int_of_nat [nitpick_simp]: 1130 "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))" 1131proof (cases "k < 0") 1132 case True 1133 then have "0 \<le> - k" by simp 1134 then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat) 1135 with True show ?thesis by simp 1136next 1137 case False 1138 then show ?thesis by (simp add: not_less) 1139qed 1140 1141end 1142 1143lemma transfer_rule_of_int: 1144 fixes R :: "'a::ring_1 \<Rightarrow> 'b::ring_1 \<Rightarrow> bool" 1145 assumes [transfer_rule]: "R 0 0" "R 1 1" 1146 "rel_fun R (rel_fun R R) plus plus" 1147 "rel_fun R R uminus uminus" 1148 shows "rel_fun HOL.eq R of_int of_int" 1149proof - 1150 note transfer_rule_of_nat [transfer_rule] 1151 have [transfer_rule]: "rel_fun HOL.eq R of_nat of_nat" 1152 by transfer_prover 1153 show ?thesis 1154 by (unfold of_int_of_nat [abs_def]) transfer_prover 1155qed 1156 1157lemma nat_mult_distrib: 1158 fixes z z' :: int 1159 assumes "0 \<le> z" 1160 shows "nat (z * z') = nat z * nat z'" 1161proof (cases "0 \<le> z'") 1162 case False 1163 with assms have "z * z' \<le> 0" 1164 by (simp add: not_le mult_le_0_iff) 1165 then have "nat (z * z') = 0" by simp 1166 moreover from False have "nat z' = 0" by simp 1167 ultimately show ?thesis by simp 1168next 1169 case True 1170 with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff) 1171 show ?thesis 1172 by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat]) 1173 (simp only: of_nat_mult of_nat_nat [OF True] 1174 of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp) 1175qed 1176 1177lemma nat_mult_distrib_neg: "z \<le> 0 \<Longrightarrow> nat (z * z') = nat (- z) * nat (- z')" 1178 for z z' :: int 1179 apply (rule trans) 1180 apply (rule_tac [2] nat_mult_distrib) 1181 apply auto 1182 done 1183 1184lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>" 1185 by (cases "z = 0 \<or> w = 0") 1186 (auto simp add: abs_if nat_mult_distrib [symmetric] 1187 nat_mult_distrib_neg [symmetric] mult_less_0_iff) 1188 1189lemma int_in_range_abs [simp]: "int n \<in> range abs" 1190proof (rule range_eqI) 1191 show "int n = \<bar>int n\<bar>" by simp 1192qed 1193 1194lemma range_abs_Nats [simp]: "range abs = (\<nat> :: int set)" 1195proof - 1196 have "\<bar>k\<bar> \<in> \<nat>" for k :: int 1197 by (cases k) simp_all 1198 moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int 1199 using that by induct simp 1200 ultimately show ?thesis by blast 1201qed 1202 1203lemma Suc_nat_eq_nat_zadd1: "0 \<le> z \<Longrightarrow> Suc (nat z) = nat (1 + z)" 1204 for z :: int 1205 by (rule sym) (simp add: nat_eq_iff) 1206 1207lemma diff_nat_eq_if: 1208 "nat z - nat z' = 1209 (if z' < 0 then nat z 1210 else 1211 let d = z - z' 1212 in if d < 0 then 0 else nat d)" 1213 by (simp add: Let_def nat_diff_distrib [symmetric]) 1214 1215lemma nat_numeral_diff_1 [simp]: "numeral v - (1::nat) = nat (numeral v - 1)" 1216 using diff_nat_numeral [of v Num.One] by simp 1217 1218 1219subsection \<open>Induction principles for int\<close> 1220 1221text \<open>Well-founded segments of the integers.\<close> 1222 1223definition int_ge_less_than :: "int \<Rightarrow> (int \<times> int) set" 1224 where "int_ge_less_than d = {(z', z). d \<le> z' \<and> z' < z}" 1225 1226lemma wf_int_ge_less_than: "wf (int_ge_less_than d)" 1227proof - 1228 have "int_ge_less_than d \<subseteq> measure (\<lambda>z. nat (z - d))" 1229 by (auto simp add: int_ge_less_than_def) 1230 then show ?thesis 1231 by (rule wf_subset [OF wf_measure]) 1232qed 1233 1234text \<open> 1235 This variant looks odd, but is typical of the relations suggested 1236 by RankFinder.\<close> 1237 1238definition int_ge_less_than2 :: "int \<Rightarrow> (int \<times> int) set" 1239 where "int_ge_less_than2 d = {(z',z). d \<le> z \<and> z' < z}" 1240 1241lemma wf_int_ge_less_than2: "wf (int_ge_less_than2 d)" 1242proof - 1243 have "int_ge_less_than2 d \<subseteq> measure (\<lambda>z. nat (1 + z - d))" 1244 by (auto simp add: int_ge_less_than2_def) 1245 then show ?thesis 1246 by (rule wf_subset [OF wf_measure]) 1247qed 1248 1249(* `set:int': dummy construction *) 1250theorem int_ge_induct [case_names base step, induct set: int]: 1251 fixes i :: int 1252 assumes ge: "k \<le> i" 1253 and base: "P k" 1254 and step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" 1255 shows "P i" 1256proof - 1257 have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i" for n 1258 proof (induct n) 1259 case 0 1260 then have "i = k" by arith 1261 with base show "P i" by simp 1262 next 1263 case (Suc n) 1264 then have "n = nat ((i - 1) - k)" by arith 1265 moreover have k: "k \<le> i - 1" using Suc.prems by arith 1266 ultimately have "P (i - 1)" by (rule Suc.hyps) 1267 from step [OF k this] show ?case by simp 1268 qed 1269 with ge show ?thesis by fast 1270qed 1271 1272(* `set:int': dummy construction *) 1273theorem int_gr_induct [case_names base step, induct set: int]: 1274 fixes i k :: int 1275 assumes gr: "k < i" 1276 and base: "P (k + 1)" 1277 and step: "\<And>i. k < i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" 1278 shows "P i" 1279 apply (rule int_ge_induct[of "k + 1"]) 1280 using gr apply arith 1281 apply (rule base) 1282 apply (rule step) 1283 apply simp_all 1284 done 1285 1286theorem int_le_induct [consumes 1, case_names base step]: 1287 fixes i k :: int 1288 assumes le: "i \<le> k" 1289 and base: "P k" 1290 and step: "\<And>i. i \<le> k \<Longrightarrow> P i \<Longrightarrow> P (i - 1)" 1291 shows "P i" 1292proof - 1293 have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i" for n 1294 proof (induct n) 1295 case 0 1296 then have "i = k" by arith 1297 with base show "P i" by simp 1298 next 1299 case (Suc n) 1300 then have "n = nat (k - (i + 1))" by arith 1301 moreover have k: "i + 1 \<le> k" using Suc.prems by arith 1302 ultimately have "P (i + 1)" by (rule Suc.hyps) 1303 from step[OF k this] show ?case by simp 1304 qed 1305 with le show ?thesis by fast 1306qed 1307 1308theorem int_less_induct [consumes 1, case_names base step]: 1309 fixes i k :: int 1310 assumes less: "i < k" 1311 and base: "P (k - 1)" 1312 and step: "\<And>i. i < k \<Longrightarrow> P i \<Longrightarrow> P (i - 1)" 1313 shows "P i" 1314 apply (rule int_le_induct[of _ "k - 1"]) 1315 using less apply arith 1316 apply (rule base) 1317 apply (rule step) 1318 apply simp_all 1319 done 1320 1321theorem int_induct [case_names base step1 step2]: 1322 fixes k :: int 1323 assumes base: "P k" 1324 and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" 1325 and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)" 1326 shows "P i" 1327proof - 1328 have "i \<le> k \<or> i \<ge> k" by arith 1329 then show ?thesis 1330 proof 1331 assume "i \<ge> k" 1332 then show ?thesis 1333 using base by (rule int_ge_induct) (fact step1) 1334 next 1335 assume "i \<le> k" 1336 then show ?thesis 1337 using base by (rule int_le_induct) (fact step2) 1338 qed 1339qed 1340 1341 1342subsection \<open>Intermediate value theorems\<close> 1343 1344lemma nat_intermed_int_val: 1345 "\<exists>i. m \<le> i \<and> i \<le> n \<and> f i = k" 1346 if "\<forall>i. m \<le> i \<and> i < n \<longrightarrow> \<bar>f (Suc i) - f i\<bar> \<le> 1" 1347 "m \<le> n" "f m \<le> k" "k \<le> f n" 1348 for m n :: nat and k :: int 1349proof - 1350 have "(\<forall>i<n. \<bar>f (Suc i) - f i\<bar> \<le> 1) \<Longrightarrow> f 0 \<le> k \<Longrightarrow> k \<le> f n 1351 \<Longrightarrow> (\<exists>i \<le> n. f i = k)" 1352 for n :: nat and f 1353 apply (induct n) 1354 apply auto 1355 apply (erule_tac x = n in allE) 1356 apply (case_tac "k = f (Suc n)") 1357 apply (auto simp add: abs_if split: if_split_asm intro: le_SucI) 1358 done 1359 from this [of "n - m" "f \<circ> plus m"] that show ?thesis 1360 apply auto 1361 apply (rule_tac x = "m + i" in exI) 1362 apply auto 1363 done 1364qed 1365 1366lemma nat0_intermed_int_val: 1367 "\<exists>i\<le>n. f i = k" 1368 if "\<forall>i<n. \<bar>f (i + 1) - f i\<bar> \<le> 1" "f 0 \<le> k" "k \<le> f n" 1369 for n :: nat and k :: int 1370 using nat_intermed_int_val [of 0 n f k] that by auto 1371 1372 1373subsection \<open>Products and 1, by T. M. Rasmussen\<close> 1374 1375lemma abs_zmult_eq_1: 1376 fixes m n :: int 1377 assumes mn: "\<bar>m * n\<bar> = 1" 1378 shows "\<bar>m\<bar> = 1" 1379proof - 1380 from mn have 0: "m \<noteq> 0" "n \<noteq> 0" by auto 1381 have "\<not> 2 \<le> \<bar>m\<bar>" 1382 proof 1383 assume "2 \<le> \<bar>m\<bar>" 1384 then have "2 * \<bar>n\<bar> \<le> \<bar>m\<bar> * \<bar>n\<bar>" by (simp add: mult_mono 0) 1385 also have "\<dots> = \<bar>m * n\<bar>" by (simp add: abs_mult) 1386 also from mn have "\<dots> = 1" by simp 1387 finally have "2 * \<bar>n\<bar> \<le> 1" . 1388 with 0 show "False" by arith 1389 qed 1390 with 0 show ?thesis by auto 1391qed 1392 1393lemma pos_zmult_eq_1_iff_lemma: "m * n = 1 \<Longrightarrow> m = 1 \<or> m = - 1" 1394 for m n :: int 1395 using abs_zmult_eq_1 [of m n] by arith 1396 1397lemma pos_zmult_eq_1_iff: 1398 fixes m n :: int 1399 assumes "0 < m" 1400 shows "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1" 1401proof - 1402 from assms have "m * n = 1 \<Longrightarrow> m = 1" 1403 by (auto dest: pos_zmult_eq_1_iff_lemma) 1404 then show ?thesis 1405 by (auto dest: pos_zmult_eq_1_iff_lemma) 1406qed 1407 1408lemma zmult_eq_1_iff: "m * n = 1 \<longleftrightarrow> (m = 1 \<and> n = 1) \<or> (m = - 1 \<and> n = - 1)" 1409 for m n :: int 1410 apply (rule iffI) 1411 apply (frule pos_zmult_eq_1_iff_lemma) 1412 apply (simp add: mult.commute [of m]) 1413 apply (frule pos_zmult_eq_1_iff_lemma) 1414 apply auto 1415 done 1416 1417lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)" 1418proof 1419 assume "finite (UNIV::int set)" 1420 moreover have "inj (\<lambda>i::int. 2 * i)" 1421 by (rule injI) simp 1422 ultimately have "surj (\<lambda>i::int. 2 * i)" 1423 by (rule finite_UNIV_inj_surj) 1424 then obtain i :: int where "1 = 2 * i" by (rule surjE) 1425 then show False by (simp add: pos_zmult_eq_1_iff) 1426qed 1427 1428 1429subsection \<open>The divides relation\<close> 1430 1431lemma zdvd_antisym_nonneg: "0 \<le> m \<Longrightarrow> 0 \<le> n \<Longrightarrow> m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n" 1432 for m n :: int 1433 by (auto simp add: dvd_def mult.assoc zero_le_mult_iff zmult_eq_1_iff) 1434 1435lemma zdvd_antisym_abs: 1436 fixes a b :: int 1437 assumes "a dvd b" and "b dvd a" 1438 shows "\<bar>a\<bar> = \<bar>b\<bar>" 1439proof (cases "a = 0") 1440 case True 1441 with assms show ?thesis by simp 1442next 1443 case False 1444 from \<open>a dvd b\<close> obtain k where k: "b = a * k" 1445 unfolding dvd_def by blast 1446 from \<open>b dvd a\<close> obtain k' where k': "a = b * k'" 1447 unfolding dvd_def by blast 1448 from k k' have "a = a * k * k'" by simp 1449 with mult_cancel_left1[where c="a" and b="k*k'"] have kk': "k * k' = 1" 1450 using \<open>a \<noteq> 0\<close> by (simp add: mult.assoc) 1451 then have "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" 1452 by (simp add: zmult_eq_1_iff) 1453 with k k' show ?thesis by auto 1454qed 1455 1456lemma zdvd_zdiffD: "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> k dvd m" 1457 for k m n :: int 1458 using dvd_add_right_iff [of k "- n" m] by simp 1459 1460lemma zdvd_reduce: "k dvd n + k * m \<longleftrightarrow> k dvd n" 1461 for k m n :: int 1462 using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps) 1463 1464lemma dvd_imp_le_int: 1465 fixes d i :: int 1466 assumes "i \<noteq> 0" and "d dvd i" 1467 shows "\<bar>d\<bar> \<le> \<bar>i\<bar>" 1468proof - 1469 from \<open>d dvd i\<close> obtain k where "i = d * k" .. 1470 with \<open>i \<noteq> 0\<close> have "k \<noteq> 0" by auto 1471 then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto 1472 then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono) 1473 with \<open>i = d * k\<close> show ?thesis by (simp add: abs_mult) 1474qed 1475 1476lemma zdvd_not_zless: 1477 fixes m n :: int 1478 assumes "0 < m" and "m < n" 1479 shows "\<not> n dvd m" 1480proof 1481 from assms have "0 < n" by auto 1482 assume "n dvd m" then obtain k where k: "m = n * k" .. 1483 with \<open>0 < m\<close> have "0 < n * k" by auto 1484 with \<open>0 < n\<close> have "0 < k" by (simp add: zero_less_mult_iff) 1485 with k \<open>0 < n\<close> \<open>m < n\<close> have "n * k < n * 1" by simp 1486 with \<open>0 < n\<close> \<open>0 < k\<close> show False unfolding mult_less_cancel_left by auto 1487qed 1488 1489lemma zdvd_mult_cancel: 1490 fixes k m n :: int 1491 assumes d: "k * m dvd k * n" 1492 and "k \<noteq> 0" 1493 shows "m dvd n" 1494proof - 1495 from d obtain h where h: "k * n = k * m * h" 1496 unfolding dvd_def by blast 1497 have "n = m * h" 1498 proof (rule ccontr) 1499 assume "\<not> ?thesis" 1500 with \<open>k \<noteq> 0\<close> have "k * n \<noteq> k * (m * h)" by simp 1501 with h show False 1502 by (simp add: mult.assoc) 1503 qed 1504 then show ?thesis by simp 1505qed 1506 1507lemma int_dvd_int_iff [simp]: 1508 "int m dvd int n \<longleftrightarrow> m dvd n" 1509proof - 1510 have "m dvd n" if "int n = int m * k" for k 1511 proof (cases k) 1512 case (nonneg q) 1513 with that have "n = m * q" 1514 by (simp del: of_nat_mult add: of_nat_mult [symmetric]) 1515 then show ?thesis .. 1516 next 1517 case (neg q) 1518 with that have "int n = int m * (- int (Suc q))" 1519 by simp 1520 also have "\<dots> = - (int m * int (Suc q))" 1521 by (simp only: mult_minus_right) 1522 also have "\<dots> = - int (m * Suc q)" 1523 by (simp only: of_nat_mult [symmetric]) 1524 finally have "- int (m * Suc q) = int n" .. 1525 then show ?thesis 1526 by (simp only: negative_eq_positive) auto 1527 qed 1528 then show ?thesis by (auto simp add: dvd_def) 1529qed 1530 1531lemma dvd_nat_abs_iff [simp]: 1532 "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd k" 1533proof - 1534 have "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd int (nat \<bar>k\<bar>)" 1535 by (simp only: int_dvd_int_iff) 1536 then show ?thesis 1537 by simp 1538qed 1539 1540lemma nat_abs_dvd_iff [simp]: 1541 "nat \<bar>k\<bar> dvd n \<longleftrightarrow> k dvd int n" 1542proof - 1543 have "nat \<bar>k\<bar> dvd n \<longleftrightarrow> int (nat \<bar>k\<bar>) dvd int n" 1544 by (simp only: int_dvd_int_iff) 1545 then show ?thesis 1546 by simp 1547qed 1548 1549lemma zdvd1_eq [simp]: "x dvd 1 \<longleftrightarrow> \<bar>x\<bar> = 1" (is "?lhs \<longleftrightarrow> ?rhs") 1550 for x :: int 1551proof 1552 assume ?lhs 1553 then have "nat \<bar>x\<bar> dvd nat \<bar>1\<bar>" 1554 by (simp only: nat_abs_dvd_iff) simp 1555 then have "nat \<bar>x\<bar> = 1" 1556 by simp 1557 then show ?rhs 1558 by (cases "x < 0") simp_all 1559next 1560 assume ?rhs 1561 then have "x = 1 \<or> x = - 1" 1562 by auto 1563 then show ?lhs 1564 by (auto intro: dvdI) 1565qed 1566 1567lemma zdvd_mult_cancel1: 1568 fixes m :: int 1569 assumes mp: "m \<noteq> 0" 1570 shows "m * n dvd m \<longleftrightarrow> \<bar>n\<bar> = 1" 1571 (is "?lhs \<longleftrightarrow> ?rhs") 1572proof 1573 assume ?rhs 1574 then show ?lhs 1575 by (cases "n > 0") (auto simp add: minus_equation_iff) 1576next 1577 assume ?lhs 1578 then have "m * n dvd m * 1" by simp 1579 from zdvd_mult_cancel[OF this mp] show ?rhs 1580 by (simp only: zdvd1_eq) 1581qed 1582 1583lemma nat_dvd_iff: "nat z dvd m \<longleftrightarrow> (if 0 \<le> z then z dvd int m else m = 0)" 1584 using nat_abs_dvd_iff [of z m] by (cases "z \<ge> 0") auto 1585 1586lemma eq_nat_nat_iff: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'" 1587 by (auto elim: nonneg_int_cases) 1588 1589lemma nat_power_eq: "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n" 1590 by (induct n) (simp_all add: nat_mult_distrib) 1591 1592lemma numeral_power_eq_nat_cancel_iff [simp]: 1593 "numeral x ^ n = nat y \<longleftrightarrow> numeral x ^ n = y" 1594 using nat_eq_iff2 by auto 1595 1596lemma nat_eq_numeral_power_cancel_iff [simp]: 1597 "nat y = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n" 1598 using numeral_power_eq_nat_cancel_iff[of x n y] 1599 by (metis (mono_tags)) 1600 1601lemma numeral_power_le_nat_cancel_iff [simp]: 1602 "numeral x ^ n \<le> nat a \<longleftrightarrow> numeral x ^ n \<le> a" 1603 using nat_le_eq_zle[of "numeral x ^ n" a] 1604 by (auto simp: nat_power_eq) 1605 1606lemma nat_le_numeral_power_cancel_iff [simp]: 1607 "nat a \<le> numeral x ^ n \<longleftrightarrow> a \<le> numeral x ^ n" 1608 by (simp add: nat_le_iff) 1609 1610lemma numeral_power_less_nat_cancel_iff [simp]: 1611 "numeral x ^ n < nat a \<longleftrightarrow> numeral x ^ n < a" 1612 using nat_less_eq_zless[of "numeral x ^ n" a] 1613 by (auto simp: nat_power_eq) 1614 1615lemma nat_less_numeral_power_cancel_iff [simp]: 1616 "nat a < numeral x ^ n \<longleftrightarrow> a < numeral x ^ n" 1617 using nat_less_eq_zless[of a "numeral x ^ n"] 1618 by (cases "a < 0") (auto simp: nat_power_eq less_le_trans[where y=0]) 1619 1620lemma zdvd_imp_le: "z dvd n \<Longrightarrow> 0 < n \<Longrightarrow> z \<le> n" 1621 for n z :: int 1622 apply (cases n) 1623 apply auto 1624 apply (cases z) 1625 apply (auto simp add: dvd_imp_le) 1626 done 1627 1628lemma zdvd_period: 1629 fixes a d :: int 1630 assumes "a dvd d" 1631 shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)" 1632 (is "?lhs \<longleftrightarrow> ?rhs") 1633proof - 1634 from assms have "a dvd (x + t) \<longleftrightarrow> a dvd ((x + t) + c * d)" 1635 by (simp add: dvd_add_left_iff) 1636 then show ?thesis 1637 by (simp add: ac_simps) 1638qed 1639 1640 1641subsection \<open>Finiteness of intervals\<close> 1642 1643lemma finite_interval_int1 [iff]: "finite {i :: int. a \<le> i \<and> i \<le> b}" 1644proof (cases "a \<le> b") 1645 case True 1646 then show ?thesis 1647 proof (induct b rule: int_ge_induct) 1648 case base 1649 have "{i. a \<le> i \<and> i \<le> a} = {a}" by auto 1650 then show ?case by simp 1651 next 1652 case (step b) 1653 then have "{i. a \<le> i \<and> i \<le> b + 1} = {i. a \<le> i \<and> i \<le> b} \<union> {b + 1}" by auto 1654 with step show ?case by simp 1655 qed 1656next 1657 case False 1658 then show ?thesis 1659 by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans) 1660qed 1661 1662lemma finite_interval_int2 [iff]: "finite {i :: int. a \<le> i \<and> i < b}" 1663 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto 1664 1665lemma finite_interval_int3 [iff]: "finite {i :: int. a < i \<and> i \<le> b}" 1666 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto 1667 1668lemma finite_interval_int4 [iff]: "finite {i :: int. a < i \<and> i < b}" 1669 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto 1670 1671 1672subsection \<open>Configuration of the code generator\<close> 1673 1674text \<open>Constructors\<close> 1675 1676definition Pos :: "num \<Rightarrow> int" 1677 where [simp, code_abbrev]: "Pos = numeral" 1678 1679definition Neg :: "num \<Rightarrow> int" 1680 where [simp, code_abbrev]: "Neg n = - (Pos n)" 1681 1682code_datatype "0::int" Pos Neg 1683 1684 1685text \<open>Auxiliary operations.\<close> 1686 1687definition dup :: "int \<Rightarrow> int" 1688 where [simp]: "dup k = k + k" 1689 1690lemma dup_code [code]: 1691 "dup 0 = 0" 1692 "dup (Pos n) = Pos (Num.Bit0 n)" 1693 "dup (Neg n) = Neg (Num.Bit0 n)" 1694 by (simp_all add: numeral_Bit0) 1695 1696definition sub :: "num \<Rightarrow> num \<Rightarrow> int" 1697 where [simp]: "sub m n = numeral m - numeral n" 1698 1699lemma sub_code [code]: 1700 "sub Num.One Num.One = 0" 1701 "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" 1702 "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" 1703 "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" 1704 "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" 1705 "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" 1706 "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" 1707 "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" 1708 "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" 1709 by (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM) 1710 1711text \<open>Implementations.\<close> 1712 1713lemma one_int_code [code]: "1 = Pos Num.One" 1714 by simp 1715 1716lemma plus_int_code [code]: 1717 "k + 0 = k" 1718 "0 + l = l" 1719 "Pos m + Pos n = Pos (m + n)" 1720 "Pos m + Neg n = sub m n" 1721 "Neg m + Pos n = sub n m" 1722 "Neg m + Neg n = Neg (m + n)" 1723 for k l :: int 1724 by simp_all 1725 1726lemma uminus_int_code [code]: 1727 "uminus 0 = (0::int)" 1728 "uminus (Pos m) = Neg m" 1729 "uminus (Neg m) = Pos m" 1730 by simp_all 1731 1732lemma minus_int_code [code]: 1733 "k - 0 = k" 1734 "0 - l = uminus l" 1735 "Pos m - Pos n = sub m n" 1736 "Pos m - Neg n = Pos (m + n)" 1737 "Neg m - Pos n = Neg (m + n)" 1738 "Neg m - Neg n = sub n m" 1739 for k l :: int 1740 by simp_all 1741 1742lemma times_int_code [code]: 1743 "k * 0 = 0" 1744 "0 * l = 0" 1745 "Pos m * Pos n = Pos (m * n)" 1746 "Pos m * Neg n = Neg (m * n)" 1747 "Neg m * Pos n = Neg (m * n)" 1748 "Neg m * Neg n = Pos (m * n)" 1749 for k l :: int 1750 by simp_all 1751 1752instantiation int :: equal 1753begin 1754 1755definition "HOL.equal k l \<longleftrightarrow> k = (l::int)" 1756 1757instance 1758 by standard (rule equal_int_def) 1759 1760end 1761 1762lemma equal_int_code [code]: 1763 "HOL.equal 0 (0::int) \<longleftrightarrow> True" 1764 "HOL.equal 0 (Pos l) \<longleftrightarrow> False" 1765 "HOL.equal 0 (Neg l) \<longleftrightarrow> False" 1766 "HOL.equal (Pos k) 0 \<longleftrightarrow> False" 1767 "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l" 1768 "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False" 1769 "HOL.equal (Neg k) 0 \<longleftrightarrow> False" 1770 "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False" 1771 "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l" 1772 by (auto simp add: equal) 1773 1774lemma equal_int_refl [code nbe]: "HOL.equal k k \<longleftrightarrow> True" 1775 for k :: int 1776 by (fact equal_refl) 1777 1778lemma less_eq_int_code [code]: 1779 "0 \<le> (0::int) \<longleftrightarrow> True" 1780 "0 \<le> Pos l \<longleftrightarrow> True" 1781 "0 \<le> Neg l \<longleftrightarrow> False" 1782 "Pos k \<le> 0 \<longleftrightarrow> False" 1783 "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l" 1784 "Pos k \<le> Neg l \<longleftrightarrow> False" 1785 "Neg k \<le> 0 \<longleftrightarrow> True" 1786 "Neg k \<le> Pos l \<longleftrightarrow> True" 1787 "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k" 1788 by simp_all 1789 1790lemma less_int_code [code]: 1791 "0 < (0::int) \<longleftrightarrow> False" 1792 "0 < Pos l \<longleftrightarrow> True" 1793 "0 < Neg l \<longleftrightarrow> False" 1794 "Pos k < 0 \<longleftrightarrow> False" 1795 "Pos k < Pos l \<longleftrightarrow> k < l" 1796 "Pos k < Neg l \<longleftrightarrow> False" 1797 "Neg k < 0 \<longleftrightarrow> True" 1798 "Neg k < Pos l \<longleftrightarrow> True" 1799 "Neg k < Neg l \<longleftrightarrow> l < k" 1800 by simp_all 1801 1802lemma nat_code [code]: 1803 "nat (Int.Neg k) = 0" 1804 "nat 0 = 0" 1805 "nat (Int.Pos k) = nat_of_num k" 1806 by (simp_all add: nat_of_num_numeral) 1807 1808lemma (in ring_1) of_int_code [code]: 1809 "of_int (Int.Neg k) = - numeral k" 1810 "of_int 0 = 0" 1811 "of_int (Int.Pos k) = numeral k" 1812 by simp_all 1813 1814 1815text \<open>Serializer setup.\<close> 1816 1817code_identifier 1818 code_module Int \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith 1819 1820quickcheck_params [default_type = int] 1821 1822hide_const (open) Pos Neg sub dup 1823 1824 1825text \<open>De-register \<open>int\<close> as a quotient type:\<close> 1826 1827lifting_update int.lifting 1828lifting_forget int.lifting 1829 1830 1831subsection \<open>Duplicates\<close> 1832 1833lemmas int_sum = of_nat_sum [where 'a=int] 1834lemmas int_prod = of_nat_prod [where 'a=int] 1835lemmas zle_int = of_nat_le_iff [where 'a=int] 1836lemmas int_int_eq = of_nat_eq_iff [where 'a=int] 1837lemmas nonneg_eq_int = nonneg_int_cases 1838lemmas double_eq_0_iff = double_zero 1839 1840lemmas int_distrib = 1841 distrib_right [of z1 z2 w] 1842 distrib_left [of w z1 z2] 1843 left_diff_distrib [of z1 z2 w] 1844 right_diff_distrib [of w z1 z2] 1845 for z1 z2 w :: int 1846 1847end 1848 1849