src/HOL/IntArith.thy
author haftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728 e2b3a1065676
parent 24195 7d1a16c77f7c
child 25162 ad4d5365d9d8
permissions -rw-r--r--
moved Finite_Set before Datatype
wenzelm@23164
     1
(*  Title:      HOL/IntArith.thy
wenzelm@23164
     2
    ID:         $Id$
wenzelm@23164
     3
    Authors:    Larry Paulson and Tobias Nipkow
wenzelm@23164
     4
*)
wenzelm@23164
     5
wenzelm@23164
     6
header {* Integer arithmetic *}
wenzelm@23164
     7
wenzelm@23164
     8
theory IntArith
wenzelm@23164
     9
imports Numeral Wellfounded_Relations
haftmann@23263
    10
uses
haftmann@23263
    11
  "~~/src/Provers/Arith/assoc_fold.ML"
haftmann@23263
    12
  "~~/src/Provers/Arith/cancel_numerals.ML"
haftmann@23263
    13
  "~~/src/Provers/Arith/combine_numerals.ML"
haftmann@23263
    14
  ("int_arith1.ML")
wenzelm@23164
    15
begin
wenzelm@23164
    16
wenzelm@23164
    17
subsection{*Inequality Reasoning for the Arithmetic Simproc*}
wenzelm@23164
    18
wenzelm@23164
    19
lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
wenzelm@23164
    20
by simp 
wenzelm@23164
    21
wenzelm@23164
    22
lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
wenzelm@23164
    23
by simp
wenzelm@23164
    24
wenzelm@23164
    25
lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
wenzelm@23164
    26
by simp 
wenzelm@23164
    27
wenzelm@23164
    28
lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
wenzelm@23164
    29
by simp
wenzelm@23164
    30
wenzelm@23164
    31
lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})"
wenzelm@23164
    32
by simp
wenzelm@23164
    33
wenzelm@23164
    34
lemma inverse_numeral_1:
wenzelm@23164
    35
  "inverse Numeral1 = (Numeral1::'a::{number_ring,field})"
wenzelm@23164
    36
by simp
wenzelm@23164
    37
wenzelm@23164
    38
text{*Theorem lists for the cancellation simprocs. The use of binary numerals
wenzelm@23164
    39
for 0 and 1 reduces the number of special cases.*}
wenzelm@23164
    40
wenzelm@23164
    41
lemmas add_0s = add_numeral_0 add_numeral_0_right
wenzelm@23164
    42
lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
wenzelm@23164
    43
                 mult_minus1 mult_minus1_right
wenzelm@23164
    44
wenzelm@23164
    45
wenzelm@23164
    46
subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
wenzelm@23164
    47
wenzelm@23164
    48
text{*Arithmetic computations are defined for binary literals, which leaves 0
wenzelm@23164
    49
and 1 as special cases. Addition already has rules for 0, but not 1.
wenzelm@23164
    50
Multiplication and unary minus already have rules for both 0 and 1.*}
wenzelm@23164
    51
wenzelm@23164
    52
wenzelm@23164
    53
lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
wenzelm@23164
    54
by simp
wenzelm@23164
    55
wenzelm@23164
    56
wenzelm@23164
    57
lemmas add_number_of_eq = number_of_add [symmetric]
wenzelm@23164
    58
wenzelm@23164
    59
text{*Allow 1 on either or both sides*}
wenzelm@23164
    60
lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
wenzelm@23164
    61
by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
wenzelm@23164
    62
wenzelm@23164
    63
lemmas add_special =
wenzelm@23164
    64
    one_add_one_is_two
wenzelm@23164
    65
    binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
wenzelm@23164
    66
    binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
wenzelm@23164
    67
wenzelm@23164
    68
text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
wenzelm@23164
    69
lemmas diff_special =
wenzelm@23164
    70
    binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
wenzelm@23164
    71
    binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
wenzelm@23164
    72
wenzelm@23164
    73
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
wenzelm@23164
    74
lemmas eq_special =
wenzelm@23164
    75
    binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
wenzelm@23164
    76
    binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
wenzelm@23164
    77
    binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
wenzelm@23164
    78
    binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
wenzelm@23164
    79
wenzelm@23164
    80
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
wenzelm@23164
    81
lemmas less_special =
wenzelm@23164
    82
  binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard]
wenzelm@23164
    83
  binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard]
wenzelm@23164
    84
  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard]
wenzelm@23164
    85
  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard]
wenzelm@23164
    86
