author  paulson 
Thu, 05 Sep 1996 18:31:14 +0200  
changeset 1957  58b60b558e48 
parent 1461  6bcb44e4d6e5 
child 2469  b50b8c0eec01 
permissions  rwrr 
1461  1 
(* Title: ZF/OrderArith.ML 
437  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
437  4 
Copyright 1994 University of Cambridge 
5 

6 
Towards ordinal arithmetic 

7 
*) 

8 

9 
open OrderArith; 

10 

11 

12 
(**** Addition of relations  disjoint sum ****) 

13 

14 
(** Rewrite rules. Can be used to obtain introduction rules **) 

15 

16 
goalw OrderArith.thy [radd_def] 

17 
"<Inl(a), Inr(b)> : radd(A,r,B,s) <> a:A & b:B"; 

18 
by (fast_tac sum_cs 1); 

760  19 
qed "radd_Inl_Inr_iff"; 
437  20 

21 
goalw OrderArith.thy [radd_def] 

859  22 
"<Inl(a'), Inl(a)> : radd(A,r,B,s) <> a':A & a:A & <a',a>:r"; 
437  23 
by (fast_tac sum_cs 1); 
760  24 
qed "radd_Inl_iff"; 
437  25 

26 
goalw OrderArith.thy [radd_def] 

859  27 
"<Inr(b'), Inr(b)> : radd(A,r,B,s) <> b':B & b:B & <b',b>:s"; 
437  28 
by (fast_tac sum_cs 1); 
760  29 
qed "radd_Inr_iff"; 
437  30 

31 
goalw OrderArith.thy [radd_def] 

32 
"<Inr(b), Inl(a)> : radd(A,r,B,s) <> False"; 

33 
by (fast_tac sum_cs 1); 

760  34 
qed "radd_Inr_Inl_iff"; 
437  35 

36 
(** Elimination Rule **) 

37 

38 
val major::prems = goalw OrderArith.thy [radd_def] 

1461  39 
"[ <p',p> : radd(A,r,B,s); \ 
40 
\ !!x y. [ p'=Inl(x); x:A; p=Inr(y); y:B ] ==> Q; \ 

41 
\ !!x' x. [ p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A ] ==> Q; \ 

42 
\ !!y' y. [ p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B ] ==> Q \ 

437  43 
\ ] ==> Q"; 
44 
by (cut_facts_tac [major] 1); 

45 
(*Split into the three cases*) 

46 
by (REPEAT_FIRST 

47 
(eresolve_tac [CollectE, Pair_inject, conjE, exE, SigmaE, disjE])); 

48 
(*Apply each premise to correct subgoal; can't just use fast_tac 

49 
because hyp_subst_tac would delete equalities too quickly*) 

50 
by (EVERY (map (fn prem => 

1461  51 
EVERY1 [rtac prem, assume_tac, REPEAT o fast_tac sum_cs]) 
52 
prems)); 

760  53 
qed "raddE"; 
437  54 

55 
(** Type checking **) 

56 

57 
goalw OrderArith.thy [radd_def] "radd(A,r,B,s) <= (A+B) * (A+B)"; 

58 
by (rtac Collect_subset 1); 

760  59 
qed "radd_type"; 
437  60 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
770
diff
changeset

61 
bind_thm ("field_radd", (radd_type RS field_rel_subset)); 
437  62 

63 
(** Linearity **) 

64 

65 
val radd_ss = sum_ss addsimps [radd_Inl_iff, radd_Inr_iff, 

1461  66 
radd_Inl_Inr_iff, radd_Inr_Inl_iff]; 
437  67 

68 
goalw OrderArith.thy [linear_def] 

69 
"!!r s. [ linear(A,r); linear(B,s) ] ==> linear(A+B,radd(A,r,B,s))"; 

70 
by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac sumE)); 

71 
by (ALLGOALS (asm_simp_tac radd_ss)); 

760  72 
qed "linear_radd"; 
437  73 

74 

75 
(** Wellfoundedness **) 

76 

77 
goal OrderArith.thy 

78 
"!!r s. [ wf[A](r); wf[B](s) ] ==> wf[A+B](radd(A,r,B,s))"; 

79 
by (rtac wf_onI2 1); 

80 
by (subgoal_tac "ALL x:A. Inl(x): Ba" 1); 

81 
(*Proving the lemma, which is needed twice!*) 

