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