wenzelm@23164
    87
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
wenzelm@23164
    88
lemmas le_special =
wenzelm@23164
    89
    binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard]
wenzelm@23164
    90
    binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard]
wenzelm@23164
    91
    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
wenzelm@23164
    92
    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
wenzelm@23164
    93
wenzelm@23164
    94
lemmas arith_special[simp] = 
wenzelm@23164
    95
       add_special diff_special eq_special less_special le_special
wenzelm@23164
    96
wenzelm@23164
    97
wenzelm@23164
    98
lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 &
wenzelm@23164
    99
                   max (0::int) 1 = 1 & max (1::int) 0 = 1"
wenzelm@23164
   100
by(simp add:min_def max_def)
wenzelm@23164
   101
wenzelm@23164
   102
lemmas min_max_special[simp] =
wenzelm@23164
   103
 min_max_01
wenzelm@23164
   104
 max_def[of "0::int" "number_of v", standard, simp]
wenzelm@23164
   105
 min_def[of "0::int" "number_of v", standard, simp]
wenzelm@23164
   106
 max_def[of "number_of u" "0::int", standard, simp]
wenzelm@23164
   107
 min_def[of "number_of u" "0::int", standard, simp]
wenzelm@23164
   108
 max_def[of "1::int" "number_of v", standard, simp]
wenzelm@23164
   109
 min_def[of "1::int" "number_of v", standard, simp]
wenzelm@23164
   110
 max_def[of "number_of u" "1::int", standard, simp]
wenzelm@23164
   111
 min_def[of "number_of u" "1::int", standard, simp]
wenzelm@23164
   112
wenzelm@23164
   113
use "int_arith1.ML"
wenzelm@24075
   114
declaration {* K int_arith_setup *}
wenzelm@23164
   115
wenzelm@23164
   116
wenzelm@23164
   117
subsection{*Lemmas About Small Numerals*}
wenzelm@23164
   118
wenzelm@23164
   119
lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
wenzelm@23164
   120
proof -
wenzelm@23164
   121
  have "(of_int -1 :: 'a) = of_int (- 1)" by simp
wenzelm@23164
   122
  also have "... = - of_int 1" by (simp only: of_int_minus)
wenzelm@23164
   123
  also have "... = -1" by simp
wenzelm@23164
   124
  finally show ?thesis .
wenzelm@23164
   125
qed
wenzelm@23164
   126
wenzelm@23164
   127
lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})"
wenzelm@23164
   128
by (simp add: abs_if)
wenzelm@23164
   129
wenzelm@23164
   130
lemma abs_power_minus_one [simp]:
wenzelm@23164
   131
     "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
wenzelm@23164
   132
by (simp add: power_abs)
wenzelm@23164
   133
wenzelm@23164
   134
lemma of_int_number_of_eq:
wenzelm@23164
   135
     "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
wenzelm@23164
   136
by (simp add: number_of_eq) 
wenzelm@23164
   137
wenzelm@23164
   138
text{*Lemmas for specialist use, NOT as default simprules*}
wenzelm@23164
   139
lemma mult_2: "2 * z = (z+z::'a::number_ring)"
wenzelm@23164
   140
proof -
wenzelm@23164
   141
  have "2*z = (1 + 1)*z" by simp
wenzelm@23164
   142
  also have "... = z+z" by (simp add: left_distrib)
wenzelm@23164
   143
  finally show ?thesis .
wenzelm@23164
   144
qed
wenzelm@23164
   145
wenzelm@23164
   146
lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
wenzelm@23164
   147
by (subst mult_commute, rule mult_2)
wenzelm@23164
   148
wenzelm@23164
   149
wenzelm@23164
   150
subsection{*More Inequality Reasoning*}
wenzelm@23164
   151
wenzelm@23164
   152
lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
wenzelm@23164
   153
by arith
wenzelm@23164
   154
wenzelm@23164
   155
lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
wenzelm@23164
   156
by arith
wenzelm@23164
   157
wenzelm@23164
   158
lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
wenzelm@23164
   159
by arith
wenzelm@23164
   160
wenzelm@23164
   161
lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
wenzelm@23164
   162
by arith
wenzelm@23164
   163
wenzelm@23164
   164
lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
wenzelm@23164
   165
by arith
wenzelm@23164
   166
wenzelm@23164
   167
wenzelm@23164
   168
subsection{*The Functions @{term nat} and @{term int}*}
wenzelm@23164
   169
wenzelm@23164
   170
