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