src/HOL/Integ/IntArith.thy
author paulson
Thu Dec 04 10:29:17 2003 +0100 (2003-12-04)
changeset 14272 5efbb548107d
parent 14271 8ed6989228bb
child 14295 7f115e5c5de4
permissions -rw-r--r--
Tidying of the integer development; towards removing the
abel_cancel simproc
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@14272
    11
subsection{*Inequality Reasoning for the Arithmetic Simproc*}
paulson@14272
    12
paulson@14272
    13
lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
paulson@14272
    14
  proof (auto simp add: zle_def zless_iff_Suc_zadd) 
paulson@14272
    15
  fix m n
paulson@14272
    16
  assume "w + 1 = w + (1 + int m) + (1 + int n)"
paulson@14272
    17
  hence "(w + 1) + (1 + int (m + n)) = (w + 1) + 0" 
paulson@14272
    18
    by (simp add: add_ac zadd_int [symmetric])
paulson@14272
    19
  hence "int (Suc(m+n)) = 0" 
paulson@14272
    20
    by (simp only: Ring_and_Field.add_left_cancel int_Suc)
paulson@14272
    21
  thus False by (simp only: int_eq_0_conv)
paulson@14272
    22
  qed
paulson@14272
    23
wenzelm@12023
    24
use "int_arith1.ML"
wenzelm@12023
    25
setup int_arith_setup
paulson@14259
    26
paulson@14272
    27
subsection{*More inequality reasoning*}
paulson@14272
    28
paulson@14272
    29
lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
paulson@14259
    30
by arith
paulson@14259
    31
paulson@14272
    32
lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
paulson@14272
    33
by arith
paulson@14272
    34
paulson@14272
    35
lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<(z::int))"
paulson@14272
    36
by arith
paulson@14272
    37
paulson@14272
    38
lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w\<le>(z::int))"
paulson@14259
    39
by arith
paulson@14259
    40
paulson@14259
    41
lemma zadd_left_cancel0 [simp]: "(z = z + w) = (w = (0::int))"
paulson@14259
    42
by arith
paulson@14259
    43
paulson@14259
    44
subsection{*Results about @{term nat}*}
paulson@14259
    45
paulson@14272
    46
lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
paulson@14259
    47
by (blast dest: nat_0_le sym)
paulson@14259
    48
paulson@14272
    49
lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
paulson@14259
    50
by auto
paulson@14259
    51
paulson@14272
    52
lemma nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
paulson@14259
    53
by auto
paulson@14259
    54
paulson@14272
    55
lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
paulson@14259
    56
apply (rule iffI)
paulson@14259
    57
apply (erule nat_0_le [THEN subst])
paulson@14259
    58
apply (simp_all del: zless_int add: zless_int [symmetric]) 
paulson@14259
    59
done
paulson@14259
    60
paulson@14272
    61
lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
paulson@14259
    62
by (auto simp add: nat_eq_iff2)
paulson@14259
    63
paulson@14259
    64
paulson@14259
    65
(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
paulson@14259
    66
declare Zero_int_def [symmetric, simp]
paulson@14259
    67
declare One_int_def [symmetric, simp]
paulson@14259
    68
paulson@14259
    69
text{*cooper.ML refers to this theorem*}
paulson@14259
    70
lemmas zdiff_def_symmetric = zdiff_def [symmetric, simp]
paulson@14259
    71
paulson@14259
    72
lemma nat_0: "nat 0 = 0"
paulson@14259
    73
by (simp add: nat_eq_iff)
paulson@14259
    74
paulson@14259
    75
lemma nat_1: "nat 1 = Suc 0"
paulson@14259
    76
by (subst nat_eq_iff, simp)
paulson@14259
    77
paulson@14259
    78
lemma nat_2: "nat 2 = Suc (Suc 0)"
paulson@14259
    79
by (subst nat_eq_iff, simp)
paulson@14259
    80
paulson@14272
    81
lemma nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
paulson@14259
    82
apply (case_tac "neg z")
paulson@14259
    83
apply (auto simp add: nat_less_iff)
paulson@14259
    84
apply (auto intro: zless_trans simp add: neg_eq_less_0 zle_def)
paulson@14259
    85
done
paulson@14259
    86
paulson@14272
    87
lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
paulson@14259
    88
by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)
paulson@14259
    89
paulson@14259
    90
subsection{*@{term abs}: Absolute Value, as an Integer*}
paulson@14259
    91
paulson@14259
    92
(* Simpler: use zabs_def as rewrite rule
paulson@14259
    93
   but arith_tac is not parameterized by such simp rules
paulson@14259
    94
*)
paulson@14259
    95
