src/HOL/Integ/IntArith.thy
author paulson
Fri Mar 19 10:44:20 2004 +0100 (2004-03-19)
changeset 14473 846c237bd9b3
parent 14436 77017c49c004
child 14479 0eca4aabf371
permissions -rw-r--r--
stylistic tweaks
paulson@14259
     1
(*  Title:      HOL/Integ/IntArith.thy
paulson@14259
     2
    ID:         $Id$
paulson@14259
     3
    Authors:    Larry Paulson and Tobias Nipkow
paulson@14259
     4
*)
wenzelm@12023
     5
wenzelm@12023
     6
header {* Integer arithmetic *}
wenzelm@12023
     7
wenzelm@9436
     8
theory IntArith = Bin
paulson@14259
     9
files ("int_arith1.ML"):
wenzelm@9436
    10
paulson@14387
    11
text{*Duplicate: can't understand why it's necessary*}
paulson@14387
    12
declare numeral_0_eq_0 [simp]
paulson@14387
    13
paulson@14387
    14
subsection{*Instantiating Binary Arithmetic for the Integers*}
paulson@14387
    15
paulson@14387
    16
instance
paulson@14387
    17
  int :: number ..
paulson@14387
    18
paulson@14387
    19
primrec (*the type constraint is essential!*)
paulson@14387
    20
  number_of_Pls: "number_of bin.Pls = 0"
paulson@14387
    21
  number_of_Min: "number_of bin.Min = - (1::int)"
paulson@14387
    22
  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
paulson@14387
    23
	                               (number_of w) + (number_of w)"
paulson@14387
    24
paulson@14387
    25
declare number_of_Pls [simp del]
paulson@14387
    26
        number_of_Min [simp del]
paulson@14387
    27
        number_of_BIT [simp del]
paulson@14387
    28
paulson@14387
    29
instance int :: number_ring
paulson@14387
    30
proof
paulson@14387
    31
  show "Numeral0 = (0::int)" by (rule number_of_Pls)
paulson@14387
    32
  show "-1 = - (1::int)" by (rule number_of_Min)
paulson@14387
    33
  fix w :: bin and x :: bool
paulson@14387
    34
  show "(number_of (w BIT x) :: int) =
paulson@14387
    35
        (if x then 1 else 0) + number_of w + number_of w"
paulson@14387
    36
    by (rule number_of_BIT)
paulson@14387
    37
qed
paulson@14387
    38
paulson@14387
    39
paulson@14353
    40
paulson@14272
    41
subsection{*Inequality Reasoning for the Arithmetic Simproc*}
paulson@14272
    42
paulson@14387
    43
lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
paulson@14387
    44
by (cut_tac w = 0 in zless_nat_conj, auto)
paulson@14387
    45
paulson@14272
    46
lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
paulson@14378
    47
apply (rule eq_Abs_Integ [of z])
paulson@14378
    48
apply (rule eq_Abs_Integ [of w])
paulson@14378
    49
apply (simp add: linorder_not_le [symmetric] zle int_def zadd One_int_def)
paulson@14378
    50
done
paulson@14378
    51
paulson@14272
    52
paulson@14387
    53
paulson@14387
    54
lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
paulson@14387
    55
by simp 
paulson@14387
    56
paulson@14387
    57
lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
paulson@14387
    58
by simp
paulson@14387
    59
paulson@14387
    60
lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
paulson@14387
    61
by simp 
paulson@14387
    62
paulson@14387
    63
lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
paulson@14387
    64
by simp
paulson@14387
    65
paulson@14387
    66
text{*Theorem lists for the cancellation simprocs. The use of binary numerals
paulson@14387
    67
for 0 and 1 reduces the number of special cases.*}
paulson@14387
    68
paulson@14387
    69
lemmas add_0s = add_numeral_0 add_numeral_0_right
paulson@14387
    70
lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
paulson@14387
    71
                 mult_minus1 mult_minus1_right
paulson@14387
    72
