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