|
1 (* Title: CCL/mono |
|
2 ID: $Id$ |
|
3 |
|
4 Modified version of |
|
5 Title: HOL/mono |
|
6 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
7 Copyright 1991 University of Cambridge |
|
8 |
|
9 Monotonicity of various operations |
|
10 *) |
|
11 |
|
12 writeln"File HOL/mono"; |
|
13 |
|
14 val prems = goal Set.thy "A<=B ==> Union(A) <= Union(B)"; |
|
15 by (cfast_tac prems 1); |
|
16 val Union_mono = result(); |
|
17 |
|
18 val prems = goal Set.thy "[| B<=A |] ==> Inter(A) <= Inter(B)"; |
|
19 by (cfast_tac prems 1); |
|
20 val Inter_anti_mono = result(); |
|
21 |
|
22 val prems = goal Set.thy |
|
23 "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \ |
|
24 \ (UN x:A. f(x)) <= (UN x:B. g(x))"; |
|
25 by (REPEAT (eresolve_tac [UN_E,ssubst] 1 |
|
26 ORELSE ares_tac ((prems RL [subsetD]) @ [subsetI,UN_I]) 1)); |
|
27 val UN_mono = result(); |
|
28 |
|
29 val prems = goal Set.thy |
|
30 "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \ |
|
31 \ (INT x:A. f(x)) <= (INT x:A. g(x))"; |
|
32 by (REPEAT (ares_tac ((prems RL [subsetD]) @ [subsetI,INT_I]) 1 |
|
33 ORELSE etac INT_D 1)); |
|
34 val INT_anti_mono = result(); |
|
35 |
|
36 val prems = goal Set.thy "[| A<=C; B<=D |] ==> A Un B <= C Un D"; |
|
37 by (cfast_tac prems 1); |
|
38 val Un_mono = result(); |
|
39 |
|
40 val prems = goal Set.thy "[| A<=C; B<=D |] ==> A Int B <= C Int D"; |
|
41 by (cfast_tac prems 1); |
|
42 val Int_mono = result(); |
|
43 |
|
44 val prems = goal Set.thy "[| A<=B |] ==> Compl(B) <= Compl(A)"; |
|
45 by (cfast_tac prems 1); |
|
46 val Compl_anti_mono = result(); |