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