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