1957  82 
by (thin_tac "y : A + B" 2); 
437  83 
by (rtac ballI 2); 
84 
by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2); 

85 
by (etac (bspec RS mp) 2); 

86 
by (fast_tac sum_cs 2); 

87 
by (best_tac (sum_cs addSEs [raddE]) 2); 

88 
(*Returning to main part of proof*) 

89 
by (REPEAT_FIRST (eresolve_tac [sumE, ssubst])); 

90 
by (best_tac sum_cs 1); 

91 
by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1); 

92 
by (etac (bspec RS mp) 1); 

93 
by (fast_tac sum_cs 1); 

94 
by (best_tac (sum_cs addSEs [raddE]) 1); 

760  95 
qed "wf_on_radd"; 
437  96 

97 
goal OrderArith.thy 

98 
"!!r s. [ wf(r); wf(s) ] ==> wf(radd(field(r),r,field(s),s))"; 

99 
by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1); 

100 
by (rtac (field_radd RSN (2, wf_on_subset_A)) 1); 

101 
by (REPEAT (ares_tac [wf_on_radd] 1)); 

760  102 
qed "wf_radd"; 
437  103 

104 
goal OrderArith.thy 

105 
"!!r s. [ well_ord(A,r); well_ord(B,s) ] ==> \ 

106 
\ well_ord(A+B, radd(A,r,B,s))"; 

107 
by (rtac well_ordI 1); 

108 
by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, wf_on_radd]) 1); 

109 
by (asm_full_simp_tac 

110 
(ZF_ss addsimps [well_ord_def, tot_ord_def, linear_radd]) 1); 

760  111 
qed "well_ord_radd"; 
437  112 

859  113 
(** An ord_iso congruence law **) 
114 

115 
val case_ss = 

116 
bij_inverse_ss addsimps [Inl_iff, Inl_Inr_iff, Inr_iff, Inr_Inl_iff, 

1461  117 
case_Inl, case_Inr, InlI, InrI]; 
859  118 

119 
goal OrderArith.thy 

120 
"!!f g. [ f: bij(A,C); g: bij(B,D) ] ==> \ 

121 
\ (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)"; 

122 
by (res_inst_tac 

123 
[("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(g)`y))")] 

124 
lam_bijective 1); 

125 
by (safe_tac (ZF_cs addSEs [sumE])); 

126 
by (ALLGOALS (asm_simp_tac case_ss)); 

127 
qed "sum_bij"; 

128 

129 
goalw OrderArith.thy [ord_iso_def] 

1461  130 
"!!r s. [ f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') ] ==> \ 
131 
\ (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) \ 

859  132 
\ : ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))"; 
133 
by (safe_tac (ZF_cs addSIs [sum_bij])); 

134 
(*Do the betareductions now*) 

135 
by (ALLGOALS (asm_full_simp_tac ZF_ss)); 

136 
by (safe_tac sum_cs); 

137 
(*8 subgoals!*) 

138 
by (ALLGOALS 

139 
(asm_full_simp_tac 

140 
(radd_ss addcongs [conj_cong] addsimps [bij_is_fun RS apply_type]))); 

141 
qed "sum_ord_iso_cong"; 

142 

143 
(*Could we prove an ord_iso result? Perhaps 

144 
ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *) 

145 
goal OrderArith.thy 

1461  146 
"!!A B. A Int B = 0 ==> \ 
859  147 
\ (lam z:A+B. case(%x.x, %y.y, z)) : bij(A+B, A Un B)"; 
148 
by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")] 

149 
lam_bijective 1); 

150 
by (fast_tac (sum_cs addSIs [if_type]) 2); 

151 
by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1)); 

152 
by (safe_tac sum_cs); 

153 
by (ALLGOALS (asm_simp_tac (sum_ss setloop split_tac [expand_if]))); 

154 
by (fast_tac (ZF_cs addEs [equalityE]) 1); 

155 
qed "sum_disjoint_bij"; 

156 

157 
(** Associativity **) 

158 

159 
goal OrderArith.thy 

160 
"(lam z:(A+B)+C. case(case(Inl, %y.Inr(Inl(y))), %y. Inr(Inr(y)), z)) \ 

161 
\ : bij((A+B)+C, A+(B+C))"; 

162 
by (res_inst_tac [("d", "case(%x.Inl(Inl(x)), case(%x.Inl(Inr(x)), Inr))")] 

163 
lam_bijective 1); 

164 
by (ALLGOALS (asm_simp_tac (case_ss setloop etac sumE))); 