text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
wenzelm@23164
   171
  @{term "w + - z"}*}
wenzelm@23164
   172
declare Zero_int_def [symmetric, simp]
wenzelm@23164
   173
declare One_int_def [symmetric, simp]
wenzelm@23164
   174
wenzelm@23164
   175
lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
wenzelm@23164
   176
wenzelm@23164
   177
lemma nat_0: "nat 0 = 0"
wenzelm@23164
   178
by (simp add: nat_eq_iff)
wenzelm@23164
   179
wenzelm@23164
   180
lemma nat_1: "nat 1 = Suc 0"
wenzelm@23164
   181
by (subst nat_eq_iff, simp)
wenzelm@23164
   182
wenzelm@23164
   183
lemma nat_2: "nat 2 = Suc (Suc 0)"
wenzelm@23164
   184
by (subst nat_eq_iff, simp)
wenzelm@23164
   185
wenzelm@23164
   186
lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
wenzelm@23164
   187
apply (insert zless_nat_conj [of 1 z])
wenzelm@23164
   188
apply (auto simp add: nat_1)
wenzelm@23164
   189
done
wenzelm@23164
   190
wenzelm@23164
   191
text{*This simplifies expressions of the form @{term "int n = z"} where
wenzelm@23164
   192
      z is an integer literal.*}
wenzelm@23164
   193
lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
wenzelm@23164
   194
wenzelm@23164
   195
lemma split_nat [arith_split]:
wenzelm@23164
   196
  "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
wenzelm@23164
   197
  (is "?P = (?L & ?R)")
wenzelm@23164
   198
proof (cases "i < 0")
haftmann@24195
   199
  case True thus ?thesis by auto
wenzelm@23164
   200
next
wenzelm@23164
   201
  case False
wenzelm@23164
   202
  have "?P = ?L"
wenzelm@23164
   203
  proof
wenzelm@23164
   204
    assume ?P thus ?L using False by clarsimp
wenzelm@23164
   205
  next
wenzelm@23164
   206
    assume ?L thus ?P using False by simp
wenzelm@23164
   207
  qed
wenzelm@23164
   208
  with False show ?thesis by simp
wenzelm@23164
   209
qed
wenzelm@23164
   210
haftmann@23851
   211
lemma of_int_of_nat: "of_int k = (if k < 0 then - of_nat (nat (- k))
haftmann@23851
   212
  else of_nat (nat k))"
haftmann@23851
   213
  by (auto simp add: of_nat_nat)
wenzelm@23164
   214
wenzelm@23164
   215
lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
wenzelm@23164
   216
apply (cases "0 \<le> z'")
wenzelm@23164
   217
apply (rule inj_int [THEN injD])
wenzelm@23164
   218
apply (simp add: int_mult zero_le_mult_iff)
wenzelm@23164
   219
apply (simp add: mult_le_0_iff)
wenzelm@23164
   220
done
wenzelm@23164
   221
wenzelm@23164
   222
lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
wenzelm@23164
   223
apply (rule trans)
wenzelm@23164
   224
apply (rule_tac [2] nat_mult_distrib, auto)
wenzelm@23164
   225
done
wenzelm@23164
   226
wenzelm@23164
   227
lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
wenzelm@23164
   228
apply (cases "z=0 | w=0")
wenzelm@23164
   229
apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
wenzelm@23164
   230
                      nat_mult_distrib_neg [symmetric] mult_less_0_iff)
wenzelm@23164
   231
done
wenzelm@23164
   232
wenzelm@23164
   233
wenzelm@23164
   234
subsection "Induction principles for int"
wenzelm@23164
   235
wenzelm@23164
   236
text{*Well-founded segments of the integers*}
wenzelm@23164
   237
wenzelm@23164
   238
definition
wenzelm@23164
   239
  int_ge_less_than  ::  "int => (int * int) set"
wenzelm@23164
   240
where
wenzelm@23164
   241
  "int_ge_less_than d = {(z',z). d \<le> z' & z' < z}"
wenzelm@23164
   242
wenzelm@23164
   243
theorem wf_int_ge_less_than: "wf (int_ge_less_than d)"
wenzelm@23164
   244
proof -
wenzelm@23164
   245
  have "int_ge_less_than d \<subseteq> measure (%z. nat (z-d))"
wenzelm@23164
   246
    by (auto simp add: int_ge_less_than_def)
wenzelm@23164
   247
  thus ?thesis 
wenzelm@23164
   248
    by (rule wf_subset [OF wf_measure]) 