paulson@14272
    96
lemma zabs_split: "P(abs(i::int)) = ((0 \<le> i --> P i) & (i < 0 --> P(-i)))"
paulson@14259
    97
by (simp add: zabs_def)
paulson@14259
    98
paulson@14272
    99
lemma zero_le_zabs [iff]: "0 \<le> abs (z::int)"
paulson@14259
   100
by (simp add: zabs_def)
paulson@14259
   101
paulson@14259
   102
paulson@14259
   103
text{*This simplifies expressions of the form @{term "int n = z"} where
paulson@14259
   104
      z is an integer literal.*}
paulson@14259
   105
declare int_eq_iff [of _ "number_of v", standard, simp]
paulson@13837
   106
wenzelm@12023
   107
declare zabs_split [arith_split]
wenzelm@12023
   108
paulson@13837
   109
lemma zabs_eq_iff:
paulson@14272
   110
    "(abs (z::int) = w) = (z = w \<and> 0 \<le> z \<or> z = -w \<and> z < 0)"
paulson@13837
   111
  by (auto simp add: zabs_def)
paulson@13837
   112
paulson@13849
   113
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
paulson@13849
   114
  by simp
paulson@13849
   115
nipkow@13575
   116
lemma split_nat[arith_split]:
paulson@14259
   117
  "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
nipkow@13575
   118
  (is "?P = (?L & ?R)")
nipkow@13575
   119
proof (cases "i < 0")
nipkow@13575
   120
  case True thus ?thesis by simp
nipkow@13575
   121
next
nipkow@13575
   122
  case False
nipkow@13575
   123
  have "?P = ?L"
nipkow@13575
   124
  proof
nipkow@13575
   125
    assume ?P thus ?L using False by clarsimp
nipkow@13575
   126
  next
nipkow@13575
   127
    assume ?L thus ?P using False by simp
nipkow@13575
   128
  qed
nipkow@13575
   129
  with False show ?thesis by simp
nipkow@13575
   130
qed
nipkow@13575
   131
nipkow@13685
   132
subsubsection "Induction principles for int"
nipkow@13685
   133
nipkow@13685
   134
                     (* `set:int': dummy construction *)
nipkow@13685
   135
theorem int_ge_induct[case_names base step,induct set:int]:
nipkow@13685
   136
  assumes ge: "k \<le> (i::int)" and
nipkow@13685
   137
        base: "P(k)" and
nipkow@13685
   138
        step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
nipkow@13685
   139
  shows "P i"
nipkow@13685
   140
proof -
paulson@14272
   141
  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
nipkow@13685
   142
    proof (induct n)
nipkow@13685
   143
      case 0
nipkow@13685
   144
      hence "i = k" by arith
nipkow@13685
   145
      thus "P i" using base by simp
nipkow@13685
   146
    next
nipkow@13685
   147
      case (Suc n)
nipkow@13685
   148
      hence "n = nat((i - 1) - k)" by arith
nipkow@13685
   149
      moreover
nipkow@13685
   150
      have ki1: "k \<le> i - 1" using Suc.prems by arith
nipkow@13685
   151
      ultimately
nipkow@13685
   152
      have "P(i - 1)" by(rule Suc.hyps)
nipkow@13685
   153
      from step[OF ki1 this] show ?case by simp
nipkow@13685
   154
    qed
nipkow@13685
   155
  }
nipkow@13685
   156
  from this ge show ?thesis by fast
nipkow@13685
   157
qed
nipkow@13685
   158
nipkow@13685
   159
                     (* `set:int': dummy construction *)
nipkow@13685
   160
theorem int_gr_induct[case_names base step,induct set:int]:
nipkow@13685
   161
  assumes gr: "k < (i::int)" and
nipkow@13685
   162
        base: "P(k+1)" and
nipkow@13685
   163
        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
nipkow@13685
   164
  shows "P i"
nipkow@13685
   165
apply(rule int_ge_induct[of "k + 1"])
nipkow@13685
   166
  using gr apply arith
nipkow@13685
   167
 apply(rule base)
paulson@14259
   168
apply (rule step, simp+)
nipkow@13685
   169
done
nipkow@13685
   170
nipkow@13685
   171
theorem int_le_induct[consumes 1,case_names base step]:
nipkow@13685
   172
  assumes le: "i \<le> (k::int)" and
nipkow@13685
   173
        base: "P(k)" and
nipkow@13685
   174
        step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
nipkow@13685
   175
  shows "P i"
nipkow@13685
   176
proof -
paulson@14272
   177
  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
nipkow@13685
   178
    proof (induct n)
nipkow@13685
   179
      case 0
nipkow@13685
   180
      hence "i = k" by arith
nipkow@13685
   181
      thus "P i" using base by simp
nipkow@13685
   182
    next
nipkow@13685
   183
      case (Suc n)
nipkow@13685
   184
      hence "n = nat(k - (i+1))" by arith
nipkow@13685
   185
      moreover
nipkow@13685
   186
      have ki1: "i + 1 \<le> k" using Suc.prems by arith
nipkow@13685
   187
      ultimately
nipkow@13685
   188
      have "P(i+1)" by(rule Suc.hyps)
nipkow@13685
   189
      from step[OF ki1 this] show ?case by simp
nipkow@13685
   190
    qed
nipkow@13685
   191
  }
