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