src/HOL/NatArith.ML
 author oheimb Wed Jan 31 10:15:55 2001 +0100 (2001-01-31) changeset 11008 f7333f055ef6 parent 10962 cda180b1e2e0 child 11367 7b2dbfb5cc3d permissions -rw-r--r--
improved theory reference in comment
```     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. [| 1<n; 1<m |] ==> 1<m*n";
```
```   100 by (case_tac "m" 1);
```
```   101 by Auto_tac;
```
```   102 qed "one_less_mult";
```
```   103
```
```   104 Goal "!!m::nat. [| 1<n; 1<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. [| 1<n; 1<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
```