nipkow@13685
   192
  from this le show ?thesis by fast
nipkow@13685
   193
qed
nipkow@13685
   194
nipkow@13685
   195
theorem int_less_induct[consumes 1,case_names base step]:
nipkow@13685
   196
  assumes less: "(i::int) < k" and
nipkow@13685
   197
        base: "P(k - 1)" and
nipkow@13685
   198
        step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
nipkow@13685
   199
  shows "P i"
nipkow@13685
   200
apply(rule int_le_induct[of _ "k - 1"])
nipkow@13685
   201
  using less apply arith
nipkow@13685
   202
 apply(rule base)
paulson@14259
   203
apply (rule step, simp+)
paulson@14259
   204
done
paulson@14259
   205
paulson@14259
   206
subsection{*Simple Equations*}
paulson@14259
   207
paulson@14259
   208
lemma int_diff_minus_eq [simp]: "x - - y = x + (y::int)"
paulson@14259
   209
by simp
paulson@14259
   210
paulson@14259
   211
lemma abs_abs [simp]: "abs(abs(x::int)) = abs(x)"
paulson@14259
   212
by arith
paulson@14259
   213
paulson@14259
   214
lemma abs_minus [simp]: "abs(-(x::int)) = abs(x)"
paulson@14259
   215
by arith
paulson@14259
   216
paulson@14272
   217
lemma triangle_ineq: "abs(x+y) \<le> abs(x) + abs(y::int)"
paulson@14259
   218
by arith
paulson@14259
   219
paulson@14259
   220
paulson@14259
   221
subsection{*Intermediate value theorems*}
paulson@14259
   222
paulson@14259
   223
lemma int_val_lemma:
paulson@14259
   224
     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
paulson@14259
   225
      f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
paulson@14271
   226
apply (induct_tac "n", simp)
paulson@14259
   227
apply (intro strip)
paulson@14259
   228
apply (erule impE, simp)
paulson@14259
   229
apply (erule_tac x = n in allE, simp)
paulson@14259
   230
apply (case_tac "k = f (n+1) ")
paulson@14259
   231
 apply force
paulson@14259
   232
apply (erule impE)
paulson@14259
   233
 apply (simp add: zabs_def split add: split_if_asm)
paulson@14259
   234
apply (blast intro: le_SucI)
paulson@14259
   235
done
paulson@14259
   236
paulson@14259
   237
lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
paulson@14259
   238
paulson@14259
   239
lemma nat_intermed_int_val:
paulson@14259
   240
     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
paulson@14259
   241
         f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
paulson@14259
   242
apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
paulson@14259
   243
       in int_val_lemma)
paulson@14259
   244
apply simp
paulson@14259
   245
apply (erule impE)
paulson@14259
   246
 apply (intro strip)
paulson@14259
   247
 apply (erule_tac x = "i+m" in allE, arith)
paulson@14259
   248
apply (erule exE)
paulson@14259
   249
apply (rule_tac x = "i+m" in exI, arith)
paulson@14259
   250
done
paulson@14259
   251
paulson@14259
   252
paulson@14259
   253
subsection{*Some convenient biconditionals for products of signs*}
paulson@14259
   254
paulson@14259
   255
lemma zmult_pos: "[| (0::int) < i; 0 < j |] ==> 0 < i*j"
paulson@14266
   256
  by (rule Ring_and_Field.mult_pos)
paulson@14259
   257
paulson@14259
   258
lemma zmult_neg: "[| i < (0::int); j < 0 |] ==> 0 < i*j"
paulson@14266
   259
  by (rule Ring_and_Field.mult_neg)
paulson@14259
   260
paulson@14259
   261
lemma zmult_pos_neg: "[| (0::int) < i; j < 0 |] ==> i*j < 0"
paulson@14266
   262
  by (rule Ring_and_Field.mult_pos_neg)
