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