src/HOL/Nat.ML
author nipkow
Wed Feb 12 18:53:59 1997 +0100 (1997-02-12)
changeset 2608 450c9b682a92
parent 2441 decc46a5cdb5
child 3023 01364e2f30ad
permissions -rw-r--r--
New class "order" and accompanying changes.
In particular reflexivity of <= is now one rewrite rule.
oheimb@2441
     1
(*  Title:      HOL/Nat.ML
clasohm@923
     2
    ID:         $Id$
nipkow@2608
     3
    Author:     Tobias Nipkow
nipkow@2608
     4
    Copyright   1997 TU Muenchen
clasohm@923
     5
*)
clasohm@923
     6
nipkow@2608
     7
goal thy "min 0 n = 0";
nipkow@2608
     8
br min_leastL 1;
nipkow@2608
     9
by(trans_tac 1);
nipkow@2608
    10
qed "min_0L";
nipkow@1301
    11
nipkow@2608
    12
goal thy "min n 0 = 0";
nipkow@2608
    13
br min_leastR 1;
nipkow@2608
    14
by(trans_tac 1);
nipkow@2608
    15
qed "min_0R";
clasohm@923
    16
nipkow@2608
    17
goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
nipkow@2608
    18
by(split_tac [expand_if] 1);
nipkow@2608
    19
by(Simp_tac 1);
nipkow@2608
    20
qed "min_Suc_Suc";
oheimb@1660
    21
nipkow@2608
    22
Addsimps [min_0L,min_0R,min_Suc_Suc];