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