src/HOL/Int.thy
author huffman
Mon Mar 30 12:07:59 2009 -0700 (2009-03-30)
changeset 30802 f9e9e800d27e
parent 30796 126701134811
child 30839 bf99ceb7d015
permissions -rw-r--r--
simplify theorem references
     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 text {*By Jeremy Avigad*}
  1386 
  1387 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
  1388   apply (cases "finite A")
  1389   apply (erule finite_induct, auto)
  1390   done
  1391 
  1392 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
  1393   apply (cases "finite A")
  1394   apply (erule finite_induct, auto)
  1395   done
  1396 
  1397 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
  1398   apply (cases "finite A")
  1399   apply (erule finite_induct, auto simp add: of_nat_mult)
  1400   done
  1401 
  1402 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
  1403   apply (cases "finite A")
  1404   apply (erule finite_induct, auto)
  1405   done
  1406 
  1407 lemma setprod_nonzero_nat:
  1408     "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
  1409   by (rule setprod_nonzero, auto)
  1410 
  1411 lemma setprod_zero_eq_nat:
  1412     "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
  1413   by (rule setprod_zero_eq, auto)
  1414 
  1415 lemma setprod_nonzero_int:
  1416     "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
  1417   by (rule setprod_nonzero, auto)
  1418 
  1419 lemma setprod_zero_eq_int:
  1420     "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
  1421   by (rule setprod_zero_eq, auto)
  1422 
  1423 lemmas int_setsum = of_nat_setsum [where 'a=int]
  1424 lemmas int_setprod = of_nat_setprod [where 'a=int]
  1425 
  1426 
  1427 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
  1428 
  1429 lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
  1430 by simp 
  1431 
  1432 lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
  1433 by simp
  1434 
  1435 lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
  1436 by simp 
  1437 
  1438 lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
  1439 by simp
  1440 
  1441 lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
  1442 by simp
  1443 
  1444 lemma inverse_numeral_1:
  1445   "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
  1446 by simp
  1447 
  1448 text{*Theorem lists for the cancellation simprocs. The use of binary numerals
  1449 for 0 and 1 reduces the number of special cases.*}
  1450 
  1451 lemmas add_0s = add_numeral_0 add_numeral_0_right
  1452 lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
  1453                  mult_minus1 mult_minus1_right
  1454 
  1455 
  1456 subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
  1457 
  1458 text{*Arithmetic computations are defined for binary literals, which leaves 0
  1459 and 1 as special cases. Addition already has rules for 0, but not 1.
  1460 Multiplication and unary minus already have rules for both 0 and 1.*}
  1461 
  1462 
  1463 lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
  1464 by simp
  1465 
  1466 
  1467 lemmas add_number_of_eq = number_of_add [symmetric]
  1468 
  1469 text{*Allow 1 on either or both sides*}
  1470 lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
  1471 by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
  1472 
  1473 lemmas add_special =
  1474     one_add_one_is_two
  1475     binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
  1476     binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
  1477 
  1478 text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
  1479 lemmas diff_special =
  1480     binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
  1481     binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
  1482 
  1483 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1484 lemmas eq_special =
  1485     binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
  1486     binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
  1487     binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
  1488     binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
  1489 
  1490 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1491 lemmas less_special =
  1492   binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard]
  1493   binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard]
  1494   binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard]
  1495   binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard]
  1496 
  1497 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
  1498 lemmas le_special =
  1499     binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard]
  1500     binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard]
  1501     binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard]
  1502     binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard]
  1503 
  1504 lemmas arith_special[simp] = 
  1505        add_special diff_special eq_special less_special le_special
  1506 
  1507 
  1508 lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 &
  1509                    max (0::int) 1 = 1 & max (1::int) 0 = 1"
  1510 by(simp add:min_def max_def)
  1511 
  1512 lemmas min_max_special[simp] =
  1513  min_max_01
  1514  max_def[of "0::int" "number_of v", standard, simp]
  1515  min_def[of "0::int" "number_of v", standard, simp]
  1516  max_def[of "number_of u" "0::int", standard, simp]
  1517  min_def[of "number_of u" "0::int", standard, simp]
  1518  max_def[of "1::int" "number_of v", standard, simp]
  1519  min_def[of "1::int" "number_of v", standard, simp]
  1520  max_def[of "number_of u" "1::int", standard, simp]
  1521  min_def[of "number_of u" "1::int", standard, simp]
  1522 
  1523 text {* Legacy theorems *}
  1524 
  1525 lemmas zle_int = of_nat_le_iff [where 'a=int]
  1526 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
  1527 
  1528 subsection {* Setting up simplification procedures *}
  1529 
  1530 lemmas int_arith_rules =
  1531   neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
  1532   minus_zero diff_minus left_minus right_minus
  1533   mult_zero_left mult_zero_right mult_Bit1 mult_1_right
  1534   mult_minus_left mult_minus_right
  1535   minus_add_distrib minus_minus mult_assoc
  1536   of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
  1537   of_int_0 of_int_1 of_int_add of_int_mult
  1538 
  1539 use "Tools/int_arith.ML"
  1540 declaration {* K Int_Arith.setup *}
  1541 
  1542 
  1543 subsection{*Lemmas About Small Numerals*}
  1544 
  1545 lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
  1546 proof -
  1547   have "(of_int -1 :: 'a) = of_int (- 1)" by simp
  1548   also have "... = - of_int 1" by (simp only: of_int_minus)
  1549   also have "... = -1" by simp
  1550   finally show ?thesis .
  1551 qed
  1552 
  1553 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})"
  1554 by (simp add: abs_if)
  1555 
  1556 lemma abs_power_minus_one [simp]:
  1557      "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
  1558 by (simp add: power_abs)
  1559 
  1560 lemma of_int_number_of_eq [simp]:
  1561      "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
  1562 by (simp add: number_of_eq) 
  1563 
  1564 text{*Lemmas for specialist use, NOT as default simprules*}
  1565 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
  1566 proof -
  1567   have "2*z = (1 + 1)*z" by simp
  1568   also have "... = z+z" by (simp add: left_distrib)
  1569   finally show ?thesis .
  1570 qed
  1571 
  1572 lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
  1573 by (subst mult_commute, rule mult_2)
  1574 
  1575 
  1576 subsection{*More Inequality Reasoning*}
  1577 
  1578 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
  1579 by arith
  1580 
  1581 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
  1582 by arith
  1583 
  1584 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
  1585 by arith
  1586 
  1587 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
  1588 by arith
  1589 
  1590 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
  1591 by arith
  1592 
  1593 
  1594 subsection{*The functions @{term nat} and @{term int}*}
  1595 
  1596 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
  1597   @{term "w + - z"}*}
  1598 declare Zero_int_def [symmetric, simp]
  1599 declare One_int_def [symmetric, simp]
  1600 
  1601 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
  1602 
  1603 lemma nat_0: "nat 0 = 0"
  1604 by (simp add: nat_eq_iff)
  1605 
  1606 lemma nat_1: "nat 1 = Suc 0"
  1607 by (subst nat_eq_iff, simp)
  1608 
  1609 lemma nat_2: "nat 2 = Suc (Suc 0)"
  1610 by (subst nat_eq_iff, simp)
  1611 
  1612 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
  1613 apply (insert zless_nat_conj [of 1 z])
  1614 apply (auto simp add: nat_1)
  1615 done
  1616 
  1617 text{*This simplifies expressions of the form @{term "int n = z"} where
  1618       z is an integer literal.*}
  1619 lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
  1620 
  1621 lemma split_nat [arith_split]:
  1622   "P(nat(i::int)) = ((\<forall>n. i = of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
  1623   (is "?P = (?L & ?R)")
  1624 proof (cases "i < 0")
  1625   case True thus ?thesis by auto
  1626 next
  1627   case False
  1628   have "?P = ?L"
  1629   proof
  1630     assume ?P thus ?L using False by clarsimp
  1631   next
  1632     assume ?L thus ?P using False by simp
  1633   qed
  1634   with False show ?thesis by simp
  1635 qed
  1636 
  1637 context ring_1
  1638 begin
  1639 
  1640 lemma of_int_of_nat [nitpick_const_simp]:
  1641   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
  1642 proof (cases "k < 0")
  1643   case True then have "0 \<le> - k" by simp
  1644   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
  1645   with True show ?thesis by simp
  1646 next
  1647   case False then show ?thesis by (simp add: not_less of_nat_nat)
  1648 qed
  1649 
  1650 end
  1651 
  1652 lemma nat_mult_distrib:
  1653   fixes z z' :: int
  1654   assumes "0 \<le> z"
  1655   shows "nat (z * z') = nat z * nat z'"
  1656 proof (cases "0 \<le> z'")
  1657   case False with assms have "z * z' \<le> 0"
  1658     by (simp add: not_le mult_le_0_iff)
  1659   then have "nat (z * z') = 0" by simp
  1660   moreover from False have "nat z' = 0" by simp
  1661   ultimately show ?thesis by simp
  1662 next
  1663   case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
  1664   show ?thesis
  1665     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
  1666       (simp only: of_nat_mult of_nat_nat [OF True]
  1667          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
  1668 qed
  1669 
  1670 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
  1671 apply (rule trans)
  1672 apply (rule_tac [2] nat_mult_distrib, auto)
  1673 done
  1674 
  1675 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
  1676 apply (cases "z=0 | w=0")
  1677 apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
  1678                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
  1679 done
  1680 
  1681 
  1682 subsection "Induction principles for int"
  1683 
  1684 text{*Well-founded segments of the integers*}
  1685 
  1686 definition
  1687   int_ge_less_than  ::  "int => (int * int) set"
  1688 where
  1689   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
  1690 
  1691 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
  1692 proof -
  1693   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
  1694     by (auto simp add: int_ge_less_than_def)
  1695   thus ?thesis 
  1696     by (rule wf_subset [OF wf_measure]) 
  1697 qed
  1698 
  1699 text{*This variant looks odd, but is typical of the relations suggested
  1700 by RankFinder.*}
  1701 
  1702 definition
  1703   int_ge_less_than2 ::  "int => (int * int) set"
  1704 where
  1705   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
  1706 
  1707 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
  1708 proof -
  1709   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))" 
  1710     by (auto simp add: int_ge_less_than2_def)
  1711   thus ?thesis 
  1712     by (rule wf_subset [OF wf_measure]) 
  1713 qed
  1714 
  1715 abbreviation
  1716   int :: "nat \<Rightarrow> int"
  1717 where
  1718   "int \<equiv> of_nat"
  1719 
  1720 (* `set:int': dummy construction *)
  1721 theorem int_ge_induct [case_names base step, induct set: int]:
  1722   fixes i :: int
  1723   assumes ge: "k \<le> i" and
  1724     base: "P k" and
  1725     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
  1726   shows "P i"
  1727 proof -
  1728   { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
  1729     proof (induct n)
  1730       case 0
  1731       hence "i = k" by arith
  1732       thus "P i" using base by simp
  1733     next
  1734       case (Suc n)
  1735       then have "n = nat((i - 1) - k)" by arith
  1736       moreover
  1737       have ki1: "k \<le> i - 1" using Suc.prems by arith
  1738       ultimately
  1739       have "P(i - 1)" by(rule Suc.hyps)
  1740       from step[OF ki1 this] show ?case by simp
  1741     qed
  1742   }
  1743   with ge show ?thesis by fast
  1744 qed
  1745 
  1746 (* `set:int': dummy construction *)
  1747 theorem int_gr_induct [case_names base step, induct set: int]:
  1748   assumes gr: "k < (i::int)" and
  1749         base: "P(k+1)" and
  1750         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
  1751   shows "P i"
  1752 apply(rule int_ge_induct[of "k + 1"])
  1753   using gr apply arith
  1754  apply(rule base)
  1755 apply (rule step, simp+)
  1756 done
  1757 
  1758 theorem int_le_induct[consumes 1,case_names base step]:
  1759   assumes le: "i \<le> (k::int)" and
  1760         base: "P(k)" and
  1761         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
  1762   shows "P i"
  1763 proof -
  1764   { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
  1765     proof (induct n)
  1766       case 0
  1767       hence "i = k" by arith
  1768       thus "P i" using base by simp
  1769     next
  1770       case (Suc n)
  1771       hence "n = nat(k - (i+1))" by arith
  1772       moreover
  1773       have ki1: "i + 1 \<le> k" using Suc.prems by arith
  1774       ultimately
  1775       have "P(i+1)" by(rule Suc.hyps)
  1776       from step[OF ki1 this] show ?case by simp
  1777     qed
  1778   }
  1779   with le show ?thesis by fast
  1780 qed
  1781 
  1782 theorem int_less_induct [consumes 1,case_names base step]:
  1783   assumes less: "(i::int) < k" and
  1784         base: "P(k - 1)" and
  1785         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
  1786   shows "P i"
  1787 apply(rule int_le_induct[of _ "k - 1"])
  1788   using less apply arith
  1789  apply(rule base)
  1790 apply (rule step, simp+)
  1791 done
  1792 
  1793 subsection{*Intermediate value theorems*}
  1794 
  1795 lemma int_val_lemma:
  1796      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
  1797       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
  1798 unfolding One_nat_def
  1799 apply (induct n, simp)
  1800 apply (intro strip)
  1801 apply (erule impE, simp)
  1802 apply (erule_tac x = n in allE, simp)
  1803 apply (case_tac "k = f (Suc n)")
  1804 apply force
  1805 apply (erule impE)
  1806  apply (simp add: abs_if split add: split_if_asm)
  1807 apply (blast intro: le_SucI)
  1808 done
  1809 
  1810 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
  1811 
  1812 lemma nat_intermed_int_val:
  1813      "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
  1814          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
  1815 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
  1816        in int_val_lemma)
  1817 unfolding One_nat_def
  1818 apply simp
  1819 apply (erule exE)
  1820 apply (rule_tac x = "i+m" in exI, arith)
  1821 done
  1822 
  1823 
  1824 subsection{*Products and 1, by T. M. Rasmussen*}
  1825 
  1826 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
  1827 by arith
  1828 
  1829 lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
  1830 apply (cases "\<bar>n\<bar>=1") 
  1831 apply (simp add: abs_mult) 
  1832 apply (rule ccontr) 
  1833 apply (auto simp add: linorder_neq_iff abs_mult) 
  1834 apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
  1835  prefer 2 apply arith 
  1836 apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp) 
  1837 apply (rule mult_mono, auto) 
  1838 done
  1839 
  1840 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
  1841 by (insert abs_zmult_eq_1 [of m n], arith)
  1842 
  1843 lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
  1844 apply (auto dest: pos_zmult_eq_1_iff_lemma) 
  1845 apply (simp add: mult_commute [of m]) 
  1846 apply (frule pos_zmult_eq_1_iff_lemma, auto) 
  1847 done
  1848 
  1849 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
  1850 apply (rule iffI) 
  1851  apply (frule pos_zmult_eq_1_iff_lemma)
  1852  apply (simp add: mult_commute [of m]) 
  1853  apply (frule pos_zmult_eq_1_iff_lemma, auto) 
  1854 done
  1855 
  1856 (* Could be simplified but Presburger only becomes available too late *)
  1857 lemma infinite_UNIV_int: "~finite(UNIV::int set)"
  1858 proof
  1859   assume "finite(UNIV::int set)"
  1860   moreover have "~(EX i::int. 2*i = 1)"
  1861     by (auto simp: pos_zmult_eq_1_iff)
  1862   ultimately show False using finite_UNIV_inj_surj[of "%n::int. n+n"]
  1863     by (simp add:inj_on_def surj_def) (blast intro:sym)
  1864 qed
  1865 
  1866 
  1867 subsection {* Integer Powers *} 
  1868 
  1869 instantiation int :: recpower
  1870 begin
  1871 
  1872 primrec power_int where
  1873   "p ^ 0 = (1\<Colon>int)"
  1874   | "p ^ (Suc n) = (p\<Colon>int) * (p ^ n)"
  1875 
  1876 instance proof
  1877   fix z :: int
  1878   fix n :: nat
  1879   show "z ^ 0 = 1" by simp
  1880   show "z ^ Suc n = z * (z ^ n)" by simp
  1881 qed
  1882 
  1883 declare power_int.simps [simp del]
  1884 
  1885 end
  1886 
  1887 lemma zpower_zadd_distrib: "x ^ (y + z) = ((x ^ y) * (x ^ z)::int)"
  1888   by (rule Power.power_add)
  1889 
  1890 lemma zpower_zpower: "(x ^ y) ^ z = (x ^ (y * z)::int)"
  1891   by (rule Power.power_mult [symmetric])
  1892 
  1893 lemma zero_less_zpower_abs_iff [simp]:
  1894   "(0 < abs x ^ n) \<longleftrightarrow> (x \<noteq> (0::int) | n = 0)"
  1895   by (induct n) (auto simp add: zero_less_mult_iff)
  1896 
  1897 lemma zero_le_zpower_abs [simp]: "(0::int) \<le> abs x ^ n"
  1898   by (induct n) (auto simp add: zero_le_mult_iff)
  1899 
  1900 lemma of_int_power:
  1901   "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
  1902   by (induct n) simp_all
  1903 
  1904 lemma int_power: "int (m^n) = (int m) ^ n"
  1905   by (rule of_nat_power)
  1906 
  1907 lemmas zpower_int = int_power [symmetric]
  1908 
  1909 
  1910 subsection {* Further theorems on numerals *}
  1911 
  1912 subsubsection{*Special Simplification for Constants*}
  1913 
  1914 text{*These distributive laws move literals inside sums and differences.*}
  1915 
  1916 lemmas left_distrib_number_of [simp] =
  1917   left_distrib [of _ _ "number_of v", standard]
  1918 
  1919 lemmas right_distrib_number_of [simp] =
  1920   right_distrib [of "number_of v", standard]
  1921 
  1922 lemmas left_diff_distrib_number_of [simp] =
  1923   left_diff_distrib [of _ _ "number_of v", standard]
  1924 
  1925 lemmas right_diff_distrib_number_of [simp] =
  1926   right_diff_distrib [of "number_of v", standard]
  1927 
  1928 text{*These are actually for fields, like real: but where else to put them?*}
  1929 
  1930 lemmas zero_less_divide_iff_number_of [simp, noatp] =
  1931   zero_less_divide_iff [of "number_of w", standard]
  1932 
  1933 lemmas divide_less_0_iff_number_of [simp, noatp] =
  1934   divide_less_0_iff [of "number_of w", standard]
  1935 
  1936 lemmas zero_le_divide_iff_number_of [simp, noatp] =
  1937   zero_le_divide_iff [of "number_of w", standard]
  1938 
  1939 lemmas divide_le_0_iff_number_of [simp, noatp] =
  1940   divide_le_0_iff [of "number_of w", standard]
  1941 
  1942 
  1943 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
  1944   strange, but then other simprocs simplify the quotient.*}
  1945 
  1946 lemmas inverse_eq_divide_number_of [simp] =
  1947   inverse_eq_divide [of "number_of w", standard]
  1948 
  1949 text {*These laws simplify inequalities, moving unary minus from a term
  1950 into the literal.*}
  1951 
  1952 lemmas less_minus_iff_number_of [simp, noatp] =
  1953   less_minus_iff [of "number_of v", standard]
  1954 
  1955 lemmas le_minus_iff_number_of [simp, noatp] =
  1956   le_minus_iff [of "number_of v", standard]
  1957 
  1958 lemmas equation_minus_iff_number_of [simp, noatp] =
  1959   equation_minus_iff [of "number_of v", standard]
  1960 
  1961 lemmas minus_less_iff_number_of [simp, noatp] =
  1962   minus_less_iff [of _ "number_of v", standard]
  1963 
  1964 lemmas minus_le_iff_number_of [simp, noatp] =
  1965   minus_le_iff [of _ "number_of v", standard]
  1966 
  1967 lemmas minus_equation_iff_number_of [simp, noatp] =
  1968   minus_equation_iff [of _ "number_of v", standard]
  1969 
  1970 
  1971 text{*To Simplify Inequalities Where One Side is the Constant 1*}
  1972 
  1973 lemma less_minus_iff_1 [simp,noatp]:
  1974   fixes b::"'b::{ordered_idom,number_ring}"
  1975   shows "(1 < - b) = (b < -1)"
  1976 by auto
  1977 
  1978 lemma le_minus_iff_1 [simp,noatp]:
  1979   fixes b::"'b::{ordered_idom,number_ring}"
  1980   shows "(1 \<le> - b) = (b \<le> -1)"
  1981 by auto
  1982 
  1983 lemma equation_minus_iff_1 [simp,noatp]:
  1984   fixes b::"'b::number_ring"
  1985   shows "(1 = - b) = (b = -1)"
  1986 by (subst equation_minus_iff, auto)
  1987 
  1988 lemma minus_less_iff_1 [simp,noatp]:
  1989   fixes a::"'b::{ordered_idom,number_ring}"
  1990   shows "(- a < 1) = (-1 < a)"
  1991 by auto
  1992 
  1993 lemma minus_le_iff_1 [simp,noatp]:
  1994   fixes a::"'b::{ordered_idom,number_ring}"
  1995   shows "(- a \<le> 1) = (-1 \<le> a)"
  1996 by auto
  1997 
  1998 lemma minus_equation_iff_1 [simp,noatp]:
  1999   fixes a::"'b::number_ring"
  2000   shows "(- a = 1) = (a = -1)"
  2001 by (subst minus_equation_iff, auto)
  2002 
  2003 
  2004 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
  2005 
  2006 lemmas mult_less_cancel_left_number_of [simp, noatp] =
  2007   mult_less_cancel_left [of "number_of v", standard]
  2008 
  2009 lemmas mult_less_cancel_right_number_of [simp, noatp] =
  2010   mult_less_cancel_right [of _ "number_of v", standard]
  2011 
  2012 lemmas mult_le_cancel_left_number_of [simp, noatp] =
  2013   mult_le_cancel_left [of "number_of v", standard]
  2014 
  2015 lemmas mult_le_cancel_right_number_of [simp, noatp] =
  2016   mult_le_cancel_right [of _ "number_of v", standard]
  2017 
  2018 
  2019 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
  2020 
  2021 lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
  2022 lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
  2023 lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
  2024 lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
  2025 lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
  2026 lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
  2027 
  2028 
  2029 subsubsection{*Optional Simplification Rules Involving Constants*}
  2030 
  2031 text{*Simplify quotients that are compared with a literal constant.*}
  2032 
  2033 lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
  2034 lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
  2035 lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
  2036 lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
  2037 lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
  2038 lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
  2039 
  2040 
  2041 text{*Not good as automatic simprules because they cause case splits.*}
  2042 lemmas divide_const_simps =
  2043   le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
  2044   divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
  2045   le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
  2046 
  2047 text{*Division By @{text "-1"}*}
  2048 
  2049 lemma divide_minus1 [simp]:
  2050      "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
  2051 by simp
  2052 
  2053 lemma minus1_divide [simp]:
  2054      "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
  2055 by (simp add: divide_inverse inverse_minus_eq)
  2056 
  2057 lemma half_gt_zero_iff:
  2058      "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
  2059 by auto
  2060 
  2061 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
  2062 
  2063 
  2064 subsection {* Configuration of the code generator *}
  2065 
  2066 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
  2067 
  2068 lemmas pred_succ_numeral_code [code] =
  2069   pred_bin_simps succ_bin_simps
  2070 
  2071 lemmas plus_numeral_code [code] =
  2072   add_bin_simps
  2073   arith_extra_simps(1) [where 'a = int]
  2074 
  2075 lemmas minus_numeral_code [code] =
  2076   minus_bin_simps
  2077   arith_extra_simps(2) [where 'a = int]
  2078   arith_extra_simps(5) [where 'a = int]
  2079 
  2080 lemmas times_numeral_code [code] =
  2081   mult_bin_simps
  2082   arith_extra_simps(4) [where 'a = int]
  2083 
  2084 instantiation int :: eq
  2085 begin
  2086 
  2087 definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
  2088 
  2089 instance by default (simp add: eq_int_def)
  2090 
  2091 end
  2092 
  2093 lemma eq_number_of_int_code [code]:
  2094   "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
  2095   unfolding eq_int_def number_of_is_id ..
  2096 
  2097 lemma eq_int_code [code]:
  2098   "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
  2099   "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
  2100   "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
  2101   "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
  2102   "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
  2103   "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
  2104   "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
  2105   "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
  2106   "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq k1 Int.Pls"
  2107   "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
  2108   "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
  2109   "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq k1 Int.Min"
  2110   "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
  2111   "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
  2112   "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
  2113   "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
  2114   unfolding eq_equals by simp_all
  2115 
  2116 lemma eq_int_refl [code nbe]:
  2117   "eq_class.eq (k::int) k \<longleftrightarrow> True"
  2118   by (rule HOL.eq_refl)
  2119 
  2120 lemma less_eq_number_of_int_code [code]:
  2121   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
  2122   unfolding number_of_is_id ..
  2123 
  2124 lemma less_eq_int_code [code]:
  2125   "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
  2126   "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
  2127   "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
  2128   "Int.Pls \<le> Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
  2129   "Int.Min \<le> Int.Pls \<longleftrightarrow> True"
  2130   "Int.Min \<le> Int.Min \<longleftrightarrow> True"
  2131   "Int.Min \<le> Int.Bit0 k \<longleftrightarrow> Int.Min < k"
  2132   "Int.Min \<le> Int.Bit1 k \<longleftrightarrow> Int.Min \<le> k"
  2133   "Int.Bit0 k \<le> Int.Pls \<longleftrightarrow> k \<le> Int.Pls"
  2134   "Int.Bit1 k \<le> Int.Pls \<longleftrightarrow> k < Int.Pls"
  2135   "Int.Bit0 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
  2136   "Int.Bit1 k \<le> Int.Min \<longleftrightarrow> k \<le> Int.Min"
  2137   "Int.Bit0 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 \<le> k2"
  2138   "Int.Bit0 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  2139   "Int.Bit1 k1 \<le> Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  2140   "Int.Bit1 k1 \<le> Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  2141   by simp_all
  2142 
  2143 lemma less_number_of_int_code [code]:
  2144   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
  2145   unfolding number_of_is_id ..
  2146 
  2147 lemma less_int_code [code]:
  2148   "Int.Pls < Int.Pls \<longleftrightarrow> False"
  2149   "Int.Pls < Int.Min \<longleftrightarrow> False"
  2150   "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
  2151   "Int.Pls < Int.Bit1 k \<longleftrightarrow> Int.Pls \<le> k"
  2152   "Int.Min < Int.Pls \<longleftrightarrow> True"
  2153   "Int.Min < Int.Min \<longleftrightarrow> False"
  2154   "Int.Min < Int.Bit0 k \<longleftrightarrow> Int.Min < k"
  2155   "Int.Min < Int.Bit1 k \<longleftrightarrow> Int.Min < k"
  2156   "Int.Bit0 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
  2157   "Int.Bit1 k < Int.Pls \<longleftrightarrow> k < Int.Pls"
  2158   "Int.Bit0 k < Int.Min \<longleftrightarrow> k \<le> Int.Min"
  2159   "Int.Bit1 k < Int.Min \<longleftrightarrow> k < Int.Min"
  2160   "Int.Bit0 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  2161   "Int.Bit0 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 \<le> k2"
  2162   "Int.Bit1 k1 < Int.Bit0 k2 \<longleftrightarrow> k1 < k2"
  2163   "Int.Bit1 k1 < Int.Bit1 k2 \<longleftrightarrow> k1 < k2"
  2164   by simp_all
  2165 
  2166 definition
  2167   nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
  2168   "nat_aux i n = nat i + n"
  2169 
  2170 lemma [code]:
  2171   "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))"  -- {* tail recursive *}
  2172   by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
  2173     dest: zless_imp_add1_zle)
  2174 
  2175 lemma [code]: "nat i = nat_aux i 0"
  2176   by (simp add: nat_aux_def)
  2177 
  2178 hide (open) const nat_aux
  2179 
  2180 lemma zero_is_num_zero [code, code inline, symmetric, code post]:
  2181   "(0\<Colon>int) = Numeral0" 
  2182   by simp
  2183 
  2184 lemma one_is_num_one [code, code inline, symmetric, code post]:
  2185   "(1\<Colon>int) = Numeral1" 
  2186   by simp
  2187 
  2188 code_modulename SML
  2189   Int Integer
  2190 
  2191 code_modulename OCaml
  2192   Int Integer
  2193 
  2194 code_modulename Haskell
  2195   Int Integer
  2196 
  2197 types_code
  2198   "int" ("int")
  2199 attach (term_of) {*
  2200 val term_of_int = HOLogic.mk_number HOLogic.intT;
  2201 *}
  2202 attach (test) {*
  2203 fun gen_int i =
  2204   let val j = one_of [~1, 1] * random_range 0 i
  2205   in (j, fn () => term_of_int j) end;
  2206 *}
  2207 
  2208 setup {*
  2209 let
  2210 
  2211 fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
  2212   | strip_number_of t = t;
  2213 
  2214 fun numeral_codegen thy defs dep module b t gr =
  2215   let val i = HOLogic.dest_numeral (strip_number_of t)
  2216   in
  2217     SOME (Codegen.str (string_of_int i),
  2218       snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
  2219   end handle TERM _ => NONE;
  2220 
  2221 in
  2222 
  2223 Codegen.add_codegen "numeral_codegen" numeral_codegen
  2224 
  2225 end
  2226 *}
  2227 
  2228 consts_code
  2229   "number_of :: int \<Rightarrow> int"    ("(_)")
  2230   "0 :: int"                   ("0")
  2231   "1 :: int"                   ("1")
  2232   "uminus :: int => int"       ("~")
  2233   "op + :: int => int => int"  ("(_ +/ _)")
  2234   "op * :: int => int => int"  ("(_ */ _)")
  2235   "op \<le> :: int => int => bool" ("(_ <=/ _)")
  2236   "op < :: int => int => bool" ("(_ </ _)")
  2237 
  2238 quickcheck_params [default_type = int]
  2239 
  2240 hide (open) const Pls Min Bit0 Bit1 succ pred
  2241 
  2242 
  2243 subsection {* Legacy theorems *}
  2244 
  2245 lemmas zminus_zminus = minus_minus [of "z::int", standard]
  2246 lemmas zminus_0 = minus_zero [where 'a=int]
  2247 lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
  2248 lemmas zadd_commute = add_commute [of "z::int" "w", standard]
  2249 lemmas zadd_assoc = add_assoc [of "z1::int" "z2" "z3", standard]
  2250 lemmas zadd_left_commute = add_left_commute [of "x::int" "y" "z", standard]
  2251 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
  2252 lemmas zmult_ac = OrderedGroup.mult_ac
  2253 lemmas zadd_0 = OrderedGroup.add_0_left [of "z::int", standard]
  2254 lemmas zadd_0_right = OrderedGroup.add_0_left [of "z::int", standard]
  2255 lemmas zadd_zminus_inverse2 = left_minus [of "z::int", standard]
  2256 lemmas zmult_zminus = mult_minus_left [of "z::int" "w", standard]
  2257 lemmas zmult_commute = mult_commute [of "z::int" "w", standard]
  2258 lemmas zmult_assoc = mult_assoc [of "z1::int" "z2" "z3", standard]
  2259 lemmas zadd_zmult_distrib = left_distrib [of "z1::int" "z2" "w", standard]
  2260 lemmas zadd_zmult_distrib2 = right_distrib [of "w::int" "z1" "z2", standard]
  2261 lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
  2262 lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
  2263 
  2264 lemmas zmult_1 = mult_1_left [of "z::int", standard]
  2265 lemmas zmult_1_right = mult_1_right [of "z::int", standard]
  2266 
  2267 lemmas zle_refl = order_refl [of "w::int", standard]
  2268 lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
  2269 lemmas zle_anti_sym = order_antisym [of "z::int" "w", standard]
  2270 lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
  2271 lemmas zless_linear = linorder_less_linear [where 'a = int]
  2272 
  2273 lemmas zadd_left_mono = add_left_mono [of "i::int" "j" "k", standard]
  2274 lemmas zadd_strict_right_mono = add_strict_right_mono [of "i::int" "j" "k", standard]
  2275 lemmas zadd_zless_mono = add_less_le_mono [of "w'::int" "w" "z'" "z", standard]
  2276 
  2277 lemmas int_0_less_1 = zero_less_one [where 'a=int]
  2278 lemmas int_0_neq_1 = zero_neq_one [where 'a=int]
  2279 
  2280 lemmas inj_int = inj_of_nat [where 'a=int]
  2281 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
  2282 lemmas int_mult = of_nat_mult [where 'a=int]
  2283 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
  2284 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
  2285 lemmas zless_int = of_nat_less_iff [where 'a=int]
  2286 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
  2287 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
  2288 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
  2289 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
  2290 lemmas int_0 = of_nat_0 [where 'a=int]
  2291 lemmas int_1 = of_nat_1 [where 'a=int]
  2292 lemmas int_Suc = of_nat_Suc [where 'a=int]
  2293 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
  2294 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
  2295 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
  2296 lemmas zless_le = less_int_def
  2297 lemmas int_eq_of_nat = TrueI
  2298 
  2299 end