|
1465
|
1 |
(* Title: HOL/Ord.ML
|
|
923
|
2 |
ID: $Id$
|
|
1465
|
3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory
|
|
923
|
4 |
Copyright 1993 University of Cambridge
|
|
|
5 |
|
|
|
6 |
The type class for ordered types
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
open Ord;
|
|
|
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 |
|