author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 170  590c9d1e0d73 
permissions  rwrr 
0  1 
(* Title: ZF/quniv 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
For quniv.thy. A small universe for lazy recursive types 

7 
*) 

8 

9 
open QUniv; 

10 

11 
(** Introduction and elimination rules avoid tiresome folding/unfolding **) 

12 

13 
goalw QUniv.thy [quniv_def] 

14 
"!!X A. X <= univ(eclose(A)) ==> X : quniv(A)"; 

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

15 
by (etac PowI 1); 
0  16 
val qunivI = result(); 
17 

18 
goalw QUniv.thy [quniv_def] 

19 
"!!X A. X : quniv(A) ==> X <= univ(eclose(A))"; 

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

20 
by (etac PowD 1); 
0  21 
val qunivD = result(); 
22 

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

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

25 
val quniv_mono = result(); 

26 

27 
(*** Closure properties ***) 

28 

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

30 
by (rtac (Transset_iff_Pow RS iffD1) 1); 

31 
by (rtac (Transset_eclose RS Transset_univ) 1); 

32 
val univ_eclose_subset_quniv = result(); 

33 

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

34 
(*Key property for proving A_subset_quniv; requires eclose in def of quniv*) 
0  35 
goal QUniv.thy "univ(A) <= quniv(A)"; 
36 
by (rtac (arg_subset_eclose RS univ_mono RS subset_trans) 1); 

37 
by (rtac univ_eclose_subset_quniv 1); 

38 
val univ_subset_quniv = result(); 

39 

40 
val univ_into_quniv = standard (univ_subset_quniv RS subsetD); 

41 

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

43 
by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1); 

44 
val Pow_univ_subset_quniv = result(); 

45 

46 
val univ_subset_into_quniv = standard 

47 
(PowI RS (Pow_univ_subset_quniv RS subsetD)); 

48 

49 
val zero_in_quniv = standard (zero_in_univ RS univ_into_quniv); 

50 
val one_in_quniv = standard (one_in_univ RS univ_into_quniv); 

51 
val two_in_quniv = standard (two_in_univ RS univ_into_quniv); 

52 

53 
val A_subset_quniv = standard 

54 
([A_subset_univ, univ_subset_quniv] MRS subset_trans); 

55 

56 
val A_into_quniv = A_subset_quniv RS subsetD; 

57 

58 
(*** univ(A) closure for Quineinspired pairs and injections ***) 

59 

60 
(*Quine ordered pairs*) 

61 
goalw QUniv.thy [QPair_def] 

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

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

64 
val QPair_subset_univ = result(); 

65 

66 
(** Quine disjoint sum **) 

67 

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

69 
by (etac (empty_subsetI RS QPair_subset_univ) 1); 

70 
val QInl_subset_univ = result(); 

71 

72 
val naturals_subset_nat = 

73 
rewrite_rule [Transset_def] (Ord_nat RS Ord_is_Transset) 

74 
RS bspec; 

75 

76 
val naturals_subset_univ = 

77 
[naturals_subset_nat, nat_subset_univ] MRS subset_trans; 

78 

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

80 
by (etac (nat_1I RS naturals_subset_univ RS QPair_subset_univ) 1); 

81 
val QInr_subset_univ = result(); 

82 

83 
(*** Closure for Quineinspired products and sums ***) 

84 

85 
(*Quine ordered pairs*) 

86 
goalw QUniv.thy [quniv_def,QPair_def] 

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

88 
by (REPEAT (dtac PowD 1)); 

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

90 
val QPair_in_quniv = result(); 

91 

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

93 
by (REPEAT (ares_tac [subsetI, QPair_in_quniv] 1 

94 
ORELSE eresolve_tac [QSigmaE, ssubst] 1)); 

95 
val QSigma_quniv = result(); 

96 

97 
val QSigma_subset_quniv = standard 

98 
(QSigma_mono RS (QSigma_quniv RSN (2,subset_trans))); 

99 

100 
(*The opposite inclusion*) 

101 
goalw QUniv.thy [quniv_def,QPair_def] 

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

129  103 
by (etac ([Transset_eclose RS Transset_univ, PowD] MRS 
104 
Transset_includes_summands RS conjE) 1); 

