src/HOL/NatArith.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16417 9bc16273c2d4
child 17085 5b57f995a179
permissions -rw-r--r--
Constant "If" is now local
nipkow@10214
     1
(*  Title:      HOL/NatArith.thy
nipkow@10214
     2
    ID:         $Id$
wenzelm@13297
     3
    Author:     Tobias Nipkow and Markus Wenzel
wenzelm@13297
     4
*)
nipkow@10214
     5
paulson@15404
     6
header {*Further Arithmetic Facts Concerning the Natural Numbers*}
nipkow@10214
     7
nipkow@15131
     8
theory NatArith
nipkow@15140
     9
imports Nat
haftmann@16417
    10
uses "arith_data.ML"
nipkow@15131
    11
begin
nipkow@10214
    12
nipkow@10214
    13
setup arith_setup
nipkow@10214
    14
paulson@15404
    15
text{*The following proofs may rely on the arithmetic proof procedures.*}
wenzelm@13297
    16
paulson@15404
    17
lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
paulson@14208
    18
by (simp add: less_eq reflcl_trancl [symmetric]
paulson@14208
    19
            del: reflcl_trancl, arith)
paulson@11454
    20
nipkow@10214
    21
lemma nat_diff_split:
paulson@10599
    22
    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
wenzelm@13297
    23
    -- {* elimination of @{text -} on @{text nat} *}
wenzelm@13297
    24
  by (cases "a<b" rule: case_split)
paulson@15404
    25
     (auto simp add: diff_is_0_eq [THEN iffD2])
paulson@11324
    26
paulson@11324
    27
lemma nat_diff_split_asm:
paulson@11324
    28
    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
wenzelm@13297
    29
    -- {* elimination of @{text -} on @{text nat} in assumptions *}
paulson@11324
    30
  by (simp split: nat_diff_split)
nipkow@10214
    31
nipkow@10214
    32
lemmas [arith_split] = nat_diff_split split_min split_max
nipkow@10214
    33
paulson@15404
    34
paulson@15404
    35
paulson@15404
    36
lemma le_square: "m \<le> m*(m::nat)"
paulson@15404
    37
by (induct_tac "m", auto)
paulson@15404
    38
paulson@15404
    39
lemma le_cube: "(m::nat) \<le> m*(m*m)"
paulson@15404
    40
by (induct_tac "m", auto)
paulson@15404
    41
paulson@15404
    42
paulson@15404
    43
text{*Subtraction laws, mostly by Clemens Ballarin*}
paulson@15404
    44
paulson@15404
    45
lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
paulson@15404
    46
by arith
paulson@15404
    47
paulson@15404
    48
lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
paulson@15404
    49
by arith
paulson@15404
    50
paulson@15404
    51
lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
paulson@15404
    52
by arith
paulson@15404
    53
paulson@15404
    54
lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
paulson@15404
    55
by arith
paulson@15404
    56
paulson@15404
    57
lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
paulson@15404
    58
by arith
paulson@15404
    59
paulson@15404
    60
lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
paulson@15404
    61
by arith
paulson@15404
    62
paulson@15404
    63
(*Replaces the previous diff_less and le_diff_less, which had the stronger
paulson@15404
    64
  second premise n\<le>m*)
nipkow@15439
    65
lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
paulson@15404
    66
by arith
paulson@15404
    67
paulson@15404
    68
paulson@15404
    69
(** Simplification of relational expressions involving subtraction **)
paulson@15404
    70
paulson@15404
    71
lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
paulson@15404
    72
by (simp split add: nat_diff_split)
paulson@15404
    73
paulson@15404
    74
lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
paulson@15404
    75
by (auto split add: nat_diff_split)
paulson@15404
    76
paulson@15404
    77
lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
paulson@15404
    78
by (auto split add: nat_diff_split)
paulson@15404
    79
paulson@15404
    80
lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
paulson@15404
    81
by (auto split add: nat_diff_split)
paulson@15404
    82
paulson@15404
    83
paulson@15404
    84
text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
paulson@15404
    85
paulson@15404
    86
(* Monotonicity of subtraction in first argument *)
paulson@15404
    87
lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
paulson@15404
    88
by (simp split add: nat_diff_split)
paulson@15404
    89
paulson@15404
    90
lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
paulson@15404
    91
by (simp split add: nat_diff_split)
paulson@15404
    92
paulson@15404
    93
lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
paulson@15404
    94
by (simp split add: nat_diff_split)
paulson@15404
    95
paulson@15404
    96
lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
paulson@15404
    97
by (simp split add: nat_diff_split)
paulson@15404
    98
paulson@15404
    99
text{*Lemmas for ex/Factorization*}
paulson@15404
   100
paulson@15404
   101
lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
paulson@15404
   102
by (case_tac "m", auto)
paulson@15404
   103
paulson@15404
   104
lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
paulson@15404
   105
by (case_tac "m", auto)
paulson@15404
   106
paulson@15404
   107
lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
paulson@15404
   108
by (case_tac "m", auto)
paulson@15404
   109
paulson@15404
   110
paulson@15404
   111
text{*Rewriting to pull differences out*}
paulson@15404
   112
paulson@15404
   113
lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
paulson@15404
   114
by arith
paulson@15404
   115
paulson@15404
   116
lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
paulson@15404
   117
by arith
paulson@15404
   118
paulson@15404
   119
lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
paulson@15404
   120
by arith
paulson@15404
   121
paulson@15404
   122
(*The others are
paulson@15404
   123
      i - j - k = i - (j + k),
paulson@15404
   124
      k \<le> j ==> j - k + i = j + i - k,
paulson@15404
   125
      k \<le> j ==> i + (j - k) = i + j - k *)
paulson@15404
   126
declare diff_diff_left [simp] 
paulson@15404
   127
        diff_add_assoc [symmetric, simp]
paulson@15404
   128
        diff_add_assoc2[symmetric, simp]
paulson@15404
   129
paulson@15404
   130
text{*At present we prove no analogue of @{text not_less_Least} or @{text
paulson@15404
   131
Least_Suc}, since there appears to be no need.*}
paulson@15404
   132
paulson@15404
   133
ML
paulson@15404
   134
{*
paulson@15404
   135
val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
paulson@15404
   136
val nat_diff_split = thm "nat_diff_split";
paulson@15404
   137
val nat_diff_split_asm = thm "nat_diff_split_asm";
paulson@15404
   138
val le_square = thm "le_square";
paulson@15404
   139
val le_cube = thm "le_cube";
paulson@15404
   140
val diff_less_mono = thm "diff_less_mono";
paulson@15404
   141
val less_diff_conv = thm "less_diff_conv";
paulson@15404
   142
val le_diff_conv = thm "le_diff_conv";
paulson@15404
   143
val le_diff_conv2 = thm "le_diff_conv2";
paulson@15404
   144
val diff_diff_cancel = thm "diff_diff_cancel";
paulson@15404
   145
val le_add_diff = thm "le_add_diff";
paulson@15404
   146
val diff_less = thm "diff_less";
paulson@15404
   147
val diff_diff_eq = thm "diff_diff_eq";
paulson@15404
   148
val eq_diff_iff = thm "eq_diff_iff";
paulson@15404
   149
val less_diff_iff = thm "less_diff_iff";
paulson@15404
   150
val le_diff_iff = thm "le_diff_iff";
paulson@15404
   151
val diff_le_mono = thm "diff_le_mono";
paulson@15404
   152
val diff_le_mono2 = thm "diff_le_mono2";
paulson@15404
   153
val diff_less_mono2 = thm "diff_less_mono2";
paulson@15404
   154
val diffs0_imp_equal = thm "diffs0_imp_equal";
paulson@15404
   155
val one_less_mult = thm "one_less_mult";
paulson@15404
   156
val n_less_m_mult_n = thm "n_less_m_mult_n";
paulson@15404
   157
val n_less_n_mult_m = thm "n_less_n_mult_m";
paulson@15404
   158
val diff_diff_right = thm "diff_diff_right";
paulson@15404
   159
val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
paulson@15404
   160
val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
paulson@15404
   161
*}
paulson@15404
   162
