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