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