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