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