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