src/CCL/mono.ML
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 1459 d12da312eff4
child 17456 bcf7544875b2
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     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";