paulson@14387
    73
paulson@14387
    74
subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
paulson@14387
    75
paulson@14387
    76
text{*Arithmetic computations are defined for binary literals, which leaves 0
paulson@14387
    77
and 1 as special cases. Addition already has rules for 0, but not 1.
paulson@14387
    78
Multiplication and unary minus already have rules for both 0 and 1.*}
paulson@14387
    79
paulson@14387
    80
paulson@14387
    81
lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
paulson@14387
    82
by simp
paulson@14387
    83
paulson@14387
    84
paulson@14387
    85
lemmas add_number_of_eq = number_of_add [symmetric]
paulson@14387
    86
paulson@14387
    87
text{*Allow 1 on either or both sides*}
paulson@14387
    88
lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
paulson@14387
    89
by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
paulson@14387
    90
paulson@14387
    91
lemmas add_special =
paulson@14387
    92
    one_add_one_is_two
paulson@14387
    93
    binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
paulson@14387
    94
    binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
paulson@14387
    95
paulson@14387
    96
text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
paulson@14387
    97
lemmas diff_special =
paulson@14387
    98
    binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
paulson@14387
    99
    binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
paulson@14387
   100
paulson@14387
   101
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
paulson@14387
   102
lemmas eq_special =
paulson@14387
   103
    binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
paulson@14387
   104
    binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
paulson@14387
   105
    binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
paulson@14387
   106
    binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
paulson@14387
   107
paulson@14387
   108
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
paulson@14387
   109
lemmas less_special =
paulson@14387
   110
  binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard]
paulson@14387
   111
  binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard]
paulson@14387
   112
  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard]
paulson@14387
   113
  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard]
paulson@14387
   114
paulson@14387
   115
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
paulson@14387
   116
lemmas le_special =
paulson@14387
   117
    binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard]
paulson@14387
   118
    binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard]
paulson@14387
   119
    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
paulson@14387
   120
    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
paulson@14387
   121
paulson@14387
   122
lemmas arith_special = 
paulson@14387
   123
       add_special diff_special eq_special less_special le_special
paulson@14387
   124
paulson@14387
   125
wenzelm@12023
   126
use "int_arith1.ML"
wenzelm@12023
   127
setup int_arith_setup
paulson@14259
   128
paulson@14353
   129
paulson@14387
   130
subsection{*Lemmas About Small Numerals*}
paulson@14387
   131
paulson@14387
   132
lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
paulson@14387
   133
proof -
paulson@14387
   134
  have "(of_int -1 :: 'a) = of_int (- 1)" by simp
paulson@14387
   135
  also have "... = - of_int 1" by (simp only: of_int_minus)
paulson@14387
   136
  also have "... = -1" by simp
paulson@14387
   137
  finally show ?thesis .
paulson@14387
   138
qed
paulson@14387
   139
paulson@14387
   140
lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_ring,number_ring})"
paulson@14387
   141
by (simp add: abs_if)
paulson@14387
   142
paulson@14436
   143
lemma abs_power_minus_one [simp]:
paulson@14436
   144
     "abs(-1 ^ n) = (1::'a::{ordered_ring,number_ring,ringpower})"
paulson@14436
   145
by (simp add: power_abs)
paulson@14436
   146
paulson@14387
   147
lemma of_int_number_of_eq:
paulson@14387
   148
     "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
paulson@14387
   149
apply (induct v)
paulson@14387
   150
apply (simp_all only: number_of of_int_add, simp_all) 
paulson@14387
   151
done
paulson@14387
   152
paulson@14387
   153
text{*Lemmas for specialist use, NOT as default simprules*}
paulson@14387
   154
lemma mult_2: "2 * z = (z+z::'a::number_ring)"
paulson@14387
   155
proof -
paulson@14387
   156
  have "2*z = (1 + 1)*z" by simp
paulson@14387
   157
  also have "... = z+z" by (simp add: left_distrib)
