src/HOL/Integ/IntArith.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17472 bcbf48d59059
child 19601 299d4cd2ef51
permissions -rw-r--r--
adaptions to codegen_package
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
nipkow@15131
     8
theory IntArith
nipkow@15140
     9
imports Numeral
haftmann@16417
    10
uses ("int_arith1.ML")
nipkow@15131
    11
begin
wenzelm@9436
    12
paulson@14387
    13
text{*Duplicate: can't understand why it's necessary*}
paulson@14387
    14
declare numeral_0_eq_0 [simp]
paulson@14387
    15
paulson@16413
    16
paulson@14387
    17
subsection{*Instantiating Binary Arithmetic for the Integers*}
paulson@14387
    18
paulson@14387
    19
instance
paulson@14387
    20
  int :: number ..
paulson@14387
    21
paulson@15013
    22
defs (overloaded)
paulson@15013
    23
  int_number_of_def: "(number_of w :: int) == of_int (Rep_Bin w)"
paulson@15013
    24
    --{*the type constraint is essential!*}
paulson@14387
    25
paulson@14387
    26
instance int :: number_ring
paulson@15013
    27
by (intro_classes, simp add: int_number_of_def) 
paulson@14387
    28
paulson@14353
    29
paulson@14272
    30
subsection{*Inequality Reasoning for the Arithmetic Simproc*}
paulson@14272
    31
paulson@14387
    32
lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
paulson@14387
    33
by simp 
paulson@14387
    34
paulson@14387
    35
lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
paulson@14387
    36
by simp
paulson@14387
    37
paulson@14387
    38
lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
paulson@14387
    39
by simp 
paulson@14387
    40
paulson@14387
    41
lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
paulson@14387
    42
by simp
paulson@14387
    43
paulson@14387
    44
text{*Theorem lists for the cancellation simprocs. The use of binary numerals
paulson@14387
    45
for 0 and 1 reduces the number of special cases.*}
paulson@14387
    46
paulson@14387
    47
lemmas add_0s = add_numeral_0 add_numeral_0_right
paulson@14387
    48
lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
paulson@14387
    49
                 mult_minus1 mult_minus1_right
paulson@14387
    50
paulson@14387
    51
paulson@14387
    52
subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
paulson@14387
    53
paulson@14387
    54
text{*Arithmetic computations are defined for binary literals, which leaves 0
paulson@14387
    55
and 1 as special cases. Addition already has rules for 0, but not 1.
paulson@14387
    56
Multiplication and unary minus already have rules for both 0 and 1.*}
paulson@14387
    57
paulson@14387
    58
paulson@14387
    59
lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
paulson@14387
    60
by simp
paulson@14387
    61
paulson@14387
    62
paulson@14387
    63
lemmas add_number_of_eq = number_of_add [symmetric]
paulson@14387
    64
paulson@14387
    65
text{*Allow 1 on either or both sides*}
paulson@14387
    66
lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
paulson@14387
    67
by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
paulson@14387
    68
paulson@14387
    69
lemmas add_special =
paulson@14387
    70
    one_add_one_is_two
paulson@14387
    71
    binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
paulson@14387
    72
    binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
paulson@14387
    73
paulson@14387
    74
text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
paulson@14387
    75
lemmas diff_special =
paulson@14387
    76
    binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
paulson@14387
    77
    binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
paulson@14387
    78
paulson@14387
    79
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
paulson@14387
    80
lemmas eq_special =
paulson@14387
    81
    binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
paulson@14387
    82
    binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
paulson@14387
    83
    binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
paulson@14387
    84
    binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
paulson@14387
    85
paulson@14387
    86
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
paulson@14387
    87
lemmas less_special =
paulson@14387
    88
  binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard]
paulson@14387
    89
  binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard]
paulson@14387
    90
  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard]
paulson@14387
    91
  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard]
paulson@14387
    92
paulson@14387
    93
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
paulson@14387
    94