165 
qed "sum_assoc_bij"; 

166 

167 
goal OrderArith.thy 

168 
"(lam z:(A+B)+C. case(case(Inl, %y.Inr(Inl(y))), %y. Inr(Inr(y)), z)) \ 

1461  169 
\ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), \ 
859  170 
\ A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))"; 
171 
by (resolve_tac [sum_assoc_bij RS ord_isoI] 1); 

172 
by (REPEAT_FIRST (etac sumE)); 

173 
by (ALLGOALS (asm_simp_tac radd_ss)); 

174 
qed "sum_assoc_ord_iso"; 

175 

437  176 

177 
(**** Multiplication of relations  lexicographic product ****) 

178 

179 
(** Rewrite rule. Can be used to obtain introduction rules **) 

180 

181 
goalw OrderArith.thy [rmult_def] 

1461  182 
"!!r s. <<a',b'>, <a,b>> : rmult(A,r,B,s) <> \ 
183 
\ (<a',a>: r & a':A & a:A & b': B & b: B)  \ 

437  184 
\ (<b',b>: s & a'=a & a:A & b': B & b: B)"; 
185 
by (fast_tac ZF_cs 1); 

760  186 
qed "rmult_iff"; 
437  187 

188 
val major::prems = goal OrderArith.thy 

1461  189 
"[ <<a',b'>, <a,b>> : rmult(A,r,B,s); \ 
190 
\ [ <a',a>: r; a':A; a:A; b':B; b:B ] ==> Q; \ 

191 
\ [ <b',b>: s; a:A; a'=a; b':B; b:B ] ==> Q \ 

437  192 
\ ] ==> Q"; 
193 
by (rtac (major RS (rmult_iff RS iffD1) RS disjE) 1); 

194 
by (DEPTH_SOLVE (eresolve_tac ([asm_rl, conjE] @ prems) 1)); 

760  195 
qed "rmultE"; 
437  196 

197 
(** Type checking **) 

198 

199 
goalw OrderArith.thy [rmult_def] "rmult(A,r,B,s) <= (A*B) * (A*B)"; 

200 
by (rtac Collect_subset 1); 

760  201 
qed "rmult_type"; 
437  202 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
770
diff
changeset

203 
bind_thm ("field_rmult", (rmult_type RS field_rel_subset)); 
437  204 

205 
(** Linearity **) 

206 

207 
val [lina,linb] = goal OrderArith.thy 

208 
"[ linear(A,r); linear(B,s) ] ==> linear(A*B,rmult(A,r,B,s))"; 

209 
by (rewtac linear_def); (*Note! the premises are NOT rewritten*) 

210 
by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac SigmaE)); 

211 
by (asm_simp_tac (ZF_ss addsimps [rmult_iff]) 1); 

212 
by (res_inst_tac [("x","xa"), ("y","xb")] (lina RS linearE) 1); 

213 
by (res_inst_tac [("x","ya"), ("y","yb")] (linb RS linearE) 4); 

214 
by (REPEAT_SOME (fast_tac ZF_cs)); 

760  215 
qed "linear_rmult"; 
437  216 

217 

218 
(** Wellfoundedness **) 

219 

220 
goal OrderArith.thy 

221 
"!!r s. [ wf[A](r); wf[B](s) ] ==> wf[A*B](rmult(A,r,B,s))"; 

222 
by (rtac wf_onI2 1); 

223 
by (etac SigmaE 1); 

224 
by (etac ssubst 1); 

225 
by (subgoal_tac "ALL b:B. <x,b>: Ba" 1); 

226 
by (fast_tac ZF_cs 1); 

227 
by (eres_inst_tac [("a","x")] wf_on_induct 1 THEN assume_tac 1); 

228 
by (rtac ballI 1); 

229 
by (eres_inst_tac [("a","b")] wf_on_induct 1 THEN assume_tac 1); 

230 
by (etac (bspec RS mp) 1); 

231 
by (fast_tac ZF_cs 1); 

232 
by (best_tac (ZF_cs addSEs [rmultE]) 1); 

760  233 
qed "wf_on_rmult"; 
437  234 

235 

236 
goal OrderArith.thy 

237 
"!!r s. [ wf(r); wf(s) ] ==> wf(rmult(field(r),r,field(s),s))"; 

238 
by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1); 

239 
by (rtac (field_rmult RSN (2, wf_on_subset_A)) 1); 

