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