lemmas le_special =
paulson@14387
    95
    binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard]
paulson@14387
    96
    binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard]
paulson@14387
    97
    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
paulson@14387
    98
    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
paulson@14387
    99
paulson@14387
   100
lemmas arith_special = 
paulson@14387
   101
       add_special diff_special eq_special less_special le_special
paulson@14387
   102
paulson@14387
   103
wenzelm@12023
   104
use "int_arith1.ML"
wenzelm@12023
   105
setup int_arith_setup
paulson@14259
   106
paulson@14353
   107
paulson@14387
   108
subsection{*Lemmas About Small Numerals*}
paulson@14387
   109
paulson@14387
   110
lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
paulson@14387
   111
proof -
paulson@14387
   112
  have "(of_int -1 :: 'a) = of_int (- 1)" by simp
paulson@14387
   113
  also have "... = - of_int 1" by (simp only: of_int_minus)
paulson@14387
   114
  also have "... = -1" by simp
paulson@14387
   115
  finally show ?thesis .
paulson@14387
   116
qed
paulson@14387
   117
obua@14738
   118
lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})"
paulson@14387
   119
by (simp add: abs_if)
paulson@14387
   120
paulson@14436
   121
lemma abs_power_minus_one [simp]:
paulson@15003
   122
     "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
paulson@14436
   123
by (simp add: power_abs)
paulson@14436
   124
paulson@14387
   125
lemma of_int_number_of_eq:
paulson@14387
   126
     "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
paulson@15013
   127
by (simp add: number_of_eq) 
paulson@14387
   128
paulson@14387
   129
text{*Lemmas for specialist use, NOT as default simprules*}
paulson@14387
   130
lemma mult_2: "2 * z = (z+z::'a::number_ring)"
paulson@14387
   131
proof -
paulson@14387
   132
  have "2*z = (1 + 1)*z" by simp
paulson@14387
   133
  also have "... = z+z" by (simp add: left_distrib)
paulson@14387
   134
  finally show ?thesis .
paulson@14387
   135
qed
paulson@14387
   136
paulson@14387
   137
lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
paulson@14387
   138
by (subst mult_commute, rule mult_2)
paulson@14387
   139
paulson@14387
   140
paulson@14387
   141
subsection{*More Inequality Reasoning*}
paulson@14272
   142
paulson@14272
   143
lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
paulson@14259
   144
by arith
paulson@14259
   145
paulson@14272
   146
lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
paulson@14272
   147
by arith
paulson@14272
   148
paulson@14479
   149
lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
paulson@14272
   150
by arith
paulson@14272
   151
paulson@14479
   152
lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
paulson@14259
   153
by arith
paulson@14259
   154
paulson@14365
   155
lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
paulson@14365
   156
by arith
paulson@14365
   157
paulson@14353
   158
paulson@14353
   159
subsection{*The Functions @{term nat} and @{term int}*}
paulson@14259
   160
paulson@14353
   161
text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
paulson@14353
   162
  @{term "w + - z"}*}
paulson@14259
   163
declare Zero_int_def [symmetric, simp]
paulson@14259
   164
declare One_int_def [symmetric, simp]
paulson@14259
   165
paulson@14259
   166
text{*cooper.ML refers to this theorem*}
paulson@14479
   167
lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
paulson@14259
   168
paulson@14259
   169
lemma nat_0: "nat 0 = 0"
paulson@14259
   170
by (simp add: nat_eq_iff)
paulson@14259
   171
paulson@14259
   172
lemma nat_1: "nat 1 = Suc 0"
paulson@14259
   173
by (subst nat_eq_iff, simp)
paulson@14259
   174
paulson@14259
   175
lemma nat_2: "nat 2 = Suc (Suc 0)"
paulson@14259
   176
by (subst nat_eq_iff, simp)
paulson@14259
   177
paulson@16413
   178
lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
paulson@16413
   179
