src/HOL/Int.thy
author haftmann
Fri Jun 11 17:14:02 2010 +0200 (2010-06-11)
changeset 37407 61dd8c145da7
parent 36811 4ab4aa5bee1c
child 37767 a2b7a20d6ea3
permissions -rw-r--r--
declare lex_prod_def [code del]
     1 (*  Title:      Int.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3                 Tobias Nipkow, Florian Haftmann, TU Muenchen
     4     Copyright   1994  University of Cambridge
     5 
     6 *)
     7 
     8 header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
     9 
    10 theory Int
    11 imports Equiv_Relations Nat Wellfounded
    12 uses
    13   ("Tools/numeral.ML")
    14   ("Tools/numeral_syntax.ML")
    15   ("Tools/int_arith.ML")
    16 begin
    17 
    18 subsection {* The equivalence relation underlying the integers *}
    19 
    20 definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
    21   [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
    22 
    23 typedef (Integ)
    24   int = "UNIV//intrel"
    25   by (auto simp add: quotient_def)
    26 
    27 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
    28 begin
    29 
    30 definition
    31   Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
    32 
    33 definition
    34   One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
    35 
    36 definition
    37   add_int_def [code del]: "z + w = Abs_Integ
    38     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
    39       intrel `` {(x + u, y + v)})"
    40 
    41 definition
    42   minus_int_def [code del]:
    43     "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
    44 
    45 definition
    46   diff_int_def [code del]:  "z - w = z + (-w \<Colon> int)"
    47 
    48 definition
    49   mult_int_def [code del]: "z * w = Abs_Integ
    50     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
    51       intrel `` {(x*u + y*v, x*v + y*u)})"
    52 
    53 definition
    54   le_int_def [code del]:
    55    "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
    56 
    57 definition
    58   less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
    59 
    60 definition
    61   zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
    62 
    63 definition
    64   zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
    65 
    66 instance ..
    67 
    68 end
    69 
    70 
    71 subsection{*Construction of the Integers*}
    72 
    73 lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"
    74 by (simp add: intrel_def)
    75 
    76 lemma equiv_intrel: "equiv UNIV intrel"
    77 by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def)
    78 
    79 text{*Reduces equality of equivalence classes to the @{term intrel} relation:
    80   @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
    81 lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
    82 
    83 text{*All equivalence classes belong to set of representatives*}
    84 lemma [simp]: "intrel``{(x,y)} \<in> Integ"
    85 by (auto simp add: Integ_def intrel_def quotient_def)
    86 
    87 text{*Reduces equality on abstractions to equality on representatives:
    88   @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
    89 declare Abs_Integ_inject [simp,no_atp]  Abs_Integ_inverse [simp,no_atp]
    90 
    91 text{*Case analysis on the representation of an integer as an equivalence
    92       class of pairs of naturals.*}
    93 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
    94      "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
    95 apply (rule Abs_Integ_cases [of z]) 
    96 apply (auto simp add: Integ_def quotient_def) 
    97 done
    98 
    99 
   100 subsection {* Arithmetic Operations *}
   101 
   102 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
   103 proof -
   104   have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
   105     by (simp add: congruent_def) 
   106   thus ?thesis
   107     by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
   108 qed
   109 
   110 lemma add:
   111      "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
   112       Abs_Integ (intrel``{(x+u, y+v)})"
   113 proof -
   114   have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
   115         respects2 intrel"
   116     by (simp add: congruent2_def)
   117   thus ?thesis
   118     by (simp add: add_int_def UN_UN_split_split_eq
   119                   UN_equiv_class2 [OF equiv_intrel equiv_intrel])
   120 qed
   121 
   122 text{*Congruence property for multiplication*}
   123 lemma mult_congruent2:
   124      "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
   125       respects2 intrel"
   126 apply (rule equiv_intrel [THEN congruent2_commuteI])
   127  apply (force simp add: mult_ac, clarify) 
   128 apply (simp add: congruent_def mult_ac)  
   129 apply (rename_tac u v w x y z)
   130 apply (subgoal_tac "u*y + x*y = w*y + v*y  &  u*z + x*z = w*z + v*z")
   131 apply (simp add: mult_ac)
   132 apply (simp add: add_mult_distrib [symmetric])
   133 done
   134 
   135 lemma mult:
   136      "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
   137       Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
   138 by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2
   139               UN_equiv_class2 [OF equiv_intrel equiv_intrel])
   140 
   141 text{*The integers form a @{text comm_ring_1}*}
   142 instance int :: comm_ring_1
   143 proof
   144   fix i j k :: int
   145   show "(i + j) + k = i + (j + k)"
   146     by (cases i, cases j, cases k) (simp add: add add_assoc)
   147   show "i + j = j + i" 
   148     by (cases i, cases j) (simp add: add_ac add)
   149   show "0 + i = i"
   150     by (cases i) (simp add: Zero_int_def add)
   151   show "- i + i = 0"
   152     by (cases i) (simp add: Zero_int_def minus add)
   153   show "i - j = i + - j"
   154     by (simp add: diff_int_def)
   155   show "(i * j) * k = i * (j * k)"
   156     by (cases i, cases j, cases k) (simp add: mult algebra_simps)
   157   show "i * j = j * i"
   158     by (cases i, cases j) (simp add: mult algebra_simps)
   159   show "1 * i = i"
   160     by (cases i) (simp add: One_int_def mult)
   161   show "(i + j) * k = i * k + j * k"
   162     by (cases i, cases j, cases k) (simp add: add mult algebra_simps)
   163   show "0 \<noteq> (1::int)"
   164     by (simp add: Zero_int_def One_int_def)
   165 qed
   166 
   167 lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
   168 by (induct m, simp_all add: Zero_int_def One_int_def add)
   169 
   170 
   171 subsection {* The @{text "\<le>"} Ordering *}
   172 
   173 lemma le:
   174   "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"
   175 by (force simp add: le_int_def)
   176 
   177 lemma less:
   178   "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"
   179 by (simp add: less_int_def le order_less_le)
   180 
   181 instance int :: linorder
   182 proof
   183   fix i j k :: int
   184   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
   185     by (cases i, cases j) (simp add: le)
   186   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
   187     by (auto simp add: less_int_def dest: antisym) 
   188   show "i \<le> i"
   189     by (cases i) (simp add: le)
   190   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
   191     by (cases i, cases j, cases k) (simp add: le)
   192   show "i \<le> j \<or> j \<le> i"
   193     by (cases i, cases j) (simp add: le linorder_linear)
   194 qed
   195 
   196 instantiation int :: distrib_lattice
   197 begin
   198 
   199 definition
   200   "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
   201 
   202 definition
   203   "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
   204 
   205 instance
   206   by intro_classes
   207     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
   208 
   209 end
   210 
   211 instance int :: ordered_cancel_ab_semigroup_add
   212 proof
   213   fix i j k :: int
   214   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
   215     by (cases i, cases j, cases k) (simp add: le add)
   216 qed
   217 
   218 
   219 text{*Strict Monotonicity of Multiplication*}
   220 
   221 text{*strict, in 1st argument; proof is by induction on k>0*}
   222 lemma zmult_zless_mono2_lemma:
   223      "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
   224 apply (induct "k", simp)
   225 apply (simp add: left_distrib)
   226 apply (case_tac "k=0")
   227 apply (simp_all add: add_strict_mono)
   228 done
   229 
   230 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
   231 apply (cases k)
   232 apply (auto simp add: le add int_def Zero_int_def)
   233 apply (rule_tac x="x-y" in exI, simp)
   234 done
   235 
   236 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
   237 apply (cases k)
   238 apply (simp add: less int_def Zero_int_def)
   239 apply (rule_tac x="x-y" in exI, simp)
   240 done
   241 
   242 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
   243 apply (drule zero_less_imp_eq_int)
   244 apply (auto simp add: zmult_zless_mono2_lemma)
   245 done
   246 
   247 text{*The integers form an ordered integral domain*}
   248 instance int :: linordered_idom
   249 proof
   250   fix i j k :: int
   251   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   252     by (rule zmult_zless_mono2)
   253   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
   254     by (simp only: zabs_def)
   255   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
   256     by (simp only: zsgn_def)
   257 qed
   258 
   259 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
   260 apply (cases w, cases z) 
   261 apply (simp add: less le add One_int_def)
   262 done
   263 
   264 lemma zless_iff_Suc_zadd:
   265   "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))"
   266 apply (cases z, cases w)
   267 apply (auto simp add: less add int_def)
   268 apply (rename_tac a b c d) 
   269 apply (rule_tac x="a+d - Suc(c+b)" in exI) 
   270 apply arith
   271 done
   272 
   273 lemmas int_distrib =
   274   left_distrib [of "z1::int" "z2" "w", standard]
   275   right_distrib [of "w::int" "z1" "z2", standard]
   276   left_diff_distrib [of "z1::int" "z2" "w", standard]
   277   right_diff_distrib [of "w::int" "z1" "z2", standard]
   278 
   279 
   280 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
   281 
   282 context ring_1
   283 begin
   284 
   285 definition of_int :: "int \<Rightarrow> 'a" where
   286   [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
   287 
   288 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
   289 proof -
   290   have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
   291     by (simp add: congruent_def algebra_simps of_nat_add [symmetric]
   292             del: of_nat_add) 
   293   thus ?thesis
   294     by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
   295 qed
   296 
   297 lemma of_int_0 [simp]: "of_int 0 = 0"
   298 by (simp add: of_int Zero_int_def)
   299 
   300 lemma of_int_1 [simp]: "of_int 1 = 1"
   301 by (simp add: of_int One_int_def)
   302 
   303 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
   304 by (cases w, cases z, simp add: algebra_simps of_int add)
   305 
   306 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
   307 by (cases z, simp add: algebra_simps of_int minus)
   308 
   309 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
   310 by (simp add: diff_minus Groups.diff_minus)
   311 
   312 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
   313 apply (cases w, cases z)
   314 apply (simp add: algebra_simps of_int mult of_nat_mult)
   315 done
   316 
   317 text{*Collapse nested embeddings*}
   318 lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
   319 by (induct n) auto
   320 
   321 lemma of_int_power:
   322   "of_int (z ^ n) = of_int z ^ n"
   323   by (induct n) simp_all
   324 
   325 end
   326 
   327 text{*Class for unital rings with characteristic zero.
   328  Includes non-ordered rings like the complex numbers.*}
   329 class ring_char_0 = ring_1 + semiring_char_0
   330 begin
   331 
   332 lemma of_int_eq_iff [simp]:
   333    "of_int w = of_int z \<longleftrightarrow> w = z"
   334 apply (cases w, cases z, simp add: of_int)
   335 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
   336 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
   337 done
   338 
   339 text{*Special cases where either operand is zero*}
   340 lemma of_int_eq_0_iff [simp]:
   341   "of_int z = 0 \<longleftrightarrow> z = 0"
   342   using of_int_eq_iff [of z 0] by simp
   343 
   344 lemma of_int_0_eq_iff [simp]:
   345   "0 = of_int z \<longleftrightarrow> z = 0"
   346   using of_int_eq_iff [of 0 z] by simp
   347 
   348 end
   349 
   350 context linordered_idom
   351 begin
   352 
   353 text{*Every @{text linordered_idom} has characteristic zero.*}
   354 subclass ring_char_0 ..
   355 
   356 lemma of_int_le_iff [simp]:
   357   "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
   358   by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
   359 
   360 lemma of_int_less_iff [simp]:
   361   "of_int w < of_int z \<longleftrightarrow> w < z"
   362   by (simp add: less_le order_less_le)
   363 
   364 lemma of_int_0_le_iff [simp]:
   365   "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
   366   using of_int_le_iff [of 0 z] by simp
   367 
   368 lemma of_int_le_0_iff [simp]:
   369   "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
   370   using of_int_le_iff [of z 0] by simp
   371 
   372 lemma of_int_0_less_iff [simp]:
   373   "0 < of_int z \<longleftrightarrow> 0 < z"
   374   using of_int_less_iff [of 0 z] by simp
   375 
   376 lemma of_int_less_0_iff [simp]:
   377   "of_int z < 0 \<longleftrightarrow> z < 0"
   378   using of_int_less_iff [of z 0] by simp
   379 
   380 end
   381 
   382 lemma of_int_eq_id [simp]: "of_int = id"
   383 proof
   384   fix z show "of_int z = id z"
   385     by (cases z) (simp add: of_int add minus int_def diff_minus)
   386 qed
   387 
   388 
   389 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
   390 
   391 definition
   392   nat :: "int \<Rightarrow> nat"
   393 where
   394   [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
   395 
   396 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
   397 proof -
   398   have "(\<lambda>(x,y). {x-y}) respects intrel"
   399     by (simp add: congruent_def) arith
   400   thus ?thesis
   401     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
   402 qed
   403 
   404 lemma nat_int [simp]: "nat (of_nat n) = n"
   405 by (simp add: nat int_def)
   406 
   407 (* FIXME: duplicates nat_0 *)
   408 lemma nat_zero [simp]: "nat 0 = 0"
   409 by (simp add: Zero_int_def nat)
   410 
   411 lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)"
   412 by (cases z, simp add: nat le int_def Zero_int_def)
   413 
   414 corollary nat_0_le: "0 \<le> z ==> of_nat (nat z) = z"
   415 by simp
   416 
   417 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
   418 by (cases z, simp add: nat le Zero_int_def)
   419 
   420 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
   421 apply (cases w, cases z) 
   422 apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
   423 done
   424 
   425 text{*An alternative condition is @{term "0 \<le> w"} *}
   426 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
   427 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   428 
   429 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
   430 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   431 
   432 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
   433 apply (cases w, cases z) 
   434 apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
   435 done
   436 
   437 lemma nonneg_eq_int:
   438   fixes z :: int
   439   assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P"
   440   shows P
   441   using assms by (blast dest: nat_0_le sym)
   442 
   443 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)"
   444 by (cases w, simp add: nat le int_def Zero_int_def, arith)
   445 
   446 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)"
   447 by (simp only: eq_commute [of m] nat_eq_iff)
   448 
   449 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
   450 apply (cases w)
   451 apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
   452 done
   453 
   454 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
   455 by(simp add: nat_eq_iff) arith
   456 
   457 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
   458 by (auto simp add: nat_eq_iff2)
   459 
   460 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
   461 by (insert zless_nat_conj [of 0], auto)
   462 
   463 lemma nat_add_distrib:
   464      "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
   465 by (cases z, cases z', simp add: nat add le Zero_int_def)
   466 
   467 lemma nat_diff_distrib:
   468      "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
   469 by (cases z, cases z', 
   470     simp add: nat add minus diff_minus le Zero_int_def)
   471 
   472 lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0"
   473 by (simp add: int_def minus nat Zero_int_def) 
   474 
   475 lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)"
   476 by (cases z, simp add: nat less int_def, arith)
   477 
   478 context ring_1
   479 begin
   480 
   481 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
   482   by (cases z rule: eq_Abs_Integ)
   483    (simp add: nat le of_int Zero_int_def of_nat_diff)
   484 
   485 end
   486 
   487 text {* For termination proofs: *}
   488 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
   489 
   490 
   491 subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
   492 
   493 lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \<Colon> int)"
   494 by (simp add: order_less_le del: of_nat_Suc)
   495 
   496 lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \<Colon> int)"
   497 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   498 
   499 lemma negative_zle_0: "- of_nat n \<le> (0 \<Colon> int)"
   500 by (simp add: minus_le_iff)
   501 
   502 lemma negative_zle [iff]: "- of_nat n \<le> (of_nat m \<Colon> int)"
   503 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
   504 
   505 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (of_nat (Suc n) \<Colon> int))"
   506 by (subst le_minus_iff, simp del: of_nat_Suc)
   507 
   508 lemma int_zle_neg: "((of_nat n \<Colon> int) \<le> - of_nat m) = (n = 0 & m = 0)"
   509 by (simp add: int_def le minus Zero_int_def)
   510 
   511 lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) < - of_nat m)"
   512 by (simp add: linorder_not_less)
   513 
   514 lemma negative_eq_positive [simp]: "((- of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)"
   515 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
   516 
   517 lemma zle_iff_zadd: "(w\<Colon>int) \<le> z \<longleftrightarrow> (\<exists>n. z = w + of_nat n)"
   518 proof -
   519   have "(w \<le> z) = (0 \<le> z - w)"
   520     by (simp only: le_diff_eq add_0_left)
   521   also have "\<dots> = (\<exists>n. z - w = of_nat n)"
   522     by (auto elim: zero_le_imp_eq_int)
   523   also have "\<dots> = (\<exists>n. z = w + of_nat n)"
   524     by (simp only: algebra_simps)
   525   finally show ?thesis .
   526 qed
   527 
   528 lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)"
   529 by simp
   530 
   531 lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)"
   532 by simp
   533 
   534 text{*This version is proved for all ordered rings, not just integers!
   535       It is proved here because attribute @{text arith_split} is not available
   536       in theory @{text Rings}.
   537       But is it really better than just rewriting with @{text abs_if}?*}
   538 lemma abs_split [arith_split,no_atp]:
   539      "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
   540 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
   541 
   542 lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x = - (of_nat (Suc n))"
   543 apply (cases x)
   544 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
   545 apply (rule_tac x="y - Suc x" in exI, arith)
   546 done
   547 
   548 
   549 subsection {* Cases and induction *}
   550 
   551 text{*Now we replace the case analysis rule by a more conventional one:
   552 whether an integer is negative or not.*}
   553 
   554 theorem int_cases [cases type: int, case_names nonneg neg]:
   555   "[|!! n. (z \<Colon> int) = of_nat n ==> P;  !! n. z =  - (of_nat (Suc n)) ==> P |] ==> P"
   556 apply (cases "z < 0", blast dest!: negD)
   557 apply (simp add: linorder_not_less del: of_nat_Suc)
   558 apply auto
   559 apply (blast dest: nat_0_le [THEN sym])
   560 done
   561 
   562 theorem int_of_nat_induct [induct type: int, case_names nonneg neg]:
   563      "[|!! n. P (of_nat n \<Colon> int);  !!n. P (- (of_nat (Suc n))) |] ==> P z"
   564   by (cases z rule: int_cases) auto
   565 
   566 text{*Contributed by Brian Huffman*}
   567 theorem int_diff_cases:
   568   obtains (diff) m n where "(z\<Colon>int) = of_nat m - of_nat n"
   569 apply (cases z rule: eq_Abs_Integ)
   570 apply (rule_tac m=x and n=y in diff)
   571 apply (simp add: int_def diff_def minus add)
   572 done
   573 
   574 
   575 subsection {* Binary representation *}
   576 
   577 text {*
   578   This formalization defines binary arithmetic in terms of the integers
   579   rather than using a datatype. This avoids multiple representations (leading
   580   zeroes, etc.)  See @{text "ZF/Tools/twos-compl.ML"}, function @{text
   581   int_of_binary}, for the numerical interpretation.
   582 
   583   The representation expects that @{text "(m mod 2)"} is 0 or 1,
   584   even if m is negative;
   585   For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
   586   @{text "-5 = (-3)*2 + 1"}.
   587   
   588   This two's complement binary representation derives from the paper 
   589   "An Efficient Representation of Arithmetic for Term Rewriting" by
   590   Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
   591   Springer LNCS 488 (240-251), 1991.
   592 *}
   593 
   594 subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
   595 
   596 definition
   597   Pls :: int where
   598   [code del]: "Pls = 0"
   599 
   600 definition
   601   Min :: int where
   602   [code del]: "Min = - 1"
   603 
   604 definition
   605   Bit0 :: "int \<Rightarrow> int" where
   606   [code del]: "Bit0 k = k + k"
   607 
   608 definition
   609   Bit1 :: "int \<Rightarrow> int" where
   610   [code del]: "Bit1 k = 1 + k + k"
   611 
   612 class number = -- {* for numeric types: nat, int, real, \dots *}
   613   fixes number_of :: "int \<Rightarrow> 'a"
   614 
   615 use "Tools/numeral.ML"
   616 
   617 syntax
   618   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
   619 
   620 use "Tools/numeral_syntax.ML"
   621 setup Numeral_Syntax.setup
   622 
   623 abbreviation
   624   "Numeral0 \<equiv> number_of Pls"
   625 
   626 abbreviation
   627   "Numeral1 \<equiv> number_of (Bit1 Pls)"
   628 
   629 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
   630   -- {* Unfold all @{text let}s involving constants *}
   631   unfolding Let_def ..
   632 
   633 definition
   634   succ :: "int \<Rightarrow> int" where
   635   [code del]: "succ k = k + 1"
   636 
   637 definition
   638   pred :: "int \<Rightarrow> int" where
   639   [code del]: "pred k = k - 1"
   640 
   641 lemmas
   642   max_number_of [simp] = max_def
   643     [of "number_of u" "number_of v", standard]
   644 and
   645   min_number_of [simp] = min_def 
   646     [of "number_of u" "number_of v", standard]
   647   -- {* unfolding @{text minx} and @{text max} on numerals *}
   648 
   649 lemmas numeral_simps = 
   650   succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
   651 
   652 text {* Removal of leading zeroes *}
   653 
   654 lemma Bit0_Pls [simp, code_post]:
   655   "Bit0 Pls = Pls"
   656   unfolding numeral_simps by simp
   657 
   658 lemma Bit1_Min [simp, code_post]:
   659   "Bit1 Min = Min"
   660   unfolding numeral_simps by simp
   661 
   662 lemmas normalize_bin_simps =
   663   Bit0_Pls Bit1_Min
   664 
   665 
   666 subsubsection {* Successor and predecessor functions *}
   667 
   668 text {* Successor *}
   669 
   670 lemma succ_Pls:
   671   "succ Pls = Bit1 Pls"
   672   unfolding numeral_simps by simp
   673 
   674 lemma succ_Min:
   675   "succ Min = Pls"
   676   unfolding numeral_simps by simp
   677 
   678 lemma succ_Bit0:
   679   "succ (Bit0 k) = Bit1 k"
   680   unfolding numeral_simps by simp
   681 
   682 lemma succ_Bit1:
   683   "succ (Bit1 k) = Bit0 (succ k)"
   684   unfolding numeral_simps by simp
   685 
   686 lemmas succ_bin_simps [simp] =
   687   succ_Pls succ_Min succ_Bit0 succ_Bit1
   688 
   689 text {* Predecessor *}
   690 
   691 lemma pred_Pls:
   692   "pred Pls = Min"
   693   unfolding numeral_simps by simp
   694 
   695 lemma pred_Min:
   696   "pred Min = Bit0 Min"
   697   unfolding numeral_simps by simp
   698 
   699 lemma pred_Bit0:
   700   "pred (Bit0 k) = Bit1 (pred k)"
   701   unfolding numeral_simps by simp 
   702 
   703 lemma pred_Bit1:
   704   "pred (Bit1 k) = Bit0 k"
   705   unfolding numeral_simps by simp
   706 
   707 lemmas pred_bin_simps [simp] =
   708   pred_Pls pred_Min pred_Bit0 pred_Bit1
   709 
   710 
   711 subsubsection {* Binary arithmetic *}
   712 
   713 text {* Addition *}
   714 
   715 lemma add_Pls:
   716   "Pls + k = k"
   717   unfolding numeral_simps by simp
   718 
   719 lemma add_Min:
   720   "Min + k = pred k"
   721   unfolding numeral_simps by simp
   722 
   723 lemma add_Bit0_Bit0:
   724   "(Bit0 k) + (Bit0 l) = Bit0 (k + l)"
   725   unfolding numeral_simps by simp
   726 
   727 lemma add_Bit0_Bit1:
   728   "(Bit0 k) + (Bit1 l) = Bit1 (k + l)"
   729   unfolding numeral_simps by simp
   730 
   731 lemma add_Bit1_Bit0:
   732   "(Bit1 k) + (Bit0 l) = Bit1 (k + l)"
   733   unfolding numeral_simps by simp
   734 
   735 lemma add_Bit1_Bit1:
   736   "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)"
   737   unfolding numeral_simps by simp
   738 
   739 lemma add_Pls_right:
   740   "k + Pls = k"
   741   unfolding numeral_simps by simp
   742 
   743 lemma add_Min_right:
   744   "k + Min = pred k"
   745   unfolding numeral_simps by simp
   746 
   747 lemmas add_bin_simps [simp] =
   748   add_Pls add_Min add_Pls_right add_Min_right
   749   add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1
   750 
   751 text {* Negation *}
   752 
   753 lemma minus_Pls:
   754   "- Pls = Pls"
   755   unfolding numeral_simps by simp
   756 
   757 lemma minus_Min:
   758   "- Min = Bit1 Pls"
   759   unfolding numeral_simps by simp
   760 
   761 lemma minus_Bit0:
   762   "- (Bit0 k) = Bit0 (- k)"
   763   unfolding numeral_simps by simp
   764 
   765 lemma minus_Bit1:
   766   "- (Bit1 k) = Bit1 (pred (- k))"
   767   unfolding numeral_simps by simp
   768 
   769 lemmas minus_bin_simps [simp] =
   770   minus_Pls minus_Min minus_Bit0 minus_Bit1
   771 
   772 text {* Subtraction *}
   773 
   774 lemma diff_bin_simps [simp]:
   775   "k - Pls = k"
   776   "k - Min = succ k"
   777   "Pls - (Bit0 l) = Bit0 (Pls - l)"
   778   "Pls - (Bit1 l) = Bit1 (Min - l)"
   779   "Min - (Bit0 l) = Bit1 (Min - l)"
   780   "Min - (Bit1 l) = Bit0 (Min - l)"
   781   "(Bit0 k) - (Bit0 l) = Bit0 (k - l)"
   782   "(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)"
   783   "(Bit1 k) - (Bit0 l) = Bit1 (k - l)"
   784   "(Bit1 k) - (Bit1 l) = Bit0 (k - l)"
   785   unfolding numeral_simps by simp_all
   786 
   787 text {* Multiplication *}
   788 
   789 lemma mult_Pls:
   790   "Pls * w = Pls"
   791   unfolding numeral_simps by simp
   792 
   793 lemma mult_Min:
   794   "Min * k = - k"
   795   unfolding numeral_simps by simp
   796 
   797 lemma mult_Bit0:
   798   "(Bit0 k) * l = Bit0 (k * l)"
   799   unfolding numeral_simps int_distrib by simp
   800 
   801 lemma mult_Bit1:
   802   "(Bit1 k) * l = (Bit0 (k * l)) + l"
   803   unfolding numeral_simps int_distrib by simp
   804 
   805 lemmas mult_bin_simps [simp] =
   806   mult_Pls mult_Min mult_Bit0 mult_Bit1
   807 
   808 
   809 subsubsection {* Binary comparisons *}
   810 
   811 text {* Preliminaries *}
   812 
   813 lemma even_less_0_iff:
   814   "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
   815 proof -
   816   have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib)
   817   also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
   818     by (simp add: mult_less_0_iff zero_less_two 
   819                   order_less_not_sym [OF zero_less_two])
   820   finally show ?thesis .
   821 qed
   822 
   823 lemma le_imp_0_less: 
   824   assumes le: "0 \<le> z"
   825   shows "(0::int) < 1 + z"
   826 proof -
   827   have "0 \<le> z" by fact
   828   also have "... < z + 1" by (rule less_add_one) 
   829   also have "... = 1 + z" by (simp add: add_ac)
   830   finally show "0 < 1 + z" .
   831 qed
   832 
   833 lemma odd_less_0_iff:
   834   "(1 + z + z < 0) = (z < (0::int))"
   835 proof (cases z rule: int_cases)
   836   case (nonneg n)
   837   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
   838                              le_imp_0_less [THEN order_less_imp_le])  
   839 next
   840   case (neg n)
   841   thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
   842     add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
   843 qed
   844 
   845 lemma bin_less_0_simps:
   846   "Pls < 0 \<longleftrightarrow> False"
   847   "Min < 0 \<longleftrightarrow> True"
   848   "Bit0 w < 0 \<longleftrightarrow> w < 0"
   849   "Bit1 w < 0 \<longleftrightarrow> w < 0"
   850   unfolding numeral_simps
   851   by (simp_all add: even_less_0_iff odd_less_0_iff)
   852 
   853 lemma less_bin_lemma: "k < l \<longleftrightarrow> k - l < (0::int)"
   854   by simp
   855 
   856 lemma le_iff_pred_less: "k \<le> l \<longleftrightarrow> pred k < l"
   857   unfolding numeral_simps
   858   proof
   859     have "k - 1 < k" by simp
   860     also assume "k \<le> l"
   861     finally show "k - 1 < l" .
   862   next
   863     assume "k - 1 < l"
   864     hence "(k - 1) + 1 \<le> l" by (rule zless_imp_add1_zle)
   865     thus "k \<le> l" by simp
   866   qed
   867 
   868 lemma succ_pred: "succ (pred x) = x"
   869   unfolding numeral_simps by simp
   870 
   871 text {* Less-than *}
   872 
   873 lemma less_bin_simps [simp]:
   874   "Pls < Pls \<longleftrightarrow> False"
   875   "Pls < Min \<longleftrightarrow> False"
   876   "Pls < Bit0 k \<longleftrightarrow> Pls < k"
   877   "Pls < Bit1 k \<longleftrightarrow> Pls \<le> k"
   878   "Min < Pls \<longleftrightarrow> True"
   879   "Min < Min \<longleftrightarrow> False"
   880   "Min < Bit0 k \<longleftrightarrow> Min < k"
   881   "Min < Bit1 k \<longleftrightarrow> Min < k"
   882   "Bit0 k < Pls \<longleftrightarrow> k < Pls"
   883   "Bit0 k < Min \<longleftrightarrow> k \<le> Min"
   884   "Bit1 k < Pls \<longleftrightarrow> k < Pls"
   885   "Bit1 k < Min \<longleftrightarrow> k < Min"
   886   "Bit0 k < Bit0 l \<longleftrightarrow> k < l"
   887   "Bit0 k < Bit1 l \<longleftrightarrow> k \<le> l"
   888   "Bit1 k < Bit0 l \<longleftrightarrow> k < l"
   889   "Bit1 k < Bit1 l \<longleftrightarrow> k < l"
   890   unfolding le_iff_pred_less
   891     less_bin_lemma [of Pls]
   892     less_bin_lemma [of Min]
   893     less_bin_lemma [of "k"]
   894     less_bin_lemma [of "Bit0 k"]
   895     less_bin_lemma [of "Bit1 k"]
   896     less_bin_lemma [of "pred Pls"]
   897     less_bin_lemma [of "pred k"]
   898   by (simp_all add: bin_less_0_simps succ_pred)
   899 
   900 text {* Less-than-or-equal *}
   901 
   902 lemma le_bin_simps [simp]:
   903   "Pls \<le> Pls \<longleftrightarrow> True"
   904   "Pls \<le> Min \<longleftrightarrow> False"
   905   "Pls \<le> Bit0 k \<longleftrightarrow> Pls \<le> k"
   906   "Pls \<le> Bit1 k \<longleftrightarrow> Pls \<le> k"
   907   "Min \<le> Pls \<longleftrightarrow> True"
   908   "Min \<le> Min \<longleftrightarrow> True"
   909   "Min \<le> Bit0 k \<longleftrightarrow> Min < k"
   910   "Min \<le> Bit1 k \<longleftrightarrow> Min \<le> k"
   911   "Bit0 k \<le> Pls \<longleftrightarrow> k \<le> Pls"
   912   "Bit0 k \<le> Min \<longleftrightarrow> k \<le> Min"
   913   "Bit1 k \<le> Pls \<longleftrightarrow> k < Pls"
   914   "Bit1 k \<le> Min \<longleftrightarrow> k \<le> Min"
   915   "Bit0 k \<le> Bit0 l \<longleftrightarrow> k \<le> l"
   916   "Bit0 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
   917   "Bit1 k \<le> Bit0 l \<longleftrightarrow> k < l"
   918   "Bit1 k \<le> Bit1 l \<longleftrightarrow> k \<le> l"
   919   unfolding not_less [symmetric]
   920   by (simp_all add: not_le)
   921 
   922 text {* Equality *}
   923 
   924 lemma eq_bin_simps [simp]:
   925   "Pls = Pls \<longleftrightarrow> True"
   926   "Pls = Min \<longleftrightarrow> False"
   927   "Pls = Bit0 l \<longleftrightarrow> Pls = l"
   928   "Pls = Bit1 l \<longleftrightarrow> False"
   929   "Min = Pls \<longleftrightarrow> False"
   930   "Min = Min \<longleftrightarrow> True"
   931   "Min = Bit0 l \<longleftrightarrow> False"
   932   "Min = Bit1 l \<longleftrightarrow> Min = l"
   933   "Bit0 k = Pls \<longleftrightarrow> k = Pls"
   934   "Bit0 k = Min \<longleftrightarrow> False"
   935   "Bit1 k = Pls \<longleftrightarrow> False"
   936   "Bit1 k = Min \<longleftrightarrow> k = Min"
   937   "Bit0 k = Bit0 l \<longleftrightarrow> k = l"
   938   "Bit0 k = Bit1 l \<longleftrightarrow> False"
   939   "Bit1 k = Bit0 l \<longleftrightarrow> False"
   940   "Bit1 k = Bit1 l \<longleftrightarrow> k = l"
   941   unfolding order_eq_iff [where 'a=int]
   942   by (simp_all add: not_less)
   943 
   944 
   945 subsection {* Converting Numerals to Rings: @{term number_of} *}
   946 
   947 class number_ring = number + comm_ring_1 +
   948   assumes number_of_eq: "number_of k = of_int k"
   949 
   950 text {* self-embedding of the integers *}
   951 
   952 instantiation int :: number_ring
   953 begin
   954 
   955 definition int_number_of_def [code del]:
   956   "number_of w = (of_int w \<Colon> int)"
   957 
   958 instance proof
   959 qed (simp only: int_number_of_def)
   960 
   961 end
   962 
   963 lemma number_of_is_id:
   964   "number_of (k::int) = k"
   965   unfolding int_number_of_def by simp
   966 
   967 lemma number_of_succ:
   968   "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
   969   unfolding number_of_eq numeral_simps by simp
   970 
   971 lemma number_of_pred:
   972   "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
   973   unfolding number_of_eq numeral_simps by simp
   974 
   975 lemma number_of_minus:
   976   "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
   977   unfolding number_of_eq by (rule of_int_minus)
   978 
   979 lemma number_of_add:
   980   "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
   981   unfolding number_of_eq by (rule of_int_add)
   982 
   983 lemma number_of_diff:
   984   "number_of (v - w) = (number_of v - number_of w::'a::number_ring)"
   985   unfolding number_of_eq by (rule of_int_diff)
   986 
   987 lemma number_of_mult:
   988   "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
   989   unfolding number_of_eq by (rule of_int_mult)
   990 
   991 text {*
   992   The correctness of shifting.
   993   But it doesn't seem to give a measurable speed-up.
   994 *}
   995 
   996 lemma double_number_of_Bit0:
   997   "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)"
   998   unfolding number_of_eq numeral_simps left_distrib by simp
   999 
  1000 text {*
  1001   Converting numerals 0 and 1 to their abstract versions.
  1002 *}
  1003 
  1004 lemma numeral_0_eq_0 [simp, code_post]:
  1005   "Numeral0 = (0::'a::number_ring)"
  1006   unfolding number_of_eq numeral_simps by simp
  1007 
  1008 lemma numeral_1_eq_1 [simp, code_post]:
  1009   "Numeral1 = (1::'a::number_ring)"
  1010   unfolding number_of_eq numeral_simps by simp
  1011 
  1012 text {*
  1013   Special-case simplification for small constants.
  1014 *}
  1015 
  1016 text{*
  1017   Unary minus for the abstract constant 1. Cannot be inserted
  1018   as a simprule until later: it is @{text number_of_Min} re-oriented!
  1019 *}
  1020 
  1021 lemma numeral_m1_eq_minus_1:
  1022   "(-1::'a::number_ring) = - 1"
  1023   unfolding number_of_eq numeral_simps by simp
  1024 
  1025 lemma mult_minus1 [simp]:
  1026   "-1 * z = -(z::'a::number_ring)"
  1027   unfolding number_of_eq numeral_simps by simp
  1028 
  1029 lemma mult_minus1_right [simp]:
  1030   "z * -1 = -(z::'a::number_ring)"
  1031   unfolding number_of_eq numeral_simps by simp
  1032 
  1033 (*Negation of a coefficient*)
  1034 lemma minus_number_of_mult [simp]:
  1035    "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
  1036    unfolding number_of_eq by simp
  1037 
  1038 text {* Subtraction *}
  1039 
  1040 lemma diff_number_of_eq:
  1041   "number_of v - number_of w =
  1042     (number_of (v + uminus w)::'a::number_ring)"
  1043   unfolding number_of_eq by simp
  1044 
  1045 lemma number_of_Pls:
  1046   "number_of Pls = (0::'a::number_ring)"
  1047   unfolding number_of_eq numeral_simps by simp
  1048 
  1049 lemma number_of_Min:
  1050   "number_of Min = (- 1::'a::number_ring)"
  1051   unfolding number_of_eq numeral_simps by simp
  1052 
  1053 lemma number_of_Bit0:
  1054   "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)"
  1055   unfolding number_of_eq numeral_simps by simp
  1056 
  1057 lemma number_of_Bit1:
  1058   "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)"
  1059   unfolding number_of_eq numeral_simps by simp
  1060 
  1061 
  1062 subsubsection {* Equality of Binary Numbers *}
  1063 
  1064 text {* First version by Norbert Voelker *}
  1065 
  1066 definition (*for simplifying equalities*) iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool" where
  1067   "iszero z \<longleftrightarrow> z = 0"
  1068 
  1069 lemma iszero_0: "iszero 0"
  1070   by (simp add: iszero_def)
  1071 
  1072 lemma iszero_Numeral0: "iszero (Numeral0 :: 'a::number_ring)"
  1073   by (simp add: iszero_0)
  1074 
  1075 lemma not_iszero_1: "\<not> iszero 1"
  1076   by (simp add: iszero_def)
  1077 
  1078 lemma not_iszero_Numeral1: "\<not> iszero (Numeral1 :: 'a::number_ring)"
  1079   by (simp add: not_iszero_1)
  1080 
  1081 lemma eq_number_of_eq [simp]:
  1082   "((number_of x::'a::number_ring) = number_of y) =
  1083      iszero (number_of (x + uminus y) :: 'a)"
  1084 unfolding iszero_def number_of_add number_of_minus
  1085 by (simp add: algebra_simps)
  1086 
  1087 lemma iszero_number_of_Pls:
  1088   "iszero ((number_of Pls)::'a::number_ring)"
  1089 unfolding iszero_def numeral_0_eq_0 ..
  1090 
  1091 lemma nonzero_number_of_Min:
  1092   "~ iszero ((number_of Min)::'a::number_ring)"
  1093 unfolding iszero_def numeral_m1_eq_minus_1 by simp
  1094 
  1095 
  1096 subsubsection {* Comparisons, for Ordered Rings *}
  1097 
  1098 lemmas double_eq_0_iff = double_zero
  1099 
  1100 lemma odd_nonzero:
  1101   "1 + z + z \<noteq> (0::int)"
  1102 proof (cases z rule: int_cases)
  1103   case (nonneg n)
  1104   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
  1105   thus ?thesis using  le_imp_0_less [OF le]
  1106     by (auto simp add: add_assoc) 
  1107 next
  1108   case (neg n)
  1109   show ?thesis
  1110   proof
  1111     assume eq: "1 + z + z = 0"
  1112     have "(0::int) < 1 + (of_nat n + of_nat n)"
  1113       by (simp add: le_imp_0_less add_increasing) 
  1114     also have "... = - (1 + z + z)" 
  1115       by (simp add: neg add_assoc [symmetric]) 
  1116     also have "... = 0" by (simp add: eq) 
  1117     finally have "0<0" ..
  1118     thus False by blast
  1119   qed
  1120 qed
  1121 
  1122 lemma iszero_number_of_Bit0:
  1123   "iszero (number_of (Bit0 w)::'a) = 
  1124    iszero (number_of w::'a::{ring_char_0,number_ring})"
  1125 proof -
  1126   have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)"
  1127   proof -
  1128     assume eq: "of_int w + of_int w = (0::'a)"
  1129     then have "of_int (w + w) = (of_int 0 :: 'a)" by simp
  1130     then have "w + w = 0" by (simp only: of_int_eq_iff)
  1131     then show "w = 0" by (simp only: double_eq_0_iff)
  1132   qed
  1133   thus ?thesis
  1134     by (auto simp add: iszero_def number_of_eq numeral_simps)
  1135 qed
  1136 
  1137 lemma iszero_number_of_Bit1:
  1138   "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})"
  1139 proof -
  1140   have "1 + of_int w + of_int w \<noteq> (0::'a)"
  1141   proof
  1142     assume eq: "1 + of_int w + of_int w = (0::'a)"
  1143     hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp 
  1144     hence "1 + w + w = 0" by (simp only: of_int_eq_iff)
  1145     with odd_nonzero show False by blast
  1146   qed
  1147   thus ?thesis
  1148     by (auto simp add: iszero_def number_of_eq numeral_simps)
  1149 qed
  1150 
  1151 lemmas iszero_simps [simp] =
  1152   iszero_0 not_iszero_1
  1153   iszero_number_of_Pls nonzero_number_of_Min
  1154   iszero_number_of_Bit0 iszero_number_of_Bit1
  1155 (* iszero_number_of_Pls would never normally be used
  1156    because its lhs simplifies to "iszero 0" *)
  1157 
  1158 subsubsection {* The Less-Than Relation *}
  1159 
  1160 lemma double_less_0_iff:
  1161   "(a + a < 0) = (a < (0::'a::linordered_idom))"
  1162 proof -
  1163   have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
  1164   also have "... = (a < 0)"
  1165     by (simp add: mult_less_0_iff zero_less_two 
  1166                   order_less_not_sym [OF zero_less_two]) 
  1167   finally show ?thesis .
  1168 qed
  1169 
  1170 lemma odd_less_0:
  1171   "(1 + z + z < 0) = (z < (0::int))"
  1172 proof (cases z rule: int_cases)
  1173   case (nonneg n)
  1174   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
  1175                              le_imp_0_less [THEN order_less_imp_le])  
  1176 next
  1177   case (neg n)
  1178   thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
  1179     add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
  1180 qed
  1181 
  1182 text {* Less-Than or Equals *}
  1183 
  1184 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
  1185 
  1186 lemmas le_number_of_eq_not_less =
  1187   linorder_not_less [of "number_of w" "number_of v", symmetric, 
  1188   standard]
  1189 
  1190 
  1191 text {* Absolute value (@{term abs}) *}
  1192 
  1193 lemma abs_number_of:
  1194   "abs(number_of x::'a::{linordered_idom,number_ring}) =
  1195    (if number_of x < (0::'a) then -number_of x else number_of x)"
  1196   by (simp add: abs_if)
  1197 
  1198 
  1199 text {* Re-orientation of the equation nnn=x *}
  1200 
  1201 lemma number_of_reorient:
  1202   "(number_of w = x) = (x = number_of w)"
  1203   by auto
  1204 
  1205 
  1206 subsubsection {* Simplification of arithmetic operations on integer constants. *}
  1207 
  1208 lemmas arith_extra_simps [standard, simp] =
  1209   number_of_add [symmetric]
  1210   number_of_minus [symmetric]
  1211   numeral_m1_eq_minus_1 [symmetric]
  1212   number_of_mult [symmetric]
  1213   diff_number_of_eq abs_number_of 
  1214 
  1215 text {*
  1216   For making a minimal simpset, one must include these default simprules.
  1217   Also include @{text simp_thms}.
  1218 *}
  1219 
  1220 lemmas arith_simps = 
  1221   normalize_bin_simps pred_bin_simps succ_bin_simps
  1222   add_bin_simps minus_bin_simps mult_bin_simps
  1223   abs_zero abs_one arith_extra_simps
  1224 
  1225 text {* Simplification of relational operations *}
  1226 
  1227 lemma less_number_of [simp]:
  1228   "(number_of x::'a::{linordered_idom,number_ring}) < number_of y \<longleftrightarrow> x < y"
  1229   unfolding number_of_eq by (rule of_int_less_iff)
  1230 
  1231 lemma le_number_of [simp]:
  1232   "(number_of x::'a::{linordered_idom,number_ring}) \<le> number_of y \<longleftrightarrow> x \<le> y"
  1233   unfolding number_of_eq by (rule of_int_le_iff)
  1234 
  1235 lemma eq_number_of [simp]:
  1236   "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \<longleftrightarrow> x = y"
  1237   unfolding number_of_eq by (rule of_int_eq_iff)
  1238 
  1239 lemmas rel_simps =
  1240   less_number_of less_bin_simps
  1241   le_number_of le_bin_simps
  1242   eq_number_of_eq eq_bin_simps
  1243   iszero_simps
  1244 
  1245 
  1246 subsubsection {* Simplification of arithmetic when nested to the right. *}
  1247 
  1248 lemma add_number_of_left [simp]:
  1249   "number_of v + (number_of w + z) =
  1250    (number_of(v + w) + z::'a::number_ring)"
  1251   by (simp add: add_assoc [symmetric])
  1252 
  1253 lemma mult_number_of_left [simp]:
  1254   "number_of v * (number_of w * z) =
  1255    (number_of(v * w) * z::'a::number_ring)"
  1256   by (simp add: mult_assoc [symmetric])
  1257 
  1258 lemma add_number_of_diff1:
  1259   "number_of v + (number_of w - c) = 
  1260   number_of(v + w) - (c::'a::number_ring)"
  1261   by (simp add: diff_minus)
  1262 
  1263 lemma add_number_of_diff2 [simp]:
  1264   "number_of v + (c - number_of w) =
  1265    number_of (v + uminus w) + (c::'a::number_ring)"
  1266 by (simp add: algebra_simps diff_number_of_eq [symmetric])
  1267 
  1268 
  1269 
  1270 
  1271 subsection {* The Set of Integers *}
  1272 
  1273 context ring_1
  1274 begin
  1275 
  1276 definition Ints  :: "'a set" where
  1277   [code del]: "Ints = range of_int"
  1278 
  1279 notation (xsymbols)
  1280   Ints  ("\<int>")
  1281 
  1282 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
  1283   by (simp add: Ints_def)
  1284 
  1285 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
  1286 apply (simp add: Ints_def)
  1287 apply (rule range_eqI)
  1288 apply (rule of_int_of_nat_eq [symmetric])
  1289 done
  1290 
  1291 lemma Ints_0 [simp]: "0 \<in> \<int>"
  1292 apply (simp add: Ints_def)
  1293 apply (rule range_eqI)
  1294 apply (rule of_int_0 [symmetric])
  1295 done
  1296 
  1297 lemma Ints_1 [simp]: "1 \<in> \<int>"
  1298 apply (simp add: Ints_def)
  1299 apply (rule range_eqI)
  1300 apply (rule of_int_1 [symmetric])
  1301 done
  1302 
  1303 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
  1304 apply (auto simp add: Ints_def)
  1305 apply (rule range_eqI)
  1306 apply (rule of_int_add [symmetric])
  1307 done
  1308 
  1309 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
  1310 apply (auto simp add: Ints_def)
  1311 apply (rule range_eqI)
  1312 apply (rule of_int_minus [symmetric])
  1313 done
  1314 
  1315 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
  1316 apply (auto simp add: Ints_def)
  1317 apply (rule range_eqI)
  1318 apply (rule of_int_diff [symmetric])
  1319 done
  1320 
  1321 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
  1322 apply (auto simp add: Ints_def)
  1323 apply (rule range_eqI)
  1324 apply (rule of_int_mult [symmetric])
  1325 done
  1326 
  1327 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
  1328 by (induct n) simp_all
  1329 
  1330 lemma Ints_cases [cases set: Ints]:
  1331   assumes "q \<in> \<int>"
  1332   obtains (of_int) z where "q = of_int z"
  1333   unfolding Ints_def
  1334 proof -
  1335   from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
  1336   then obtain z where "q = of_int z" ..
  1337   then show thesis ..
  1338 qed
  1339 
  1340 lemma Ints_induct [case_names of_int, induct set: Ints]:
  1341   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
  1342   by (rule Ints_cases) auto
  1343 
  1344 end
  1345 
  1346 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
  1347 
  1348 lemma Ints_double_eq_0_iff:
  1349   assumes in_Ints: "a \<in> Ints"
  1350   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
  1351 proof -
  1352   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  1353   then obtain z where a: "a = of_int z" ..
  1354   show ?thesis
  1355   proof
  1356     assume "a = 0"
  1357     thus "a + a = 0" by simp
  1358   next
  1359     assume eq: "a + a = 0"
  1360     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
  1361     hence "z + z = 0" by (simp only: of_int_eq_iff)
  1362     hence "z = 0" by (simp only: double_eq_0_iff)
  1363     thus "a = 0" by (simp add: a)
  1364   qed
  1365 qed
  1366 
  1367 lemma Ints_odd_nonzero:
  1368   assumes in_Ints: "a \<in> Ints"
  1369   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
  1370 proof -
  1371   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  1372   then obtain z where a: "a = of_int z" ..
  1373   show ?thesis
  1374   proof
  1375     assume eq: "1 + a + a = 0"
  1376     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
  1377     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
  1378     with odd_nonzero show False by blast
  1379   qed
  1380 qed 
  1381 
  1382 lemma Ints_number_of [simp]:
  1383   "(number_of w :: 'a::number_ring) \<in> Ints"
  1384   unfolding number_of_eq Ints_def by simp
  1385 
  1386 lemma Nats_number_of [simp]:
  1387   "Int.Pls \<le> w \<Longrightarrow> (number_of w :: 'a::number_ring) \<in> Nats"
  1388 unfolding Int.Pls_def number_of_eq
  1389 by (simp only: of_nat_nat [symmetric] of_nat_in_Nats)
  1390 
  1391 lemma Ints_odd_less_0: 
  1392   assumes in_Ints: "a \<in> Ints"
  1393   shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
  1394 proof -
  1395   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  1396   then obtain z where a: "a = of_int z" ..
  1397   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
  1398     by (simp add: a)
  1399   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
  1400   also have "... = (a < 0)" by (simp add: a)
  1401   finally show ?thesis .
  1402 qed
  1403 
  1404 
  1405 subsection {* @{term setsum} and @{term setprod} *}
  1406 
  1407 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
  1408   apply (cases "finite A")
  1409   apply (erule finite_induct, auto)
  1410   done
  1411 
  1412 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
  1413   apply (cases "finite A")
  1414   apply (erule finite_induct, auto)
  1415   done
  1416 
  1417 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
  1418   apply (cases "finite A")
  1419   apply (erule finite_induct, auto simp add: of_nat_mult)
  1420   done
  1421 
  1422 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
  1423   apply (cases "finite A")
  1424   apply (erule finite_induct, auto)
  1425   done
  1426 
  1427 lemmas int_setsum = of_nat_setsum [where 'a=int]
  1428 lemmas int_setprod = of_nat_setprod [where 'a=int]
  1429 
  1430 
  1431 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
  1432 
  1433 lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
  1434 by simp 
  1435 
  1436 lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
  1437 by simp
  1438 
  1439 lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
  1440 by simp 
  1441 
  1442 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
  1443 by simp
  1444 
  1445 lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
  1446 by simp
  1447 
  1448 lemma inverse_numeral_1:
  1449   "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
  1450 by simp
  1451 
  1452 text{*Theorem lists for the cancellation simprocs. The use of binary numerals
  1453 for 0 and 1 reduces the number of special cases.*}
  1454 
  1455 lemmas add_0s = add_numeral_0 add_numeral_0_right
  1456 lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
  1457                  mult_minus1 mult_minus1_right
  1458 
  1459 
  1460 subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
  1461 
  1462 text{*Arithmetic computations are defined for binary literals, which leaves 0
  1463 and 1 as special cases. Addition already has rules for 0, but not 1.
  1464 Multiplication and unary minus already have rules for both 0 and 1.*}
  1465 
  1466 
  1467 lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
  1468 by simp
  1469 
  1470 
  1471 lemmas add_number_of_eq = number_of_add [symmetric]
  1472 
  1473 text{*Allow 1 on either or both sides*}
  1474 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
  1475 by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric])
  1476 
  1477 lemmas add_special =
  1478     one_add_one_is_two
  1479     binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
  1480     binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
  1481 
  1482 text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
  1483 lemmas diff_special =
  1484     binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
  1485     binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
  1486 
  1487 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1488 lemmas eq_special =
  1489     binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
  1490     binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
  1491     binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
  1492     binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
  1493 
  1494 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1495 lemmas less_special =
  1496   binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard]
  1497   binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard]
  1498   binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard]
  1499   binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard]
  1500 
  1501 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1502 lemmas le_special =
  1503     binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard]
  1504     binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard]
  1505     binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard]
  1506     binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard]
  1507 
  1508 lemmas arith_special[simp] = 
  1509        add_special diff_special eq_special less_special le_special
  1510 
  1511 
  1512 text {* Legacy theorems *}
  1513 
  1514 lemmas zle_int = of_nat_le_iff [where 'a=int]
  1515 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
  1516 
  1517 subsection {* Setting up simplification procedures *}
  1518 
  1519 lemmas int_arith_rules =
  1520   neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
  1521   minus_zero diff_minus left_minus right_minus
  1522   mult_zero_left mult_zero_right mult_Bit1 mult_1_left mult_1_right
  1523   mult_minus_left mult_minus_right
  1524   minus_add_distrib minus_minus mult_assoc
  1525   of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
  1526   of_int_0 of_int_1 of_int_add of_int_mult
  1527 
  1528 use "Tools/int_arith.ML"
  1529 setup {* Int_Arith.global_setup *}
  1530 declaration {* K Int_Arith.setup *}
  1531 
  1532 setup {*
  1533   Reorient_Proc.add
  1534     (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
  1535 *}
  1536 
  1537 simproc_setup reorient_numeral ("number_of w = x") = Reorient_Proc.proc
  1538 
  1539 
  1540 subsection{*Lemmas About Small Numerals*}
  1541 
  1542 lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
  1543 proof -
  1544   have "(of_int -1 :: 'a) = of_int (- 1)" by simp
  1545   also have "... = - of_int 1" by (simp only: of_int_minus)
  1546   also have "... = -1" by simp
  1547   finally show ?thesis .
  1548 qed
  1549 
  1550 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{linordered_idom,number_ring})"
  1551 by (simp add: abs_if)
  1552 
  1553 lemma abs_power_minus_one [simp]:
  1554   "abs(-1 ^ n) = (1::'a::{linordered_idom,number_ring})"
  1555 by (simp add: power_abs)
  1556 
  1557 lemma of_int_number_of_eq [simp]:
  1558      "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
  1559 by (simp add: number_of_eq) 
  1560 
  1561 text{*Lemmas for specialist use, NOT as default simprules*}
  1562 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
  1563 unfolding one_add_one_is_two [symmetric] left_distrib by simp
  1564 
  1565 lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
  1566 by (subst mult_commute, rule mult_2)
  1567 
  1568 
  1569 subsection{*More Inequality Reasoning*}
  1570 
  1571 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
  1572 by arith
  1573 
  1574 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
  1575 by arith
  1576 
  1577 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
  1578 by arith
  1579 
  1580 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
  1581 by arith
  1582 
  1583 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
  1584 by arith
  1585 
  1586 
  1587 subsection{*The functions @{term nat} and @{term int}*}
  1588 
  1589 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
  1590   @{term "w + - z"}*}
  1591 declare Zero_int_def [symmetric, simp]
  1592 declare One_int_def [symmetric, simp]
  1593 
  1594 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
  1595 
  1596 (* FIXME: duplicates nat_zero *)
  1597 lemma nat_0: "nat 0 = 0"
  1598 by (simp add: nat_eq_iff)
  1599 
  1600 lemma nat_1: "nat 1 = Suc 0"
  1601 by (subst nat_eq_iff, simp)
  1602 
  1603 lemma nat_2: "nat 2 = Suc (Suc 0)"
  1604 by (subst nat_eq_iff, simp)
  1605 
  1606 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
  1607 apply (insert zless_nat_conj [of 1 z])
  1608 apply (auto simp add: nat_1)
  1609 done
  1610 
  1611 text{*This simplifies expressions of the form @{term "int n = z"} where
  1612       z is an integer literal.*}
  1613 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
  1614 
  1615 lemma split_nat [arith_split]:
  1616   "P(nat(i::int)) = ((\<forall>n. i = of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
  1617   (is "?P = (?L & ?R)")
  1618 proof (cases "i < 0")
  1619   case True thus ?thesis by auto
  1620 next
  1621   case False
  1622   have "?P = ?L"
  1623   proof
  1624     assume ?P thus ?L using False by clarsimp
  1625   next
  1626     assume ?L thus ?P using False by simp
  1627   qed
  1628   with False show ?thesis by simp
  1629 qed
  1630 
  1631 context ring_1
  1632 begin
  1633 
  1634 lemma of_int_of_nat [nitpick_simp]:
  1635   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
  1636 proof (cases "k < 0")
  1637   case True then have "0 \<le> - k" by simp
  1638   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
  1639   with True show ?thesis by simp
  1640 next
  1641   case False then show ?thesis by (simp add: not_less of_nat_nat)
  1642 qed
  1643 
  1644 end
  1645 
  1646 lemma nat_mult_distrib:
  1647   fixes z z' :: int
  1648   assumes "0 \<le> z"
  1649   shows "nat (z * z') = nat z * nat z'"
  1650 proof (cases "0 \<le> z'")
  1651   case False with assms have "z * z' \<le> 0"
  1652     by (simp add: not_le mult_le_0_iff)
  1653   then have "nat (z * z') = 0" by simp
  1654   moreover from False have "nat z' = 0" by simp
  1655   ultimately show ?thesis by simp
  1656 next
  1657   case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
  1658   show ?thesis
  1659     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
  1660       (simp only: of_nat_mult of_nat_nat [OF True]
  1661          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
  1662 qed
  1663 
  1664 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
  1665 apply (rule trans)
  1666 apply (rule_tac [2] nat_mult_distrib, auto)
  1667 done
  1668 
  1669 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
  1670 apply (cases "z=0 | w=0")
  1671 apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
  1672                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
  1673 done
  1674 
  1675 
  1676 subsection "Induction principles for int"
  1677 
  1678 text{*Well-founded segments of the integers*}
  1679 
  1680 definition
  1681   int_ge_less_than  ::  "int => (int * int) set"
  1682 where
  1683   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
  1684 
  1685 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
  1686 proof -
  1687   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
  1688     by (auto simp add: int_ge_less_than_def)
  1689   thus ?thesis 
  1690     by (rule wf_subset [OF wf_measure]) 
  1691 qed
  1692 
  1693 text{*This variant looks odd, but is typical of the relations suggested
  1694 by RankFinder.*}
  1695 
  1696 definition
  1697   int_ge_less_than2 ::  "int => (int * int) set"
  1698 where
  1699   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
  1700 
  1701 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
  1702 proof -
  1703   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))" 
  1704     by (auto simp add: int_ge_less_than2_def)
  1705   thus ?thesis 
  1706     by (rule wf_subset [OF wf_measure]) 
  1707 qed
  1708 
  1709 abbreviation
  1710   int :: "nat \<Rightarrow> int"
  1711 where
  1712   "int \<equiv> of_nat"
  1713 
  1714 (* `set:int': dummy construction *)
  1715 theorem int_ge_induct [case_names base step, induct set: int]:
  1716   fixes i :: int
  1717   assumes ge: "k \<le> i" and
  1718     base: "P k" and
  1719     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
  1720   shows "P i"
  1721 proof -
  1722   { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
  1723     proof (induct n)
  1724       case 0
  1725       hence "i = k" by arith
  1726       thus "P i" using base by simp
  1727     next
  1728       case (Suc n)
  1729       then have "n = nat((i - 1) - k)" by arith
  1730       moreover
  1731       have ki1: "k \<le> i - 1" using Suc.prems by arith
  1732       ultimately
  1733       have "P(i - 1)" by(rule Suc.hyps)
  1734       from step[OF ki1 this] show ?case by simp
  1735     qed
  1736   }
  1737   with ge show ?thesis by fast
  1738 qed
  1739 
  1740 (* `set:int': dummy construction *)
  1741 theorem int_gr_induct [case_names base step, induct set: int]:
  1742   assumes gr: "k < (i::int)" and
  1743         base: "P(k+1)" and
  1744         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
  1745   shows "P i"
  1746 apply(rule int_ge_induct[of "k + 1"])
  1747   using gr apply arith
  1748  apply(rule base)
  1749 apply (rule step, simp+)
  1750 done
  1751 
  1752 theorem int_le_induct[consumes 1,case_names base step]:
  1753   assumes le: "i \<le> (k::int)" and
  1754         base: "P(k)" and
  1755         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
  1756   shows "P i"
  1757 proof -
  1758   { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
  1759     proof (induct n)
  1760       case 0
  1761       hence "i = k" by arith
  1762       thus "P i" using base by simp
  1763     next
  1764       case (Suc n)
  1765       hence "n = nat(k - (i+1))" by arith
  1766       moreover
  1767       have ki1: "i + 1 \<le> k" using Suc.prems by arith
  1768       ultimately
  1769       have "P(i+1)" by(rule Suc.hyps)
  1770       from step[OF ki1 this] show ?case by simp
  1771     qed
  1772   }
  1773   with le show ?thesis by fast
  1774 qed
  1775 
  1776 theorem int_less_induct [consumes 1,case_names base step]:
  1777   assumes less: "(i::int) < k" and
  1778         base: "P(k - 1)" and
  1779         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
  1780   shows "P i"
  1781 apply(rule int_le_induct[of _ "k - 1"])
  1782   using less apply arith
  1783  apply(rule base)
  1784 apply (rule step, simp+)
  1785 done
  1786 
  1787 theorem int_induct [case_names base step1 step2]:
  1788   fixes k :: int
  1789   assumes base: "P k"
  1790     and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
  1791     and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
  1792   shows "P i"
  1793 proof -
  1794   have "i \<le> k \<or> i \<ge> k" by arith
  1795   then show ?thesis proof
  1796     assume "i \<ge> k" then show ?thesis using base
  1797       by (rule int_ge_induct) (fact step1)
  1798   next
  1799     assume "i \<le> k" then show ?thesis using base
  1800       by (rule int_le_induct) (fact step2)
  1801   qed
  1802 qed
  1803 
  1804 subsection{*Intermediate value theorems*}
  1805 
  1806 lemma int_val_lemma:
  1807      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
  1808       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
  1809 unfolding One_nat_def
  1810 apply (induct n, simp)
  1811 apply (intro strip)
  1812 apply (erule impE, simp)
  1813 apply (erule_tac x = n in allE, simp)
  1814 apply (case_tac "k = f (Suc n)")
  1815 apply force
  1816 apply (erule impE)
  1817  apply (simp add: abs_if split add: split_if_asm)
  1818 apply (blast intro: le_SucI)
  1819 done
  1820 
  1821 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
  1822 
  1823 lemma nat_intermed_int_val:
  1824      "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
  1825          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
  1826 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
  1827        in int_val_lemma)
  1828 unfolding One_nat_def
  1829 apply simp
  1830 apply (erule exE)
  1831 apply (rule_tac x = "i+m" in exI, arith)
  1832 done
  1833 
  1834 
  1835 subsection{*Products and 1, by T. M. Rasmussen*}
  1836 
  1837 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
  1838 by arith
  1839 
  1840 lemma abs_zmult_eq_1:
  1841   assumes mn: "\<bar>m * n\<bar> = 1"
  1842   shows "\<bar>m\<bar> = (1::int)"
  1843 proof -
  1844   have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
  1845     by auto
  1846   have "~ (2 \<le> \<bar>m\<bar>)"
  1847   proof
  1848     assume "2 \<le> \<bar>m\<bar>"
  1849     hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
  1850       by (simp add: mult_mono 0) 
  1851     also have "... = \<bar>m*n\<bar>" 
  1852       by (simp add: abs_mult)
  1853     also have "... = 1"
  1854       by (simp add: mn)
  1855     finally have "2*\<bar>n\<bar> \<le> 1" .
  1856     thus "False" using 0
  1857       by auto
  1858   qed
  1859   thus ?thesis using 0
  1860     by auto
  1861 qed
  1862 
  1863 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
  1864 by (insert abs_zmult_eq_1 [of m n], arith)
  1865 
  1866 lemma pos_zmult_eq_1_iff:
  1867   assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
  1868 proof -
  1869   from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
  1870   thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
  1871 qed
  1872 
  1873 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
  1874 apply (rule iffI) 
  1875  apply (frule pos_zmult_eq_1_iff_lemma)
  1876  apply (simp add: mult_commute [of m]) 
  1877  apply (frule pos_zmult_eq_1_iff_lemma, auto) 
  1878 done
  1879 
  1880 lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
  1881 proof
  1882   assume "finite (UNIV::int set)"
  1883   moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
  1884     by (rule injI) simp
  1885   ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
  1886     by (rule finite_UNIV_inj_surj)
  1887   then obtain i :: int where "1 = 2 * i" by (rule surjE)
  1888   then show False by (simp add: pos_zmult_eq_1_iff)
  1889 qed
  1890 
  1891 
  1892 subsection {* Further theorems on numerals *}
  1893 
  1894 subsubsection{*Special Simplification for Constants*}
  1895 
  1896 text{*These distributive laws move literals inside sums and differences.*}
  1897 
  1898 lemmas left_distrib_number_of [simp] =
  1899   left_distrib [of _ _ "number_of v", standard]
  1900 
  1901 lemmas right_distrib_number_of [simp] =
  1902   right_distrib [of "number_of v", standard]
  1903 
  1904 lemmas left_diff_distrib_number_of [simp] =
  1905   left_diff_distrib [of _ _ "number_of v", standard]
  1906 
  1907 lemmas right_diff_distrib_number_of [simp] =
  1908   right_diff_distrib [of "number_of v", standard]
  1909 
  1910 text{*These are actually for fields, like real: but where else to put them?*}
  1911 
  1912 lemmas zero_less_divide_iff_number_of [simp, no_atp] =
  1913   zero_less_divide_iff [of "number_of w", standard]
  1914 
  1915 lemmas divide_less_0_iff_number_of [simp, no_atp] =
  1916   divide_less_0_iff [of "number_of w", standard]
  1917 
  1918 lemmas zero_le_divide_iff_number_of [simp, no_atp] =
  1919   zero_le_divide_iff [of "number_of w", standard]
  1920 
  1921 lemmas divide_le_0_iff_number_of [simp, no_atp] =
  1922   divide_le_0_iff [of "number_of w", standard]
  1923 
  1924 
  1925 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
  1926   strange, but then other simprocs simplify the quotient.*}
  1927 
  1928 lemmas inverse_eq_divide_number_of [simp] =
  1929   inverse_eq_divide [of "number_of w", standard]
  1930 
  1931 text {*These laws simplify inequalities, moving unary minus from a term
  1932 into the literal.*}
  1933 
  1934 lemmas less_minus_iff_number_of [simp, no_atp] =
  1935   less_minus_iff [of "number_of v", standard]
  1936 
  1937 lemmas le_minus_iff_number_of [simp, no_atp] =
  1938   le_minus_iff [of "number_of v", standard]
  1939 
  1940 lemmas equation_minus_iff_number_of [simp, no_atp] =
  1941   equation_minus_iff [of "number_of v", standard]
  1942 
  1943 lemmas minus_less_iff_number_of [simp, no_atp] =
  1944   minus_less_iff [of _ "number_of v", standard]
  1945 
  1946 lemmas minus_le_iff_number_of [simp, no_atp] =
  1947   minus_le_iff [of _ "number_of v", standard]
  1948 
  1949 lemmas minus_equation_iff_number_of [simp, no_atp] =
  1950   minus_equation_iff [of _ "number_of v", standard]
  1951 
  1952 
  1953 text{*To Simplify Inequalities Where One Side is the Constant 1*}
  1954 
  1955 lemma less_minus_iff_1 [simp,no_atp]:
  1956   fixes b::"'b::{linordered_idom,number_ring}"
  1957   shows "(1 < - b) = (b < -1)"
  1958 by auto
  1959 
  1960 lemma le_minus_iff_1 [simp,no_atp]:
  1961   fixes b::"'b::{linordered_idom,number_ring}"
  1962   shows "(1 \<le> - b) = (b \<le> -1)"
  1963 by auto
  1964 
  1965 lemma equation_minus_iff_1 [simp,no_atp]:
  1966   fixes b::"'b::number_ring"
  1967   shows "(1 = - b) = (b = -1)"
  1968 by (subst equation_minus_iff, auto)
  1969 
  1970 lemma minus_less_iff_1 [simp,no_atp]:
  1971   fixes a::"'b::{linordered_idom,number_ring}"
  1972   shows "(- a < 1) = (-1 < a)"
  1973 by auto
  1974 
  1975 lemma minus_le_iff_1 [simp,no_atp]:
  1976   fixes a::"'b::{linordered_idom,number_ring}"
  1977   shows "(- a \<le> 1) = (-1 \<le> a)"
  1978 by auto
  1979 
  1980 lemma minus_equation_iff_1 [simp,no_atp]:
  1981   fixes a::"'b::number_ring"
  1982   shows "(- a = 1) = (a = -1)"
  1983 by (subst minus_equation_iff, auto)
  1984 
  1985 
  1986 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
  1987 
  1988 lemmas mult_less_cancel_left_number_of [simp, no_atp] =
  1989   mult_less_cancel_left [of "number_of v", standard]
  1990 
  1991 lemmas mult_less_cancel_right_number_of [simp, no_atp] =
  1992   mult_less_cancel_right [of _ "number_of v", standard]
  1993 
  1994 lemmas mult_le_cancel_left_number_of [simp, no_atp] =
  1995   mult_le_cancel_left [of "number_of v", standard]
  1996 
  1997 lemmas mult_le_cancel_right_number_of [simp, no_atp] =
  1998   mult_le_cancel_right [of _ "number_of v", standard]
  1999 
  2000 
  2001 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
  2002 
  2003 lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
  2004 lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
  2005 lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
  2006 lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
  2007 lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
  2008 lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
  2009 
  2010 
  2011 subsubsection{*Optional Simplification Rules Involving Constants*}
  2012 
  2013 text{*Simplify quotients that are compared with a literal constant.*}
  2014 
  2015 lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
  2016 lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
  2017 lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
  2018 lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
  2019 lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
  2020 lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
  2021 
  2022 
  2023 text{*Not good as automatic simprules because they cause case splits.*}
  2024 lemmas divide_const_simps =
  2025   le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
  2026   divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
  2027   le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
  2028 
  2029 text{*Division By @{text "-1"}*}
  2030 
  2031 lemma divide_minus1 [simp]:
  2032      "x/-1 = -(x::'a::{field_inverse_zero, number_ring})"
  2033 by simp
  2034 
  2035 lemma minus1_divide [simp]:
  2036      "-1 / (x::'a::{field_inverse_zero, number_ring}) = - (1/x)"
  2037 by (simp add: divide_inverse)
  2038 
  2039 lemma half_gt_zero_iff:
  2040      "(0 < r/2) = (0 < (r::'a::{linordered_field_inverse_zero,number_ring}))"
  2041 by auto
  2042 
  2043 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
  2044 
  2045 lemma divide_Numeral1:
  2046   "(x::'a::{field, number_ring}) / Numeral1 = x"
  2047   by simp
  2048 
  2049 lemma divide_Numeral0:
  2050   "(x::'a::{field_inverse_zero, number_ring}) / Numeral0 = 0"
  2051   by simp
  2052 
  2053 
  2054 subsection {* The divides relation *}
  2055 
  2056 lemma zdvd_antisym_nonneg:
  2057     "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
  2058   apply (simp add: dvd_def, auto)
  2059   apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff)
  2060   done
  2061 
  2062 lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" 
  2063   shows "\<bar>a\<bar> = \<bar>b\<bar>"
  2064 proof cases
  2065   assume "a = 0" with assms show ?thesis by simp
  2066 next
  2067   assume "a \<noteq> 0"
  2068   from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
  2069   from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
  2070   from k k' have "a = a*k*k'" by simp
  2071   with mult_cancel_left1[where c="a" and b="k*k'"]
  2072   have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
  2073   hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
  2074   thus ?thesis using k k' by auto
  2075 qed
  2076 
  2077 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
  2078   apply (subgoal_tac "m = n + (m - n)")
  2079    apply (erule ssubst)
  2080    apply (blast intro: dvd_add, simp)
  2081   done
  2082 
  2083 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
  2084 apply (rule iffI)
  2085  apply (erule_tac [2] dvd_add)
  2086  apply (subgoal_tac "n = (n + k * m) - k * m")
  2087   apply (erule ssubst)
  2088   apply (erule dvd_diff)
  2089   apply(simp_all)
  2090 done
  2091 
  2092 lemma dvd_imp_le_int:
  2093   fixes d i :: int
  2094   assumes "i \<noteq> 0" and "d dvd i"
  2095   shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
  2096 proof -
  2097   from `d dvd i` obtain k where "i = d * k" ..
  2098   with `i \<noteq> 0` have "k \<noteq> 0" by auto
  2099   then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
  2100   then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
  2101   with `i = d * k` show ?thesis by (simp add: abs_mult)
  2102 qed
  2103 
  2104 lemma zdvd_not_zless:
  2105   fixes m n :: int
  2106   assumes "0 < m" and "m < n"
  2107   shows "\<not> n dvd m"
  2108 proof
  2109   from assms have "0 < n" by auto
  2110   assume "n dvd m" then obtain k where k: "m = n * k" ..
  2111   with `0 < m` have "0 < n * k" by auto
  2112   with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
  2113   with k `0 < n` `m < n` have "n * k < n * 1" by simp
  2114   with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
  2115 qed
  2116 
  2117 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
  2118   shows "m dvd n"
  2119 proof-
  2120   from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
  2121   {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
  2122     with h have False by (simp add: mult_assoc)}
  2123   hence "n = m * h" by blast
  2124   thus ?thesis by simp
  2125 qed
  2126 
  2127 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
  2128 proof -
  2129   have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
  2130   proof -
  2131     fix k
  2132     assume A: "int y = int x * k"
  2133     then show "x dvd y" proof (cases k)
  2134       case (1 n) with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
  2135       then show ?thesis ..
  2136     next
  2137       case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
  2138       also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
  2139       also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
  2140       finally have "- int (x * Suc n) = int y" ..
  2141       then show ?thesis by (simp only: negative_eq_positive) auto
  2142     qed
  2143   qed
  2144   then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
  2145 qed
  2146 
  2147 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
  2148 proof
  2149   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
  2150   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
  2151   hence "nat \<bar>x\<bar> = 1"  by simp
  2152   thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
  2153 next
  2154   assume "\<bar>x\<bar>=1"
  2155   then have "x = 1 \<or> x = -1" by auto
  2156   then show "x dvd 1" by (auto intro: dvdI)
  2157 qed
  2158 
  2159 lemma zdvd_mult_cancel1: 
  2160   assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
  2161 proof
  2162   assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
  2163     by (cases "n >0", auto simp add: minus_equation_iff)
  2164 next
  2165   assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
  2166   from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
  2167 qed
  2168 
  2169 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
  2170   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
  2171 
  2172 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
  2173   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
  2174 
  2175 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
  2176   by (auto simp add: dvd_int_iff)
  2177 
  2178 lemma eq_nat_nat_iff:
  2179   "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
  2180   by (auto elim!: nonneg_eq_int)
  2181 
  2182 lemma nat_power_eq:
  2183   "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
  2184   by (induct n) (simp_all add: nat_mult_distrib)
  2185 
  2186 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
  2187   apply (rule_tac z=n in int_cases)
  2188   apply (auto simp add: dvd_int_iff)
  2189   apply (rule_tac z=z in int_cases)
  2190   apply (auto simp add: dvd_imp_le)
  2191   done
  2192 
  2193 lemma zdvd_period:
  2194   fixes a d :: int
  2195   assumes "a dvd d"
  2196   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
  2197 proof -
  2198   from assms obtain k where "d = a * k" by (rule dvdE)
  2199   show ?thesis proof
  2200     assume "a dvd (x + t)"
  2201     then obtain l where "x + t = a * l" by (rule dvdE)
  2202     then have "x = a * l - t" by simp
  2203     with `d = a * k` show "a dvd x + c * d + t" by simp
  2204   next
  2205     assume "a dvd x + c * d + t"
  2206     then obtain l where "x + c * d + t = a * l" by (rule dvdE)
  2207     then have "x = a * l - c * d - t" by simp
  2208     with `d = a * k` show "a dvd (x + t)" by simp
  2209   qed
  2210 qed
  2211 
  2212 
  2213 subsection {* Configuration of the code generator *}
  2214 
  2215 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
  2216 
  2217 lemmas pred_succ_numeral_code [code] =
  2218   pred_bin_simps succ_bin_simps
  2219 
  2220 lemmas plus_numeral_code [code] =
  2221   add_bin_simps
  2222   arith_extra_simps(1) [where 'a = int]
  2223 
  2224 lemmas minus_numeral_code [code] =
  2225   minus_bin_simps
  2226   arith_extra_simps(2) [where 'a = int]
  2227   arith_extra_simps(5) [where 'a = int]
  2228 
  2229 lemmas times_numeral_code [code] =
  2230   mult_bin_simps
  2231   arith_extra_simps(4) [where 'a = int]
  2232 
  2233 instantiation int :: eq
  2234 begin
  2235 
  2236 definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
  2237 
  2238 instance by default (simp add: eq_int_def)
  2239 
  2240 end
  2241 
  2242 lemma eq_number_of_int_code [code]:
  2243   "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
  2244   unfolding eq_int_def number_of_is_id ..
  2245 
  2246 lemma eq_int_code [code]:
  2247   "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
  2248   "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
  2249   "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
  2250   "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
  2251   "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
  2252   "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
  2253   "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
  2254   "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
  2255   "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq k1 Int.Pls"
  2256   "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
  2257   "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
  2258   "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq k1 Int.Min"
  2259   "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
  2260   "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
  2261   "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
  2262   "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
  2263   unfolding eq_equals by simp_all
  2264 
  2265 lemma eq_int_refl [code nbe]:
  2266   "eq_class.eq (k::int) k \<longleftrightarrow> True"
  2267   by (rule HOL.eq_refl)
  2268 
  2269 lemma less_eq_number_of_int_code [code]:
  2270   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
  2271   unfolding number_of_is_id ..
  2272 
  2273 lemma less_eq_int_code [code]:
  2274   "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
  2275   "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
  2276   "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
  2277   "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
  2278   "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
  2279   "Int.Min \<le> Int.Min \<longleftrightarrow> True"
  2280   "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
  2281   "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
  2282   "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
  2283   "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
  2284   "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
  2285   "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
  2286   "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
  2287   "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  2288   "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  2289   "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  2290   by simp_all
  2291 
  2292 lemma less_number_of_int_code [code]:
  2293   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
  2294   unfolding number_of_is_id ..
  2295 
  2296 lemma less_int_code [code]:
  2297   "Int.Pls < Int.Pls \<longleftrightarrow> False"
  2298   "Int.Pls < Int.Min \<longleftrightarrow> False"
  2299   "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
  2300   "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
  2301   "Int.Min < Int.Pls \<longleftrightarrow> True"
  2302   "Int.Min < Int.Min \<longleftrightarrow> False"
  2303   "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
  2304   "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
  2305   "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
  2306   "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
  2307   "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
  2308   "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
  2309   "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  2310   "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  2311   "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  2312   "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
  2313   by simp_all
  2314 
  2315 definition
  2316   nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
  2317   "nat_aux i n = nat i + n"
  2318 
  2319 lemma [code]:
  2320   "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))"  -- {* tail recursive *}
  2321   by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
  2322     dest: zless_imp_add1_zle)
  2323 
  2324 lemma [code]: "nat i = nat_aux i 0"
  2325   by (simp add: nat_aux_def)
  2326 
  2327 hide_const (open) nat_aux
  2328 
  2329 lemma zero_is_num_zero [code, code_unfold_post]:
  2330   "(0\<Colon>int) = Numeral0" 
  2331   by simp
  2332 
  2333 lemma one_is_num_one [code, code_unfold_post]:
  2334   "(1\<Colon>int) = Numeral1" 
  2335   by simp
  2336 
  2337 code_modulename SML
  2338   Int Arith
  2339 
  2340 code_modulename OCaml
  2341   Int Arith
  2342 
  2343 code_modulename Haskell
  2344   Int Arith
  2345 
  2346 types_code
  2347   "int" ("int")
  2348 attach (term_of) {*
  2349 val term_of_int = HOLogic.mk_number HOLogic.intT;
  2350 *}
  2351 attach (test) {*
  2352 fun gen_int i =
  2353   let val j = one_of [~1, 1] * random_range 0 i
  2354   in (j, fn () => term_of_int j) end;
  2355 *}
  2356 
  2357 setup {*
  2358 let
  2359 
  2360 fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
  2361   | strip_number_of t = t;
  2362 
  2363 fun numeral_codegen thy defs dep module b t gr =
  2364   let val i = HOLogic.dest_numeral (strip_number_of t)
  2365   in
  2366     SOME (Codegen.str (string_of_int i),
  2367       snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
  2368   end handle TERM _ => NONE;
  2369 
  2370 in
  2371 
  2372 Codegen.add_codegen "numeral_codegen" numeral_codegen
  2373 
  2374 end
  2375 *}
  2376 
  2377 consts_code
  2378   "number_of :: int \<Rightarrow> int"    ("(_)")
  2379   "0 :: int"                   ("0")
  2380   "1 :: int"                   ("1")
  2381   "uminus :: int => int"       ("~")
  2382   "op + :: int => int => int"  ("(_ +/ _)")
  2383   "op * :: int => int => int"  ("(_ */ _)")
  2384   "op \<le> :: int => int => bool" ("(_ <=/ _)")
  2385   "op < :: int => int => bool" ("(_ </ _)")
  2386 
  2387 quickcheck_params [default_type = int]
  2388 
  2389 hide_const (open) Pls Min Bit0 Bit1 succ pred
  2390 
  2391 
  2392 subsection {* Legacy theorems *}
  2393 
  2394 lemmas zminus_zminus = minus_minus [of "z::int", standard]
  2395 lemmas zminus_0 = minus_zero [where 'a=int]
  2396 lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
  2397 lemmas zadd_commute = add_commute [of "z::int" "w", standard]
  2398 lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
  2399 lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
  2400 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
  2401 lemmas zmult_ac = mult_ac
  2402 lemmas zadd_0 = add_0_left [of "z::int", standard]
  2403 lemmas zadd_0_right = add_0_right [of "z::int", standard]
  2404 lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
  2405 lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
  2406 lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
  2407 lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
  2408 lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
  2409 lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
  2410 lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
  2411 lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
  2412 
  2413 lemmas zmult_1 = mult_1_left [of "z::int", standard]
  2414 lemmas zmult_1_right = mult_1_right [of "z::int", standard]
  2415 
  2416 lemmas zle_refl = order_refl [of "w::int", standard]
  2417 lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
  2418 lemmas zle_antisym = order_antisym [of "z::int" "w", standard]
  2419 lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
  2420 lemmas zless_linear = linorder_less_linear [where 'a = int]
  2421 
  2422 lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
  2423 lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
  2424 lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
  2425 
  2426 lemmas int_0_less_1 = zero_less_one [where 'a=int]
  2427 lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
  2428 
  2429 lemmas inj_int = inj_of_nat [where 'a=int]
  2430 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
  2431 lemmas int_mult = of_nat_mult [where 'a=int]
  2432 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
  2433 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
  2434 lemmas zless_int = of_nat_less_iff [where 'a=int]
  2435 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
  2436 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
  2437 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
  2438 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
  2439 lemmas int_0 = of_nat_0 [where 'a=int]
  2440 lemmas int_1 = of_nat_1 [where 'a=int]
  2441 lemmas int_Suc = of_nat_Suc [where 'a=int]
  2442 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
  2443 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
  2444 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
  2445 lemmas zless_le = less_int_def
  2446 lemmas int_eq_of_nat = TrueI
  2447 
  2448 lemma zpower_zadd_distrib:
  2449   "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
  2450   by (rule power_add)
  2451 
  2452 lemma zero_less_zpower_abs_iff:
  2453   "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
  2454   by (rule zero_less_power_abs_iff)
  2455 
  2456 lemma zero_le_zpower_abs: "(0::int) \<le> abs x ^ n"
  2457   by (rule zero_le_power_abs)
  2458 
  2459 lemma zpower_zpower:
  2460   "(x ^ y) ^ z = (x ^ (y * z)::int)"
  2461   by (rule power_mult [symmetric])
  2462 
  2463 lemma int_power:
  2464   "int (m ^ n) = int m ^ n"
  2465   by (rule of_nat_power)
  2466 
  2467 lemmas zpower_int = int_power [symmetric]
  2468 
  2469 end