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