apply (insert zless_nat_conj [of 1 z])
paulson@16413
   180
apply (auto simp add: nat_1)
paulson@16413
   181
done
paulson@16413
   182
paulson@14259
   183
text{*This simplifies expressions of the form @{term "int n = z"} where
paulson@14259
   184
      z is an integer literal.*}
paulson@17085
   185
lemmas int_eq_iff_number_of = int_eq_iff [of _ "number_of v", standard]
paulson@17085
   186
declare int_eq_iff_number_of [simp]
paulson@17085
   187
paulson@13837
   188
paulson@14295
   189
lemma split_nat [arith_split]:
paulson@14259
   190
  "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
nipkow@13575
   191
  (is "?P = (?L & ?R)")
nipkow@13575
   192
proof (cases "i < 0")
nipkow@13575
   193
  case True thus ?thesis by simp
nipkow@13575
   194
next
nipkow@13575
   195
  case False
nipkow@13575
   196
  have "?P = ?L"
nipkow@13575
   197
  proof
nipkow@13575
   198
    assume ?P thus ?L using False by clarsimp
nipkow@13575
   199
  next
nipkow@13575
   200
    assume ?L thus ?P using False by simp
nipkow@13575
   201
  qed
nipkow@13575
   202
  with False show ?thesis by simp
nipkow@13575
   203
qed
nipkow@13575
   204
paulson@14387
   205
paulson@14479
   206
(*Analogous to zadd_int*)
paulson@15013
   207
lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)" 
paulson@14479
   208
by (induct m n rule: diff_induct, simp_all)
paulson@14479
   209
paulson@14479
   210
lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
paulson@14479
   211
apply (case_tac "0 \<le> z'")
paulson@14479
   212
apply (rule inj_int [THEN injD])
paulson@16413
   213
apply (simp add: int_mult zero_le_mult_iff)
paulson@14479
   214
apply (simp add: mult_le_0_iff)
paulson@14479
   215
done
paulson@14479
   216
paulson@14479
   217
lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
paulson@14479
   218
apply (rule trans)
paulson@14479
   219
apply (rule_tac [2] nat_mult_distrib, auto)
paulson@14479
   220
done
paulson@14479
   221
paulson@14479
   222
lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
paulson@14479
   223
apply (case_tac "z=0 | w=0")
paulson@15003
   224
apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
paulson@14479
   225
                      nat_mult_distrib_neg [symmetric] mult_less_0_iff)
paulson@14479
   226
done
paulson@14479
   227
paulson@14479
   228
wenzelm@17472
   229
subsection "Induction principles for int"
nipkow@13685
   230
