src/HOL/Ord.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2608 450c9b682a92
child 2935 998cb95fdd43
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/Ord.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 The type class for ordered types
     7 *)
     8 
     9 (** mono **)
    10 
    11 val [prem] = goalw Ord.thy [mono_def]
    12     "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
    13 by (REPEAT (ares_tac [allI, impI, prem] 1));
    14 qed "monoI";
    15 
    16 val [major,minor] = goalw Ord.thy [mono_def]
    17     "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
    18 by (rtac (major RS spec RS spec RS mp) 1);
    19 by (rtac minor 1);
    20 qed "monoD";
    21 
    22 
    23 section "Orders";
    24 
    25 AddIffs [order_refl];
    26 
    27 goal Ord.thy "~ x < (x::'a::order)";
    28 by(simp_tac (!simpset addsimps [order_less_le]) 1);
    29 qed "order_less_irrefl";
    30 AddIffs [order_less_irrefl];
    31 
    32 goal thy "(x::'a::order) <= y = (x < y | x = y)";
    33 by(simp_tac (!simpset addsimps [order_less_le]) 1);
    34 by(Fast_tac 1);
    35 qed "order_le_less";
    36 
    37 (** min **)
    38 
    39 goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
    40 by(split_tac [expand_if] 1);
    41 by(Asm_simp_tac 1);
    42 qed "min_leastL";
    43 
    44 val prems = goalw thy [min_def]
    45  "(!!x::'a::order. least <= x) ==> min x least = least";
    46 by(cut_facts_tac prems 1);
    47 by(split_tac [expand_if] 1);
    48 by(Asm_simp_tac 1);
    49 by(fast_tac (!claset addEs [order_antisym]) 1);
    50 qed "min_leastR";