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