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