author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2033  639de962ded4 
permissions  rwrr 
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)"; 
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset

22 
by (rtac (Int_Un_distrib RS ssubst) 1); 
120edb26ee93
Moved Transset_includes_summands and Transset_sum_Int_subset
lcp
parents:
803
diff
changeset

23 
by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1); 
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 

28 
goalw QUniv.thy [quniv_def] 

29 
"!!X A. 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 

33 
goalw QUniv.thy [quniv_def] 

34 
"!!X A. 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 

38 
goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)"; 

39 
by (etac (eclose_mono RS univ_mono RS Pow_mono) 1); 

760  40 
qed "quniv_mono"; 
0  41 

42 
(*** Closure properties ***) 

43 

44 
goalw QUniv.thy [quniv_def] "univ(eclose(A)) <= quniv(A)"; 

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*) 
0  50 
goal QUniv.thy "univ(A) <= quniv(A)"; 
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 

57 
goalw QUniv.thy [quniv_def] "Pow(univ(A)) <= quniv(A)"; 

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 Quineinspired pairs and injections ***) 

74 

75 
(*Quine ordered pairs*) 

76 
goalw QUniv.thy [QPair_def] 

77 
"!!A a. [ a <= univ(A); b <= univ(A) ] ==> <a;b> <= univ(A)"; 

78 
by (REPEAT (ares_tac [sum_subset_univ] 1)); 

760  79 
qed "QPair_subset_univ"; 
0  80 

81 
(** Quine disjoint sum **) 

82 

83 
goalw QUniv.thy [QInl_def] "!!A a. a <= univ(A) ==> QInl(a) <= univ(A)"; 

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 

94 
goalw QUniv.thy [QInr_def] "!!A a. a <= univ(A) ==> QInr(a) <= univ(A)"; 

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 Quineinspired products and sums ***) 

99 

100 
(*Quine ordered pairs*) 

101 
goalw QUniv.thy [quniv_def,QPair_def] 

102 
"!!A a. [ a: quniv(A); b: quniv(A) ] ==> <a;b> : quniv(A)"; 

103 
by (REPEAT (dtac PowD 1)); 

104 
by (REPEAT (ares_tac [PowI, sum_subset_univ] 1)); 

760  105 
qed "QPair_in_quniv"; 
0  106 

107 
goal QUniv.thy "quniv(A) <*> quniv(A) <= quniv(A)"; 

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*) 

116 
goalw QUniv.thy [quniv_def,QPair_def] 

117 
"!!A a b. <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 

125 
goal QUniv.thy "<a;b> : quniv(A) <> a: quniv(A) & b: quniv(A)"; 

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 

133 
goalw QUniv.thy [QInl_def] "!!A a. a: quniv(A) ==> QInl(a) : quniv(A)"; 

134 
by (REPEAT (ares_tac [zero_in_quniv,QPair_in_quniv] 1)); 

760  135 
qed "QInl_in_quniv"; 
0  136 

137 
goalw QUniv.thy [QInr_def] "!!A b. b: quniv(A) ==> QInr(b) : quniv(A)"; 

138 
by (REPEAT (ares_tac [one_in_quniv, QPair_in_quniv] 1)); 

760  139 
qed "QInr_in_quniv"; 
0  140 

141 
goal QUniv.thy "quniv(C) <+> quniv(C) <= quniv(C)"; 

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 
(**** Properties of Vfrom analogous to the "takelemma" ****) 

164 

165 
(*** Intersecting a*b with Vfrom... ***) 

166 

167 
(*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*) 

168 
goal Univ.thy 

169 
"!!X. [ {a,b} : Vfrom(X,succ(i)); Transset(X) ] ==> \ 

170 
\ a: Vfrom(X,i) & b: Vfrom(X,i)"; 

15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

171 
by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

172 
by (assume_tac 1); 
0  173 
by (fast_tac ZF_cs 1); 
760  174 
qed "doubleton_in_Vfrom_D"; 
0  175 

176 
(*This weaker version says a, b exist at the same level*) 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

177 
bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D); 
0  178 

179 
(** Using only the weaker theorem would prove <a,b> : Vfrom(X,i) 

180 
implies a, b : Vfrom(X,i), which is useless for induction. 

181 
Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i))) 

182 
implies a, b : Vfrom(X,i), leaving the succ(i) case untreated. 

183 
The combination gives a reduction by precisely one level, which is 

184 
most convenient for proofs. 

185 
**) 

186 

187 
goalw Univ.thy [Pair_def] 

188 
"!!X. [ <a,b> : Vfrom(X,succ(i)); Transset(X) ] ==> \ 

189 
\ a: Vfrom(X,i) & b: Vfrom(X,i)"; 

190 
by (fast_tac (ZF_cs addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1); 

760  191 
qed "Pair_in_Vfrom_D"; 
0  192 

193 
goal Univ.thy 

1461  194 
"!!X. Transset(X) ==> \ 
0  195 
\ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))"; 
196 
by (fast_tac (ZF_cs addSDs [Pair_in_Vfrom_D]) 1); 

760  197 
qed "product_Int_Vfrom_subset"; 
0  198 

199 
(*** Intersecting <a;b> with Vfrom... ***) 

200 

201 
goalw QUniv.thy [QPair_def,sum_def] 

1461  202 
"!!X. Transset(X) ==> \ 
0  203 
\ <a;b> Int Vfrom(X, succ(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

204 
by (rtac (Int_Un_distrib RS ssubst) 1); 
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

205 
by (rtac Un_mono 1); 
0  206 
by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans, 
1461  207 
[Int_lower1, subset_refl] MRS Sigma_mono] 1)); 
760  208 
qed "QPair_Int_Vfrom_succ_subset"; 
0  209 

170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

210 
(**** "Takelemma" rules for proving a=b by coinduction and c: quniv(A) ****) 
0  211 

170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

212 
(*Rule for level i  preserving the level, not decreasing it*) 
0  213 

214 
goalw QUniv.thy [QPair_def] 

1461  215 
"!!X. Transset(X) ==> \ 
0  216 
\ <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

217 
by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1); 
760  218 
qed "QPair_Int_Vfrom_subset"; 
0  219 

170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

220 
(*[ 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

221 
bind_thm ("QPair_Int_Vset_subset_trans", 
1461  222 
[Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans); 
0  223 

170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

224 
goal QUniv.thy 
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

225 
"!!i. [ Ord(i) \ 
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

226 
\ ] ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)"; 
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

227 
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

228 
(*0 case*) 
0  229 
by (rtac (Vfrom_0 RS ssubst) 1); 
230 
by (fast_tac ZF_cs 1); 

170
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

231 
(*succ(j) case*) 
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

232 
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

233 
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

234 
(*Limit(i) case*) 
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

235 
by (asm_simp_tac (ZF_ss addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl, 
1461  236 
UN_mono, QPair_Int_Vset_subset_trans]) 1); 
760  237 
qed "QPair_Int_Vset_subset_UN"; 