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