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