src/HOL/NatArith.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10214 77349ed89f45
child 10962 cda180b1e2e0
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/NatArith.ML
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     5
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     6
Further proofs about elementary arithmetic, using the arithmetic proof
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     7
procedures.
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     8
*)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     9
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    10
(*legacy ...*)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    11
structure NatArith = struct val thy = the_context () end;
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    12
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    13
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    14
Goal "m <= m*(m::nat)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    15
by (induct_tac "m" 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    16
by Auto_tac;
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    17
qed "le_square";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    18
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    19
Goal "(m::nat) <= m*(m*m)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    20
by (induct_tac "m" 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    21
by Auto_tac;
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    22
qed "le_cube";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    23
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    24
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    25
(*** Subtraction laws -- mostly from Clemens Ballarin ***)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    26
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    27
Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    28
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    29
qed "diff_less_mono";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    30
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    31
Goal "(i < j-k) = (i+k < (j::nat))";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    32
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    33
qed "less_diff_conv";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    34
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    35
Goal "(j-k <= (i::nat)) = (j <= i+k)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    36
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    37
qed "le_diff_conv";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    38
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    39
Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    40
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    41
qed "le_diff_conv2";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    42
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    43
Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    44
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    45
qed "Suc_diff_Suc";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    46
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    47
Goal "i <= (n::nat) ==> n - (n - i) = i";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    48
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    49
qed "diff_diff_cancel";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    50
Addsimps [diff_diff_cancel];
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    51
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    52
Goal "k <= (n::nat) ==> m <= n + m - k";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    53
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    54
qed "le_add_diff";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    55
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    56
Goal "m-1 < n ==> m <= n";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    57
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    58
qed "pred_less_imp_le";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    59
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    60
Goal "j<=i ==> i - j < Suc i - j";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    61
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    62
qed "diff_less_Suc_diff";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    63
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    64
Goal "i - j <= Suc i - j";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    65
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    66
qed "diff_le_Suc_diff";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    67
AddIffs [diff_le_Suc_diff];
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    68
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    69
Goal "n - Suc i <= n - i";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    70
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    71
qed "diff_Suc_le_diff";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    72
AddIffs [diff_Suc_le_diff];
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    73
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    74
Goal "!!m::nat. 0 < n ==> (m <= n-1) = (m<n)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    75
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    76
qed "le_pred_eq";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    77
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    78
Goal "!!m::nat. 0 < n ==> (m-1 < n) = (m<=n)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    79
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    80
qed "less_pred_eq";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    81
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    82
(*Replaces the previous diff_less and le_diff_less, which had the stronger
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    83
  second premise n<=m*)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    84
Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    85
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    86
qed "diff_less";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    87
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    88
Goal "j <= (k::nat) ==> (j+i)-k = i-(k-j)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    89
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    90
qed "diff_add_assoc_diff";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    91
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    92
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    93
(*** Reducing subtraction to addition ***)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    94
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    95
Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    96
by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    97
qed_spec_mp "Suc_diff_add_le";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    98
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    99
Goal "i<n ==> n - Suc i < n - i";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   100
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   101
qed "diff_Suc_less_diff";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   102
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   103
Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   104
by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   105
qed "if_Suc_diff_le";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   106
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   107
Goal "Suc(m)-n <= Suc(m-n)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   108
by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   109
qed "diff_Suc_le_Suc_diff";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   110
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   111
(** Simplification of relational expressions involving subtraction **)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   112
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   113
Goal "[| k <= m;  k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   114
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   115
qed "diff_diff_eq";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   116
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   117
Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   118
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   119
qed "eq_diff_iff";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   120
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   121
Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k < n-k) = (m<n)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   122
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   123
qed "less_diff_iff";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   124
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   125
Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   126
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   127
qed "le_diff_iff";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   128
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   129
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   130
(** (Anti)Monotonicity of subtraction -- by Stephan Merz **)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   131
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   132
(* Monotonicity of subtraction in first argument *)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   133
Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   134
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   135
qed "diff_le_mono";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   136
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   137
Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   138
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   139
qed "diff_le_mono2";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   140
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   141
Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   142
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   143
qed "diff_less_mono2";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   144
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   145
Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   146
by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   147
qed "diffs0_imp_equal";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   148
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   149
(** Lemmas for ex/Factorization **)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   150
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   151
Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   152
by (case_tac "m" 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   153
by Auto_tac;
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   154
qed "one_less_mult"; 
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   155
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   156
Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   157
by (case_tac "m" 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   158
by Auto_tac;
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   159
qed "n_less_m_mult_n"; 
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   160
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   161
Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   162
by (case_tac "m" 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   163
by Auto_tac;
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   164
qed "n_less_n_mult_m"; 
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   165
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   166
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   167
(** Rewriting to pull differences out **)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   168
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   169
Goal "k<=j --> i - (j - k) = i + (k::nat) - j";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   170
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   171
qed "diff_diff_right";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   172
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   173
Goal "k <= j ==> m - Suc (j - k) = m + k - Suc j";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   174
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   175
qed "diff_Suc_diff_eq1"; 
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   176
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   177
Goal "k <= j ==> Suc (j - k) - m = Suc j - (k + m)";
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   178
by (arith_tac 1);
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   179
qed "diff_Suc_diff_eq2"; 
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   180
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   181
(*The others are
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   182
      i - j - k = i - (j + k),
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   183
      k <= j ==> j - k + i = j + i - k,
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   184
      k <= j ==> i + (j - k) = i + j - k *)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   185
Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym, 
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   186
	  diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2];
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   187