paulson@14259
   263
paulson@14259
   264
lemma int_0_less_mult_iff: "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
paulson@14266
   265
  by (rule Ring_and_Field.zero_less_mult_iff)
paulson@14259
   266
paulson@14259
   267
lemma int_0_le_mult_iff: "((0::int) \<le> x*y) = (0 \<le> x & 0 \<le> y | x \<le> 0 & y \<le> 0)"
paulson@14266
   268
  by (rule Ring_and_Field.zero_le_mult_iff)
paulson@14259
   269
paulson@14259
   270
lemma zmult_less_0_iff: "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)"
paulson@14266
   271
  by (rule Ring_and_Field.mult_less_0_iff)
paulson@14259
   272
paulson@14259
   273
lemma zmult_le_0_iff: "(x*y \<le> (0::int)) = (0 \<le> x & y \<le> 0 | x \<le> 0 & 0 \<le> y)"
paulson@14266
   274
  by (rule Ring_and_Field.mult_le_0_iff)
paulson@14259
   275
paulson@14259
   276
lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::int))"
paulson@14266
   277
  by (rule Ring_and_Field.abs_eq_0)
paulson@14259
   278
paulson@14259
   279
lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::int))"
paulson@14266
   280
  by (rule Ring_and_Field.zero_less_abs_iff)
paulson@14259
   281
paulson@14259
   282
lemma square_nonzero [simp]: "0 \<le> x * (x::int)"
paulson@14266
   283
  by (rule Ring_and_Field.zero_le_square)
paulson@14259
   284
paulson@14259
   285
paulson@14259
   286
subsection{*Products and 1, by T. M. Rasmussen*}
paulson@14259
   287
paulson@14259
   288
lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
paulson@14259
   289
apply auto
paulson@14259
   290
apply (subgoal_tac "m*1 = m*n")
paulson@14259
   291
apply (drule zmult_cancel1 [THEN iffD1], auto)
nipkow@13685
   292
done
nipkow@13685
   293
paulson@14259
   294
lemma zless_1_zmult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)"
paulson@14259
   295
apply (rule_tac y = "1*n" in order_less_trans)
paulson@14259
   296
apply (rule_tac [2] zmult_zless_mono1)
paulson@14259
   297
apply (simp_all (no_asm_simp))
paulson@14259
   298
done
paulson@14259
   299
paulson@14259
   300
lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
paulson@14259
   301
apply auto
paulson@14259
   302
apply (case_tac "m=1")
paulson@14259
   303
apply (case_tac [2] "n=1")
paulson@14259
   304
apply (case_tac [4] "m=1")
paulson@14259
   305
apply (case_tac [5] "n=1", auto)
paulson@14259
   306
apply (tactic"distinct_subgoals_tac")
paulson@14259
   307
apply (subgoal_tac "1<m*n", simp)
paulson@14259
   308
apply (rule zless_1_zmult, arith)
paulson@14259
   309
apply (subgoal_tac "0<n", arith)
paulson@14259
   310
apply (subgoal_tac "0<m*n")
paulson@14259
   311
apply (drule int_0_less_mult_iff [THEN iffD1], auto)
paulson@14259
   312
done
paulson@14259
   313
paulson@14259
   314
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
paulson@14259
   315
apply (case_tac "0<m")
paulson@14271
   316
apply (simp add: pos_zmult_eq_1_iff)
paulson@14259
   317
apply (case_tac "m=0")
paulson@14271
   318
apply (simp del: number_of_reorient)
paulson@14259
   319
apply (subgoal_tac "0 < -m")
paulson@14259
   320
apply (drule_tac n = "-n" in pos_zmult_eq_1_iff, auto)
paulson@14259
   321
done
paulson@14259
   322
paulson@14259
   323
paulson@14259
   324
subsection{*More about nat*}
paulson@14259
   325
paulson@14271
   326
(*Analogous to zadd_int*)
paulson@14271
   327
lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)"
paulson@14271
   328
by (induct m n rule: diff_induct, simp_all)
paulson@14271
   329
paulson@14259
   330
lemma nat_add_distrib:
paulson@14259
   331
     "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
paulson@14259
   332
apply (rule inj_int [THEN injD])
paulson@14271
   333
apply (simp add: zadd_int [symmetric])
paulson@14259
   334
done
paulson@14259
   335
paulson@14259
   336
lemma nat_diff_distrib:
paulson@14259
   337
     "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
paulson@14259
   338
apply (rule inj_int [THEN injD])
paulson@14271
   339
