author | paulson |
Mon, 13 Jul 1998 16:43:57 +0200 | |
changeset 5137 | 60205b0de9b9 |
parent 5116 | 8eb343ab5748 |
child 5147 | 825877190618 |
permissions | -rw-r--r-- |
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 |
||
5067 | 16 |
Goalw [radd_def] |
437 | 17 |
"<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B"; |
2925 | 18 |
by (Blast_tac 1); |
760 | 19 |
qed "radd_Inl_Inr_iff"; |
437 | 20 |
|
5067 | 21 |
Goalw [radd_def] |
859 | 22 |
"<Inl(a'), Inl(a)> : radd(A,r,B,s) <-> a':A & a:A & <a',a>:r"; |
2925 | 23 |
by (Blast_tac 1); |
760 | 24 |
qed "radd_Inl_iff"; |
437 | 25 |
|
5067 | 26 |
Goalw [radd_def] |
859 | 27 |
"<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s"; |
2925 | 28 |
by (Blast_tac 1); |
760 | 29 |
qed "radd_Inr_iff"; |
437 | 30 |
|
5067 | 31 |
Goalw [radd_def] |
437 | 32 |
"<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False"; |
2925 | 33 |
by (Blast_tac 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*) |
|
2925 | 46 |
by (REPEAT_FIRST (*can't use safe_tac: don't want hyp_subst_tac*) |
437 | 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 => |
|
2493 | 51 |
EVERY1 [rtac prem, assume_tac, REPEAT o Fast_tac]) |
1461 | 52 |
prems)); |
760 | 53 |
qed "raddE"; |
437 | 54 |
|
55 |
(** Type checking **) |
|
56 |
||
5067 | 57 |
Goalw [radd_def] "radd(A,r,B,s) <= (A+B) * (A+B)"; |
437 | 58 |
by (rtac Collect_subset 1); |
760 | 59 |
qed "radd_type"; |
437 | 60 |
|
2469 | 61 |
bind_thm ("field_radd", radd_type RS field_rel_subset); |
437 | 62 |
|
63 |
(** Linearity **) |
|
64 |
||
2469 | 65 |
Addsimps [radd_Inl_iff, radd_Inr_iff, |
2493 | 66 |
radd_Inl_Inr_iff, radd_Inr_Inl_iff]; |
437 | 67 |
|
5067 | 68 |
Goalw [linear_def] |
437 | 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)); |
|
2469 | 71 |
by (ALLGOALS Asm_simp_tac); |
760 | 72 |
qed "linear_radd"; |
437 | 73 |
|
74 |
||
75 |
(** Well-foundedness **) |
|
76 |
||
5067 | 77 |
Goal |
437 | 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); |
|
4091 | 85 |
by (best_tac (claset() addSEs [raddE, bspec RS mp]) 2); |
437 | 86 |
(*Returning to main part of proof*) |
87 |
by (REPEAT_FIRST (eresolve_tac [sumE, ssubst])); |
|
3016 | 88 |
by (Blast_tac 1); |
437 | 89 |
by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1); |
4091 | 90 |
by (best_tac (claset() addSEs [raddE, bspec RS mp]) 1); |
760 | 91 |
qed "wf_on_radd"; |
437 | 92 |
|
5067 | 93 |
Goal |
437 | 94 |
"!!r s. [| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))"; |
4091 | 95 |
by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1); |
437 | 96 |
by (rtac (field_radd RSN (2, wf_on_subset_A)) 1); |
97 |
by (REPEAT (ares_tac [wf_on_radd] 1)); |
|
760 | 98 |
qed "wf_radd"; |
437 | 99 |
|
5067 | 100 |
Goal |
437 | 101 |
"!!r s. [| well_ord(A,r); well_ord(B,s) |] ==> \ |
102 |
\ well_ord(A+B, radd(A,r,B,s))"; |
|
103 |
by (rtac well_ordI 1); |
|
4091 | 104 |
by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_radd]) 1); |
437 | 105 |
by (asm_full_simp_tac |
4091 | 106 |
(simpset() addsimps [well_ord_def, tot_ord_def, linear_radd]) 1); |
760 | 107 |
qed "well_ord_radd"; |
437 | 108 |
|
859 | 109 |
(** An ord_iso congruence law **) |
110 |
||
5067 | 111 |
Goal |
859 | 112 |
"!!f g. [| f: bij(A,C); g: bij(B,D) |] ==> \ |
113 |
\ (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)"; |
|
114 |
by (res_inst_tac |
|
115 |
[("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(g)`y))")] |
|
116 |
lam_bijective 1); |
|
4091 | 117 |
by (safe_tac (claset() addSEs [sumE])); |
2469 | 118 |
by (ALLGOALS (asm_simp_tac bij_inverse_ss)); |
859 | 119 |
qed "sum_bij"; |
120 |
||
5067 | 121 |
Goalw [ord_iso_def] |
1461 | 122 |
"!!r s. [| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ==> \ |
123 |
\ (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) \ |
|
859 | 124 |
\ : ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))"; |
4091 | 125 |
by (safe_tac (claset() addSIs [sum_bij])); |
859 | 126 |
(*Do the beta-reductions now*) |
2469 | 127 |
by (ALLGOALS (Asm_full_simp_tac)); |
4152 | 128 |
by Safe_tac; |
859 | 129 |
(*8 subgoals!*) |
130 |
by (ALLGOALS |
|
131 |
(asm_full_simp_tac |
|
4091 | 132 |
(simpset() addcongs [conj_cong] addsimps [bij_is_fun RS apply_type]))); |
859 | 133 |
qed "sum_ord_iso_cong"; |
134 |
||
135 |
(*Could we prove an ord_iso result? Perhaps |
|
136 |
ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *) |
|
5067 | 137 |
Goal |
1461 | 138 |
"!!A B. A Int B = 0 ==> \ |
3840 | 139 |
\ (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)"; |
859 | 140 |
by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")] |
141 |
lam_bijective 1); |
|
4091 | 142 |
by (blast_tac (claset() addSIs [if_type]) 2); |
859 | 143 |
by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1)); |
4152 | 144 |
by Safe_tac; |
5137 | 145 |
by (ALLGOALS Asm_simp_tac); |
4091 | 146 |
by (blast_tac (claset() addEs [equalityE]) 1); |
859 | 147 |
qed "sum_disjoint_bij"; |
148 |
||
149 |
(** Associativity **) |
|
150 |
||
5067 | 151 |
Goal |
3840 | 152 |
"(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \ |
859 | 153 |
\ : bij((A+B)+C, A+(B+C))"; |
3840 | 154 |
by (res_inst_tac [("d", "case(%x. Inl(Inl(x)), case(%x. Inl(Inr(x)), Inr))")] |
859 | 155 |
lam_bijective 1); |
4091 | 156 |
by (ALLGOALS (asm_simp_tac (simpset() setloop etac sumE))); |
859 | 157 |
qed "sum_assoc_bij"; |
158 |
||
5067 | 159 |
Goal |
3840 | 160 |
"(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \ |
1461 | 161 |
\ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), \ |
859 | 162 |
\ A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))"; |
163 |
by (resolve_tac [sum_assoc_bij RS ord_isoI] 1); |
|
164 |
by (REPEAT_FIRST (etac sumE)); |
|
2469 | 165 |
by (ALLGOALS Asm_simp_tac); |
859 | 166 |
qed "sum_assoc_ord_iso"; |
167 |
||
437 | 168 |
|
169 |
(**** Multiplication of relations -- lexicographic product ****) |
|
170 |
||
171 |
(** Rewrite rule. Can be used to obtain introduction rules **) |
|
172 |
||
5067 | 173 |
Goalw [rmult_def] |
1461 | 174 |
"!!r s. <<a',b'>, <a,b>> : rmult(A,r,B,s) <-> \ |
175 |
\ (<a',a>: r & a':A & a:A & b': B & b: B) | \ |
|
437 | 176 |
\ (<b',b>: s & a'=a & a:A & b': B & b: B)"; |
2925 | 177 |
by (Blast_tac 1); |
760 | 178 |
qed "rmult_iff"; |
437 | 179 |
|
2469 | 180 |
Addsimps [rmult_iff]; |
181 |
||
437 | 182 |
val major::prems = goal OrderArith.thy |
1461 | 183 |
"[| <<a',b'>, <a,b>> : rmult(A,r,B,s); \ |
184 |
\ [| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q; \ |
|
185 |
\ [| <b',b>: s; a:A; a'=a; b':B; b:B |] ==> Q \ |
|
437 | 186 |
\ |] ==> Q"; |
187 |
by (rtac (major RS (rmult_iff RS iffD1) RS disjE) 1); |
|
188 |
by (DEPTH_SOLVE (eresolve_tac ([asm_rl, conjE] @ prems) 1)); |
|
760 | 189 |
qed "rmultE"; |
437 | 190 |
|
191 |
(** Type checking **) |
|
192 |
||
5067 | 193 |
Goalw [rmult_def] "rmult(A,r,B,s) <= (A*B) * (A*B)"; |
437 | 194 |
by (rtac Collect_subset 1); |
760 | 195 |
qed "rmult_type"; |
437 | 196 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
770
diff
changeset
|
197 |
bind_thm ("field_rmult", (rmult_type RS field_rel_subset)); |
437 | 198 |
|
199 |
(** Linearity **) |
|
200 |
||
201 |
val [lina,linb] = goal OrderArith.thy |
|
202 |
"[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"; |
|
203 |
by (rewtac linear_def); (*Note! the premises are NOT rewritten*) |
|
204 |
by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac SigmaE)); |
|
2469 | 205 |
by (Asm_simp_tac 1); |
437 | 206 |
by (res_inst_tac [("x","xa"), ("y","xb")] (lina RS linearE) 1); |
207 |
by (res_inst_tac [("x","ya"), ("y","yb")] (linb RS linearE) 4); |
|
2925 | 208 |
by (REPEAT_SOME (Blast_tac)); |
760 | 209 |
qed "linear_rmult"; |
437 | 210 |
|
211 |
||
212 |
(** Well-foundedness **) |
|
213 |
||
5067 | 214 |
Goal |
437 | 215 |
"!!r s. [| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))"; |
216 |
by (rtac wf_onI2 1); |
|
217 |
by (etac SigmaE 1); |
|
218 |
by (etac ssubst 1); |
|
219 |
by (subgoal_tac "ALL b:B. <x,b>: Ba" 1); |
|
2925 | 220 |
by (Blast_tac 1); |
437 | 221 |
by (eres_inst_tac [("a","x")] wf_on_induct 1 THEN assume_tac 1); |
222 |
by (rtac ballI 1); |
|
223 |
by (eres_inst_tac [("a","b")] wf_on_induct 1 THEN assume_tac 1); |
|
4091 | 224 |
by (best_tac (claset() addSEs [rmultE, bspec RS mp]) 1); |
760 | 225 |
qed "wf_on_rmult"; |
437 | 226 |
|
227 |
||
5067 | 228 |
Goal |
437 | 229 |
"!!r s. [| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))"; |
4091 | 230 |
by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1); |
437 | 231 |
by (rtac (field_rmult RSN (2, wf_on_subset_A)) 1); |
232 |
by (REPEAT (ares_tac [wf_on_rmult] 1)); |
|
760 | 233 |
qed "wf_rmult"; |
437 | 234 |
|
5067 | 235 |
Goal |
437 | 236 |
"!!r s. [| well_ord(A,r); well_ord(B,s) |] ==> \ |
237 |
\ well_ord(A*B, rmult(A,r,B,s))"; |
|
238 |
by (rtac well_ordI 1); |
|
4091 | 239 |
by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_rmult]) 1); |
437 | 240 |
by (asm_full_simp_tac |
4091 | 241 |
(simpset() addsimps [well_ord_def, tot_ord_def, linear_rmult]) 1); |
760 | 242 |
qed "well_ord_rmult"; |
437 | 243 |
|
244 |
||
859 | 245 |
(** An ord_iso congruence law **) |
246 |
||
5067 | 247 |
Goal |
859 | 248 |
"!!f g. [| f: bij(A,C); g: bij(B,D) |] ==> \ |
1095
6d0aad5f50a5
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
859
diff
changeset
|
249 |
\ (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)"; |
6d0aad5f50a5
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
859
diff
changeset
|
250 |
by (res_inst_tac [("d", "%<x,y>. <converse(f)`x, converse(g)`y>")] |
859 | 251 |
lam_bijective 1); |
4152 | 252 |
by Safe_tac; |
859 | 253 |
by (ALLGOALS (asm_simp_tac bij_inverse_ss)); |
254 |
qed "prod_bij"; |
|
255 |
||
5067 | 256 |
Goalw [ord_iso_def] |
1461 | 257 |
"!!r s. [| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ==> \ |
258 |
\ (lam <x,y>:A*B. <f`x, g`y>) \ |
|
859 | 259 |
\ : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))"; |
4091 | 260 |
by (safe_tac (claset() addSIs [prod_bij])); |
859 | 261 |
by (ALLGOALS |
4091 | 262 |
(asm_full_simp_tac (simpset() addsimps [bij_is_fun RS apply_type]))); |
2925 | 263 |
by (Blast_tac 1); |
4091 | 264 |
by (blast_tac (claset() addIs [bij_is_inj RS inj_apply_equality]) 1); |
859 | 265 |
qed "prod_ord_iso_cong"; |
266 |
||
5067 | 267 |
Goal "(lam z:A. <x,z>) : bij(A, {x}*A)"; |
859 | 268 |
by (res_inst_tac [("d", "snd")] lam_bijective 1); |
4152 | 269 |
by Safe_tac; |
2469 | 270 |
by (ALLGOALS Asm_simp_tac); |
859 | 271 |
qed "singleton_prod_bij"; |
272 |
||
273 |
(*Used??*) |
|
5067 | 274 |
Goal |
1461 | 275 |
"!!x xr. well_ord({x},xr) ==> \ |
859 | 276 |
\ (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))"; |
277 |
by (resolve_tac [singleton_prod_bij RS ord_isoI] 1); |
|
2469 | 278 |
by (Asm_simp_tac 1); |
4091 | 279 |
by (blast_tac (claset() addEs [well_ord_is_wf RS wf_on_not_refl RS notE]) 1); |
859 | 280 |
qed "singleton_prod_ord_iso"; |
281 |
||
282 |
(*Here we build a complicated function term, then simplify it using |
|
283 |
case_cong, id_conv, comp_lam, case_case.*) |
|
5067 | 284 |
Goal |
859 | 285 |
"!!a. a~:C ==> \ |
3840 | 286 |
\ (lam x:C*B + D. case(%x. x, %y.<a,y>, x)) \ |
859 | 287 |
\ : bij(C*B + D, C*B Un {a}*D)"; |
1461 | 288 |
by (rtac subst_elem 1); |
859 | 289 |
by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1); |
1461 | 290 |
by (rtac singleton_prod_bij 1); |
291 |
by (rtac sum_disjoint_bij 1); |
|
2925 | 292 |
by (Blast_tac 1); |
4091 | 293 |
by (asm_simp_tac (simpset() addcongs [case_cong] addsimps [id_conv]) 1); |
859 | 294 |
by (resolve_tac [comp_lam RS trans RS sym] 1); |
4091 | 295 |
by (fast_tac (claset() addSEs [case_type]) 1); |
296 |
by (asm_simp_tac (simpset() addsimps [case_case]) 1); |
|
859 | 297 |
qed "prod_sum_singleton_bij"; |
298 |
||
5067 | 299 |
Goal |
859 | 300 |
"!!A. [| a:A; well_ord(A,r) |] ==> \ |
3840 | 301 |
\ (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x)) \ |
1461 | 302 |
\ : ord_iso(pred(A,a,r)*B + pred(B,b,s), \ |
303 |
\ radd(A*B, rmult(A,r,B,s), B, s), \ |
|
859 | 304 |
\ pred(A,a,r)*B Un {a}*pred(B,b,s), rmult(A,r,B,s))"; |
305 |
by (resolve_tac [prod_sum_singleton_bij RS ord_isoI] 1); |
|
306 |
by (asm_simp_tac |
|
4091 | 307 |
(simpset() addsimps [pred_iff, well_ord_is_wf RS wf_on_not_refl]) 1); |
2469 | 308 |
by (Asm_simp_tac 1); |
859 | 309 |
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, predE])); |
3016 | 310 |
by (ALLGOALS Asm_simp_tac); |
4091 | 311 |
by (ALLGOALS (blast_tac (claset() addEs [well_ord_is_wf RS wf_on_asym]))); |
859 | 312 |
qed "prod_sum_singleton_ord_iso"; |
313 |
||
314 |
(** Distributive law **) |
|
315 |
||
5067 | 316 |
Goal |
3840 | 317 |
"(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \ |
859 | 318 |
\ : bij((A+B)*C, (A*C)+(B*C))"; |
319 |
by (res_inst_tac |
|
1095
6d0aad5f50a5
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
859
diff
changeset
|
320 |
[("d", "case(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1); |
4091 | 321 |
by (safe_tac (claset() addSEs [sumE])); |
2469 | 322 |
by (ALLGOALS Asm_simp_tac); |
859 | 323 |
qed "sum_prod_distrib_bij"; |
324 |
||
5067 | 325 |
Goal |
3840 | 326 |
"(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \ |
859 | 327 |
\ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \ |
328 |
\ (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"; |
|
329 |
by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1); |
|
330 |
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE])); |
|
3016 | 331 |
by (ALLGOALS Asm_simp_tac); |
859 | 332 |
qed "sum_prod_distrib_ord_iso"; |
333 |
||
334 |
(** Associativity **) |
|
335 |
||
5067 | 336 |
Goal |
1095
6d0aad5f50a5
Changed some definitions and proofs to use pattern-matching.
lcp
parents:
859
diff
changeset
|
337 |
"(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 pattern-matching.
lcp
parents:
859
diff
changeset
|
338 |
by (res_inst_tac [("d", "%<x, <y,z>>. <<x,y>, z>")] lam_bijective 1); |
4091 | 339 |
by (ALLGOALS (asm_simp_tac (simpset() setloop etac SigmaE))); |
859 | 340 |
qed "prod_assoc_bij"; |
341 |
||
5067 | 342 |
Goal |
1461 | 343 |
"(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) \ |
344 |
\ : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), \ |
|
859 | 345 |
\ A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"; |
346 |
by (resolve_tac [prod_assoc_bij RS ord_isoI] 1); |
|
347 |
by (REPEAT_FIRST (eresolve_tac [SigmaE, ssubst])); |
|
2469 | 348 |
by (Asm_simp_tac 1); |
2925 | 349 |
by (Blast_tac 1); |
859 | 350 |
qed "prod_assoc_ord_iso"; |
351 |
||
437 | 352 |
(**** Inverse image of a relation ****) |
353 |
||
354 |
(** Rewrite rule **) |
|
355 |
||
5067 | 356 |
Goalw [rvimage_def] |
437 | 357 |
"<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A"; |
2925 | 358 |
by (Blast_tac 1); |
760 | 359 |
qed "rvimage_iff"; |
437 | 360 |
|
361 |
(** Type checking **) |
|
362 |
||
5067 | 363 |
Goalw [rvimage_def] "rvimage(A,f,r) <= A*A"; |
437 | 364 |
by (rtac Collect_subset 1); |
760 | 365 |
qed "rvimage_type"; |
437 | 366 |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
770
diff
changeset
|
367 |
bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset)); |
437 | 368 |
|
5067 | 369 |
Goalw [rvimage_def] |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
370 |
"rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))"; |
2925 | 371 |
by (Blast_tac 1); |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
372 |
qed "rvimage_converse"; |
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
373 |
|
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
374 |
|
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
375 |
(** Partial Ordering Properties **) |
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
376 |
|
5067 | 377 |
Goalw [irrefl_def, rvimage_def] |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
378 |
"!!A B. [| f: inj(A,B); irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))"; |
4091 | 379 |
by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1); |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
380 |
qed "irrefl_rvimage"; |
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
381 |
|
5067 | 382 |
Goalw [trans_on_def, rvimage_def] |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
383 |
"!!A B. [| f: inj(A,B); trans[B](r) |] ==> trans[A](rvimage(A,f,r))"; |
4091 | 384 |
by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1); |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
385 |
qed "trans_on_rvimage"; |
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
386 |
|
5067 | 387 |
Goalw [part_ord_def] |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
388 |
"!!A B. [| f: inj(A,B); part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))"; |
4091 | 389 |
by (blast_tac (claset() addSIs [irrefl_rvimage, trans_on_rvimage]) 1); |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
390 |
qed "part_ord_rvimage"; |
437 | 391 |
|
392 |
(** Linearity **) |
|
393 |
||
394 |
val [finj,lin] = goalw OrderArith.thy [inj_def] |
|
395 |
"[| f: inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))"; |
|
396 |
by (rewtac linear_def); (*Note! the premises are NOT rewritten*) |
|
397 |
by (REPEAT_FIRST (ares_tac [ballI])); |
|
4091 | 398 |
by (asm_simp_tac (simpset() addsimps [rvimage_iff]) 1); |
437 | 399 |
by (cut_facts_tac [finj] 1); |
400 |
by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1); |
|
4091 | 401 |
by (REPEAT_SOME (blast_tac (claset() addIs [apply_funtype]))); |
760 | 402 |
qed "linear_rvimage"; |
437 | 403 |
|
5067 | 404 |
Goalw [tot_ord_def] |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
405 |
"!!A B. [| f: inj(A,B); tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))"; |
4091 | 406 |
by (blast_tac (claset() addSIs [part_ord_rvimage, linear_rvimage]) 1); |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
407 |
qed "tot_ord_rvimage"; |
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
408 |
|
437 | 409 |
|
410 |
(** Well-foundedness **) |
|
411 |
||
5067 | 412 |
Goal |
437 | 413 |
"!!r. [| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))"; |
414 |
by (rtac wf_onI2 1); |
|
415 |
by (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba" 1); |
|
2925 | 416 |
by (Blast_tac 1); |
437 | 417 |
by (eres_inst_tac [("a","f`y")] wf_on_induct 1); |
4091 | 418 |
by (blast_tac (claset() addSIs [apply_funtype]) 1); |
419 |
by (blast_tac (claset() addSIs [apply_funtype] |
|
2925 | 420 |
addSDs [rvimage_iff RS iffD1]) 1); |
760 | 421 |
qed "wf_on_rvimage"; |
437 | 422 |
|
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
423 |
(*Note that we need only wf[A](...) and linear(A,...) to get the result!*) |
5067 | 424 |
Goal |
437 | 425 |
"!!r. [| f: inj(A,B); well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))"; |
426 |
by (rtac well_ordI 1); |
|
427 |
by (rewrite_goals_tac [well_ord_def, tot_ord_def]); |
|
4091 | 428 |
by (blast_tac (claset() addSIs [wf_on_rvimage, inj_is_fun]) 1); |
429 |
by (blast_tac (claset() addSIs [linear_rvimage]) 1); |
|
760 | 430 |
qed "well_ord_rvimage"; |
815 | 431 |
|
5067 | 432 |
Goalw [ord_iso_def] |
815 | 433 |
"!!A B. f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)"; |
4091 | 434 |
by (asm_full_simp_tac (simpset() addsimps [rvimage_iff]) 1); |
815 | 435 |
qed "ord_iso_rvimage"; |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
436 |
|
5067 | 437 |
Goalw [ord_iso_def, rvimage_def] |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
438 |
"!!A B. f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A"; |
3016 | 439 |
by (Blast_tac 1); |
835
313ac9b513f1
Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
lcp
parents:
815
diff
changeset
|
440 |
qed "ord_iso_rvimage_eq"; |