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