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