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