src/HOL/Int.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 47207 9368aa814518
child 47226 ea712316fc87
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     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 Wellfounded
    10 uses
    11   ("Tools/numeral.ML")
    12   ("Tools/int_arith.ML")
    13 begin
    14 
    15 subsection {* The equivalence relation underlying the integers *}
    16 
    17 definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
    18   "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
    19 
    20 definition "Integ = UNIV//intrel"
    21 
    22 typedef (open) int = Integ
    23   morphisms Rep_Integ Abs_Integ
    24   unfolding Integ_def by (auto simp add: quotient_def)
    25 
    26 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
    27 begin
    28 
    29 definition
    30   Zero_int_def: "0 = Abs_Integ (intrel `` {(0, 0)})"
    31 
    32 definition
    33   One_int_def: "1 = Abs_Integ (intrel `` {(1, 0)})"
    34 
    35 definition
    36   add_int_def: "z + w = Abs_Integ
    37     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
    38       intrel `` {(x + u, y + v)})"
    39 
    40 definition
    41   minus_int_def:
    42     "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
    43 
    44 definition
    45   diff_int_def:  "z - w = z + (-w \<Colon> int)"
    46 
    47 definition
    48   mult_int_def: "z * w = Abs_Integ
    49     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
    50       intrel `` {(x*u + y*v, x*v + y*u)})"
    51 
    52 definition
    53   le_int_def:
    54    "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)"
    55 
    56 definition
    57   less_int_def: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
    58 
    59 definition
    60   zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
    61 
    62 definition
    63   zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
    64 
    65 instance ..
    66 
    67 end
    68 
    69 
    70 subsection{*Construction of the Integers*}
    71 
    72 lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)"
    73 by (simp add: intrel_def)
    74 
    75 lemma equiv_intrel: "equiv UNIV intrel"
    76 by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def)
    77 
    78 text{*Reduces equality of equivalence classes to the @{term intrel} relation:
    79   @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}
    80 lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I]
    81 
    82 text{*All equivalence classes belong to set of representatives*}
    83 lemma [simp]: "intrel``{(x,y)} \<in> Integ"
    84 by (auto simp add: Integ_def intrel_def quotient_def)
    85 
    86 text{*Reduces equality on abstractions to equality on representatives:
    87   @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
    88 declare Abs_Integ_inject [simp,no_atp]  Abs_Integ_inverse [simp,no_atp]
    89 
    90 text{*Case analysis on the representation of an integer as an equivalence
    91       class of pairs of naturals.*}
    92 lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
    93      "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
    94 apply (rule Abs_Integ_cases [of z]) 
    95 apply (auto simp add: Integ_def quotient_def) 
    96 done
    97 
    98 
    99 subsection {* Arithmetic Operations *}
   100 
   101 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
   102 proof -
   103   have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
   104     by (auto simp add: congruent_def)
   105   thus ?thesis
   106     by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
   107 qed
   108 
   109 lemma add:
   110      "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
   111       Abs_Integ (intrel``{(x+u, y+v)})"
   112 proof -
   113   have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
   114         respects2 intrel"
   115     by (auto simp add: congruent2_def)
   116   thus ?thesis
   117     by (simp add: add_int_def UN_UN_split_split_eq
   118                   UN_equiv_class2 [OF equiv_intrel equiv_intrel])
   119 qed
   120 
   121 text{*Congruence property for multiplication*}
   122 lemma mult_congruent2:
   123      "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
   124       respects2 intrel"
   125 apply (rule equiv_intrel [THEN congruent2_commuteI])
   126  apply (force simp add: mult_ac, clarify) 
   127 apply (simp add: congruent_def mult_ac)  
   128 apply (rename_tac u v w x y z)
   129 apply (subgoal_tac "u*y + x*y = w*y + v*y  &  u*z + x*z = w*z + v*z")
   130 apply (simp add: mult_ac)
   131 apply (simp add: add_mult_distrib [symmetric])
   132 done
   133 
   134 lemma mult:
   135      "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
   136       Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
   137 by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2
   138               UN_equiv_class2 [OF equiv_intrel equiv_intrel])
   139 
   140 text{*The integers form a @{text comm_ring_1}*}
   141 instance int :: comm_ring_1
   142 proof
   143   fix i j k :: int
   144   show "(i + j) + k = i + (j + k)"
   145     by (cases i, cases j, cases k) (simp add: add add_assoc)
   146   show "i + j = j + i" 
   147     by (cases i, cases j) (simp add: add_ac add)
   148   show "0 + i = i"
   149     by (cases i) (simp add: Zero_int_def add)
   150   show "- i + i = 0"
   151     by (cases i) (simp add: Zero_int_def minus add)
   152   show "i - j = i + - j"
   153     by (simp add: diff_int_def)
   154   show "(i * j) * k = i * (j * k)"
   155     by (cases i, cases j, cases k) (simp add: mult algebra_simps)
   156   show "i * j = j * i"
   157     by (cases i, cases j) (simp add: mult algebra_simps)
   158   show "1 * i = i"
   159     by (cases i) (simp add: One_int_def mult)
   160   show "(i + j) * k = i * k + j * k"
   161     by (cases i, cases j, cases k) (simp add: add mult algebra_simps)
   162   show "0 \<noteq> (1::int)"
   163     by (simp add: Zero_int_def One_int_def)
   164 qed
   165 
   166 abbreviation int :: "nat \<Rightarrow> int" where
   167   "int \<equiv> of_nat"
   168 
   169 lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
   170 by (induct m) (simp_all add: Zero_int_def One_int_def add)
   171 
   172 
   173 subsection {* The @{text "\<le>"} Ordering *}
   174 
   175 lemma le:
   176   "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"
   177 by (force simp add: le_int_def)
   178 
   179 lemma less:
   180   "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"
   181 by (simp add: less_int_def le order_less_le)
   182 
   183 instance int :: linorder
   184 proof
   185   fix i j k :: int
   186   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
   187     by (cases i, cases j) (simp add: le)
   188   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
   189     by (auto simp add: less_int_def dest: antisym) 
   190   show "i \<le> i"
   191     by (cases i) (simp add: le)
   192   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
   193     by (cases i, cases j, cases k) (simp add: le)
   194   show "i \<le> j \<or> j \<le> i"
   195     by (cases i, cases j) (simp add: le linorder_linear)
   196 qed
   197 
   198 instantiation int :: distrib_lattice
   199 begin
   200 
   201 definition
   202   "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
   203 
   204 definition
   205   "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
   206 
   207 instance
   208   by intro_classes
   209     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
   210 
   211 end
   212 
   213 instance int :: ordered_cancel_ab_semigroup_add
   214 proof
   215   fix i j k :: int
   216   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
   217     by (cases i, cases j, cases k) (simp add: le add)
   218 qed
   219 
   220 
   221 text{*Strict Monotonicity of Multiplication*}
   222 
   223 text{*strict, in 1st argument; proof is by induction on k>0*}
   224 lemma zmult_zless_mono2_lemma:
   225      "(i::int)<j ==> 0<k ==> int k * i < int k * j"
   226 apply (induct k)
   227 apply simp
   228 apply (simp add: left_distrib)
   229 apply (case_tac "k=0")
   230 apply (simp_all add: add_strict_mono)
   231 done
   232 
   233 lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n"
   234 apply (cases k)
   235 apply (auto simp add: le add int_def Zero_int_def)
   236 apply (rule_tac x="x-y" in exI, simp)
   237 done
   238 
   239 lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n"
   240 apply (cases k)
   241 apply (simp add: less int_def Zero_int_def)
   242 apply (rule_tac x="x-y" in exI, simp)
   243 done
   244 
   245 lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
   246 apply (drule zero_less_imp_eq_int)
   247 apply (auto simp add: zmult_zless_mono2_lemma)
   248 done
   249 
   250 text{*The integers form an ordered integral domain*}
   251 instance int :: linordered_idom
   252 proof
   253   fix i j k :: int
   254   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   255     by (rule zmult_zless_mono2)
   256   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
   257     by (simp only: zabs_def)
   258   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
   259     by (simp only: zsgn_def)
   260 qed
   261 
   262 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
   263 apply (cases w, cases z) 
   264 apply (simp add: less le add One_int_def)
   265 done
   266 
   267 lemma zless_iff_Suc_zadd:
   268   "(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
   269 apply (cases z, cases w)
   270 apply (auto simp add: less add int_def)
   271 apply (rename_tac a b c d) 
   272 apply (rule_tac x="a+d - Suc(c+b)" in exI) 
   273 apply arith
   274 done
   275 
   276 lemmas int_distrib =
   277   left_distrib [of z1 z2 w]
   278   right_distrib [of w z1 z2]
   279   left_diff_distrib [of z1 z2 w]
   280   right_diff_distrib [of w z1 z2]
   281   for z1 z2 w :: int
   282 
   283 
   284 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
   285 
   286 context ring_1
   287 begin
   288 
   289 definition of_int :: "int \<Rightarrow> 'a" where
   290   "of_int z = the_elem (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
   291 
   292 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
   293 proof -
   294   have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
   295     by (auto simp add: congruent_def) (simp add: algebra_simps of_nat_add [symmetric]
   296             del: of_nat_add) 
   297   thus ?thesis
   298     by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
   299 qed
   300 
   301 lemma of_int_0 [simp]: "of_int 0 = 0"
   302 by (simp add: of_int Zero_int_def)
   303 
   304 lemma of_int_1 [simp]: "of_int 1 = 1"
   305 by (simp add: of_int One_int_def)
   306 
   307 lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z"
   308 by (cases w, cases z) (simp add: algebra_simps of_int add)
   309 
   310 lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)"
   311 by (cases z) (simp add: algebra_simps of_int minus)
   312 
   313 lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
   314 by (simp add: diff_minus Groups.diff_minus)
   315 
   316 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
   317 apply (cases w, cases z)
   318 apply (simp add: algebra_simps of_int mult of_nat_mult)
   319 done
   320 
   321 text{*Collapse nested embeddings*}
   322 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
   323 by (induct n) auto
   324 
   325 lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
   326   by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
   327 
   328 lemma of_int_neg_numeral [simp, code_post]: "of_int (neg_numeral k) = neg_numeral k"
   329   unfolding neg_numeral_def neg_numeral_class.neg_numeral_def
   330   by (simp only: of_int_minus of_int_numeral)
   331 
   332 lemma of_int_power:
   333   "of_int (z ^ n) = of_int z ^ n"
   334   by (induct n) simp_all
   335 
   336 end
   337 
   338 context ring_char_0
   339 begin
   340 
   341 lemma of_int_eq_iff [simp]:
   342    "of_int w = of_int z \<longleftrightarrow> w = z"
   343 apply (cases w, cases z)
   344 apply (simp add: of_int)
   345 apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq)
   346 apply (simp only: of_nat_add [symmetric] of_nat_eq_iff)
   347 done
   348 
   349 text{*Special cases where either operand is zero*}
   350 lemma of_int_eq_0_iff [simp]:
   351   "of_int z = 0 \<longleftrightarrow> z = 0"
   352   using of_int_eq_iff [of z 0] by simp
   353 
   354 lemma of_int_0_eq_iff [simp]:
   355   "0 = of_int z \<longleftrightarrow> z = 0"
   356   using of_int_eq_iff [of 0 z] by simp
   357 
   358 end
   359 
   360 context linordered_idom
   361 begin
   362 
   363 text{*Every @{text linordered_idom} has characteristic zero.*}
   364 subclass ring_char_0 ..
   365 
   366 lemma of_int_le_iff [simp]:
   367   "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
   368   by (cases w, cases z)
   369     (simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add)
   370 
   371 lemma of_int_less_iff [simp]:
   372   "of_int w < of_int z \<longleftrightarrow> w < z"
   373   by (simp add: less_le order_less_le)
   374 
   375 lemma of_int_0_le_iff [simp]:
   376   "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
   377   using of_int_le_iff [of 0 z] by simp
   378 
   379 lemma of_int_le_0_iff [simp]:
   380   "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
   381   using of_int_le_iff [of z 0] by simp
   382 
   383 lemma of_int_0_less_iff [simp]:
   384   "0 < of_int z \<longleftrightarrow> 0 < z"
   385   using of_int_less_iff [of 0 z] by simp
   386 
   387 lemma of_int_less_0_iff [simp]:
   388   "of_int z < 0 \<longleftrightarrow> z < 0"
   389   using of_int_less_iff [of z 0] by simp
   390 
   391 end
   392 
   393 lemma of_int_eq_id [simp]: "of_int = id"
   394 proof
   395   fix z show "of_int z = id z"
   396     by (cases z) (simp add: of_int add minus int_def diff_minus)
   397 qed
   398 
   399 
   400 subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *}
   401 
   402 definition nat :: "int \<Rightarrow> nat" where
   403   "nat z = the_elem (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
   404 
   405 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
   406 proof -
   407   have "(\<lambda>(x,y). {x-y}) respects intrel"
   408     by (auto simp add: congruent_def)
   409   thus ?thesis
   410     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
   411 qed
   412 
   413 lemma nat_int [simp]: "nat (int n) = n"
   414 by (simp add: nat int_def)
   415 
   416 lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   417 by (cases z) (simp add: nat le int_def Zero_int_def)
   418 
   419 corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
   420 by simp
   421 
   422 lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
   423 by (cases z) (simp add: nat le Zero_int_def)
   424 
   425 lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
   426 apply (cases w, cases z) 
   427 apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith)
   428 done
   429 
   430 text{*An alternative condition is @{term "0 \<le> w"} *}
   431 corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
   432 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   433 
   434 corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
   435 by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
   436 
   437 lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
   438 apply (cases w, cases z) 
   439 apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
   440 done
   441 
   442 lemma nonneg_eq_int:
   443   fixes z :: int
   444   assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
   445   shows P
   446   using assms by (blast dest: nat_0_le sym)
   447 
   448 lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
   449 by (cases w) (simp add: nat le int_def Zero_int_def, arith)
   450 
   451 corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
   452 by (simp only: eq_commute [of m] nat_eq_iff)
   453 
   454 lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
   455 apply (cases w)
   456 apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith)
   457 done
   458 
   459 lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
   460   by (cases x, simp add: nat le int_def le_diff_conv)
   461 
   462 lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
   463   by (cases x, cases y, simp add: nat le)
   464 
   465 lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0"
   466 by(simp add: nat_eq_iff) arith
   467 
   468 lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)"
   469 by (auto simp add: nat_eq_iff2)
   470 
   471 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
   472 by (insert zless_nat_conj [of 0], auto)
   473 
   474 lemma nat_add_distrib:
   475      "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
   476 by (cases z, cases z') (simp add: nat add le Zero_int_def)
   477 
   478 lemma nat_diff_distrib:
   479      "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
   480 by (cases z, cases z')
   481   (simp add: nat add minus diff_minus le Zero_int_def)
   482 
   483 lemma nat_zminus_int [simp]: "nat (- int n) = 0"
   484 by (simp add: int_def minus nat Zero_int_def) 
   485 
   486 lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
   487 by (cases z) (simp add: nat less int_def, arith)
   488 
   489 context ring_1
   490 begin
   491 
   492 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
   493   by (cases z rule: eq_Abs_Integ)
   494    (simp add: nat le of_int Zero_int_def of_nat_diff)
   495 
   496 end
   497 
   498 text {* For termination proofs: *}
   499 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" ..
   500 
   501 
   502 subsection{*Lemmas about the Function @{term of_nat} and Orderings*}
   503 
   504 lemma negative_zless_0: "- (int (Suc n)) < (0 \<Colon> int)"
   505 by (simp add: order_less_le del: of_nat_Suc)
   506 
   507 lemma negative_zless [iff]: "- (int (Suc n)) < int m"
   508 by (rule negative_zless_0 [THEN order_less_le_trans], simp)
   509 
   510 lemma negative_zle_0: "- int n \<le> 0"
   511 by (simp add: minus_le_iff)
   512 
   513 lemma negative_zle [iff]: "- int n \<le> int m"
   514 by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
   515 
   516 lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
   517 by (subst le_minus_iff, simp del: of_nat_Suc)
   518 
   519 lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
   520 by (simp add: int_def le minus Zero_int_def)
   521 
   522 lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
   523 by (simp add: linorder_not_less)
   524 
   525 lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
   526 by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
   527 
   528 lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
   529 proof -
   530   have "(w \<le> z) = (0 \<le> z - w)"
   531     by (simp only: le_diff_eq add_0_left)
   532   also have "\<dots> = (\<exists>n. z - w = of_nat n)"
   533     by (auto elim: zero_le_imp_eq_int)
   534   also have "\<dots> = (\<exists>n. z = w + of_nat n)"
   535     by (simp only: algebra_simps)
   536   finally show ?thesis .
   537 qed
   538 
   539 lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
   540 by simp
   541 
   542 lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   543 by simp
   544 
   545 text{*This version is proved for all ordered rings, not just integers!
   546       It is proved here because attribute @{text arith_split} is not available
   547       in theory @{text Rings}.
   548       But is it really better than just rewriting with @{text abs_if}?*}
   549 lemma abs_split [arith_split,no_atp]:
   550      "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
   551 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
   552 
   553 lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
   554 apply (cases x)
   555 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
   556 apply (rule_tac x="y - Suc x" in exI, arith)
   557 done
   558 
   559 
   560 subsection {* Cases and induction *}
   561 
   562 text{*Now we replace the case analysis rule by a more conventional one:
   563 whether an integer is negative or not.*}
   564 
   565 theorem int_cases [case_names nonneg neg, cases type: int]:
   566   "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   567 apply (cases "z < 0")
   568 apply (blast dest!: negD)
   569 apply (simp add: linorder_not_less del: of_nat_Suc)
   570 apply auto
   571 apply (blast dest: nat_0_le [THEN sym])
   572 done
   573 
   574 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
   575      "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
   576   by (cases z) auto
   577 
   578 lemma nonneg_int_cases:
   579   assumes "0 \<le> k" obtains n where "k = int n"
   580   using assms by (cases k, simp, simp del: of_nat_Suc)
   581 
   582 text{*Contributed by Brian Huffman*}
   583 theorem int_diff_cases:
   584   obtains (diff) m n where "z = int m - int n"
   585 apply (cases z rule: eq_Abs_Integ)
   586 apply (rule_tac m=x and n=y in diff)
   587 apply (simp add: int_def minus add diff_minus)
   588 done
   589 
   590 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   591   -- {* Unfold all @{text let}s involving constants *}
   592   unfolding Let_def ..
   593 
   594 lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)"
   595   -- {* Unfold all @{text let}s involving constants *}
   596   unfolding Let_def ..
   597 
   598 text {* Unfold @{text min} and @{text max} on numerals. *}
   599 
   600 lemmas max_number_of [simp] =
   601   max_def [of "numeral u" "numeral v"]
   602   max_def [of "numeral u" "neg_numeral v"]
   603   max_def [of "neg_numeral u" "numeral v"]
   604   max_def [of "neg_numeral u" "neg_numeral v"] for u v
   605 
   606 lemmas min_number_of [simp] =
   607   min_def [of "numeral u" "numeral v"]
   608   min_def [of "numeral u" "neg_numeral v"]
   609   min_def [of "neg_numeral u" "numeral v"]
   610   min_def [of "neg_numeral u" "neg_numeral v"] for u v
   611 
   612 
   613 subsubsection {* Binary comparisons *}
   614 
   615 text {* Preliminaries *}
   616 
   617 lemma even_less_0_iff:
   618   "a + a < 0 \<longleftrightarrow> a < (0::'a::linordered_idom)"
   619 proof -
   620   have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib del: one_add_one)
   621   also have "(1+1)*a < 0 \<longleftrightarrow> a < 0"
   622     by (simp add: mult_less_0_iff zero_less_two 
   623                   order_less_not_sym [OF zero_less_two])
   624   finally show ?thesis .
   625 qed
   626 
   627 lemma le_imp_0_less: 
   628   assumes le: "0 \<le> z"
   629   shows "(0::int) < 1 + z"
   630 proof -
   631   have "0 \<le> z" by fact
   632   also have "... < z + 1" by (rule less_add_one)
   633   also have "... = 1 + z" by (simp add: add_ac)
   634   finally show "0 < 1 + z" .
   635 qed
   636 
   637 lemma odd_less_0_iff:
   638   "(1 + z + z < 0) = (z < (0::int))"
   639 proof (cases z)
   640   case (nonneg n)
   641   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
   642                              le_imp_0_less [THEN order_less_imp_le])  
   643 next
   644   case (neg n)
   645   thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1
   646     add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
   647 qed
   648 
   649 subsubsection {* Comparisons, for Ordered Rings *}
   650 
   651 lemmas double_eq_0_iff = double_zero
   652 
   653 lemma odd_nonzero:
   654   "1 + z + z \<noteq> (0::int)"
   655 proof (cases z)
   656   case (nonneg n)
   657   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
   658   thus ?thesis using  le_imp_0_less [OF le]
   659     by (auto simp add: add_assoc) 
   660 next
   661   case (neg n)
   662   show ?thesis
   663   proof
   664     assume eq: "1 + z + z = 0"
   665     have "(0::int) < 1 + (int n + int n)"
   666       by (simp add: le_imp_0_less add_increasing) 
   667     also have "... = - (1 + z + z)" 
   668       by (simp add: neg add_assoc [symmetric]) 
   669     also have "... = 0" by (simp add: eq) 
   670     finally have "0<0" ..
   671     thus False by blast
   672   qed
   673 qed
   674 
   675 
   676 subsection {* The Set of Integers *}
   677 
   678 context ring_1
   679 begin
   680 
   681 definition Ints  :: "'a set" where
   682   "Ints = range of_int"
   683 
   684 notation (xsymbols)
   685   Ints  ("\<int>")
   686 
   687 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
   688   by (simp add: Ints_def)
   689 
   690 lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
   691   using Ints_of_int [of "of_nat n"] by simp
   692 
   693 lemma Ints_0 [simp]: "0 \<in> \<int>"
   694   using Ints_of_int [of "0"] by simp
   695 
   696 lemma Ints_1 [simp]: "1 \<in> \<int>"
   697   using Ints_of_int [of "1"] by simp
   698 
   699 lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
   700 apply (auto simp add: Ints_def)
   701 apply (rule range_eqI)
   702 apply (rule of_int_add [symmetric])
   703 done
   704 
   705 lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
   706 apply (auto simp add: Ints_def)
   707 apply (rule range_eqI)
   708 apply (rule of_int_minus [symmetric])
   709 done
   710 
   711 lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
   712 apply (auto simp add: Ints_def)
   713 apply (rule range_eqI)
   714 apply (rule of_int_diff [symmetric])
   715 done
   716 
   717 lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
   718 apply (auto simp add: Ints_def)
   719 apply (rule range_eqI)
   720 apply (rule of_int_mult [symmetric])
   721 done
   722 
   723 lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
   724 by (induct n) simp_all
   725 
   726 lemma Ints_cases [cases set: Ints]:
   727   assumes "q \<in> \<int>"
   728   obtains (of_int) z where "q = of_int z"
   729   unfolding Ints_def
   730 proof -
   731   from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def .
   732   then obtain z where "q = of_int z" ..
   733   then show thesis ..
   734 qed
   735 
   736 lemma Ints_induct [case_names of_int, induct set: Ints]:
   737   "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
   738   by (rule Ints_cases) auto
   739 
   740 end
   741 
   742 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
   743 
   744 lemma Ints_double_eq_0_iff:
   745   assumes in_Ints: "a \<in> Ints"
   746   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
   747 proof -
   748   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   749   then obtain z where a: "a = of_int z" ..
   750   show ?thesis
   751   proof
   752     assume "a = 0"
   753     thus "a + a = 0" by simp
   754   next
   755     assume eq: "a + a = 0"
   756     hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
   757     hence "z + z = 0" by (simp only: of_int_eq_iff)
   758     hence "z = 0" by (simp only: double_eq_0_iff)
   759     thus "a = 0" by (simp add: a)
   760   qed
   761 qed
   762 
   763 lemma Ints_odd_nonzero:
   764   assumes in_Ints: "a \<in> Ints"
   765   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
   766 proof -
   767   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   768   then obtain z where a: "a = of_int z" ..
   769   show ?thesis
   770   proof
   771     assume eq: "1 + a + a = 0"
   772     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
   773     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
   774     with odd_nonzero show False by blast
   775   qed
   776 qed 
   777 
   778 lemma Nats_numeral [simp]: "numeral w \<in> Nats"
   779   using of_nat_in_Nats [of "numeral w"] by simp
   780 
   781 lemma Ints_odd_less_0: 
   782   assumes in_Ints: "a \<in> Ints"
   783   shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
   784 proof -
   785   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   786   then obtain z where a: "a = of_int z" ..
   787   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
   788     by (simp add: a)
   789   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff)
   790   also have "... = (a < 0)" by (simp add: a)
   791   finally show ?thesis .
   792 qed
   793 
   794 
   795 subsection {* @{term setsum} and @{term setprod} *}
   796 
   797 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
   798   apply (cases "finite A")
   799   apply (erule finite_induct, auto)
   800   done
   801 
   802 lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
   803   apply (cases "finite A")
   804   apply (erule finite_induct, auto)
   805   done
   806 
   807 lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
   808   apply (cases "finite A")
   809   apply (erule finite_induct, auto simp add: of_nat_mult)
   810   done
   811 
   812 lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
   813   apply (cases "finite A")
   814   apply (erule finite_induct, auto)
   815   done
   816 
   817 lemmas int_setsum = of_nat_setsum [where 'a=int]
   818 lemmas int_setprod = of_nat_setprod [where 'a=int]
   819 
   820 
   821 text {* Legacy theorems *}
   822 
   823 lemmas zle_int = of_nat_le_iff [where 'a=int]
   824 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
   825 lemmas numeral_1_eq_1 = numeral_One
   826 
   827 subsection {* Setting up simplification procedures *}
   828 
   829 lemmas int_arith_rules =
   830   neg_le_iff_le numeral_One
   831   minus_zero diff_minus left_minus right_minus
   832   mult_zero_left mult_zero_right mult_1_left mult_1_right
   833   mult_minus_left mult_minus_right
   834   minus_add_distrib minus_minus mult_assoc
   835   of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
   836   of_int_0 of_int_1 of_int_add of_int_mult
   837 
   838 use "Tools/numeral.ML"
   839 use "Tools/int_arith.ML"
   840 declaration {* K Int_Arith.setup *}
   841 
   842 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
   843   "(m::'a::linordered_idom) <= n" |
   844   "(m::'a::linordered_idom) = n") =
   845   {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
   846 
   847 setup {*
   848   Reorient_Proc.add
   849     (fn Const (@{const_name numeral}, _) $ _ => true
   850     | Const (@{const_name neg_numeral}, _) $ _ => true
   851     | _ => false)
   852 *}
   853 
   854 simproc_setup reorient_numeral
   855   ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
   856 
   857 
   858 subsection{*Lemmas About Small Numerals*}
   859 
   860 lemma abs_power_minus_one [simp]:
   861   "abs(-1 ^ n) = (1::'a::linordered_idom)"
   862 by (simp add: power_abs)
   863 
   864 
   865 subsection{*More Inequality Reasoning*}
   866 
   867 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
   868 by arith
   869 
   870 lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
   871 by arith
   872 
   873 lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
   874 by arith
   875 
   876 lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
   877 by arith
   878 
   879 lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
   880 by arith
   881 
   882 
   883 subsection{*The functions @{term nat} and @{term int}*}
   884 
   885 text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
   886   @{term "w + - z"}*}
   887 declare Zero_int_def [symmetric, simp]
   888 declare One_int_def [symmetric, simp]
   889 
   890 lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
   891 
   892 lemma nat_0 [simp]: "nat 0 = 0"
   893 by (simp add: nat_eq_iff)
   894 
   895 lemma nat_1 [simp]: "nat 1 = Suc 0"
   896 by (subst nat_eq_iff, simp)
   897 
   898 lemma nat_2: "nat 2 = Suc (Suc 0)"
   899 by (subst nat_eq_iff, simp)
   900 
   901 lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
   902 apply (insert zless_nat_conj [of 1 z])
   903 apply auto
   904 done
   905 
   906 text{*This simplifies expressions of the form @{term "int n = z"} where
   907       z is an integer literal.*}
   908 lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
   909 
   910 lemma split_nat [arith_split]:
   911   "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
   912   (is "?P = (?L & ?R)")
   913 proof (cases "i < 0")
   914   case True thus ?thesis by auto
   915 next
   916   case False
   917   have "?P = ?L"
   918   proof
   919     assume ?P thus ?L using False by clarsimp
   920   next
   921     assume ?L thus ?P using False by simp
   922   qed
   923   with False show ?thesis by simp
   924 qed
   925 
   926 context ring_1
   927 begin
   928 
   929 lemma of_int_of_nat [nitpick_simp]:
   930   "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
   931 proof (cases "k < 0")
   932   case True then have "0 \<le> - k" by simp
   933   then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
   934   with True show ?thesis by simp
   935 next
   936   case False then show ?thesis by (simp add: not_less of_nat_nat)
   937 qed
   938 
   939 end
   940 
   941 lemma nat_mult_distrib:
   942   fixes z z' :: int
   943   assumes "0 \<le> z"
   944   shows "nat (z * z') = nat z * nat z'"
   945 proof (cases "0 \<le> z'")
   946   case False with assms have "z * z' \<le> 0"
   947     by (simp add: not_le mult_le_0_iff)
   948   then have "nat (z * z') = 0" by simp
   949   moreover from False have "nat z' = 0" by simp
   950   ultimately show ?thesis by simp
   951 next
   952   case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
   953   show ?thesis
   954     by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
   955       (simp only: of_nat_mult of_nat_nat [OF True]
   956          of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
   957 qed
   958 
   959 lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
   960 apply (rule trans)
   961 apply (rule_tac [2] nat_mult_distrib, auto)
   962 done
   963 
   964 lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
   965 apply (cases "z=0 | w=0")
   966 apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
   967                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
   968 done
   969 
   970 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
   971 apply (rule sym)
   972 apply (simp add: nat_eq_iff)
   973 done
   974 
   975 lemma diff_nat_eq_if:
   976      "nat z - nat z' =  
   977         (if z' < 0 then nat z   
   978          else let d = z-z' in     
   979               if d < 0 then 0 else nat d)"
   980 by (simp add: Let_def nat_diff_distrib [symmetric])
   981 
   982 (* nat_diff_distrib has too-strong premises *)
   983 lemma nat_diff_distrib': "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x - y) = nat x - nat y"
   984 apply (rule int_int_eq [THEN iffD1], clarsimp)
   985 apply (subst of_nat_diff)
   986 apply (rule nat_mono, simp_all)
   987 done
   988 
   989 lemma nat_numeral [simp, code_abbrev]:
   990   "nat (numeral k) = numeral k"
   991   by (simp add: nat_eq_iff)
   992 
   993 lemma nat_neg_numeral [simp]:
   994   "nat (neg_numeral k) = 0"
   995   by simp
   996 
   997 lemma diff_nat_numeral [simp]: 
   998   "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
   999   by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
  1000 
  1001 lemma nat_numeral_diff_1 [simp]:
  1002   "numeral v - (1::nat) = nat (numeral v - 1)"
  1003   using diff_nat_numeral [of v Num.One] by simp
  1004 
  1005 
  1006 subsection "Induction principles for int"
  1007 
  1008 text{*Well-founded segments of the integers*}
  1009 
  1010 definition
  1011   int_ge_less_than  ::  "int => (int * int) set"
  1012 where
  1013   "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
  1014 
  1015 theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
  1016 proof -
  1017   have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
  1018     by (auto simp add: int_ge_less_than_def)
  1019   thus ?thesis 
  1020     by (rule wf_subset [OF wf_measure]) 
  1021 qed
  1022 
  1023 text{*This variant looks odd, but is typical of the relations suggested
  1024 by RankFinder.*}
  1025 
  1026 definition
  1027   int_ge_less_than2 ::  "int => (int * int) set"
  1028 where
  1029   "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
  1030 
  1031 theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
  1032 proof -
  1033   have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))" 
  1034     by (auto simp add: int_ge_less_than2_def)
  1035   thus ?thesis 
  1036     by (rule wf_subset [OF wf_measure]) 
  1037 qed
  1038 
  1039 (* `set:int': dummy construction *)
  1040 theorem int_ge_induct [case_names base step, induct set: int]:
  1041   fixes i :: int
  1042   assumes ge: "k \<le> i" and
  1043     base: "P k" and
  1044     step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
  1045   shows "P i"
  1046 proof -
  1047   { fix n
  1048     have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
  1049     proof (induct n)
  1050       case 0
  1051       hence "i = k" by arith
  1052       thus "P i" using base by simp
  1053     next
  1054       case (Suc n)
  1055       then have "n = nat((i - 1) - k)" by arith
  1056       moreover
  1057       have ki1: "k \<le> i - 1" using Suc.prems by arith
  1058       ultimately
  1059       have "P (i - 1)" by (rule Suc.hyps)
  1060       from step [OF ki1 this] show ?case by simp
  1061     qed
  1062   }
  1063   with ge show ?thesis by fast
  1064 qed
  1065 
  1066 (* `set:int': dummy construction *)
  1067 theorem int_gr_induct [case_names base step, induct set: int]:
  1068   assumes gr: "k < (i::int)" and
  1069         base: "P(k+1)" and
  1070         step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
  1071   shows "P i"
  1072 apply(rule int_ge_induct[of "k + 1"])
  1073   using gr apply arith
  1074  apply(rule base)
  1075 apply (rule step, simp+)
  1076 done
  1077 
  1078 theorem int_le_induct [consumes 1, case_names base step]:
  1079   assumes le: "i \<le> (k::int)" and
  1080         base: "P(k)" and
  1081         step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
  1082   shows "P i"
  1083 proof -
  1084   { fix n
  1085     have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
  1086     proof (induct n)
  1087       case 0
  1088       hence "i = k" by arith
  1089       thus "P i" using base by simp
  1090     next
  1091       case (Suc n)
  1092       hence "n = nat (k - (i + 1))" by arith
  1093       moreover
  1094       have ki1: "i + 1 \<le> k" using Suc.prems by arith
  1095       ultimately
  1096       have "P (i + 1)" by(rule Suc.hyps)
  1097       from step[OF ki1 this] show ?case by simp
  1098     qed
  1099   }
  1100   with le show ?thesis by fast
  1101 qed
  1102 
  1103 theorem int_less_induct [consumes 1, case_names base step]:
  1104   assumes less: "(i::int) < k" and
  1105         base: "P(k - 1)" and
  1106         step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
  1107   shows "P i"
  1108 apply(rule int_le_induct[of _ "k - 1"])
  1109   using less apply arith
  1110  apply(rule base)
  1111 apply (rule step, simp+)
  1112 done
  1113 
  1114 theorem int_induct [case_names base step1 step2]:
  1115   fixes k :: int
  1116   assumes base: "P k"
  1117     and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
  1118     and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
  1119   shows "P i"
  1120 proof -
  1121   have "i \<le> k \<or> i \<ge> k" by arith
  1122   then show ?thesis
  1123   proof
  1124     assume "i \<ge> k"
  1125     then show ?thesis using base
  1126       by (rule int_ge_induct) (fact step1)
  1127   next
  1128     assume "i \<le> k"
  1129     then show ?thesis using base
  1130       by (rule int_le_induct) (fact step2)
  1131   qed
  1132 qed
  1133 
  1134 subsection{*Intermediate value theorems*}
  1135 
  1136 lemma int_val_lemma:
  1137      "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
  1138       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
  1139 unfolding One_nat_def
  1140 apply (induct n)
  1141 apply simp
  1142 apply (intro strip)
  1143 apply (erule impE, simp)
  1144 apply (erule_tac x = n in allE, simp)
  1145 apply (case_tac "k = f (Suc n)")
  1146 apply force
  1147 apply (erule impE)
  1148  apply (simp add: abs_if split add: split_if_asm)
  1149 apply (blast intro: le_SucI)
  1150 done
  1151 
  1152 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
  1153 
  1154 lemma nat_intermed_int_val:
  1155      "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
  1156          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
  1157 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
  1158        in int_val_lemma)
  1159 unfolding One_nat_def
  1160 apply simp
  1161 apply (erule exE)
  1162 apply (rule_tac x = "i+m" in exI, arith)
  1163 done
  1164 
  1165 
  1166 subsection{*Products and 1, by T. M. Rasmussen*}
  1167 
  1168 lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
  1169 by arith
  1170 
  1171 lemma abs_zmult_eq_1:
  1172   assumes mn: "\<bar>m * n\<bar> = 1"
  1173   shows "\<bar>m\<bar> = (1::int)"
  1174 proof -
  1175   have 0: "m \<noteq> 0 & n \<noteq> 0" using mn
  1176     by auto
  1177   have "~ (2 \<le> \<bar>m\<bar>)"
  1178   proof
  1179     assume "2 \<le> \<bar>m\<bar>"
  1180     hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>"
  1181       by (simp add: mult_mono 0) 
  1182     also have "... = \<bar>m*n\<bar>" 
  1183       by (simp add: abs_mult)
  1184     also have "... = 1"
  1185       by (simp add: mn)
  1186     finally have "2*\<bar>n\<bar> \<le> 1" .
  1187     thus "False" using 0
  1188       by arith
  1189   qed
  1190   thus ?thesis using 0
  1191     by auto
  1192 qed
  1193 
  1194 ML_val {* @{const_name neg_numeral} *}
  1195 
  1196 lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
  1197 by (insert abs_zmult_eq_1 [of m n], arith)
  1198 
  1199 lemma pos_zmult_eq_1_iff:
  1200   assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)"
  1201 proof -
  1202   from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma)
  1203   thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma)
  1204 qed
  1205 
  1206 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
  1207 apply (rule iffI) 
  1208  apply (frule pos_zmult_eq_1_iff_lemma)
  1209  apply (simp add: mult_commute [of m]) 
  1210  apply (frule pos_zmult_eq_1_iff_lemma, auto) 
  1211 done
  1212 
  1213 lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
  1214 proof
  1215   assume "finite (UNIV::int set)"
  1216   moreover have "inj (\<lambda>i\<Colon>int. 2 * i)"
  1217     by (rule injI) simp
  1218   ultimately have "surj (\<lambda>i\<Colon>int. 2 * i)"
  1219     by (rule finite_UNIV_inj_surj)
  1220   then obtain i :: int where "1 = 2 * i" by (rule surjE)
  1221   then show False by (simp add: pos_zmult_eq_1_iff)
  1222 qed
  1223 
  1224 
  1225 subsection {* Further theorems on numerals *}
  1226 
  1227 subsubsection{*Special Simplification for Constants*}
  1228 
  1229 text{*These distributive laws move literals inside sums and differences.*}
  1230 
  1231 lemmas left_distrib_numeral [simp] = left_distrib [of _ _ "numeral v"] for v
  1232 lemmas right_distrib_numeral [simp] = right_distrib [of "numeral v"] for v
  1233 lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
  1234 lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
  1235 
  1236 text{*These are actually for fields, like real: but where else to put them?*}
  1237 
  1238 lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w
  1239 lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w
  1240 lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w
  1241 lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
  1242 
  1243 
  1244 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
  1245   strange, but then other simprocs simplify the quotient.*}
  1246 
  1247 lemmas inverse_eq_divide_numeral [simp] =
  1248   inverse_eq_divide [of "numeral w"] for w
  1249 
  1250 lemmas inverse_eq_divide_neg_numeral [simp] =
  1251   inverse_eq_divide [of "neg_numeral w"] for w
  1252 
  1253 text {*These laws simplify inequalities, moving unary minus from a term
  1254 into the literal.*}
  1255 
  1256 lemmas le_minus_iff_numeral [simp, no_atp] =
  1257   le_minus_iff [of "numeral v"]
  1258   le_minus_iff [of "neg_numeral v"] for v
  1259 
  1260 lemmas equation_minus_iff_numeral [simp, no_atp] =
  1261   equation_minus_iff [of "numeral v"]
  1262   equation_minus_iff [of "neg_numeral v"] for v
  1263 
  1264 lemmas minus_less_iff_numeral [simp, no_atp] =
  1265   minus_less_iff [of _ "numeral v"]
  1266   minus_less_iff [of _ "neg_numeral v"] for v
  1267 
  1268 lemmas minus_le_iff_numeral [simp, no_atp] =
  1269   minus_le_iff [of _ "numeral v"]
  1270   minus_le_iff [of _ "neg_numeral v"] for v
  1271 
  1272 lemmas minus_equation_iff_numeral [simp, no_atp] =
  1273   minus_equation_iff [of _ "numeral v"]
  1274   minus_equation_iff [of _ "neg_numeral v"] for v
  1275 
  1276 text{*To Simplify Inequalities Where One Side is the Constant 1*}
  1277 
  1278 lemma less_minus_iff_1 [simp,no_atp]:
  1279   fixes b::"'b::linordered_idom"
  1280   shows "(1 < - b) = (b < -1)"
  1281 by auto
  1282 
  1283 lemma le_minus_iff_1 [simp,no_atp]:
  1284   fixes b::"'b::linordered_idom"
  1285   shows "(1 \<le> - b) = (b \<le> -1)"
  1286 by auto
  1287 
  1288 lemma equation_minus_iff_1 [simp,no_atp]:
  1289   fixes b::"'b::ring_1"
  1290   shows "(1 = - b) = (b = -1)"
  1291 by (subst equation_minus_iff, auto)
  1292 
  1293 lemma minus_less_iff_1 [simp,no_atp]:
  1294   fixes a::"'b::linordered_idom"
  1295   shows "(- a < 1) = (-1 < a)"
  1296 by auto
  1297 
  1298 lemma minus_le_iff_1 [simp,no_atp]:
  1299   fixes a::"'b::linordered_idom"
  1300   shows "(- a \<le> 1) = (-1 \<le> a)"
  1301 by auto
  1302 
  1303 lemma minus_equation_iff_1 [simp,no_atp]:
  1304   fixes a::"'b::ring_1"
  1305   shows "(- a = 1) = (a = -1)"
  1306 by (subst minus_equation_iff, auto)
  1307 
  1308 
  1309 text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
  1310 
  1311 lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v
  1312 lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v
  1313 lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v
  1314 lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v
  1315 
  1316 
  1317 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
  1318 
  1319 lemmas le_divide_eq_numeral1 [simp] =
  1320   pos_le_divide_eq [of "numeral w", OF zero_less_numeral]
  1321   neg_le_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
  1322 
  1323 lemmas divide_le_eq_numeral1 [simp] =
  1324   pos_divide_le_eq [of "numeral w", OF zero_less_numeral]
  1325   neg_divide_le_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
  1326 
  1327 lemmas less_divide_eq_numeral1 [simp] =
  1328   pos_less_divide_eq [of "numeral w", OF zero_less_numeral]
  1329   neg_less_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
  1330 
  1331 lemmas divide_less_eq_numeral1 [simp] =
  1332   pos_divide_less_eq [of "numeral w", OF zero_less_numeral]
  1333   neg_divide_less_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w
  1334 
  1335 lemmas eq_divide_eq_numeral1 [simp] =
  1336   eq_divide_eq [of _ _ "numeral w"]
  1337   eq_divide_eq [of _ _ "neg_numeral w"] for w
  1338 
  1339 lemmas divide_eq_eq_numeral1 [simp] =
  1340   divide_eq_eq [of _ "numeral w"]
  1341   divide_eq_eq [of _ "neg_numeral w"] for w
  1342 
  1343 subsubsection{*Optional Simplification Rules Involving Constants*}
  1344 
  1345 text{*Simplify quotients that are compared with a literal constant.*}
  1346 
  1347 lemmas le_divide_eq_numeral =
  1348   le_divide_eq [of "numeral w"]
  1349   le_divide_eq [of "neg_numeral w"] for w
  1350 
  1351 lemmas divide_le_eq_numeral =
  1352   divide_le_eq [of _ _ "numeral w"]
  1353   divide_le_eq [of _ _ "neg_numeral w"] for w
  1354 
  1355 lemmas less_divide_eq_numeral =
  1356   less_divide_eq [of "numeral w"]
  1357   less_divide_eq [of "neg_numeral w"] for w
  1358 
  1359 lemmas divide_less_eq_numeral =
  1360   divide_less_eq [of _ _ "numeral w"]
  1361   divide_less_eq [of _ _ "neg_numeral w"] for w
  1362 
  1363 lemmas eq_divide_eq_numeral =
  1364   eq_divide_eq [of "numeral w"]
  1365   eq_divide_eq [of "neg_numeral w"] for w
  1366 
  1367 lemmas divide_eq_eq_numeral =
  1368   divide_eq_eq [of _ _ "numeral w"]
  1369   divide_eq_eq [of _ _ "neg_numeral w"] for w
  1370 
  1371 
  1372 text{*Not good as automatic simprules because they cause case splits.*}
  1373 lemmas divide_const_simps =
  1374   le_divide_eq_numeral divide_le_eq_numeral less_divide_eq_numeral
  1375   divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral
  1376   le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
  1377 
  1378 text{*Division By @{text "-1"}*}
  1379 
  1380 lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x"
  1381   unfolding minus_one [symmetric]
  1382   unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric]
  1383   by simp
  1384 
  1385 lemma minus1_divide [simp]: "-1 / (x::'a::field) = - (1 / x)"
  1386   unfolding minus_one [symmetric] by (rule divide_minus_left)
  1387 
  1388 lemma half_gt_zero_iff:
  1389      "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))"
  1390 by auto
  1391 
  1392 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
  1393 
  1394 lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x"
  1395   by simp
  1396 
  1397 
  1398 subsection {* The divides relation *}
  1399 
  1400 lemma zdvd_antisym_nonneg:
  1401     "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
  1402   apply (simp add: dvd_def, auto)
  1403   apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff)
  1404   done
  1405 
  1406 lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" 
  1407   shows "\<bar>a\<bar> = \<bar>b\<bar>"
  1408 proof cases
  1409   assume "a = 0" with assms show ?thesis by simp
  1410 next
  1411   assume "a \<noteq> 0"
  1412   from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
  1413   from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
  1414   from k k' have "a = a*k*k'" by simp
  1415   with mult_cancel_left1[where c="a" and b="k*k'"]
  1416   have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
  1417   hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
  1418   thus ?thesis using k k' by auto
  1419 qed
  1420 
  1421 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
  1422   apply (subgoal_tac "m = n + (m - n)")
  1423    apply (erule ssubst)
  1424    apply (blast intro: dvd_add, simp)
  1425   done
  1426 
  1427 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
  1428 apply (rule iffI)
  1429  apply (erule_tac [2] dvd_add)
  1430  apply (subgoal_tac "n = (n + k * m) - k * m")
  1431   apply (erule ssubst)
  1432   apply (erule dvd_diff)
  1433   apply(simp_all)
  1434 done
  1435 
  1436 lemma dvd_imp_le_int:
  1437   fixes d i :: int
  1438   assumes "i \<noteq> 0" and "d dvd i"
  1439   shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
  1440 proof -
  1441   from `d dvd i` obtain k where "i = d * k" ..
  1442   with `i \<noteq> 0` have "k \<noteq> 0" by auto
  1443   then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
  1444   then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
  1445   with `i = d * k` show ?thesis by (simp add: abs_mult)
  1446 qed
  1447 
  1448 lemma zdvd_not_zless:
  1449   fixes m n :: int
  1450   assumes "0 < m" and "m < n"
  1451   shows "\<not> n dvd m"
  1452 proof
  1453   from assms have "0 < n" by auto
  1454   assume "n dvd m" then obtain k where k: "m = n * k" ..
  1455   with `0 < m` have "0 < n * k" by auto
  1456   with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
  1457   with k `0 < n` `m < n` have "n * k < n * 1" by simp
  1458   with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
  1459 qed
  1460 
  1461 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
  1462   shows "m dvd n"
  1463 proof-
  1464   from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
  1465   {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
  1466     with h have False by (simp add: mult_assoc)}
  1467   hence "n = m * h" by blast
  1468   thus ?thesis by simp
  1469 qed
  1470 
  1471 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
  1472 proof -
  1473   have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
  1474   proof -
  1475     fix k
  1476     assume A: "int y = int x * k"
  1477     then show "x dvd y"
  1478     proof (cases k)
  1479       case (nonneg n)
  1480       with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
  1481       then show ?thesis ..
  1482     next
  1483       case (neg n)
  1484       with A have "int y = int x * (- int (Suc n))" by simp
  1485       also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
  1486       also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
  1487       finally have "- int (x * Suc n) = int y" ..
  1488       then show ?thesis by (simp only: negative_eq_positive) auto
  1489     qed
  1490   qed
  1491   then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
  1492 qed
  1493 
  1494 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\<bar>x\<bar> = 1)"
  1495 proof
  1496   assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
  1497   hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
  1498   hence "nat \<bar>x\<bar> = 1"  by simp
  1499   thus "\<bar>x\<bar> = 1" by (cases "x < 0") auto
  1500 next
  1501   assume "\<bar>x\<bar>=1"
  1502   then have "x = 1 \<or> x = -1" by auto
  1503   then show "x dvd 1" by (auto intro: dvdI)
  1504 qed
  1505 
  1506 lemma zdvd_mult_cancel1: 
  1507   assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
  1508 proof
  1509   assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m" 
  1510     by (cases "n >0") (auto simp add: minus_equation_iff)
  1511 next
  1512   assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
  1513   from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
  1514 qed
  1515 
  1516 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
  1517   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
  1518 
  1519 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
  1520   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
  1521 
  1522 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
  1523   by (auto simp add: dvd_int_iff)
  1524 
  1525 lemma eq_nat_nat_iff:
  1526   "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
  1527   by (auto elim!: nonneg_eq_int)
  1528 
  1529 lemma nat_power_eq:
  1530   "0 \<le> z \<Longrightarrow> nat (z ^ n) = nat z ^ n"
  1531   by (induct n) (simp_all add: nat_mult_distrib)
  1532 
  1533 lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
  1534   apply (cases n)
  1535   apply (auto simp add: dvd_int_iff)
  1536   apply (cases z)
  1537   apply (auto simp add: dvd_imp_le)
  1538   done
  1539 
  1540 lemma zdvd_period:
  1541   fixes a d :: int
  1542   assumes "a dvd d"
  1543   shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
  1544 proof -
  1545   from assms obtain k where "d = a * k" by (rule dvdE)
  1546   show ?thesis
  1547   proof
  1548     assume "a dvd (x + t)"
  1549     then obtain l where "x + t = a * l" by (rule dvdE)
  1550     then have "x = a * l - t" by simp
  1551     with `d = a * k` show "a dvd x + c * d + t" by simp
  1552   next
  1553     assume "a dvd x + c * d + t"
  1554     then obtain l where "x + c * d + t = a * l" by (rule dvdE)
  1555     then have "x = a * l - c * d - t" by simp
  1556     with `d = a * k` show "a dvd (x + t)" by simp
  1557   qed
  1558 qed
  1559 
  1560 
  1561 subsection {* Finiteness of intervals *}
  1562 
  1563 lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}"
  1564 proof (cases "a <= b")
  1565   case True
  1566   from this show ?thesis
  1567   proof (induct b rule: int_ge_induct)
  1568     case base
  1569     have "{i. a <= i & i <= a} = {a}" by auto
  1570     from this show ?case by simp
  1571   next
  1572     case (step b)
  1573     from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \<union> {b + 1}" by auto
  1574     from this step show ?case by simp
  1575   qed
  1576 next
  1577   case False from this show ?thesis
  1578     by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans)
  1579 qed
  1580 
  1581 lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}"
  1582 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
  1583 
  1584 lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}"
  1585 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
  1586 
  1587 lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}"
  1588 by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
  1589 
  1590 
  1591 subsection {* Configuration of the code generator *}
  1592 
  1593 text {* Constructors *}
  1594 
  1595 definition Pos :: "num \<Rightarrow> int" where
  1596   [simp, code_abbrev]: "Pos = numeral"
  1597 
  1598 definition Neg :: "num \<Rightarrow> int" where
  1599   [simp, code_abbrev]: "Neg = neg_numeral"
  1600 
  1601 code_datatype "0::int" Pos Neg
  1602 
  1603 
  1604 text {* Auxiliary operations *}
  1605 
  1606 definition dup :: "int \<Rightarrow> int" where
  1607   [simp]: "dup k = k + k"
  1608 
  1609 lemma dup_code [code]:
  1610   "dup 0 = 0"
  1611   "dup (Pos n) = Pos (Num.Bit0 n)"
  1612   "dup (Neg n) = Neg (Num.Bit0 n)"
  1613   unfolding Pos_def Neg_def neg_numeral_def
  1614   by (simp_all add: numeral_Bit0)
  1615 
  1616 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
  1617   [simp]: "sub m n = numeral m - numeral n"
  1618 
  1619 lemma sub_code [code]:
  1620   "sub Num.One Num.One = 0"
  1621   "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)"
  1622   "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)"
  1623   "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)"
  1624   "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)"
  1625   "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)"
  1626   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
  1627   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
  1628   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
  1629   unfolding sub_def dup_def numeral.simps Pos_def Neg_def
  1630     neg_numeral_def numeral_BitM
  1631   by (simp_all only: algebra_simps)
  1632 
  1633 
  1634 text {* Implementations *}
  1635 
  1636 lemma one_int_code [code, code_unfold]:
  1637   "1 = Pos Num.One"
  1638   by simp
  1639 
  1640 lemma plus_int_code [code]:
  1641   "k + 0 = (k::int)"
  1642   "0 + l = (l::int)"
  1643   "Pos m + Pos n = Pos (m + n)"
  1644   "Pos m + Neg n = sub m n"
  1645   "Neg m + Pos n = sub n m"
  1646   "Neg m + Neg n = Neg (m + n)"
  1647   by simp_all
  1648 
  1649 lemma uminus_int_code [code]:
  1650   "uminus 0 = (0::int)"
  1651   "uminus (Pos m) = Neg m"
  1652   "uminus (Neg m) = Pos m"
  1653   by simp_all
  1654 
  1655 lemma minus_int_code [code]:
  1656   "k - 0 = (k::int)"
  1657   "0 - l = uminus (l::int)"
  1658   "Pos m - Pos n = sub m n"
  1659   "Pos m - Neg n = Pos (m + n)"
  1660   "Neg m - Pos n = Neg (m + n)"
  1661   "Neg m - Neg n = sub n m"
  1662   by simp_all
  1663 
  1664 lemma times_int_code [code]:
  1665   "k * 0 = (0::int)"
  1666   "0 * l = (0::int)"
  1667   "Pos m * Pos n = Pos (m * n)"
  1668   "Pos m * Neg n = Neg (m * n)"
  1669   "Neg m * Pos n = Neg (m * n)"
  1670   "Neg m * Neg n = Pos (m * n)"
  1671   by simp_all
  1672 
  1673 instantiation int :: equal
  1674 begin
  1675 
  1676 definition
  1677   "HOL.equal k l \<longleftrightarrow> k = (l::int)"
  1678 
  1679 instance by default (rule equal_int_def)
  1680 
  1681 end
  1682 
  1683 lemma equal_int_code [code]:
  1684   "HOL.equal 0 (0::int) \<longleftrightarrow> True"
  1685   "HOL.equal 0 (Pos l) \<longleftrightarrow> False"
  1686   "HOL.equal 0 (Neg l) \<longleftrightarrow> False"
  1687   "HOL.equal (Pos k) 0 \<longleftrightarrow> False"
  1688   "HOL.equal (Pos k) (Pos l) \<longleftrightarrow> HOL.equal k l"
  1689   "HOL.equal (Pos k) (Neg l) \<longleftrightarrow> False"
  1690   "HOL.equal (Neg k) 0 \<longleftrightarrow> False"
  1691   "HOL.equal (Neg k) (Pos l) \<longleftrightarrow> False"
  1692   "HOL.equal (Neg k) (Neg l) \<longleftrightarrow> HOL.equal k l"
  1693   by (auto simp add: equal)
  1694 
  1695 lemma equal_int_refl [code nbe]:
  1696   "HOL.equal (k::int) k \<longleftrightarrow> True"
  1697   by (fact equal_refl)
  1698 
  1699 lemma less_eq_int_code [code]:
  1700   "0 \<le> (0::int) \<longleftrightarrow> True"
  1701   "0 \<le> Pos l \<longleftrightarrow> True"
  1702   "0 \<le> Neg l \<longleftrightarrow> False"
  1703   "Pos k \<le> 0 \<longleftrightarrow> False"
  1704   "Pos k \<le> Pos l \<longleftrightarrow> k \<le> l"
  1705   "Pos k \<le> Neg l \<longleftrightarrow> False"
  1706   "Neg k \<le> 0 \<longleftrightarrow> True"
  1707   "Neg k \<le> Pos l \<longleftrightarrow> True"
  1708   "Neg k \<le> Neg l \<longleftrightarrow> l \<le> k"
  1709   by simp_all
  1710 
  1711 lemma less_int_code [code]:
  1712   "0 < (0::int) \<longleftrightarrow> False"
  1713   "0 < Pos l \<longleftrightarrow> True"
  1714   "0 < Neg l \<longleftrightarrow> False"
  1715   "Pos k < 0 \<longleftrightarrow> False"
  1716   "Pos k < Pos l \<longleftrightarrow> k < l"
  1717   "Pos k < Neg l \<longleftrightarrow> False"
  1718   "Neg k < 0 \<longleftrightarrow> True"
  1719   "Neg k < Pos l \<longleftrightarrow> True"
  1720   "Neg k < Neg l \<longleftrightarrow> l < k"
  1721   by simp_all
  1722 
  1723 lemma nat_code [code]:
  1724   "nat (Int.Neg k) = 0"
  1725   "nat 0 = 0"
  1726   "nat (Int.Pos k) = nat_of_num k"
  1727   by (simp_all add: nat_of_num_numeral nat_numeral)
  1728 
  1729 lemma (in ring_1) of_int_code [code]:
  1730   "of_int (Int.Neg k) = neg_numeral k"
  1731   "of_int 0 = 0"
  1732   "of_int (Int.Pos k) = numeral k"
  1733   by simp_all
  1734 
  1735 
  1736 text {* Serializer setup *}
  1737 
  1738 code_modulename SML
  1739   Int Arith
  1740 
  1741 code_modulename OCaml
  1742   Int Arith
  1743 
  1744 code_modulename Haskell
  1745   Int Arith
  1746 
  1747 quickcheck_params [default_type = int]
  1748 
  1749 hide_const (open) Pos Neg sub dup
  1750 
  1751 
  1752 subsection {* Legacy theorems *}
  1753 
  1754 lemmas inj_int = inj_of_nat [where 'a=int]
  1755 lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
  1756 lemmas int_mult = of_nat_mult [where 'a=int]
  1757 lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
  1758 lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
  1759 lemmas zless_int = of_nat_less_iff [where 'a=int]
  1760 lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k
  1761 lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
  1762 lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
  1763 lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n
  1764 lemmas int_0 = of_nat_0 [where 'a=int]
  1765 lemmas int_1 = of_nat_1 [where 'a=int]
  1766 lemmas int_Suc = of_nat_Suc [where 'a=int]
  1767 lemmas int_numeral = of_nat_numeral [where 'a=int]
  1768 lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
  1769 lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
  1770 lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
  1771 
  1772 lemma zpower_zpower:
  1773   "(x ^ y) ^ z = (x ^ (y * z)::int)"
  1774   by (rule power_mult [symmetric])
  1775 
  1776 lemma int_power:
  1777   "int (m ^ n) = int m ^ n"
  1778   by (rule of_nat_power)
  1779 
  1780 lemmas zpower_int = int_power [symmetric]
  1781 
  1782 end