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