4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Monotonicity of various operations |
6 Monotonicity of various operations |
7 *) |
7 *) |
8 |
8 |
9 goal Set.thy "!!A B. A<=B ==> f``A <= f``B"; |
9 Goal "A<=B ==> f``A <= f``B"; |
10 by (Blast_tac 1); |
10 by (Blast_tac 1); |
11 qed "image_mono"; |
11 qed "image_mono"; |
12 |
12 |
13 goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)"; |
13 Goal "A<=B ==> Pow(A) <= Pow(B)"; |
14 by (Blast_tac 1); |
14 by (Blast_tac 1); |
15 qed "Pow_mono"; |
15 qed "Pow_mono"; |
16 |
16 |
17 goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)"; |
17 Goal "A<=B ==> Union(A) <= Union(B)"; |
18 by (Blast_tac 1); |
18 by (Blast_tac 1); |
19 qed "Union_mono"; |
19 qed "Union_mono"; |
20 |
20 |
21 goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)"; |
21 Goal "B<=A ==> Inter(A) <= Inter(B)"; |
22 by (Blast_tac 1); |
22 by (Blast_tac 1); |
23 qed "Inter_anti_mono"; |
23 qed "Inter_anti_mono"; |
24 |
24 |
25 val prems = goal Set.thy |
25 val prems = Goal |
26 "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \ |
26 "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \ |
27 \ (UN x:A. f(x)) <= (UN x:B. g(x))"; |
27 \ (UN x:A. f(x)) <= (UN x:B. g(x))"; |
28 by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
28 by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
29 qed "UN_mono"; |
29 qed "UN_mono"; |
30 |
30 |
31 (*The last inclusion is POSITIVE! *) |
31 (*The last inclusion is POSITIVE! *) |
32 val prems = goal Set.thy |
32 val prems = Goal |
33 "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \ |
33 "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \ |
34 \ (INT x:A. f(x)) <= (INT x:A. g(x))"; |
34 \ (INT x:A. f(x)) <= (INT x:A. g(x))"; |
35 by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
35 by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
36 qed "INT_anti_mono"; |
36 qed "INT_anti_mono"; |
37 |
37 |
38 goal Set.thy "!!C D. C<=D ==> insert a C <= insert a D"; |
38 Goal "C<=D ==> insert a C <= insert a D"; |
39 by (Blast_tac 1); |
39 by (Blast_tac 1); |
40 qed "insert_mono"; |
40 qed "insert_mono"; |
41 |
41 |
42 goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Un B <= C Un D"; |
42 Goal "[| A<=C; B<=D |] ==> A Un B <= C Un D"; |
43 by (Blast_tac 1); |
43 by (Blast_tac 1); |
44 qed "Un_mono"; |
44 qed "Un_mono"; |
45 |
45 |
46 goal Set.thy "!!A B. [| A<=C; B<=D |] ==> A Int B <= C Int D"; |
46 Goal "[| A<=C; B<=D |] ==> A Int B <= C Int D"; |
47 by (Blast_tac 1); |
47 by (Blast_tac 1); |
48 qed "Int_mono"; |
48 qed "Int_mono"; |
49 |
49 |
50 goal Set.thy "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D"; |
50 Goal "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D"; |
51 by (Blast_tac 1); |
51 by (Blast_tac 1); |
52 qed "Diff_mono"; |
52 qed "Diff_mono"; |
53 |
53 |
54 goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)"; |
54 Goal "A<=B ==> Compl(B) <= Compl(A)"; |
55 by (Blast_tac 1); |
55 by (Blast_tac 1); |
56 qed "Compl_anti_mono"; |
56 qed "Compl_anti_mono"; |
57 |
57 |
58 (** Monotonicity of implications. For inductive definitions **) |
58 (** Monotonicity of implications. For inductive definitions **) |
59 |
59 |
60 goal Set.thy "!!A B x. A<=B ==> x:A --> x:B"; |
60 Goal "A<=B ==> x:A --> x:B"; |
61 by (rtac impI 1); |
61 by (rtac impI 1); |
62 by (etac subsetD 1); |
62 by (etac subsetD 1); |
63 by (assume_tac 1); |
63 by (assume_tac 1); |
64 qed "in_mono"; |
64 qed "in_mono"; |
65 |
65 |
66 goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"; |
66 Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"; |
67 by (Blast_tac 1); |
67 by (Blast_tac 1); |
68 qed "conj_mono"; |
68 qed "conj_mono"; |
69 |
69 |
70 goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"; |
70 Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"; |
71 by (Blast_tac 1); |
71 by (Blast_tac 1); |
72 qed "disj_mono"; |
72 qed "disj_mono"; |
73 |
73 |
74 goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"; |
74 Goal "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"; |
75 by (Blast_tac 1); |
75 by (Blast_tac 1); |
76 qed "imp_mono"; |
76 qed "imp_mono"; |
77 |
77 |
78 goal HOL.thy "P-->P"; |
78 Goal "P-->P"; |
79 by (rtac impI 1); |
79 by (rtac impI 1); |
80 by (assume_tac 1); |
80 by (assume_tac 1); |
81 qed "imp_refl"; |
81 qed "imp_refl"; |
82 |
82 |
83 val [PQimp] = goal HOL.thy |
83 val [PQimp] = Goal |
84 "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))"; |
84 "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))"; |
85 by (blast_tac (claset() addIs [PQimp RS mp]) 1); |
85 by (blast_tac (claset() addIs [PQimp RS mp]) 1); |
86 qed "ex_mono"; |
86 qed "ex_mono"; |
87 |
87 |
88 val [PQimp] = goal HOL.thy |
88 val [PQimp] = Goal |
89 "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))"; |
89 "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))"; |
90 by (blast_tac (claset() addIs [PQimp RS mp]) 1); |
90 by (blast_tac (claset() addIs [PQimp RS mp]) 1); |
91 qed "all_mono"; |
91 qed "all_mono"; |
92 |
92 |
93 val [PQimp] = goal Set.thy |
93 val [PQimp] = Goal |
94 "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)"; |
94 "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)"; |
95 by (blast_tac (claset() addIs [PQimp RS mp]) 1); |
95 by (blast_tac (claset() addIs [PQimp RS mp]) 1); |
96 qed "Collect_mono"; |
96 qed "Collect_mono"; |
97 |
97 |
98 val [subs,PQimp] = goal Set.thy |
98 val [subs,PQimp] = Goal |
99 "[| A<=B; !!x. x:A ==> P(x) --> Q(x) \ |
99 "[| A<=B; !!x. x:A ==> P(x) --> Q(x) \ |
100 \ |] ==> A Int Collect(P) <= B Int Collect(Q)"; |
100 \ |] ==> A Int Collect(P) <= B Int Collect(Q)"; |
101 by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1); |
101 by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1); |
102 qed "Int_Collect_mono"; |
102 qed "Int_Collect_mono"; |
103 |
103 |