2441
|
1 |
(* Title: HOL/Nat.ML
|
923
|
2 |
ID: $Id$
|
2608
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1997 TU Muenchen
|
923
|
5 |
*)
|
|
6 |
|
2608
|
7 |
goal thy "min 0 n = 0";
|
3023
|
8 |
by (rtac min_leastL 1);
|
|
9 |
by (trans_tac 1);
|
2608
|
10 |
qed "min_0L";
|
1301
|
11 |
|
2608
|
12 |
goal thy "min n 0 = 0";
|
3023
|
13 |
by (rtac min_leastR 1);
|
|
14 |
by (trans_tac 1);
|
2608
|
15 |
qed "min_0R";
|
923
|
16 |
|
2608
|
17 |
goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
|
3023
|
18 |
by (split_tac [expand_if] 1);
|
|
19 |
by (Simp_tac 1);
|
2608
|
20 |
qed "min_Suc_Suc";
|
1660
|
21 |
|
2608
|
22 |
Addsimps [min_0L,min_0R,min_Suc_Suc];
|