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