src/HOL/Ord.ML
author nipkow
Sat Mar 07 16:29:29 1998 +0100 (1998-03-07)
changeset 4686 74a12e86b20b
parent 4640 ac6cf9f18653
child 5069 3ea049f7979d
permissions -rw-r--r--
Removed `addsplits [expand_if]'
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
paulson@4600
    27
(*This form is useful with the classical reasoner*)
paulson@4600
    28
goal Ord.thy "!!x::'a::order. x = y ==> x <= y";
paulson@4600
    29
by (etac ssubst 1);
paulson@4600
    30
by (rtac order_refl 1);
paulson@4600
    31
qed "order_eq_refl";
paulson@4600
    32
nipkow@2608
    33
goal Ord.thy "~ x < (x::'a::order)";
wenzelm@4089
    34
by (simp_tac (simpset() addsimps [order_less_le]) 1);
nipkow@2608
    35
qed "order_less_irrefl";
nipkow@2608
    36
AddIffs [order_less_irrefl];
nipkow@2608
    37
nipkow@2608
    38
goal thy "(x::'a::order) <= y = (x < y | x = y)";
wenzelm@4089
    39
by (simp_tac (simpset() addsimps [order_less_le]) 1);
paulson@2935
    40
by (Blast_tac 1);
nipkow@2608
    41
qed "order_le_less";
nipkow@2608
    42
nipkow@2608
    43
(** min **)
nipkow@2608
    44
nipkow@2608
    45
goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
paulson@2935
    46
by (Asm_simp_tac 1);
nipkow@2608
    47
qed "min_leastL";
nipkow@2608
    48
nipkow@2608
    49
val prems = goalw thy [min_def]
nipkow@2608
    50
 "(!!x::'a::order. least <= x) ==> min x least = least";
paulson@2935
    51
by (cut_facts_tac prems 1);
paulson@2935
    52
by (Asm_simp_tac 1);
wenzelm@4089
    53
by (blast_tac (claset() addIs [order_antisym]) 1);
nipkow@2608
    54
qed "min_leastR";
nipkow@4640
    55
nipkow@4640
    56
nipkow@4640
    57
section "Linear/Total Orders";
nipkow@4640
    58
nipkow@4640
    59
goal thy "!!x::'a::linorder. x<y | x=y | y<x";
nipkow@4640
    60
by (simp_tac (simpset() addsimps [order_less_le]) 1);
nipkow@4640
    61
by(cut_facts_tac [linorder_linear] 1);
nipkow@4640
    62
by (Blast_tac 1);
nipkow@4640
    63
qed "linorder_less_linear";
nipkow@4640
    64
nipkow@4640
    65
goalw thy [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
nipkow@4686
    66
by (Simp_tac 1);
nipkow@4640
    67
by(cut_facts_tac [linorder_linear] 1);
nipkow@4640
    68
by (blast_tac (claset() addIs [order_trans]) 1);
nipkow@4640
    69
qed "le_max_iff_disj";
nipkow@4640
    70
nipkow@4640
    71
goalw thy [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
nipkow@4686
    72
by (Simp_tac 1);
nipkow@4640
    73
by(cut_facts_tac [linorder_linear] 1);
nipkow@4640
    74
by (blast_tac (claset() addIs [order_trans]) 1);
nipkow@4640
    75
qed "max_le_iff_conj";
nipkow@4640
    76
nipkow@4640
    77
goalw thy [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
nipkow@4686
    78
by (Simp_tac 1);
nipkow@4640
    79
by(cut_facts_tac [linorder_linear] 1);
nipkow@4640
    80
by (blast_tac (claset() addIs [order_trans]) 1);
nipkow@4640
    81
qed "le_min_iff_conj";
nipkow@4640
    82
nipkow@4640
    83
goalw thy [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
nipkow@4686
    84
by (Simp_tac 1);
nipkow@4640
    85
by(cut_facts_tac [linorder_linear] 1);
nipkow@4640
    86
by (blast_tac (claset() addIs [order_trans]) 1);
nipkow@4640
    87
qed "min_le_iff_disj";
nipkow@4640
    88
nipkow@4640
    89