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