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