wenzelm@23164
   249
qed
wenzelm@23164
   250
wenzelm@23164
   251
text{*This variant looks odd, but is typical of the relations suggested
wenzelm@23164
   252
by RankFinder.*}
wenzelm@23164
   253
wenzelm@23164
   254
definition
wenzelm@23164
   255
  int_ge_less_than2 ::  "int => (int * int) set"
wenzelm@23164
   256
where
wenzelm@23164
   257
  "int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}"
wenzelm@23164
   258
wenzelm@23164
   259
theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
wenzelm@23164
   260
proof -
wenzelm@23164
   261
  have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+z-d))" 
wenzelm@23164
   262
    by (auto simp add: int_ge_less_than2_def)
wenzelm@23164
   263
  thus ?thesis 
wenzelm@23164
   264
    by (rule wf_subset [OF wf_measure]) 
wenzelm@23164
   265
qed
wenzelm@23164
   266
haftmann@24195
   267
(* `set:int': dummy construction *)
haftmann@24195
   268
theorem int_ge_induct [case_names base step, induct set:int]:
haftmann@24195
   269
  fixes i :: int
haftmann@24195
   270
  assumes ge: "k \<le> i" and
haftmann@24195
   271
    base: "P k" and
haftmann@24195
   272
    step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
wenzelm@23164
   273
  shows "P i"
wenzelm@23164
   274
proof -
wenzelm@23164
   275
  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
wenzelm@23164
   276
    proof (induct n)
wenzelm@23164
   277
      case 0
wenzelm@23164
   278
      hence "i = k" by arith
wenzelm@23164
   279
      thus "P i" using base by simp
wenzelm@23164
   280
    next
wenzelm@23164
   281
      case (Suc n)
haftmann@24195
   282
      then have "n = nat((i - 1) - k)" by arith
wenzelm@23164
   283
      moreover
wenzelm@23164
   284
      have ki1: "k \<le> i - 1" using Suc.prems by arith
wenzelm@23164
   285
      ultimately
wenzelm@23164
   286
      have "P(i - 1)" by(rule Suc.hyps)
wenzelm@23164
   287
      from step[OF ki1 this] show ?case by simp
wenzelm@23164
   288
    qed
wenzelm@23164
   289
  }
wenzelm@23164
   290
  with ge show ?thesis by fast
wenzelm@23164
   291
qed
wenzelm@23164
   292
wenzelm@23164
   293
                     (* `set:int': dummy construction *)
wenzelm@23164
   294
theorem int_gr_induct[case_names base step,induct set:int]:
wenzelm@23164
   295
  assumes gr: "k < (i::int)" and
wenzelm@23164
   296
        base: "P(k+1)" and
wenzelm@23164
   297
        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
wenzelm@23164
   298
  shows "P i"
wenzelm@23164
   299
apply(rule int_ge_induct[of "k + 1"])
wenzelm@23164
   300
  using gr apply arith
wenzelm@23164
   301
 apply(rule base)
wenzelm@23164
   302
apply (rule step, simp+)
wenzelm@23164
   303
done
wenzelm@23164
   304
wenzelm@23164
   305
theorem int_le_induct[consumes 1,case_names base step]:
wenzelm@23164
   306
  assumes le: "i \<le> (k::int)" and
wenzelm@23164
   307
        base: "P(k)" and
wenzelm@23164
   308
        step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
wenzelm@23164
   309
  shows "P i"
wenzelm@23164
   310
proof -
wenzelm@23164
   311
  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
wenzelm@23164
   312
    proof (induct n)
wenzelm@23164
   313
      case 0
wenzelm@23164
   314
      hence "i = k" by arith
wenzelm@23164
   315
      thus "P i" using base by simp
wenzelm@23164
   316
    next
wenzelm@23164
   317
      case (Suc n)
wenzelm@23164
   318
      hence "n = nat(k - (i+1))" by arith
wenzelm@23164
   319
      moreover
wenzelm@23164
   320
      have ki1: "i + 1 \<le> k" using Suc.prems by arith
wenzelm@23164
   321
      ultimately
wenzelm@23164
   322
      have "P(i+1)" by(rule Suc.hyps)
wenzelm@23164
   323
      from step[OF ki1 this] show ?case by simp
wenzelm@23164
   324
    qed
wenzelm@23164
   325
  }
wenzelm@23164
   326
  with le show ?thesis by fast
wenzelm@23164
   327
qed
wenzelm@23164
   328
wenzelm@23164
   329
