author | wenzelm |
Mon, 22 Jun 1998 17:26:46 +0200 | |
changeset 5069 | 3ea049f7979d |
parent 4686 | 74a12e86b20b |
child 5188 | 633ec5f6c155 |
permissions | -rw-r--r-- |
2441 | 1 |
(* Title: HOL/Nat.ML |
923 | 2 |
ID: $Id$ |
2608 | 3 |
Author: Tobias Nipkow |
4 |
Copyright 1997 TU Muenchen |
|
923 | 5 |
*) |
6 |
||
5069 | 7 |
Goal "min 0 n = 0"; |
3023 | 8 |
by (rtac min_leastL 1); |
9 |
by (trans_tac 1); |
|
2608 | 10 |
qed "min_0L"; |
1301 | 11 |
|
5069 | 12 |
Goal "min n 0 = 0"; |
3023 | 13 |
by (rtac min_leastR 1); |
14 |
by (trans_tac 1); |
|
2608 | 15 |
qed "min_0R"; |
923 | 16 |
|
5069 | 17 |
Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)"; |
3023 | 18 |
by (Simp_tac 1); |
2608 | 19 |
qed "min_Suc_Suc"; |
1660 | 20 |
|
2608 | 21 |
Addsimps [min_0L,min_0R,min_Suc_Suc]; |