author | paulson |
Fri, 14 Aug 1998 18:37:28 +0200 | |
changeset 5321 | f8848433d240 |
parent 5268 | 59ef39008514 |
child 5809 | bacf85370ce0 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/quniv |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
For quniv.thy. A small universe for lazy recursive types |
|
7 |
*) |
|
8 |
||
9 |
open QUniv; |
|
10 |
||
838
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
11 |
(** Properties involving Transset and Sum **) |
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
12 |
|
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
13 |
val [prem1,prem2] = goalw QUniv.thy [sum_def] |
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
14 |
"[| Transset(C); A+B <= C |] ==> A <= C & B <= C"; |
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
15 |
by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1); |
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
16 |
by (REPEAT (etac (prem1 RS Transset_includes_range) 1 |
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
17 |
ORELSE resolve_tac [conjI, singletonI] 1)); |
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
18 |
qed "Transset_includes_summands"; |
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
19 |
|
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
20 |
val [prem] = goalw QUniv.thy [sum_def] |
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
21 |
"Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)"; |
2033 | 22 |
by (stac Int_Un_distrib 1); |
4091 | 23 |
by (blast_tac (claset() addSDs [prem RS Transset_Pair_D]) 1); |
838
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
24 |
qed "Transset_sum_Int_subset"; |
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset
|
25 |
|
0 | 26 |
(** Introduction and elimination rules avoid tiresome folding/unfolding **) |
27 |
||
5067 | 28 |
Goalw [quniv_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
29 |
"X <= univ(eclose(A)) ==> X : quniv(A)"; |
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
30 |
by (etac PowI 1); |
760 | 31 |
qed "qunivI"; |
0 | 32 |
|
5067 | 33 |
Goalw [quniv_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
34 |
"X : quniv(A) ==> X <= univ(eclose(A))"; |
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
35 |
by (etac PowD 1); |
760 | 36 |
qed "qunivD"; |
0 | 37 |
|
5137 | 38 |
Goalw [quniv_def] "A<=B ==> quniv(A) <= quniv(B)"; |
0 | 39 |
by (etac (eclose_mono RS univ_mono RS Pow_mono) 1); |
760 | 40 |
qed "quniv_mono"; |
0 | 41 |
|
42 |
(*** Closure properties ***) |
|
43 |
||
5067 | 44 |
Goalw [quniv_def] "univ(eclose(A)) <= quniv(A)"; |
0 | 45 |
by (rtac (Transset_iff_Pow RS iffD1) 1); |
46 |
by (rtac (Transset_eclose RS Transset_univ) 1); |
|
760 | 47 |
qed "univ_eclose_subset_quniv"; |
0 | 48 |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
49 |
(*Key property for proving A_subset_quniv; requires eclose in def of quniv*) |
5067 | 50 |
Goal "univ(A) <= quniv(A)"; |
0 | 51 |
by (rtac (arg_subset_eclose RS univ_mono RS subset_trans) 1); |
52 |
by (rtac univ_eclose_subset_quniv 1); |
|
760 | 53 |
qed "univ_subset_quniv"; |
0 | 54 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
55 |
bind_thm ("univ_into_quniv", univ_subset_quniv RS subsetD); |
0 | 56 |
|
5067 | 57 |
Goalw [quniv_def] "Pow(univ(A)) <= quniv(A)"; |
0 | 58 |
by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1); |
760 | 59 |
qed "Pow_univ_subset_quniv"; |
0 | 60 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
61 |
bind_thm ("univ_subset_into_quniv", |
1461 | 62 |
PowI RS (Pow_univ_subset_quniv RS subsetD)); |
0 | 63 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
64 |
bind_thm ("zero_in_quniv", zero_in_univ RS univ_into_quniv); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
65 |
bind_thm ("one_in_quniv", one_in_univ RS univ_into_quniv); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
66 |
bind_thm ("two_in_quniv", two_in_univ RS univ_into_quniv); |
0 | 67 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
68 |
bind_thm ("A_subset_quniv", |
1461 | 69 |
[A_subset_univ, univ_subset_quniv] MRS subset_trans); |
0 | 70 |
|
71 |
val A_into_quniv = A_subset_quniv RS subsetD; |
|
72 |
||
73 |
(*** univ(A) closure for Quine-inspired pairs and injections ***) |
|
74 |
||
75 |
(*Quine ordered pairs*) |
|
5067 | 76 |
Goalw [QPair_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
77 |
"[| a <= univ(A); b <= univ(A) |] ==> <a;b> <= univ(A)"; |
0 | 78 |
by (REPEAT (ares_tac [sum_subset_univ] 1)); |
760 | 79 |
qed "QPair_subset_univ"; |
0 | 80 |
|
81 |
(** Quine disjoint sum **) |
|
82 |
||
5137 | 83 |
Goalw [QInl_def] "a <= univ(A) ==> QInl(a) <= univ(A)"; |
0 | 84 |
by (etac (empty_subsetI RS QPair_subset_univ) 1); |
760 | 85 |
qed "QInl_subset_univ"; |
0 | 86 |
|
87 |
val naturals_subset_nat = |
|
88 |
rewrite_rule [Transset_def] (Ord_nat RS Ord_is_Transset) |
|
89 |
RS bspec; |
|
90 |
||
91 |
val naturals_subset_univ = |
|
92 |
[naturals_subset_nat, nat_subset_univ] MRS subset_trans; |
|
93 |
||
5137 | 94 |
Goalw [QInr_def] "a <= univ(A) ==> QInr(a) <= univ(A)"; |
0 | 95 |
by (etac (nat_1I RS naturals_subset_univ RS QPair_subset_univ) 1); |
760 | 96 |
qed "QInr_subset_univ"; |
0 | 97 |
|
98 |
(*** Closure for Quine-inspired products and sums ***) |
|
99 |
||
100 |
(*Quine ordered pairs*) |
|
5067 | 101 |
Goalw [quniv_def,QPair_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
102 |
"[| a: quniv(A); b: quniv(A) |] ==> <a;b> : quniv(A)"; |
0 | 103 |
by (REPEAT (dtac PowD 1)); |
104 |
by (REPEAT (ares_tac [PowI, sum_subset_univ] 1)); |
|
760 | 105 |
qed "QPair_in_quniv"; |
0 | 106 |
|
5067 | 107 |
Goal "quniv(A) <*> quniv(A) <= quniv(A)"; |
0 | 108 |
by (REPEAT (ares_tac [subsetI, QPair_in_quniv] 1 |
109 |
ORELSE eresolve_tac [QSigmaE, ssubst] 1)); |
|
760 | 110 |
qed "QSigma_quniv"; |
0 | 111 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
112 |
bind_thm ("QSigma_subset_quniv", |
1461 | 113 |
[QSigma_mono, QSigma_quniv] MRS subset_trans); |
0 | 114 |
|
115 |
(*The opposite inclusion*) |
|
5067 | 116 |
Goalw [quniv_def,QPair_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
117 |
"<a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)"; |
129 | 118 |
by (etac ([Transset_eclose RS Transset_univ, PowD] MRS |
1461 | 119 |
Transset_includes_summands RS conjE) 1); |
0 | 120 |
by (REPEAT (ares_tac [conjI,PowI] 1)); |
760 | 121 |
qed "quniv_QPair_D"; |
0 | 122 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
123 |
bind_thm ("quniv_QPair_E", quniv_QPair_D RS conjE); |
0 | 124 |
|
5067 | 125 |
Goal "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)"; |
0 | 126 |
by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1 |
127 |
ORELSE etac conjE 1)); |
|
760 | 128 |
qed "quniv_QPair_iff"; |
0 | 129 |
|
130 |
||
131 |
(** Quine disjoint sum **) |
|
132 |
||
5137 | 133 |
Goalw [QInl_def] "a: quniv(A) ==> QInl(a) : quniv(A)"; |
0 | 134 |
by (REPEAT (ares_tac [zero_in_quniv,QPair_in_quniv] 1)); |
760 | 135 |
qed "QInl_in_quniv"; |
0 | 136 |
|
5137 | 137 |
Goalw [QInr_def] "b: quniv(A) ==> QInr(b) : quniv(A)"; |
0 | 138 |
by (REPEAT (ares_tac [one_in_quniv, QPair_in_quniv] 1)); |
760 | 139 |
qed "QInr_in_quniv"; |
0 | 140 |
|
5067 | 141 |
Goal "quniv(C) <+> quniv(C) <= quniv(C)"; |
0 | 142 |
by (REPEAT (ares_tac [subsetI, QInl_in_quniv, QInr_in_quniv] 1 |
143 |
ORELSE eresolve_tac [qsumE, ssubst] 1)); |
|
760 | 144 |
qed "qsum_quniv"; |
0 | 145 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
146 |
bind_thm ("qsum_subset_quniv", [qsum_mono, qsum_quniv] MRS subset_trans); |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
147 |
|
0 | 148 |
|
149 |
(*** The natural numbers ***) |
|
150 |
||
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
151 |
bind_thm ("nat_subset_quniv", |
1461 | 152 |
[nat_subset_univ, univ_subset_quniv] MRS subset_trans); |
0 | 153 |
|
154 |
(* n:nat ==> n:quniv(A) *) |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
155 |
bind_thm ("nat_into_quniv", (nat_subset_quniv RS subsetD)); |
0 | 156 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
157 |
bind_thm ("bool_subset_quniv", |
1461 | 158 |
[bool_subset_univ, univ_subset_quniv] MRS subset_trans); |
0 | 159 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
160 |
bind_thm ("bool_into_quniv", bool_subset_quniv RS subsetD); |
0 | 161 |
|
162 |
||
163 |
(*** Intersecting <a;b> with Vfrom... ***) |
|
164 |
||
5067 | 165 |
Goalw [QPair_def,sum_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
166 |
"Transset(X) ==> \ |
0 | 167 |
\ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; |
2033 | 168 |
by (stac Int_Un_distrib 1); |
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
169 |
by (rtac Un_mono 1); |
0 | 170 |
by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans, |
1461 | 171 |
[Int_lower1, subset_refl] MRS Sigma_mono] 1)); |
760 | 172 |
qed "QPair_Int_Vfrom_succ_subset"; |
0 | 173 |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
174 |
(**** "Take-lemma" rules for proving a=b by coinduction and c: quniv(A) ****) |
0 | 175 |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
176 |
(*Rule for level i -- preserving the level, not decreasing it*) |
0 | 177 |
|
5067 | 178 |
Goalw [QPair_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
179 |
"Transset(X) ==> \ |
0 | 180 |
\ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; |
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset
|
181 |
by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1); |
760 | 182 |
qed "QPair_Int_Vfrom_subset"; |
0 | 183 |
|
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
184 |
(*[| a Int Vset(i) <= c; b Int Vset(i) <= d |] ==> <a;b> Int Vset(i) <= <c;d>*) |
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset
|
185 |
bind_thm ("QPair_Int_Vset_subset_trans", |
1461 | 186 |
[Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans); |
0 | 187 |
|
5268 | 188 |
Goal "Ord(i) ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)"; |
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
189 |
by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
190 |
(*0 case*) |
2033 | 191 |
by (stac Vfrom_0 1); |
2469 | 192 |
by (Fast_tac 1); |
170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
193 |
(*succ(j) case*) |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
194 |
by (rtac (Transset_0 RS QPair_Int_Vfrom_succ_subset RS subset_trans) 1); |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
195 |
by (rtac (succI1 RS UN_upper) 1); |
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset
|
196 |
(*Limit(i) case*) |
5268 | 197 |
by (asm_simp_tac |
198 |
(simpset() addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl, |
|
199 |
UN_mono, QPair_Int_Vset_subset_trans]) 1); |
|
760 | 200 |
qed "QPair_Int_Vset_subset_UN"; |