paulson@14387
   158
  finally show ?thesis .
paulson@14387
   159
qed
paulson@14387
   160
paulson@14387
   161
lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
paulson@14387
   162
by (subst mult_commute, rule mult_2)
paulson@14387
   163
paulson@14387
   164
paulson@14387
   165
subsection{*More Inequality Reasoning*}
paulson@14272
   166
paulson@14272
   167
lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
paulson@14259
   168
by arith
paulson@14259
   169
paulson@14272
   170
lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
paulson@14272
   171
by arith
paulson@14272
   172
paulson@14272
   173
lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<(z::int))"
paulson@14272
   174
by arith
paulson@14272
   175
paulson@14272
   176
lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w\<le>(z::int))"
paulson@14259
   177
by arith
paulson@14259
   178
paulson@14365
   179
lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
paulson@14365
   180
by arith
paulson@14365
   181
paulson@14353
   182
paulson@14353
   183
subsection{*The Functions @{term nat} and @{term int}*}
paulson@14259
   184
paulson@14272
   185
lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
paulson@14259
   186
by (blast dest: nat_0_le sym)
paulson@14259
   187
paulson@14272
   188
lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
paulson@14259
   189
by auto
paulson@14259
   190
paulson@14272
   191
lemma nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
paulson@14259
   192
by auto
paulson@14259
   193
paulson@14272
   194
lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
paulson@14259
   195
apply (rule iffI)
paulson@14259
   196
apply (erule nat_0_le [THEN subst])
paulson@14259
   197
apply (simp_all del: zless_int add: zless_int [symmetric]) 
paulson@14259
   198
done
paulson@14259
   199
paulson@14272
   200
lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
paulson@14259
   201
by (auto simp add: nat_eq_iff2)
paulson@14259
   202
paulson@14259
   203
paulson@14353
   204
text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
paulson@14353
   205
  @{term "w + - z"}*}
paulson@14259
   206
declare Zero_int_def [symmetric, simp]
paulson@14259
   207
declare One_int_def [symmetric, simp]
paulson@14259
   208
paulson@14259
   209
text{*cooper.ML refers to this theorem*}
paulson@14259
   210
lemmas zdiff_def_symmetric = zdiff_def [symmetric, simp]
paulson@14259
   211
paulson@14259
   212
lemma nat_0: "nat 0 = 0"
paulson@14259
   213
by (simp add: nat_eq_iff)
paulson@14259
   214
paulson@14259
   215
lemma nat_1: "nat 1 = Suc 0"
paulson@14259
   216
by (subst nat_eq_iff, simp)
paulson@14259
   217
paulson@14259
   218
lemma nat_2: "nat 2 = Suc (Suc 0)"
paulson@14259
   219
by (subst nat_eq_iff, simp)
paulson@14259
   220
paulson@14272
   221
lemma nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
paulson@14378
   222
apply (case_tac "z < 0")
paulson@14259
   223
apply (auto simp add: nat_less_iff)
paulson@14259
   224
done
paulson@14259
   225
paulson@14272
   226
lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
paulson@14259
   227
by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)
paulson@14259
   228
paulson@14259
   229
paulson@14259
   230
text{*This simplifies expressions of the form @{term "int n = z"} where
paulson@14259
   231
      z is an integer literal.*}
paulson@14259
   232
declare int_eq_iff [of _ "number_of v", standard, simp]
paulson@13837
   233
paulson@13849
   234
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
paulson@13849
   235
  by simp
paulson@13849
   236
paulson@14295
   237
lemma split_nat [arith_split]:
paulson@14259
   238
  "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
nipkow@13575
   239
  (is "?P = (?L & ?R)")
nipkow@13575
   240
proof (cases "i < 0")
nipkow@13575
   241
  case True thus ?thesis by simp
nipkow@13575
   242
next
nipkow@13575
   243
  case False
nipkow@13575
   244
  have "?P = ?L"
nipkow@13575
   245
  proof
