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