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