theorem int_less_induct [consumes 1,case_names base step]:
wenzelm@23164
   330
  assumes less: "(i::int) < k" and
wenzelm@23164
   331
        base: "P(k - 1)" and
wenzelm@23164
   332
        step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
wenzelm@23164
   333
  shows "P i"
wenzelm@23164
   334
apply(rule int_le_induct[of _ "k - 1"])
wenzelm@23164
   335
  using less apply arith
wenzelm@23164
   336
 apply(rule base)
wenzelm@23164
   337
apply (rule step, simp+)
wenzelm@23164
   338
done
wenzelm@23164
   339
wenzelm@23164
   340
subsection{*Intermediate value theorems*}
wenzelm@23164
   341
wenzelm@23164
   342
lemma int_val_lemma:
wenzelm@23164
   343
     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
wenzelm@23164
   344
      f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
wenzelm@23164
   345
apply (induct_tac "n", simp)
wenzelm@23164
   346
apply (intro strip)
wenzelm@23164
   347
apply (erule impE, simp)
wenzelm@23164
   348
apply (erule_tac x = n in allE, simp)
wenzelm@23164
   349
apply (case_tac "k = f (n+1) ")
wenzelm@23164
   350
 apply force
wenzelm@23164
   351
apply (erule impE)
wenzelm@23164
   352
 apply (simp add: abs_if split add: split_if_asm)
wenzelm@23164
   353
apply (blast intro: le_SucI)
wenzelm@23164
   354
done
wenzelm@23164
   355
wenzelm@23164
   356
lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
wenzelm@23164
   357
wenzelm@23164
   358
lemma nat_intermed_int_val:
wenzelm@23164
   359
     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
wenzelm@23164
   360
         f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
wenzelm@23164
   361
apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
wenzelm@23164
   362
       in int_val_lemma)
wenzelm@23164
   363
apply simp
wenzelm@23164
   364
apply (erule exE)
wenzelm@23164
   365
apply (rule_tac x = "i+m" in exI, arith)
wenzelm@23164
   366
done
wenzelm@23164
   367
wenzelm@23164
   368
wenzelm@23164
   369
subsection{*Products and 1, by T. M. Rasmussen*}
wenzelm@23164
   370
wenzelm@23164
   371
lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
wenzelm@23164
   372
by arith
wenzelm@23164
   373
wenzelm@23164
   374
lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
wenzelm@23164
   375
apply (cases "\<bar>n\<bar>=1") 
wenzelm@23164
   376
apply (simp add: abs_mult) 
wenzelm@23164
   377
apply (rule ccontr) 
wenzelm@23164
   378
apply (auto simp add: linorder_neq_iff abs_mult) 
wenzelm@23164
   379
apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
wenzelm@23164
   380
 prefer 2 apply arith 
wenzelm@23164
   381
apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp) 
wenzelm@23164
   382
apply (rule mult_mono, auto) 
wenzelm@23164
   383
done
wenzelm@23164
   384
wenzelm@23164
   385
lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
wenzelm@23164
   386
by (insert abs_zmult_eq_1 [of m n], arith)
wenzelm@23164
   387
wenzelm@23164
   388
lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
wenzelm@23164
   389
apply (auto dest: pos_zmult_eq_1_iff_lemma) 
wenzelm@23164
   390
apply (simp add: mult_commute [of m]) 
wenzelm@23164
   391
apply (frule pos_zmult_eq_1_iff_lemma, auto) 
wenzelm@23164
   392
done
wenzelm@23164
   393
wenzelm@23164
   394
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
wenzelm@23164
   395
apply (rule iffI) 
wenzelm@23164
   396
 apply (frule pos_zmult_eq_1_iff_lemma)
wenzelm@23164
   397
 apply (simp add: mult_commute [of m]) 
wenzelm@23164
   398
 apply (frule pos_zmult_eq_1_iff_lemma, auto) 
wenzelm@23164
   399
done
wenzelm@23164
   400
wenzelm@23164
   401
wenzelm@23164
   402
subsection {* Legacy ML bindings *}
wenzelm@23164
   403
wenzelm@23164
   404
ML {*
wenzelm@23164
   405
val of_int_number_of_eq = @{thm of_int_number_of_eq};
wenzelm@23164
   406
val nat_0 = @{thm nat_0};
wenzelm@23164
   407
val nat_1 = @{thm nat_1};
wenzelm@23164
   408
*}
wenzelm@23164
   409
wenzelm@23164
   410
end