nipkow@15539
   163
subsection{*Embedding of the Naturals into any @{text
nipkow@15539
   164
comm_semiring_1_cancel}: @{term of_nat}*}
nipkow@15539
   165
nipkow@15539
   166
consts of_nat :: "nat => 'a::comm_semiring_1_cancel"
nipkow@15539
   167
nipkow@15539
   168
primrec
nipkow@15539
   169
  of_nat_0:   "of_nat 0 = 0"
nipkow@15539
   170
  of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
nipkow@15539
   171
nipkow@15539
   172
lemma of_nat_1 [simp]: "of_nat 1 = 1"
nipkow@15539
   173
by simp
nipkow@15539
   174
nipkow@15539
   175
lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
nipkow@15539
   176
apply (induct m)
nipkow@15539
   177
apply (simp_all add: add_ac)
nipkow@15539
   178
done
nipkow@15539
   179
nipkow@15539
   180
lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
nipkow@15539
   181
apply (induct m)
nipkow@15539
   182
apply (simp_all add: mult_ac add_ac right_distrib)
nipkow@15539
   183
done
nipkow@15539
   184
nipkow@15539
   185
lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
nipkow@15539
   186
apply (induct m, simp_all)
nipkow@15539
   187
apply (erule order_trans)
nipkow@15539
   188
apply (rule less_add_one [THEN order_less_imp_le])
nipkow@15539
   189
done
nipkow@15539
   190
nipkow@15539
   191
lemma less_imp_of_nat_less:
nipkow@15539
   192
     "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
nipkow@15539
   193
apply (induct m n rule: diff_induct, simp_all)
nipkow@15539
   194
apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
nipkow@15539
   195
done
nipkow@15539
   196
nipkow@15539
   197
lemma of_nat_less_imp_less:
nipkow@15539
   198
     "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
nipkow@15539
   199
apply (induct m n rule: diff_induct, simp_all)
nipkow@15539
   200
apply (insert zero_le_imp_of_nat)
nipkow@15539
   201
apply (force simp add: linorder_not_less [symmetric])
nipkow@15539
   202
done
nipkow@15539
   203
nipkow@15539
   204
lemma of_nat_less_iff [simp]:
nipkow@15539
   205
     "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
nipkow@15539
   206
by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
nipkow@15539
   207
nipkow@15539
   208
text{*Special cases where either operand is zero*}
nipkow@15539
   209
declare of_nat_less_iff [of 0, simplified, simp]
nipkow@15539
   210
declare of_nat_less_iff [of _ 0, simplified, simp]
nipkow@15539
   211
nipkow@15539
   212
lemma of_nat_le_iff [simp]:
nipkow@15539
   213
     "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
nipkow@15539
   214
by (simp add: linorder_not_less [symmetric])
nipkow@15539
   215
nipkow@15539
   216
text{*Special cases where either operand is zero*}
nipkow@15539
   217
declare of_nat_le_iff [of 0, simplified, simp]
nipkow@15539
   218
declare of_nat_le_iff [of _ 0, simplified, simp]
nipkow@15539
   219
nipkow@15539
   220
text{*The ordering on the @{text comm_semiring_1_cancel} is necessary
nipkow@15539
   221
to exclude the possibility of a finite field, which indeed wraps back to
nipkow@15539
   222
zero.*}
nipkow@15539
   223
lemma of_nat_eq_iff [simp]:
nipkow@15539
   224
     "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
nipkow@15539
   225
by (simp add: order_eq_iff)
nipkow@15539
   226
nipkow@15539
   227
text{*Special cases where either operand is zero*}
nipkow@15539
   228
declare of_nat_eq_iff [of 0, simplified, simp]
nipkow@15539
   229
declare of_nat_eq_iff [of _ 0, simplified, simp]
nipkow@15539
   230
nipkow@15539
   231
lemma of_nat_diff [simp]:
nipkow@15539
   232
     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"
nipkow@15539
   233
by (simp del: of_nat_add
nipkow@15539
   234
	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
nipkow@15539
   235
paulson@15404
   236
nipkow@10214
   237
end