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