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