src/HOL/mono.ML
 author wenzelm Thu Mar 11 13:20:35 1999 +0100 (1999-03-11) changeset 6349 f7750d816c21 parent 5490 85855f65d0c6 child 7064 b053e0ab9f60 permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
1 (*  Title:      HOL/mono.ML
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   1991  University of Cambridge
6 Monotonicity of various operations
7 *)
9 Goal "A<=B ==> f``A <= f``B";
10 by (Blast_tac 1);
11 qed "image_mono";
13 Goal "A<=B ==> Pow(A) <= Pow(B)";
14 by (Blast_tac 1);
15 qed "Pow_mono";
17 Goal "A<=B ==> Union(A) <= Union(B)";
18 by (Blast_tac 1);
19 qed "Union_mono";
21 Goal "B<=A ==> Inter(A) <= Inter(B)";
22 by (Blast_tac 1);
23 qed "Inter_anti_mono";
25 val prems = Goal
26     "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==> \
27 \    (UN x:A. f(x)) <= (UN x:B. g(x))";
28 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
29 qed "UN_mono";
31 (*The last inclusion is POSITIVE! *)
32 val prems = Goal
33     "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==> \
34 \    (INT x:A. f(x)) <= (INT x:A. g(x))";
35 by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
36 qed "INT_anti_mono";
38 Goal "C<=D ==> insert a C <= insert a D";
39 by (Blast_tac 1);
40 qed "insert_mono";
42 Goal "[| A<=C;  B<=D |] ==> A Un B <= C Un D";
43 by (Blast_tac 1);
44 qed "Un_mono";
46 Goal "[| A<=C;  B<=D |] ==> A Int B <= C Int D";
47 by (Blast_tac 1);
48 qed "Int_mono";
50 Goal "!!A::'a set. [| A<=C;  D<=B |] ==> A-B <= C-D";
51 by (Blast_tac 1);
52 qed "Diff_mono";
54 Goal "!!A::'a set. A <= B ==> -B <= -A";
55 by (Blast_tac 1);
56 qed "Compl_anti_mono";
58 (** Monotonicity of implications.  For inductive definitions **)
60 Goal "A<=B ==> x:A --> x:B";
61 by (rtac impI 1);
62 by (etac subsetD 1);
63 by (assume_tac 1);
64 qed "in_mono";
66 Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
67 by (Blast_tac 1);
68 qed "conj_mono";
70 Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
71 by (Blast_tac 1);
72 qed "disj_mono";
74 Goal "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
75 by (Blast_tac 1);
76 qed "imp_mono";
78 Goal "P-->P";
79 by (rtac impI 1);
80 by (assume_tac 1);
81 qed "imp_refl";
83 val [PQimp] = Goal
84     "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))";
85 by (blast_tac (claset() addIs [PQimp RS mp]) 1);
86 qed "ex_mono";
88 val [PQimp] = Goal
89     "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))";
90 by (blast_tac (claset() addIs [PQimp RS mp]) 1);
91 qed "all_mono";
93 val [PQimp] = Goal
94     "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
95 by (blast_tac (claset() addIs [PQimp RS mp]) 1);
96 qed "Collect_mono";
98 val [subs,PQimp] = Goal
99     "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) \
100 \    |] ==> A Int Collect(P) <= B Int Collect(Q)";
101 by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1);
102 qed "Int_Collect_mono";
104 (*Used in individual datatype definitions*)
105 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono,
106                    ex_mono, Collect_mono, in_mono];