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