240 
by (REPEAT (ares_tac [wf_on_rmult] 1)); 

760  241 
qed "wf_rmult"; 
437  242 

243 
goal OrderArith.thy 

244 
"!!r s. [ well_ord(A,r); well_ord(B,s) ] ==> \ 

245 
\ well_ord(A*B, rmult(A,r,B,s))"; 

246 
by (rtac well_ordI 1); 

247 
by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, wf_on_rmult]) 1); 

248 
by (asm_full_simp_tac 

249 
(ZF_ss addsimps [well_ord_def, tot_ord_def, linear_rmult]) 1); 

760  250 
qed "well_ord_rmult"; 
437  251 

252 

859  253 
(** An ord_iso congruence law **) 
254 

255 
goal OrderArith.thy 

256 
"!!f g. [ f: bij(A,C); g: bij(B,D) ] ==> \ 

1095
6d0aad5f50a5
Changed some definitions and proofs to use patternmatching.
lcp
parents:
859
diff
changeset

257 
\ (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)"; 
6d0aad5f50a5
Changed some definitions and proofs to use patternmatching.
lcp
parents:
859
diff
changeset

258 
by (res_inst_tac [("d", "%<x,y>. <converse(f)`x, converse(g)`y>")] 
859  259 
lam_bijective 1); 
260 
by (safe_tac ZF_cs); 

261 
by (ALLGOALS (asm_simp_tac bij_inverse_ss)); 

262 
qed "prod_bij"; 

263 

264 
goalw OrderArith.thy [ord_iso_def] 

1461  265 
"!!r s. [ f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') ] ==> \ 
266 
\ (lam <x,y>:A*B. <f`x, g`y>) \ 

859  267 
\ : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))"; 
268 
by (safe_tac (ZF_cs addSIs [prod_bij])); 

269 
by (ALLGOALS 

270 
(asm_full_simp_tac 

271 
(ZF_ss addsimps [rmult_iff, bij_is_fun RS apply_type]))); 

272 
by (fast_tac ZF_cs 1); 

273 
by (fast_tac (ZF_cs addSEs [bij_is_inj RS inj_apply_equality]) 1); 

274 
qed "prod_ord_iso_cong"; 

275 

276 
goal OrderArith.thy "(lam z:A. <x,z>) : bij(A, {x}*A)"; 

277 
by (res_inst_tac [("d", "snd")] lam_bijective 1); 

278 
by (safe_tac ZF_cs); 

279 
by (ALLGOALS (asm_simp_tac ZF_ss)); 

280 
qed "singleton_prod_bij"; 

281 

282 
(*Used??*) 

283 
goal OrderArith.thy 

1461  284 
"!!x xr. well_ord({x},xr) ==> \ 
859  285 
\ (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))"; 
286 
by (resolve_tac [singleton_prod_bij RS ord_isoI] 1); 

287 
by (asm_simp_tac (ZF_ss addsimps [rmult_iff]) 1); 

288 
by (fast_tac (ZF_cs addEs [well_ord_is_wf RS wf_on_not_refl RS notE]) 1); 

289 
qed "singleton_prod_ord_iso"; 

290 

291 
(*Here we build a complicated function term, then simplify it using 

292 
case_cong, id_conv, comp_lam, case_case.*) 

293 
goal OrderArith.thy 

294 
"!!a. a~:C ==> \ 

295 
\ (lam x:C*B + D. case(%x.x, %y.<a,y>, x)) \ 

296 
\ : bij(C*B + D, C*B Un {a}*D)"; 

1461  297 
by (rtac subst_elem 1); 
859  298 
by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1); 
1461  299 
by (rtac singleton_prod_bij 1); 
300 
by (rtac sum_disjoint_bij 1); 

859  301 
by (fast_tac eq_cs 1); 
302 
by (asm_simp_tac (ZF_ss addcongs [case_cong] addsimps [id_conv]) 1); 

303 
by (resolve_tac [comp_lam RS trans RS sym] 1); 

304 
by (fast_tac (sum_cs addSEs [case_type]) 1); 

305 
by (asm_simp_tac (ZF_ss addsimps [case_case]) 1); 

306 
qed "prod_sum_singleton_bij"; 

307 

308 
goal OrderArith.thy 

309 
"!!A. [ a:A; well_ord(A,r) ] ==> \ 

310 
\ (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x.x, %y.<a,y>, x)) \ 

