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