author | wenzelm |
Sat, 15 Apr 2000 15:00:57 +0200 | |
changeset 8717 | 20c42415c07d |
parent 6053 | 8a1059aa01f0 |
child 9907 | 473a6604da94 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/mono |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 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*) |
|
5137 | 13 |
Goal "A<=B ==> Replace(A,P) <= Replace(B,P)"; |
4091 | 14 |
by (blast_tac (claset() addSEs [ReplaceE]) 1); |
760 | 15 |
qed "Replace_mono"; |
0 | 16 |
|
5137 | 17 |
Goal "A<=B ==> {f(x). x:A} <= {f(x). x:B}"; |
2925 | 18 |
by (Blast_tac 1); |
760 | 19 |
qed "RepFun_mono"; |
0 | 20 |
|
5137 | 21 |
Goal "A<=B ==> Pow(A) <= Pow(B)"; |
2925 | 22 |
by (Blast_tac 1); |
760 | 23 |
qed "Pow_mono"; |
0 | 24 |
|
5137 | 25 |
Goal "A<=B ==> Union(A) <= Union(B)"; |
2925 | 26 |
by (Blast_tac 1); |
760 | 27 |
qed "Union_mono"; |
0 | 28 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5137
diff
changeset
|
29 |
val prems = Goal |
0 | 30 |
"[| A<=C; !!x. x:A ==> B(x)<=D(x) \ |
31 |
\ |] ==> (UN x:A. B(x)) <= (UN x:C. D(x))"; |
|
4091 | 32 |
by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
760 | 33 |
qed "UN_mono"; |
0 | 34 |
|
35 |
(*Intersection is ANTI-monotonic. There are TWO premises! *) |
|
5137 | 36 |
Goal "[| A<=B; a:A |] ==> Inter(B) <= Inter(A)"; |
2925 | 37 |
by (Blast_tac 1); |
760 | 38 |
qed "Inter_anti_mono"; |
0 | 39 |
|
5137 | 40 |
Goal "C<=D ==> cons(a,C) <= cons(a,D)"; |
2925 | 41 |
by (Blast_tac 1); |
760 | 42 |
qed "cons_mono"; |
0 | 43 |
|
5137 | 44 |
Goal "[| A<=C; B<=D |] ==> A Un B <= C Un D"; |
2925 | 45 |
by (Blast_tac 1); |
760 | 46 |
qed "Un_mono"; |
0 | 47 |
|
5137 | 48 |
Goal "[| A<=C; B<=D |] ==> A Int B <= C Int D"; |
2925 | 49 |
by (Blast_tac 1); |
760 | 50 |
qed "Int_mono"; |
0 | 51 |
|
5137 | 52 |
Goal "[| A<=C; D<=B |] ==> A-B <= C-D"; |
2925 | 53 |
by (Blast_tac 1); |
760 | 54 |
qed "Diff_mono"; |
0 | 55 |
|
56 |
(** Standard products, sums and function spaces **) |
|
57 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5137
diff
changeset
|
58 |
Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> Sigma(A,B) <= Sigma(C,D)"; |
2925 | 59 |
by (Blast_tac 1); |
760 | 60 |
qed "Sigma_mono_lemma"; |
0 | 61 |
val Sigma_mono = ballI RSN (2,Sigma_mono_lemma); |
62 |
||
5137 | 63 |
Goalw sum_defs "[| A<=C; B<=D |] ==> A+B <= C+D"; |
0 | 64 |
by (REPEAT (ares_tac [subset_refl,Un_mono,Sigma_mono] 1)); |
760 | 65 |
qed "sum_mono"; |
0 | 66 |
|
67 |
(*Note that B->A and C->A are typically disjoint!*) |
|
5137 | 68 |
Goal "B<=C ==> A->B <= A->C"; |
4091 | 69 |
by (blast_tac (claset() addIs [lam_type] addEs [Pi_lamE]) 1); |
760 | 70 |
qed "Pi_mono"; |
0 | 71 |
|
5137 | 72 |
Goalw [lam_def] "A<=B ==> Lambda(A,c) <= Lambda(B,c)"; |
0 | 73 |
by (etac RepFun_mono 1); |
760 | 74 |
qed "lam_mono"; |
0 | 75 |
|
76 |
(** Quine-inspired ordered pairs, products, injections and sums **) |
|
77 |
||
5137 | 78 |
Goalw [QPair_def] "[| a<=c; b<=d |] ==> <a;b> <= <c;d>"; |
0 | 79 |
by (REPEAT (ares_tac [sum_mono] 1)); |
760 | 80 |
qed "QPair_mono"; |
0 | 81 |
|
5137 | 82 |
Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> \ |
0 | 83 |
\ QSigma(A,B) <= QSigma(C,D)"; |
2925 | 84 |
by (Blast_tac 1); |
760 | 85 |
qed "QSigma_mono_lemma"; |
0 | 86 |
val QSigma_mono = ballI RSN (2,QSigma_mono_lemma); |
87 |
||
5137 | 88 |
Goalw [QInl_def] "a<=b ==> QInl(a) <= QInl(b)"; |
0 | 89 |
by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1)); |
760 | 90 |
qed "QInl_mono"; |
0 | 91 |
|
5137 | 92 |
Goalw [QInr_def] "a<=b ==> QInr(a) <= QInr(b)"; |
0 | 93 |
by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1)); |
760 | 94 |
qed "QInr_mono"; |
0 | 95 |
|
5137 | 96 |
Goal "[| A<=C; B<=D |] ==> A <+> B <= C <+> D"; |
2925 | 97 |
by (Blast_tac 1); |
760 | 98 |
qed "qsum_mono"; |
0 | 99 |
|
100 |
||
101 |
(** Converse, domain, range, field **) |
|
102 |
||
5137 | 103 |
Goal "r<=s ==> converse(r) <= converse(s)"; |
2925 | 104 |
by (Blast_tac 1); |
760 | 105 |
qed "converse_mono"; |
0 | 106 |
|
5137 | 107 |
Goal "r<=s ==> domain(r)<=domain(s)"; |
2925 | 108 |
by (Blast_tac 1); |
760 | 109 |
qed "domain_mono"; |
0 | 110 |
|
811
9bac814082e4
Used bind_thm to store domain_rel_subset and range_rel_subset
lcp
parents:
760
diff
changeset
|
111 |
bind_thm ("domain_rel_subset", [domain_mono, domain_subset] MRS subset_trans); |
0 | 112 |
|
5137 | 113 |
Goal "r<=s ==> range(r)<=range(s)"; |
2925 | 114 |
by (Blast_tac 1); |
760 | 115 |
qed "range_mono"; |
0 | 116 |
|
811
9bac814082e4
Used bind_thm to store domain_rel_subset and range_rel_subset
lcp
parents:
760
diff
changeset
|
117 |
bind_thm ("range_rel_subset", [range_mono, range_subset] MRS subset_trans); |
0 | 118 |
|
5137 | 119 |
Goal "r<=s ==> field(r)<=field(s)"; |
2925 | 120 |
by (Blast_tac 1); |
760 | 121 |
qed "field_mono"; |
0 | 122 |
|
5137 | 123 |
Goal "r <= A*A ==> field(r) <= A"; |
0 | 124 |
by (etac (field_mono RS subset_trans) 1); |
2925 | 125 |
by (Blast_tac 1); |
760 | 126 |
qed "field_rel_subset"; |
0 | 127 |
|
128 |
||
129 |
(** Images **) |
|
130 |
||
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5137
diff
changeset
|
131 |
val [prem1,prem2] = Goal |
0 | 132 |
"[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r``A <= s``B"; |
4091 | 133 |
by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1); |
760 | 134 |
qed "image_pair_mono"; |
0 | 135 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5137
diff
changeset
|
136 |
val [prem1,prem2] = Goal |
0 | 137 |
"[| !! x y. <x,y>:r ==> <x,y>:s; A<=B |] ==> r-``A <= s-``B"; |
4091 | 138 |
by (blast_tac (claset() addIs [prem1, prem2 RS subsetD]) 1); |
760 | 139 |
qed "vimage_pair_mono"; |
0 | 140 |
|
5137 | 141 |
Goal "[| r<=s; A<=B |] ==> r``A <= s``B"; |
2925 | 142 |
by (Blast_tac 1); |
760 | 143 |
qed "image_mono"; |
0 | 144 |
|
5137 | 145 |
Goal "[| r<=s; A<=B |] ==> r-``A <= s-``B"; |
2925 | 146 |
by (Blast_tac 1); |
760 | 147 |
qed "vimage_mono"; |
0 | 148 |
|
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5137
diff
changeset
|
149 |
val [sub,PQimp] = Goal |
0 | 150 |
"[| A<=B; !!x. x:A ==> P(x) --> Q(x) |] ==> Collect(A,P) <= Collect(B,Q)"; |
4091 | 151 |
by (blast_tac (claset() addIs [sub RS subsetD, PQimp RS mp]) 1); |
760 | 152 |
qed "Collect_mono"; |
0 | 153 |
|
154 |
(** Monotonicity of implications -- some could go to FOL **) |
|
155 |
||
5137 | 156 |
Goal "A<=B ==> x:A --> x:B"; |
2925 | 157 |
by (Blast_tac 1); |
760 | 158 |
qed "in_mono"; |
0 | 159 |
|
160 |
goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"; |
|
2602
5ac837d98a85
Renamed structure Int (intuitionistic prover) to IntPr
paulson
parents:
2469
diff
changeset
|
161 |
by (IntPr.fast_tac 1); |
760 | 162 |
qed "conj_mono"; |
0 | 163 |
|
164 |
goal IFOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"; |
|
2602
5ac837d98a85
Renamed structure Int (intuitionistic prover) to IntPr
paulson
parents:
2469
diff
changeset
|
165 |
by (IntPr.fast_tac 1); |
760 | 166 |
qed "disj_mono"; |
0 | 167 |
|
168 |
goal IFOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"; |
|
2602
5ac837d98a85
Renamed structure Int (intuitionistic prover) to IntPr
paulson
parents:
2469
diff
changeset
|
169 |
by (IntPr.fast_tac 1); |
760 | 170 |
qed "imp_mono"; |
0 | 171 |
|
172 |
goal IFOL.thy "P-->P"; |
|
173 |
by (rtac impI 1); |
|
174 |
by (assume_tac 1); |
|
760 | 175 |
qed "imp_refl"; |
0 | 176 |
|
177 |
val [PQimp] = goal IFOL.thy |
|
3840 | 178 |
"[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))"; |
2803
734fc343ec2a
Conducted the IFOL proofs using intuitionistic tools
paulson
parents:
2602
diff
changeset
|
179 |
by IntPr.safe_tac; |
3015 | 180 |
by (etac (PQimp RS mp RS exI) 1); |
760 | 181 |
qed "ex_mono"; |
0 | 182 |
|
183 |
val [PQimp] = goal IFOL.thy |
|
3840 | 184 |
"[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))"; |
2803
734fc343ec2a
Conducted the IFOL proofs using intuitionistic tools
paulson
parents:
2602
diff
changeset
|
185 |
by IntPr.safe_tac; |
3015 | 186 |
by (etac (spec RS (PQimp RS mp)) 1); |
760 | 187 |
qed "all_mono"; |
516 | 188 |
|
189 |
(*Used in intr_elim.ML and in individual datatype definitions*) |
|
190 |
val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, |
|
1461 | 191 |
ex_mono, Collect_mono, Part_mono, in_mono]; |
516 | 192 |