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