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