apply (simp add: zdiff_int [symmetric] nat_le_eq_zle)
paulson@14259
   340
done
paulson@14259
   341
paulson@14259
   342
lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
paulson@14259
   343
apply (case_tac "0 \<le> z'")
paulson@14259
   344
apply (rule inj_int [THEN injD])
paulson@14271
   345
apply (simp add: zmult_int [symmetric] int_0_le_mult_iff)
paulson@14259
   346
apply (simp add: zmult_le_0_iff)
paulson@14259
   347
done
paulson@14259
   348
paulson@14259
   349
lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
paulson@14259
   350
apply (rule trans)
paulson@14259
   351
apply (rule_tac [2] nat_mult_distrib, auto)
paulson@14259
   352
done
paulson@14259
   353
paulson@14259
   354
lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
paulson@14259
   355
apply (case_tac "z=0 | w=0")
paulson@14259
   356
apply (auto simp add: zabs_def nat_mult_distrib [symmetric] 
paulson@14259
   357
                      nat_mult_distrib_neg [symmetric] zmult_less_0_iff)
paulson@14259
   358
done
paulson@14259
   359
paulson@14259
   360
ML
paulson@14259
   361
{*
paulson@14259
   362
val zle_diff1_eq = thm "zle_diff1_eq";
paulson@14259
   363
val zle_add1_eq_le = thm "zle_add1_eq_le";
paulson@14259
   364
val nonneg_eq_int = thm "nonneg_eq_int";
paulson@14259
   365
val nat_eq_iff = thm "nat_eq_iff";
paulson@14259
   366
val nat_eq_iff2 = thm "nat_eq_iff2";
paulson@14259
   367
val nat_less_iff = thm "nat_less_iff";
paulson@14259
   368
val int_eq_iff = thm "int_eq_iff";
paulson@14259
   369
val nat_0 = thm "nat_0";
paulson@14259
   370
val nat_1 = thm "nat_1";
paulson@14259
   371
val nat_2 = thm "nat_2";
paulson@14259
   372
val nat_less_eq_zless = thm "nat_less_eq_zless";
paulson@14259
   373
val nat_le_eq_zle = thm "nat_le_eq_zle";
paulson@14259
   374
val zabs_split = thm "zabs_split";
paulson@14259
   375
val zero_le_zabs = thm "zero_le_zabs";
paulson@14259
   376
paulson@14259
   377
val int_diff_minus_eq = thm "int_diff_minus_eq";
paulson@14259
   378
val abs_abs = thm "abs_abs";
paulson@14259
   379
val abs_minus = thm "abs_minus";
paulson@14259
   380
val triangle_ineq = thm "triangle_ineq";
paulson@14259
   381
val nat_intermed_int_val = thm "nat_intermed_int_val";
paulson@14259
   382
val zmult_pos = thm "zmult_pos";
paulson@14259
   383
val zmult_neg = thm "zmult_neg";
paulson@14259
   384
val zmult_pos_neg = thm "zmult_pos_neg";
paulson@14259
   385
val int_0_less_mult_iff = thm "int_0_less_mult_iff";
paulson@14259
   386
val int_0_le_mult_iff = thm "int_0_le_mult_iff";
paulson@14259
   387
val zmult_less_0_iff = thm "zmult_less_0_iff";
paulson@14259
   388
val zmult_le_0_iff = thm "zmult_le_0_iff";
paulson@14259
   389
val abs_mult = thm "abs_mult";
paulson@14259
   390
val abs_eq_0 = thm "abs_eq_0";
paulson@14259
   391
val zero_less_abs_iff = thm "zero_less_abs_iff";
paulson@14259
   392
val square_nonzero = thm "square_nonzero";
paulson@14259
   393
val zmult_eq_self_iff = thm "zmult_eq_self_iff";
paulson@14259
   394
val zless_1_zmult = thm "zless_1_zmult";
paulson@14259
   395
val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
paulson@14259
   396
val zmult_eq_1_iff = thm "zmult_eq_1_iff";
paulson@14259
   397
val nat_add_distrib = thm "nat_add_distrib";
paulson@14259
   398
val nat_diff_distrib = thm "nat_diff_distrib";
paulson@14259
   399
val nat_mult_distrib = thm "nat_mult_distrib";
paulson@14259
   400
val nat_mult_distrib_neg = thm "nat_mult_distrib_neg";
paulson@14259
   401
val nat_abs_mult_distrib = thm "nat_abs_mult_distrib";
paulson@14259
   402
*}
paulson@14259
   403
wenzelm@7707
   404
end