src/HOL/NatArith.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 11701 3d51fbf81c17
permissions -rw-r--r--
import -> imports
nipkow@10214
     1
(*  Title:      HOL/NatArith.ML
nipkow@10214
     2
    ID:         $Id$
nipkow@10214
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
nipkow@10214
     4
    Copyright   1998  University of Cambridge
nipkow@10214
     5
nipkow@10214
     6
Further proofs about elementary arithmetic, using the arithmetic proof
nipkow@10214
     7
procedures.
nipkow@10214
     8
*)
nipkow@10214
     9
nipkow@10214
    10
(*legacy ...*)
nipkow@10214
    11
structure NatArith = struct val thy = the_context () end;
nipkow@10214
    12
nipkow@10214
    13
nipkow@10214
    14
Goal "m <= m*(m::nat)";
nipkow@10214
    15
by (induct_tac "m" 1);
nipkow@10214
    16
by Auto_tac;
nipkow@10214
    17
qed "le_square";
nipkow@10214
    18
nipkow@10214
    19
Goal "(m::nat) <= m*(m*m)";
nipkow@10214
    20
by (induct_tac "m" 1);
nipkow@10214
    21
by Auto_tac;
nipkow@10214
    22
qed "le_cube";
nipkow@10214
    23
nipkow@10214
    24
nipkow@10214
    25
(*** Subtraction laws -- mostly from Clemens Ballarin ***)
nipkow@10214
    26
nipkow@10214
    27
Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
nipkow@10214
    28
by (arith_tac 1);
nipkow@10214
    29
qed "diff_less_mono";
nipkow@10214
    30
nipkow@10214
    31
Goal "(i < j-k) = (i+k < (j::nat))";
nipkow@10214
    32
by (arith_tac 1);
nipkow@10214
    33
qed "less_diff_conv";
nipkow@10214
    34
nipkow@10214
    35
Goal "(j-k <= (i::nat)) = (j <= i+k)";
nipkow@10214
    36
by (arith_tac 1);
nipkow@10214
    37
qed "le_diff_conv";
nipkow@10214
    38
nipkow@10214
    39
Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
nipkow@10214
    40
by (arith_tac 1);
nipkow@10214
    41
qed "le_diff_conv2";
nipkow@10214
    42
nipkow@10214
    43
Goal "i <= (n::nat) ==> n - (n - i) = i";
nipkow@10214
    44
by (arith_tac 1);
nipkow@10214
    45
qed "diff_diff_cancel";
nipkow@10214
    46
Addsimps [diff_diff_cancel];
nipkow@10214
    47
nipkow@10214
    48
Goal "k <= (n::nat) ==> m <= n + m - k";
nipkow@10214
    49
by (arith_tac 1);
nipkow@10214
    50
qed "le_add_diff";
nipkow@10214
    51
nipkow@10214
    52
(*Replaces the previous diff_less and le_diff_less, which had the stronger
nipkow@10214
    53
  second premise n<=m*)
nipkow@10214
    54
Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
nipkow@10214
    55
by (arith_tac 1);
nipkow@10214
    56
qed "diff_less";
nipkow@10214
    57
nipkow@10214
    58
nipkow@10214
    59
(** Simplification of relational expressions involving subtraction **)
nipkow@10214
    60
nipkow@10214
    61
Goal "[| k <= m;  k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)";
nipkow@10214
    62
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
nipkow@10214
    63
qed "diff_diff_eq";
nipkow@10214
    64
nipkow@10214
    65
Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
nipkow@10214
    66
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
nipkow@10214
    67
qed "eq_diff_iff";
nipkow@10214
    68
nipkow@10214
    69
Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k < n-k) = (m<n)";
nipkow@10214
    70
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
nipkow@10214
    71
qed "less_diff_iff";
nipkow@10214
    72
nipkow@10214
    73
Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)";
nipkow@10214
    74
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
nipkow@10214
    75
qed "le_diff_iff";
nipkow@10214
    76
nipkow@10214
    77
nipkow@10214
    78
(** (Anti)Monotonicity of subtraction -- by Stephan Merz **)
nipkow@10214
    79
nipkow@10214
    80
(* Monotonicity of subtraction in first argument *)
nipkow@10214
    81
Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
nipkow@10214
    82
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
nipkow@10214
    83
qed "diff_le_mono";
nipkow@10214
    84
nipkow@10214
    85
Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
nipkow@10214
    86
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
nipkow@10214
    87
qed "diff_le_mono2";
nipkow@10214
    88
nipkow@10214
    89
Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
nipkow@10214
    90
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
nipkow@10214
    91
qed "diff_less_mono2";
nipkow@10214
    92
nipkow@10214
    93
Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n";
nipkow@10214
    94
by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
nipkow@10214
    95
qed "diffs0_imp_equal";
nipkow@10214
    96
nipkow@10214
    97
(** Lemmas for ex/Factorization **)
nipkow@10214
    98
wenzelm@11701
    99
Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n";
nipkow@10214
   100
by (case_tac "m" 1);
nipkow@10214
   101
by Auto_tac;
nipkow@10214
   102
qed "one_less_mult"; 
nipkow@10214
   103
wenzelm@11701
   104
Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> n<m*n";
nipkow@10214
   105
by (case_tac "m" 1);
nipkow@10214
   106
by Auto_tac;
nipkow@10214
   107
qed "n_less_m_mult_n"; 
nipkow@10214
   108
wenzelm@11701
   109
Goal "!!m::nat. [| Suc 0 < n; Suc 0 < m |] ==> n<n*m";
nipkow@10214
   110
by (case_tac "m" 1);
nipkow@10214
   111
by Auto_tac;
nipkow@10214
   112
qed "n_less_n_mult_m"; 
nipkow@10214
   113
nipkow@10214
   114
nipkow@10214
   115
(** Rewriting to pull differences out **)
nipkow@10214
   116
nipkow@10214
   117
Goal "k<=j --> i - (j - k) = i + (k::nat) - j";
nipkow@10214
   118
by (arith_tac 1);
nipkow@10214
   119
qed "diff_diff_right";
nipkow@10214
   120
nipkow@10214
   121
Goal "k <= j ==> m - Suc (j - k) = m + k - Suc j";
nipkow@10214
   122
by (arith_tac 1);
nipkow@10214
   123
qed "diff_Suc_diff_eq1"; 
nipkow@10214
   124
nipkow@10214
   125
Goal "k <= j ==> Suc (j - k) - m = Suc j - (k + m)";
nipkow@10214
   126
by (arith_tac 1);
nipkow@10214
   127
qed "diff_Suc_diff_eq2"; 
nipkow@10214
   128
nipkow@10214
   129
(*The others are
nipkow@10214
   130
      i - j - k = i - (j + k),
nipkow@10214
   131
      k <= j ==> j - k + i = j + i - k,
nipkow@10214
   132
      k <= j ==> i + (j - k) = i + j - k *)
nipkow@10214
   133
Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym, 
nipkow@10214
   134
	  diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2];
nipkow@10214
   135
paulson@11367
   136
paulson@11367
   137
paulson@11367
   138
(*No analogue of not_less_Least or Least_Suc yet, since it isn't used much*)
paulson@11367
   139