nipkow@13575
   246
    assume ?P thus ?L using False by clarsimp
nipkow@13575
   247
  next
nipkow@13575
   248
    assume ?L thus ?P using False by simp
nipkow@13575
   249
  qed
nipkow@13575
   250
  with False show ?thesis by simp
nipkow@13575
   251
qed
nipkow@13575
   252
paulson@14387
   253
nipkow@13685
   254
subsubsection "Induction principles for int"
nipkow@13685
   255
nipkow@13685
   256
                     (* `set:int': dummy construction *)
nipkow@13685
   257
theorem int_ge_induct[case_names base step,induct set:int]:
nipkow@13685
   258
  assumes ge: "k \<le> (i::int)" and
nipkow@13685
   259
        base: "P(k)" and
nipkow@13685
   260
        step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
nipkow@13685
   261
  shows "P i"
nipkow@13685
   262
proof -
paulson@14272
   263
  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
nipkow@13685
   264
    proof (induct n)
nipkow@13685
   265
      case 0
nipkow@13685
   266
      hence "i = k" by arith
nipkow@13685
   267
      thus "P i" using base by simp
nipkow@13685
   268
    next
nipkow@13685
   269
      case (Suc n)
nipkow@13685
   270
      hence "n = nat((i - 1) - k)" by arith
nipkow@13685
   271
      moreover
nipkow@13685
   272
      have ki1: "k \<le> i - 1" using Suc.prems by arith
nipkow@13685
   273
      ultimately
nipkow@13685
   274
      have "P(i - 1)" by(rule Suc.hyps)
nipkow@13685
   275
      from step[OF ki1 this] show ?case by simp
nipkow@13685
   276
    qed
nipkow@13685
   277
  }
paulson@14473
   278
  with ge show ?thesis by fast
nipkow@13685
   279
qed
nipkow@13685
   280
nipkow@13685
   281
                     (* `set:int': dummy construction *)
nipkow@13685
   282
theorem int_gr_induct[case_names base step,induct set:int]:
nipkow@13685
   283
  assumes gr: "k < (i::int)" and
nipkow@13685
   284
        base: "P(k+1)" and
nipkow@13685
   285
        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
nipkow@13685
   286
  shows "P i"
nipkow@13685
   287
apply(rule int_ge_induct[of "k + 1"])
nipkow@13685
   288
  using gr apply arith
nipkow@13685
   289
 apply(rule base)
paulson@14259
   290
apply (rule step, simp+)
nipkow@13685
   291
done
nipkow@13685
   292
nipkow@13685
   293
theorem int_le_induct[consumes 1,case_names base step]:
nipkow@13685
   294
  assumes le: "i \<le> (k::int)" and
nipkow@13685
   295
        base: "P(k)" and
nipkow@13685
   296
        step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
nipkow@13685
   297
  shows "P i"
nipkow@13685
   298
proof -
paulson@14272
   299
  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
nipkow@13685
   300
    proof (induct n)
nipkow@13685
   301
      case 0
nipkow@13685
   302
      hence "i = k" by arith
nipkow@13685
   303
      thus "P i" using base by simp
nipkow@13685
   304
    next
nipkow@13685
   305
      case (Suc n)
nipkow@13685
   306
      hence "n = nat(k - (i+1))" by arith
nipkow@13685
   307
      moreover
nipkow@13685
   308
      have ki1: "i + 1 \<le> k" using Suc.prems by arith
nipkow@13685
   309
      ultimately
nipkow@13685
   310
      have "P(i+1)" by(rule Suc.hyps)
nipkow@13685
   311
      from step[OF ki1 this] show ?case by simp
nipkow@13685
   312
    qed
nipkow@13685
   313
  }
paulson@14473
   314
  with le show ?thesis by fast
nipkow@13685
   315
qed
nipkow@13685
   316
paulson@14387
   317
theorem int_less_induct [consumes 1,case_names base step]:
nipkow@13685
   318
  assumes less: "(i::int) < k" and