1461  311 
\ : ord_iso(pred(A,a,r)*B + pred(B,b,s), \ 
312 
\ radd(A*B, rmult(A,r,B,s), B, s), \ 

859  313 
\ pred(A,a,r)*B Un {a}*pred(B,b,s), rmult(A,r,B,s))"; 
314 
by (resolve_tac [prod_sum_singleton_bij RS ord_isoI] 1); 

315 
by (asm_simp_tac 

316 
(ZF_ss addsimps [pred_iff, well_ord_is_wf RS wf_on_not_refl]) 1); 

317 
by (asm_simp_tac ZF_ss 1); 

318 
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, predE])); 

319 
by (ALLGOALS (asm_simp_tac (radd_ss addsimps [rmult_iff]))); 

320 
by (ALLGOALS (fast_tac (ZF_cs addEs [well_ord_is_wf RS wf_on_asym]))); 

321 
qed "prod_sum_singleton_ord_iso"; 

322 

323 
(** Distributive law **) 

324 

325 
goal OrderArith.thy 

1095
6d0aad5f50a5
Changed some definitions and proofs to use patternmatching.
lcp
parents:
859
diff
changeset

326 
"(lam <x,z>:(A+B)*C. case(%y.Inl(<y,z>), %y.Inr(<y,z>), x)) \ 
859  327 
\ : bij((A+B)*C, (A*C)+(B*C))"; 
328 
by (res_inst_tac 

1095
6d0aad5f50a5
Changed some definitions and proofs to use patternmatching.
lcp
parents:
859
diff
changeset

329 
[("d", "case(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1); 
859  330 
by (safe_tac (ZF_cs addSEs [sumE])); 
331 
by (ALLGOALS (asm_simp_tac case_ss)); 

332 
qed "sum_prod_distrib_bij"; 

333 

334 
goal OrderArith.thy 

1095
6d0aad5f50a5
Changed some definitions and proofs to use patternmatching.
lcp
parents:
859
diff
changeset

335 
"(lam <x,z>:(A+B)*C. case(%y.Inl(<y,z>), %y.Inr(<y,z>), x)) \ 
859  336 
\ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \ 
337 
\ (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"; 

338 
by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1); 

339 
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE])); 

340 
by (ALLGOALS (asm_simp_tac (radd_ss addsimps [rmult_iff]))); 

341 
qed "sum_prod_distrib_ord_iso"; 

342 

343 
(** Associativity **) 

344 

345 
goal OrderArith.thy 

1095
6d0aad5f50a5
Changed some definitions and proofs to use patternmatching.
lcp
parents:
859
diff
changeset

346 
"(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))"; 
6d0aad5f50a5
Changed some definitions and proofs to use patternmatching.
lcp
parents:
859
diff
changeset

347 
by (res_inst_tac [("d", "%<x, <y,z>>. <<x,y>, z>")] lam_bijective 1); 
859  348 
by (ALLGOALS (asm_simp_tac (case_ss setloop etac SigmaE))); 
349 
qed "prod_assoc_bij"; 

350 

351 
goal OrderArith.thy 

1461  352 
"(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) \ 
353 
\ : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), \ 

859  354 
\ A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"; 
355 
by (resolve_tac [prod_assoc_bij RS ord_isoI] 1); 

356 
by (REPEAT_FIRST (eresolve_tac [SigmaE, ssubst])); 

357 
by (asm_simp_tac (ZF_ss addsimps [rmult_iff]) 1); 

358 
by (fast_tac ZF_cs 1); 

359 
qed "prod_assoc_ord_iso"; 

360 

437  361 
(**** Inverse image of a relation ****) 
362 

363 
(** Rewrite rule **) 

364 

365 
goalw OrderArith.thy [rvimage_def] 

366 
"<a,b> : rvimage(A,f,r) <> <f`a,f`b>: r & a:A & b:A"; 

367 
by (fast_tac ZF_cs 1); 

760  368 
qed "rvimage_iff"; 
437  369 

370 
(** Type checking **) 

371 

372 
goalw OrderArith.thy [rvimage_def] "rvimage(A,f,r) <= A*A"; 

373 
by (rtac Collect_subset 1); 

760  374 
qed "rvimage_type"; 
437  375 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
770
diff
changeset

376 
bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset)); 
437  377 

835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

378 
goalw OrderArith.thy [rvimage_def] 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

379 
"rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))"; 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

380 
by (fast_tac eq_cs 1); 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

