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