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