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