nipkow@13685
   231
                     (* `set:int': dummy construction *)
nipkow@13685
   232
theorem int_ge_induct[case_names base step,induct set:int]:
nipkow@13685
   233
  assumes ge: "k \<le> (i::int)" and
nipkow@13685
   234
        base: "P(k)" and
nipkow@13685
   235
        step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
nipkow@13685
   236
  shows "P i"
nipkow@13685
   237
proof -
paulson@14272
   238
  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
nipkow@13685
   239
    proof (induct n)
nipkow@13685
   240
      case 0
nipkow@13685
   241
      hence "i = k" by arith
nipkow@13685
   242
      thus "P i" using base by simp
nipkow@13685
   243
    next
nipkow@13685
   244
      case (Suc n)
nipkow@13685
   245
      hence "n = nat((i - 1) - k)" by arith
nipkow@13685
   246
      moreover
nipkow@13685
   247
      have ki1: "k \<le> i - 1" using Suc.prems by arith
nipkow@13685
   248
      ultimately
nipkow@13685
   249
      have "P(i - 1)" by(rule Suc.hyps)
nipkow@13685
   250
      from step[OF ki1 this] show ?case by simp
nipkow@13685
   251
    qed
nipkow@13685
   252
  }
paulson@14473
   253
  with ge show ?thesis by fast
nipkow@13685
   254
qed
nipkow@13685
   255
nipkow@13685
   256
                     (* `set:int': dummy construction *)
nipkow@13685
   257
theorem int_gr_induct[case_names base step,induct set:int]:
nipkow@13685
   258
  assumes gr: "k < (i::int)" and
nipkow@13685
   259
        base: "P(k+1)" and
nipkow@13685
   260
        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
nipkow@13685
   261
  shows "P i"
nipkow@13685
   262
apply(rule int_ge_induct[of "k + 1"])
nipkow@13685
   263
  using gr apply arith
nipkow@13685
   264
 apply(rule base)
paulson@14259
   265
apply (rule step, simp+)
nipkow@13685
   266
done
nipkow@13685
   267
nipkow@13685
   268
theorem int_le_induct[consumes 1,case_names base step]:
nipkow@13685
   269
  assumes le: "i \<le> (k::int)" and
nipkow@13685
   270
        base: "P(k)" and
nipkow@13685
   271
        step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
nipkow@13685
   272
  shows "P i"
nipkow@13685
   273
proof -
paulson@14272
   274
  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
nipkow@13685
   275
    proof (induct n)
nipkow@13685
   276
      case 0
nipkow@13685
   277
      hence "i = k" by arith
nipkow@13685
   278
      thus "P i" using base by simp
nipkow@13685
   279
    next
nipkow@13685
   280
      case (Suc n)
nipkow@13685
   281
      hence "n = nat(k - (i+1))" by arith
nipkow@13685
   282
      moreover
nipkow@13685
   283
      have ki1: "i + 1 \<le> k" using Suc.prems by arith
nipkow@13685
   284
      ultimately
nipkow@13685
   285
      have "P(i+1)" by(rule Suc.hyps)
nipkow@13685
   286
      from step[OF ki1 this] show ?case by simp
nipkow@13685
   287
    qed
nipkow@13685
   288
  }
paulson@14473
   289
  with le show ?thesis by fast
nipkow@13685
   290
qed
nipkow@13685
   291
paulson@14387
   292
theorem int_less_induct [consumes 1,case_names base step]:
nipkow@13685
   293
  assumes less: "(i::int) < k" and
nipkow@13685
   294
        base: "P(k - 1)" and
nipkow@13685
   295
        step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
nipkow@13685
   296
  shows "P i"
nipkow@13685
   297
apply(rule int_le_induct[of _ "k - 1"])
nipkow@13685
   298
  using less apply arith
nipkow@13685
   299
 apply(rule base)
paulson@14259
   300
apply (rule step, simp+)
paulson@14259
   301
done
paulson@14259
   302
paulson@14259
   303
subsection{*Intermediate value theorems*}
paulson@14259
   304
paulson@14259
   305
lemma int_val_lemma:
paulson@14259
   306
     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
paulson@14259
   307
      f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
paulson@14271
   308
apply (induct_tac "n", simp)
paulson@14259
   309
apply (intro strip)
paulson@14259
   310
apply (erule impE, simp)
paulson@14259
   311
apply (erule_tac x = n in allE, simp)
paulson@14259
   312
apply (case_tac "k = f (n+1) ")
paulson@14259
   313
 apply force
paulson@14259
   314
apply (erule impE)
paulson@15003
   315
 apply (simp add: abs_if split add: split_if_asm)
paulson@14259
   316
apply (blast intro: le_SucI)
paulson@14259
   317
done
paulson@14259
   318
paulson@14259
   319
lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
paulson@14259
   320
paulson@14259
   321
lemma nat_intermed_int_val:
paulson@14259
   322
     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
paulson@14259
   323
         f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
paulson@14259
   324
apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
paulson@14259
   325
       in int_val_lemma)
paulson@14259
   326
apply simp
paulson@14259
   327
apply (erule impE)
paulson@14259
   328
 apply (intro strip)
paulson@14259
   329
 apply (erule_tac x = "i+m" in allE, arith)
paulson@14259
   330
