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