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