|
1459
|
1 |
(* Title: CCL/mono
|
|
0
|
2 |
ID: $Id$
|
|
|
3 |
|
|
|
4 |
Modified version of
|
|
1459
|
5 |
Title: HOL/mono
|
|
|
6 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
0
|
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);
|
|
757
|
16 |
qed "Union_mono";
|
|
0
|
17 |
|
|
|
18 |
val prems = goal Set.thy "[| B<=A |] ==> Inter(A) <= Inter(B)";
|
|
|
19 |
by (cfast_tac prems 1);
|
|
757
|
20 |
qed "Inter_anti_mono";
|
|
0
|
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));
|
|
757
|
27 |
qed "UN_mono";
|
|
0
|
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));
|
|
757
|
34 |
qed "INT_anti_mono";
|
|
0
|
35 |
|
|
|
36 |
val prems = goal Set.thy "[| A<=C; B<=D |] ==> A Un B <= C Un D";
|
|
|
37 |
by (cfast_tac prems 1);
|
|
757
|
38 |
qed "Un_mono";
|
|
0
|
39 |
|
|
|
40 |
val prems = goal Set.thy "[| A<=C; B<=D |] ==> A Int B <= C Int D";
|
|
|
41 |
by (cfast_tac prems 1);
|
|
757
|
42 |
qed "Int_mono";
|
|
0
|
43 |
|
|
|
44 |
val prems = goal Set.thy "[| A<=B |] ==> Compl(B) <= Compl(A)";
|
|
|
45 |
by (cfast_tac prems 1);
|
|
757
|
46 |
qed "Compl_anti_mono";
|