apply (erule exE)
paulson@14259
   331
apply (rule_tac x = "i+m" in exI, arith)
paulson@14259
   332
done
paulson@14259
   333
paulson@14259
   334
paulson@14259
   335
subsection{*Products and 1, by T. M. Rasmussen*}
paulson@14259
   336
paulson@15234
   337
lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
paulson@15234
   338
by arith
paulson@15234
   339
paulson@15234
   340
lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
paulson@15234
   341
apply (case_tac "\<bar>n\<bar>=1") 
paulson@15234
   342
apply (simp add: abs_mult) 
paulson@15234
   343
apply (rule ccontr) 
paulson@15234
   344
apply (auto simp add: linorder_neq_iff abs_mult) 
paulson@15234
   345
apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
paulson@15234
   346
 prefer 2 apply arith 
paulson@15234
   347
apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp) 
paulson@15234
   348
apply (rule mult_mono, auto) 
nipkow@13685
   349
done
nipkow@13685
   350
paulson@15234
   351
lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
paulson@15234
   352
by (insert abs_zmult_eq_1 [of m n], arith)
paulson@15234
   353
paulson@14259
   354
lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
paulson@15234
   355
apply (auto dest: pos_zmult_eq_1_iff_lemma) 
paulson@15234
   356
apply (simp add: mult_commute [of m]) 
paulson@15234
   357
apply (frule pos_zmult_eq_1_iff_lemma, auto) 
paulson@14259
   358
done
paulson@14259
   359
paulson@14259
   360
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
paulson@15234
   361
apply (rule iffI) 
paulson@15234
   362
 apply (frule pos_zmult_eq_1_iff_lemma)
paulson@15234
   363
 apply (simp add: mult_commute [of m]) 
paulson@15234
   364
 apply (frule pos_zmult_eq_1_iff_lemma, auto) 
paulson@14259
   365
done
paulson@14259
   366
paulson@14259
   367
ML
paulson@14259
   368
{*
paulson@14259
   369
val zle_diff1_eq = thm "zle_diff1_eq";
paulson@14259
   370
val zle_add1_eq_le = thm "zle_add1_eq_le";
paulson@14259
   371
val nonneg_eq_int = thm "nonneg_eq_int";
paulson@14387
   372
val abs_minus_one = thm "abs_minus_one";
paulson@14390
   373
val of_int_number_of_eq = thm"of_int_number_of_eq";
paulson@14259
   374
val nat_eq_iff = thm "nat_eq_iff";
paulson@14259
   375
val nat_eq_iff2 = thm "nat_eq_iff2";
paulson@14259
   376
val nat_less_iff = thm "nat_less_iff";
paulson@14259
   377
val int_eq_iff = thm "int_eq_iff";
paulson@14259
   378
val nat_0 = thm "nat_0";
paulson@14259
   379
val nat_1 = thm "nat_1";
paulson@14259
   380
val nat_2 = thm "nat_2";
paulson@14259
   381
val nat_less_eq_zless = thm "nat_less_eq_zless";
paulson@14259
   382
val nat_le_eq_zle = thm "nat_le_eq_zle";
paulson@14259
   383
paulson@14259
   384
val nat_intermed_int_val = thm "nat_intermed_int_val";
paulson@14259
   385
val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
paulson@14259
   386
val zmult_eq_1_iff = thm "zmult_eq_1_iff";
paulson@14259
   387
val nat_add_distrib = thm "nat_add_distrib";
paulson@14259
   388
val nat_diff_distrib = thm "nat_diff_distrib";
paulson@14259
   389
val nat_mult_distrib = thm "nat_mult_distrib";
paulson@14259
   390
val nat_mult_distrib_neg = thm "nat_mult_distrib_neg";
paulson@14259
   391
val nat_abs_mult_distrib = thm "nat_abs_mult_distrib";
paulson@14259
   392
*}
paulson@14259
   393
wenzelm@7707
   394
end