0  105 
by (REPEAT (ares_tac [conjI,PowI] 1)); 
106 
val quniv_QPair_D = result(); 

107 

108 
val quniv_QPair_E = standard (quniv_QPair_D RS conjE); 

109 

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

111 
by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1 

112 
ORELSE etac conjE 1)); 

113 
val quniv_QPair_iff = result(); 

114 

115 

116 
(** Quine disjoint sum **) 

117 

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

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

120 
val QInl_in_quniv = result(); 

121 

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

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

124 
val QInr_in_quniv = result(); 

125 

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

127 
by (REPEAT (ares_tac [subsetI, QInl_in_quniv, QInr_in_quniv] 1 

128 
ORELSE eresolve_tac [qsumE, ssubst] 1)); 

129 
val qsum_quniv = result(); 

130 

131 
val qsum_subset_quniv = standard 

132 
(qsum_mono RS (qsum_quniv RSN (2,subset_trans))); 

133 

134 
(*** The natural numbers ***) 

135 

136 
val nat_subset_quniv = standard 

137 
([nat_subset_univ, univ_subset_quniv] MRS subset_trans); 

138 

139 
(* n:nat ==> n:quniv(A) *) 

140 
val nat_into_quniv = standard (nat_subset_quniv RS subsetD); 

141 

142 
val bool_subset_quniv = standard 

143 
([bool_subset_univ, univ_subset_quniv] MRS subset_trans); 

144 

145 
val bool_into_quniv = standard (bool_subset_quniv RS subsetD); 

146 

147 

148 
(**** Properties of Vfrom analogous to the "takelemma" ****) 

149 

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

151 

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

153 
goal Univ.thy 

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

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

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

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

157 
by (assume_tac 1); 
0  158 
by (fast_tac ZF_cs 1); 
159 
val doubleton_in_Vfrom_D = result(); 

160 

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

162 
val Vfrom_doubleton_D = standard (Transset_Vfrom RS Transset_doubleton_D); 

163 

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

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

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

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

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

169 
most convenient for proofs. 

170 
**) 

171 

172 
goalw Univ.thy [Pair_def] 

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

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

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

176 
val Pair_in_Vfrom_D = result(); 

177 

178 
goal Univ.thy 

179 
"!!X. Transset(X) ==> \ 

180 
\ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))"; 

181 
by (fast_tac (ZF_cs addSDs [Pair_in_Vfrom_D]) 1); 

182 
val product_Int_Vfrom_subset = result(); 

183 

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

185 

186 
goalw QUniv.thy [QPair_def,sum_def] 

187 
"!!X. Transset(X) ==> \ 

188 
\ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; 

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

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

190 
by (rtac Un_mono 1); 
0  191 
by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans, 
192 
[Int_lower1, subset_refl] MRS Sigma_mono] 1)); 

193 
val QPair_Int_Vfrom_succ_subset = result(); 

194 

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

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

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

197 
(*Rule for level i  preserving the level, not decreasing it*) 
0  198 

199 
goalw QUniv.thy [QPair_def] 

200 
"!!X. Transset(X) ==> \ 

201 
\ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; 

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

202 
by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1); 
0  203 
val QPair_Int_Vfrom_subset = result(); 
204 

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

205 
(*[ a Int Vset(i) <= c; b Int Vset(i) <= d ] ==> <a;b> Int Vset(i) <= <c;d>*) 
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

206 
val QPair_Int_Vset_subset_trans = standard 
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

207 
([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans); 
0  208 

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

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

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

211 
\ ] ==> <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

212 
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

213 
(*0 case*) 
0  214 
by (rtac (Vfrom_0 RS ssubst) 1); 
215 
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

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

217 
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

218 
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

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

220 
by (asm_simp_tac (ZF_ss addsimps [Limit_Vfrom_eq, Int_UN_distrib, subset_refl, 
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

221 
UN_mono, QPair_Int_Vset_subset_trans]) 1); 
590c9d1e0d73
ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many
lcp
parents:
129
diff
changeset

222 
val QPair_Int_Vset_subset_UN = result(); 