nipkow@13685
   319
        base: "P(k - 1)" and
nipkow@13685
   320
        step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
nipkow@13685
   321
  shows "P i"
nipkow@13685
   322
apply(rule int_le_induct[of _ "k - 1"])
nipkow@13685
   323
  using less apply arith
nipkow@13685
   324
 apply(rule base)
paulson@14259
   325
apply (rule step, simp+)
paulson@14259
   326
done
paulson@14259
   327
paulson@14259
   328
subsection{*Intermediate value theorems*}
paulson@14259
   329
paulson@14259
   330
lemma int_val_lemma:
paulson@14259
   331
     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
paulson@14259
   332
      f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
paulson@14271
   333
apply (induct_tac "n", simp)
paulson@14259
   334
apply (intro strip)
paulson@14259
   335
apply (erule impE, simp)
paulson@14259
   336
apply (erule_tac x = n in allE, simp)
paulson@14259
   337
apply (case_tac "k = f (n+1) ")
paulson@14259
   338
 apply force
paulson@14259
   339
apply (erule impE)
paulson@14259
   340
 apply (simp add: zabs_def split add: split_if_asm)
paulson@14259
   341
apply (blast intro: le_SucI)
paulson@14259
   342
done
paulson@14259
   343
paulson@14259
   344
lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
paulson@14259
   345
paulson@14259
   346
lemma nat_intermed_int_val:
paulson@14259
   347
     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
paulson@14259
   348
         f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
paulson@14259
   349
apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
paulson@14259
   350
       in int_val_lemma)
paulson@14259
   351
apply simp
paulson@14259
   352
apply (erule impE)
paulson@14259
   353
 apply (intro strip)
paulson@14259
   354
 apply (erule_tac x = "i+m" in allE, arith)
paulson@14259
   355
apply (erule exE)
paulson@14259
   356
apply (rule_tac x = "i+m" in exI, arith)
paulson@14259
   357
done
paulson@14259
   358
paulson@14259
   359
paulson@14259
   360
subsection{*Products and 1, by T. M. Rasmussen*}
paulson@14259
   361
paulson@14259
   362
lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
paulson@14259
   363
apply auto
paulson@14259
   364
apply (subgoal_tac "m*1 = m*n")
paulson@14378
   365
apply (drule mult_cancel_left [THEN iffD1], auto)
nipkow@13685
   366
done
nipkow@13685
   367
paulson@14387
   368
text{*FIXME: tidy*}
paulson@14259
   369
lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
paulson@14259
   370
apply auto
paulson@14259
   371
apply (case_tac "m=1")
paulson@14259
   372
apply (case_tac [2] "n=1")
paulson@14259
   373
apply (case_tac [4] "m=1")
paulson@14259
   374
apply (case_tac [5] "n=1", auto)
paulson@14259
   375
apply (tactic"distinct_subgoals_tac")
paulson@14259
   376
apply (subgoal_tac "1<m*n", simp)
paulson@14387
   377
apply (rule less_1_mult, arith)
paulson@14259
   378
apply (subgoal_tac "0<n", arith)
paulson@14259
   379
apply (subgoal_tac "0<m*n")
paulson@14353
   380
apply (drule zero_less_mult_iff [THEN iffD1], auto)
paulson@14259
   381
done
paulson@14259
   382
paulson@14259
   383
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
paulson@14259
   384
apply (case_tac "0<m")
paulson@14271
   385
apply (simp add: pos_zmult_eq_1_iff)
paulson@14259
   386
apply (case_tac "m=0")
paulson@14271
   387
apply (simp del: number_of_reorient)
paulson@14259
   388
apply (subgoal_tac "0 < -m")
paulson@14259
   389
apply (drule_tac n = "-n" in pos_zmult_eq_1_iff, auto)
paulson@14259
   390
done
paulson@14259
   391
paulson@14259
   392
paulson@14259
   393
subsection{*More about nat*}
paulson@14259
   394
