17456
|
1 |
(* Title: CCL/mono.ML
|
0
|
2 |
ID: $Id$
|
|
3 |
|
17456
|
4 |
Monotonicity of various operations.
|
0
|
5 |
*)
|
|
6 |
|
17456
|
7 |
val prems = goal (the_context ()) "A<=B ==> Union(A) <= Union(B)";
|
0
|
8 |
by (cfast_tac prems 1);
|
757
|
9 |
qed "Union_mono";
|
0
|
10 |
|
17456
|
11 |
val prems = goal (the_context ()) "[| B<=A |] ==> Inter(A) <= Inter(B)";
|
0
|
12 |
by (cfast_tac prems 1);
|
757
|
13 |
qed "Inter_anti_mono";
|
0
|
14 |
|
17456
|
15 |
val prems = goal (the_context ())
|
0
|
16 |
"[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \
|
|
17 |
\ (UN x:A. f(x)) <= (UN x:B. g(x))";
|
|
18 |
by (REPEAT (eresolve_tac [UN_E,ssubst] 1
|
|
19 |
ORELSE ares_tac ((prems RL [subsetD]) @ [subsetI,UN_I]) 1));
|
757
|
20 |
qed "UN_mono";
|
0
|
21 |
|
17456
|
22 |
val prems = goal (the_context ())
|
0
|
23 |
"[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \
|
|
24 |
\ (INT x:A. f(x)) <= (INT x:A. g(x))";
|
|
25 |
by (REPEAT (ares_tac ((prems RL [subsetD]) @ [subsetI,INT_I]) 1
|
|
26 |
ORELSE etac INT_D 1));
|
757
|
27 |
qed "INT_anti_mono";
|
0
|
28 |
|
17456
|
29 |
val prems = goal (the_context ()) "[| A<=C; B<=D |] ==> A Un B <= C Un D";
|
0
|
30 |
by (cfast_tac prems 1);
|
757
|
31 |
qed "Un_mono";
|
0
|
32 |
|
17456
|
33 |
val prems = goal (the_context ()) "[| A<=C; B<=D |] ==> A Int B <= C Int D";
|
0
|
34 |
by (cfast_tac prems 1);
|
757
|
35 |
qed "Int_mono";
|
0
|
36 |
|
17456
|
37 |
val prems = goal (the_context ()) "[| A<=B |] ==> Compl(B) <= Compl(A)";
|
0
|
38 |
by (cfast_tac prems 1);
|
757
|
39 |
qed "Compl_anti_mono";
|