src/HOL/Ord.ML
author nipkow
Wed, 12 Feb 1997 18:53:59 +0100
changeset 2608 450c9b682a92
parent 1465 5d7a7e439cec
child 2935 998cb95fdd43
permissions -rw-r--r--
New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 923
diff changeset
     1
(*  Title:      HOL/Ord.ML
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 923
diff changeset
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
The type class for ordered types
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
     9
(** mono **)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
val [prem] = goalw Ord.thy [mono_def]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
    "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
by (REPEAT (ares_tac [allI, impI, prem] 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
qed "monoI";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
val [major,minor] = goalw Ord.thy [mono_def]
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
    "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
by (rtac (major RS spec RS spec RS mp) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
by (rtac minor 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
qed "monoD";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    22
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    23
section "Orders";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    24
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    25
AddIffs [order_refl];
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    26
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    27
goal Ord.thy "~ x < (x::'a::order)";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    28
by(simp_tac (!simpset addsimps [order_less_le]) 1);
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    29
qed "order_less_irrefl";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    30
AddIffs [order_less_irrefl];
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    31
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    32
goal thy "(x::'a::order) <= y = (x < y | x = y)";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    33
by(simp_tac (!simpset addsimps [order_less_le]) 1);
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    34
by(Fast_tac 1);
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    35
qed "order_le_less";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    36
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    37
(** min **)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    38
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    39
goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    40
by(split_tac [expand_if] 1);
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    41
by(Asm_simp_tac 1);
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    42
qed "min_leastL";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    43
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    44
val prems = goalw thy [min_def]
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    45
 "(!!x::'a::order. least <= x) ==> min x least = least";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    46
by(cut_facts_tac prems 1);
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    47
by(split_tac [expand_if] 1);
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    48
by(Asm_simp_tac 1);
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    49
by(fast_tac (!claset addEs [order_antisym]) 1);
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    50
qed "min_leastR";