src/CCL/mono.ML
 author paulson Mon Dec 07 18:26:25 1998 +0100 (1998-12-07) changeset 6019 0e55c2fb2ebb parent 1459 d12da312eff4 child 17456 bcf7544875b2 permissions -rw-r--r--
tidying
```     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 qed "Union_mono";
```
```    17
```
```    18 val prems = goal Set.thy "[| B<=A |] ==> Inter(A) <= Inter(B)";
```
```    19 by (cfast_tac prems 1);
```
```    20 qed "Inter_anti_mono";
```
```    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 qed "UN_mono";
```
```    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 qed "INT_anti_mono";
```
```    35
```
```    36 val prems = goal Set.thy "[| A<=C;  B<=D |] ==> A Un B <= C Un D";
```
```    37 by (cfast_tac prems 1);
```
```    38 qed "Un_mono";
```
```    39
```
```    40 val prems = goal Set.thy "[| A<=C;  B<=D |] ==> A Int B <= C Int D";
```
```    41 by (cfast_tac prems 1);
```
```    42 qed "Int_mono";
```
```    43
```
```    44 val prems = goal Set.thy "[| A<=B |] ==> Compl(B) <= Compl(A)";
```
```    45 by (cfast_tac prems 1);
```
```    46 qed "Compl_anti_mono";
```