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