|
1 (* Title: ZF/mono |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Monotonicity of various operations (for lattice properties see subset.ML) |
|
7 *) |
|
8 |
|
9 (** Replacement, in its various formulations **) |
|
10 |
|
11 (*Not easy to express monotonicity in P, since any "bigger" predicate |
|
12 would have to be single-valued*) |
|
13 goal ZF.thy "!!A B. A<=B ==> Replace(A,P) <= Replace(B,P)"; |
|
14 by (fast_tac ZF_cs 1); |
|
15 val Replace_mono = result(); |
|
16 |
|
17 goal ZF.thy "!!A B. A<=B ==> {f(x). x:A} <= {f(x). x:B}"; |
|
18 by (fast_tac ZF_cs 1); |
|
19 val RepFun_mono = result(); |
|
20 |
|
21 goal ZF.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)"; |
|
22 by (fast_tac ZF_cs 1); |
|
23 val Pow_mono = result(); |
|
24 |
|
25 goal ZF.thy "!!A B. A<=B ==> Union(A) <= Union(B)"; |
|
26 by (fast_tac ZF_cs 1); |
|
27 val Union_mono = result(); |
|
28 |
|
29 val prems = goal ZF.thy |
|
30 "[| A<=C; !!x. x:A ==> B(x)<=D(x) \ |
|
31 \ |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))"; |
|
32 by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1); |
|
33 val UN_mono = result(); |
|
34 |
|
35 (*Intersection is ANTI-monotonic. There are TWO premises! *) |
|
36 goal ZF.thy "!!A B. [| A<=B; a:A |] ==> Inter(B) <= Inter(A)"; |
|
37 by (fast_tac ZF_cs 1); |
|
38 val Inter_anti_mono = result(); |
|
39 |
|
40 goal ZF.thy "!!C D. C<=D ==> cons(a,C) <= cons(a,D)"; |
|
41 by (fast_tac ZF_cs 1); |
|
42 val cons_mono = result(); |
|
43 |
|
44 goal ZF.thy "!!A B C D. [| A<=C; B<=D |] ==> A Un B <= C Un D"; |
|
45 by (fast_tac ZF_cs 1); |
|
46 val Un_mono = result(); |
|
47 |
|
48 goal ZF.thy "!!A B C D. [| A<=C; B<=D |] ==> A Int B <= C Int D"; |
|
49 by (fast_tac ZF_cs 1); |
|
50 val Int_mono = result(); |
|
51 |
|
52 goal ZF.thy "!!A B C D. [| A<=C; D<=B |] ==> A-B <= C-D"; |
|
53 by (fast_tac ZF_cs 1); |
|
54 val Diff_mono = result(); |
|
55 |
|
56 (** Standard products, sums and function spaces **) |
|
57 |
|
58 goal ZF.thy "!!A B C D. [| A<=C; ALL x:A. B(x) <= D(x) |] ==> \ |
|
59 \ Sigma(A,B) <= Sigma(C,D)"; |
|
60 by (fast_tac ZF_cs 1); |
|
61 val Sigma_mono_lemma = result(); |
|
62 val Sigma_mono = ballI RSN (2,Sigma_mono_lemma); |
|
63 |
|
64 goalw Sum.thy sum_defs "!!A B C D. [| A<=C; B<=D |] ==> A+B <= C+D"; |
|
65 by (REPEAT (ares_tac [subset_refl,Un_mono,Sigma_mono] 1)); |
|
66 val sum_mono = result(); |
|
67 |
|
68 (*Note that B->A and C->A are typically disjoint!*) |
|
69 goal ZF.thy "!!A B C. B<=C ==> A->B <= A->C"; |
|
70 by (fast_tac (ZF_cs addIs [lam_type] addEs [Pi_lamE]) 1); |
|
71 val Pi_mono = result(); |
|
72 |
|
73 goalw ZF.thy [lam_def] "!!A B. A<=B ==> Lambda(A,c) <= Lambda(B,c)"; |
|
74 by (etac RepFun_mono 1); |
|
75 val lam_mono = result(); |
|
76 |
|
77 (** Quine-inspired ordered pairs, products, injections and sums **) |
|
78 |
|
79 goalw QPair.thy [QPair_def] "!!a b c d. [| a<=c; b<=d |] ==> <a;b> <= <c;d>"; |
|
80 by (REPEAT (ares_tac [sum_mono] 1)); |
|
81 val QPair_mono = result(); |
|
82 |
|
83 goal QPair.thy "!!A B C D. [| A<=C; ALL x:A. B(x) <= D(x) |] ==> \ |
|
84 \ QSigma(A,B) <= QSigma(C,D)"; |
|
85 by (fast_tac (ZF_cs addIs [QSigmaI] addSEs [QSigmaE]) 1); |
|
86 val QSigma_mono_lemma = result(); |
|
87 val QSigma_mono = ballI RSN (2,QSigma_mono_lemma); |
|
88 |
|
89 goalw QPair.thy [QInl_def] "!!a b. a<=b ==> QInl(a) <= QInl(b)"; |
|
90 by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1)); |
|
91 val QInl_mono = result(); |
|
92 |
|
93 goalw QPair.thy [QInr_def] "!!a b. a<=b ==> QInr(a) <= QInr(b)"; |
|
94 by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1)); |
|
95 val QInr_mono = result(); |
|
96 |
|
97 goal QPair.thy "!!A B C D. [| A<=C; B<=D |] ==> A <+> B <= C <+> D"; |
|
98 by (fast_tac qsum_cs 1); |
|
99 val qsum_mono = result(); |
|
100 |
|
101 |
|
102 (** Converse, domain, range, field **) |
|
103 |
|
104 goal ZF.thy "!!r s. r<=s ==> converse(r) <= converse(s)"; |
|
105 by (fast_tac ZF_cs 1); |
|
106 val converse_mono = result(); |
|
107 |
|
108 goal ZF.thy "!!r s. r<=s ==> domain(r)<=domain(s)"; |
|
109 by (fast_tac ZF_cs 1); |
|
110 val domain_mono = result(); |
|
111 |
|
112 val [prem] = goal ZF.thy "r <= Sigma(A,B) ==> domain(r) <= A"; |
|
113 by (rtac (domain_subset RS (prem RS domain_mono RS subset_trans)) 1); |
|
114 val domain_rel_subset = result(); |
|
115 |
|
116 goal ZF.thy "!!r s. r<=s ==> range(r)<=range(s)"; |
|
117 by (fast_tac ZF_cs 1); |
|
118 val range_mono = result(); |
|
119 |
|
120 val [prem] = goal ZF.thy "r <= A*B ==> range(r) <= B"; |
|
121 by (rtac (range_subset RS (prem RS range_mono RS subset_trans)) 1); |
|
122 val range_rel_subset = result(); |
|
123 |
|
124 goal ZF.thy "!!r s. r<=s ==> field(r)<=field(s)"; |
|
125 by (fast_tac ZF_cs 1); |
|
126 val field_mono = result(); |
|
127 |
|
128 goal ZF.thy "!!r A. r <= A*A ==> field(r) <= A"; |
|
129 by (etac (field_mono RS subset_trans) 1); |
|
130 by (fast_tac ZF_cs 1); |
|
131 val field_rel_subset = result(); |
|
132 |
|
133 |
|
134 (** Images **) |
|
135 |
|
136 val [prem1,prem2] = goal ZF.thy |
|
137 "[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r``A <= s``B"; |
|
138 by (fast_tac (ZF_cs addIs [prem1, prem2 RS subsetD]) 1); |
|
139 val image_pair_mono = result(); |
|
140 |
|
141 val [prem1,prem2] = goal ZF.thy |
|
142 "[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r-``A <= s-``B"; |
|
143 by (fast_tac (ZF_cs addIs [prem1, prem2 RS subsetD]) 1); |
|
144 val vimage_pair_mono = result(); |
|
145 |
|
146 goal ZF.thy "!!r s. [| r<=s; A<=B |] ==> r``A <= s``B"; |
|
147 by (fast_tac ZF_cs 1); |
|
148 val image_mono = result(); |
|
149 |
|
150 goal ZF.thy "!!r s. [| r<=s; A<=B |] ==> r-``A <= s-``B"; |
|
151 by (fast_tac ZF_cs 1); |
|
152 val vimage_mono = result(); |
|
153 |
|
154 val [sub,PQimp] = goal ZF.thy |
|
155 "[| A<=B; !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)"; |
|
156 by (fast_tac (ZF_cs addIs [sub RS subsetD, PQimp RS mp]) 1); |
|
157 val Collect_mono = result(); |
|
158 |
|
159 (** Monotonicity of implications -- some could go to FOL **) |
|
160 |
|
161 goal ZF.thy "!!A B x. A<=B ==> x:A --> x:B"; |
|
162 by (rtac impI 1); |
|
163 by (etac subsetD 1); |
|
164 by (assume_tac 1); |
|
165 val in_mono = result(); |
|
166 |
|
167 goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"; |
|
168 by (Int.fast_tac 1); |
|
169 val conj_mono = result(); |
|
170 |
|
171 goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"; |
|
172 by (Int.fast_tac 1); |
|
173 val disj_mono = result(); |
|
174 |
|
175 goal IFOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"; |
|
176 by (Int.fast_tac 1); |
|
177 val imp_mono = result(); |
|
178 |
|
179 goal IFOL.thy "P-->P"; |
|
180 by (rtac impI 1); |
|
181 by (assume_tac 1); |
|
182 val imp_refl = result(); |
|
183 |
|
184 val [PQimp] = goal IFOL.thy |
|
185 "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))"; |
|
186 by (fast_tac (FOL_cs addIs [PQimp RS mp]) 1); |
|
187 val ex_mono = result(); |
|
188 |
|
189 val [PQimp] = goal IFOL.thy |
|
190 "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))"; |
|
191 by (fast_tac (FOL_cs addIs [PQimp RS mp]) 1); |
|
192 val all_mono = result(); |