author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 2034  5079fdf938dd 
permissions  rwrr 
1461  1 
(* Title: ZF/Coind/Map.ML 
915  2 
ID: $Id$ 
1461  3 
Author: Jacob Frost, Cambridge University Computer Laboratory 
915  4 
Copyright 1995 University of Cambridge 
5 
*) 

6 

7 
open Map; 

8 

9 
(* ############################################################ *) 

10 
(* Lemmas *) 

11 
(* ############################################################ *) 

12 

13 
goal Map.thy "!!A. a:A ==> Sigma(A,B)``{a} = B(a)"; 

14 
by (fast_tac eq_cs 1); 

15 
qed "qbeta"; 

16 

17 
goal Map.thy "!!A. a~:A ==> Sigma(A,B)``{a} = 0"; 

18 
by (fast_tac eq_cs 1); 

19 
qed "qbeta_emp"; 

20 

21 
goal Map.thy "!!A.a ~: A ==> Sigma(A,B)``{a}=0"; 

22 
by (fast_tac eq_cs 1); 

23 
qed "image_Sigma1"; 

24 

25 
goal Map.thy "0``A = 0"; 

26 
by (fast_tac eq_cs 1); 

27 
qed "image_02"; 

28 

29 
(* ############################################################ *) 

30 
(* Inclusion in Quine Universes *) 

31 
(* ############################################################ *) 

32 

33 
(* Lemmas *) 

34 

35 
goalw Map.thy [quniv_def] 

36 
"!!A. A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)"; 

37 
by (rtac Pow_mono 1); 

38 
by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1); 

39 
by (etac subset_trans 1); 

40 
by (rtac (arg_subset_eclose RS univ_mono) 1); 

41 
by (simp_tac (ZF_ss addsimps [Union_Pow_eq]) 1); 

42 
qed "MapQU_lemma"; 

43 

44 
(* Theorems *) 

45 

46 
val prems = goalw Map.thy [PMap_def,TMap_def] 

47 
"[ m:PMap(A,quniv(B)); !!x.x:A ==> x:univ(B) ] ==> m:quniv(B)"; 

48 
by (cut_facts_tac prems 1); 

49 
by (rtac (MapQU_lemma RS subsetD) 1); 

50 
by (rtac subsetI 1); 

51 
by (eresolve_tac prems 1); 

52 
by (fast_tac ZF_cs 1); 

53 
qed "mapQU"; 

54 

55 
(* ############################################################ *) 

56 
(* Monotonicity *) 

57 
(* ############################################################ *) 

58 

59 
goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)"; 

60 
by (fast_tac ZF_cs 1); 

61 
qed "map_mono"; 

62 

63 
(* Rename to pmap_mono *) 

64 

65 
(* ############################################################ *) 

66 
(* Introduction Rules *) 

67 
(* ############################################################ *) 

68 

69 
(** map_emp **) 

70 

71 
goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)"; 

72 
by (safe_tac ZF_cs); 

73 
by (rtac image_02 1); 

74 
qed "pmap_empI"; 

75 

76 
(** map_owr **) 

77 

1020
76d72126a9e7
Modified proofs for new hyp_subst_tac, and simplified them.
lcp
parents:
915
diff
changeset

78 

915  79 
goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
80 
"!! A.[ m:PMap(A,B); a:A; b:B ] ==> map_owr(m,a,b):PMap(A,B)"; 

81 
by (safe_tac ZF_cs); 

1075
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset

82 
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [if_iff]))); 
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset

83 
by (fast_tac ZF_cs 1); 
915  84 
by (fast_tac ZF_cs 1); 
85 
by (fast_tac ZF_cs 1); 

1075
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset

86 

915  87 
by (rtac (excluded_middle RS disjE) 1); 
88 
by (etac image_Sigma1 1); 

1075
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset

89 
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1); 
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset

90 
by (asm_full_simp_tac 
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset

91 
(ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1); 
1020
76d72126a9e7
Modified proofs for new hyp_subst_tac, and simplified them.
lcp
parents:
915
diff
changeset

92 
by (safe_tac FOL_cs); 
1075
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset

93 
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3); 
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset

94 
by (ALLGOALS (asm_full_simp_tac ZF_ss)); 
915  95 
by (fast_tac ZF_cs 1); 
96 
qed "pmap_owrI"; 

97 

98 
(** map_app **) 

99 

100 
goalw Map.thy [TMap_def,map_app_def] 

101 
"!!m.[ m:TMap(A,B); a:domain(m) ] ==> map_app(m,a) ~=0"; 

102 
by (etac domainE 1); 

103 
by (dtac imageI 1); 

104 
by (fast_tac ZF_cs 1); 

105 
by (etac not_emptyI 1); 

106 
qed "tmap_app_notempty"; 

107 

108 
goalw Map.thy [TMap_def,map_app_def,domain_def] 

109 
"!!m.[ m:TMap(A,B); a:domain(m) ] ==> map_app(m,a):B"; 

110 
by (fast_tac eq_cs 1); 

111 
qed "tmap_appI"; 

112 

113 
goalw Map.thy [PMap_def] 

114 
"!!m.[ m:PMap(A,B); a:domain(m) ] ==> map_app(m,a):B"; 

115 
by (forward_tac [tmap_app_notempty] 1); 

116 
by (assume_tac 1); 

117 
by (dtac tmap_appI 1); 

118 
by (assume_tac 1); 

119 
by (fast_tac ZF_cs 1); 

120 
qed "pmap_appI"; 

121 

122 
(** domain **) 

123 

124 
goalw Map.thy [TMap_def] 

125 
"!!m.[ m:TMap(A,B); a:domain(m) ] ==> a:A"; 

126 
by (fast_tac eq_cs 1); 

127 
qed "tmap_domainD"; 

128 

129 
goalw Map.thy [PMap_def,TMap_def] 

130 
"!!m.[ m:PMap(A,B); a:domain(m) ] ==> a:A"; 

131 
by (fast_tac eq_cs 1); 

132 
qed "pmap_domainD"; 

133 

134 
(* ############################################################ *) 

135 
(* Equalitites *) 

136 
(* ############################################################ *) 

137 

138 
(** Domain **) 

139 

140 
(* Lemmas *) 

141 

142 
goal Map.thy "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))"; 

143 
by (fast_tac eq_cs 1); 

144 
qed "domain_UN"; 

145 

146 
goal Map.thy "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}"; 

147 
by (simp_tac (ZF_ss addsimps [domain_UN,domain_0,domain_cons]) 1); 

148 
by (fast_tac eq_cs 1); 

149 
qed "domain_Sigma"; 

150 

151 
(* Theorems *) 

152 

153 
goalw Map.thy [map_emp_def] "domain(map_emp) = 0"; 

154 
by (fast_tac eq_cs 1); 

155 
qed "map_domain_emp"; 

156 

157 
goalw Map.thy [map_owr_def] 

158 
"!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"; 

159 
by (simp_tac (if_ss addsimps [domain_Sigma]) 1); 

160 
by (rtac equalityI 1); 

161 
by (fast_tac eq_cs 1); 

162 
by (rtac subsetI 1); 

163 
by (rtac CollectI 1); 

164 
by (assume_tac 1); 

165 
by (etac UnE' 1); 

166 
by (etac singletonE 1); 

167 
by (asm_simp_tac if_ss 1); 

168 
by (fast_tac eq_cs 1); 

169 
by (etac notsingletonE 1); 

170 
by (asm_simp_tac if_ss 1); 

171 
by (fast_tac eq_cs 1); 

172 
qed "map_domain_owr"; 

173 

174 
(** Application **) 

175 

176 
goalw Map.thy [map_app_def,map_owr_def] 

177 
"map_app(map_owr(f,a,b),a) = b"; 

178 
by (rtac (qbeta RS ssubst) 1); 

179 
by (fast_tac ZF_cs 1); 

180 
by (simp_tac if_ss 1); 

181 
qed "map_app_owr1"; 

182 

183 
goalw Map.thy [map_app_def,map_owr_def] 

184 
"!!a.c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)"; 

185 
by (rtac (excluded_middle RS disjE) 1); 

186 
by (rtac (qbeta_emp RS ssubst) 1); 

187 
by (assume_tac 1); 

188 
by (fast_tac eq_cs 1); 

189 
by (etac (qbeta RS ssubst) 1); 

190 
by (asm_simp_tac if_ss 1); 

191 
qed "map_app_owr2"; 

192 

193 

194 

195 

196 

197 

198 

199 

200 

201 

202 

203 

204 

205 

206 

207 

208 

209 

210 

211 

212 

213 

214 

215 

216 

217 

218 

219 

220 

221 

222 

223 

224 

225 

226 

227 

228 

229 

230 

231 

232 