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