381 
qed "rvimage_converse"; 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

382 

313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

383 

313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

384 
(** Partial Ordering Properties **) 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

385 

313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

386 
goalw OrderArith.thy [irrefl_def, rvimage_def] 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

387 
"!!A B. [ f: inj(A,B); irrefl(B,r) ] ==> irrefl(A, rvimage(A,f,r))"; 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

388 
by (fast_tac (ZF_cs addIs [inj_is_fun RS apply_type]) 1); 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

389 
qed "irrefl_rvimage"; 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

390 

313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

391 
goalw OrderArith.thy [trans_on_def, rvimage_def] 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

392 
"!!A B. [ f: inj(A,B); trans[B](r) ] ==> trans[A](rvimage(A,f,r))"; 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

393 
by (fast_tac (ZF_cs addIs [inj_is_fun RS apply_type]) 1); 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

394 
qed "trans_on_rvimage"; 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

395 

313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

396 
goalw OrderArith.thy [part_ord_def] 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

397 
"!!A B. [ f: inj(A,B); part_ord(B,r) ] ==> part_ord(A, rvimage(A,f,r))"; 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

398 
by (fast_tac (ZF_cs addSIs [irrefl_rvimage, trans_on_rvimage]) 1); 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

399 
qed "part_ord_rvimage"; 
437  400 

401 
(** Linearity **) 

402 

403 
val [finj,lin] = goalw OrderArith.thy [inj_def] 

404 
"[ f: inj(A,B); linear(B,r) ] ==> linear(A,rvimage(A,f,r))"; 

405 
by (rewtac linear_def); (*Note! the premises are NOT rewritten*) 

406 
by (REPEAT_FIRST (ares_tac [ballI])); 

407 
by (asm_simp_tac (ZF_ss addsimps [rvimage_iff]) 1); 

408 
by (cut_facts_tac [finj] 1); 

409 
by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1); 

410 
by (REPEAT_SOME (fast_tac (ZF_cs addSIs [apply_type]))); 

760  411 
qed "linear_rvimage"; 
437  412 

835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

413 
goalw OrderArith.thy [tot_ord_def] 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

414 
"!!A B. [ f: inj(A,B); tot_ord(B,r) ] ==> tot_ord(A, rvimage(A,f,r))"; 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

415 
by (fast_tac (ZF_cs addSIs [part_ord_rvimage, linear_rvimage]) 1); 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

416 
qed "tot_ord_rvimage"; 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

417 

437  418 

419 
(** Wellfoundedness **) 

420 

421 
goal OrderArith.thy 

422 
"!!r. [ f: A>B; wf[B](r) ] ==> wf[A](rvimage(A,f,r))"; 

423 
by (rtac wf_onI2 1); 

424 
by (subgoal_tac "ALL z:A. f`z=f`y > z: Ba" 1); 

425 
by (fast_tac ZF_cs 1); 

426 
by (eres_inst_tac [("a","f`y")] wf_on_induct 1); 

427 
by (fast_tac (ZF_cs addSIs [apply_type]) 1); 

428 
by (best_tac (ZF_cs addSIs [apply_type] addSDs [rvimage_iff RS iffD1]) 1); 

760  429 
qed "wf_on_rvimage"; 
437  430 

835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

431 
(*Note that we need only wf[A](...) and linear(A,...) to get the result!*) 
437  432 
goal OrderArith.thy 
433 
"!!r. [ f: inj(A,B); well_ord(B,r) ] ==> well_ord(A, rvimage(A,f,r))"; 

434 
by (rtac well_ordI 1); 

435 
by (rewrite_goals_tac [well_ord_def, tot_ord_def]); 

436 
by (fast_tac (ZF_cs addSIs [wf_on_rvimage, inj_is_fun]) 1); 

437 
by (fast_tac (ZF_cs addSIs [linear_rvimage]) 1); 

760  438 
qed "well_ord_rvimage"; 
815  439 

440 
goalw OrderArith.thy [ord_iso_def] 

441 
"!!A B. f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)"; 

442 
by (asm_full_simp_tac (ZF_ss addsimps [rvimage_iff]) 1); 

443 
qed "ord_iso_rvimage"; 

835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

444 

313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

445 
goalw OrderArith.thy [ord_iso_def, rvimage_def] 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

446 
"!!A B. f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A"; 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

447 
by (fast_tac eq_cs 1); 
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset

448 
qed "ord_iso_rvimage_eq"; 