paulson@14271
   395
(*Analogous to zadd_int*)
paulson@14271
   396
lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)"
paulson@14271
   397
by (induct m n rule: diff_induct, simp_all)
paulson@14271
   398
paulson@14259
   399
lemma nat_add_distrib:
paulson@14259
   400
     "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
paulson@14259
   401
apply (rule inj_int [THEN injD])
paulson@14271
   402
apply (simp add: zadd_int [symmetric])
paulson@14259
   403
done
paulson@14259
   404
paulson@14259
   405
lemma nat_diff_distrib:
paulson@14259
   406
     "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
paulson@14259
   407
apply (rule inj_int [THEN injD])
paulson@14271
   408
apply (simp add: zdiff_int [symmetric] nat_le_eq_zle)
paulson@14259
   409
done
paulson@14259
   410
paulson@14259
   411
lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
paulson@14259
   412
apply (case_tac "0 \<le> z'")
paulson@14259
   413
apply (rule inj_int [THEN injD])
paulson@14353
   414
apply (simp add: zmult_int [symmetric] zero_le_mult_iff)
paulson@14353
   415
apply (simp add: mult_le_0_iff)
paulson@14259
   416
done
paulson@14259
   417
paulson@14259
   418
lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
paulson@14259
   419
apply (rule trans)
paulson@14259
   420
apply (rule_tac [2] nat_mult_distrib, auto)
paulson@14259
   421
done
paulson@14259
   422
paulson@14259
   423
lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
paulson@14259
   424
apply (case_tac "z=0 | w=0")
paulson@14259
   425
apply (auto simp add: zabs_def nat_mult_distrib [symmetric] 
paulson@14353
   426
                      nat_mult_distrib_neg [symmetric] mult_less_0_iff)
paulson@14259
   427
done
paulson@14259
   428
paulson@14353
   429
paulson@14259
   430
ML
paulson@14259
   431
{*
paulson@14259
   432
val zle_diff1_eq = thm "zle_diff1_eq";
paulson@14259
   433
val zle_add1_eq_le = thm "zle_add1_eq_le";
paulson@14259
   434
val nonneg_eq_int = thm "nonneg_eq_int";
paulson@14387
   435
val abs_minus_one = thm "abs_minus_one";
paulson@14390
   436
val of_int_number_of_eq = thm"of_int_number_of_eq";
paulson@14259
   437
val nat_eq_iff = thm "nat_eq_iff";
paulson@14259
   438
val nat_eq_iff2 = thm "nat_eq_iff2";
paulson@14259
   439
val nat_less_iff = thm "nat_less_iff";
paulson@14259
   440
val int_eq_iff = thm "int_eq_iff";
paulson@14259
   441
val nat_0 = thm "nat_0";
paulson@14259
   442
val nat_1 = thm "nat_1";
paulson@14259
   443
val nat_2 = thm "nat_2";
paulson@14259
   444
val nat_less_eq_zless = thm "nat_less_eq_zless";
paulson@14259
   445
val nat_le_eq_zle = thm "nat_le_eq_zle";
paulson@14259
   446
paulson@14259
   447
val nat_intermed_int_val = thm "nat_intermed_int_val";
paulson@14259
   448
val zmult_eq_self_iff = thm "zmult_eq_self_iff";
paulson@14259
   449
val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
paulson@14259
   450
val zmult_eq_1_iff = thm "zmult_eq_1_iff";
paulson@14259
   451
val nat_add_distrib = thm "nat_add_distrib";
paulson@14259
   452
val nat_diff_distrib = thm "nat_diff_distrib";
paulson@14259
   453
val nat_mult_distrib = thm "nat_mult_distrib";
paulson@14259
   454
val nat_mult_distrib_neg = thm "nat_mult_distrib_neg";
paulson@14259
   455
val nat_abs_mult_distrib = thm "nat_abs_mult_distrib";
paulson@14259
   456
*}
paulson@14259
   457
wenzelm@7707
   458
end