44 "well_ord(A,r) == tot_ord(A,r) & wf[A](r)" |
44 "well_ord(A,r) == tot_ord(A,r) & wf[A](r)" |
45 |
45 |
46 definition |
46 definition |
47 mono_map :: "[i,i,i,i]=>i" (*Order-preserving maps*) where |
47 mono_map :: "[i,i,i,i]=>i" (*Order-preserving maps*) where |
48 "mono_map(A,r,B,s) == |
48 "mono_map(A,r,B,s) == |
49 {f: A->B. \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longrightarrow> <f`x,f`y>:s}" |
49 {f \<in> A->B. \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longrightarrow> <f`x,f`y>:s}" |
50 |
50 |
51 definition |
51 definition |
52 ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*) where |
52 ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*) where |
53 "ord_iso(A,r,B,s) == |
53 "ord_iso(A,r,B,s) == |
54 {f: bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longleftrightarrow> <f`x,f`y>:s}" |
54 {f \<in> bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longleftrightarrow> <f`x,f`y>:s}" |
55 |
55 |
56 definition |
56 definition |
57 pred :: "[i,i,i]=>i" (*Set of predecessors*) where |
57 pred :: "[i,i,i]=>i" (*Set of predecessors*) where |
58 "pred(A,x,r) == {y:A. <y,x>:r}" |
58 "pred(A,x,r) == {y \<in> A. <y,x>:r}" |
59 |
59 |
60 definition |
60 definition |
61 ord_iso_map :: "[i,i,i,i]=>i" (*Construction for linearity theorem*) where |
61 ord_iso_map :: "[i,i,i,i]=>i" (*Construction for linearity theorem*) where |
62 "ord_iso_map(A,r,B,s) == |
62 "ord_iso_map(A,r,B,s) == |
63 \<Union>x\<in>A. \<Union>y\<in>B. \<Union>f \<in> ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}" |
63 \<Union>x\<in>A. \<Union>y\<in>B. \<Union>f \<in> ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}" |
64 |
64 |
65 definition |
65 definition |
66 first :: "[i, i, i] => o" where |
66 first :: "[i, i, i] => o" where |
67 "first(u, X, R) == u:X & (\<forall>v\<in>X. v\<noteq>u \<longrightarrow> <u,v> \<in> R)" |
67 "first(u, X, R) == u \<in> X & (\<forall>v\<in>X. v\<noteq>u \<longrightarrow> <u,v> \<in> R)" |
68 |
68 |
69 |
69 |
70 notation (xsymbols) |
70 notation (xsymbols) |
71 ord_iso ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51) |
71 ord_iso ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51) |
72 |
72 |
105 by (unfold well_ord_def tot_ord_def, blast) |
105 by (unfold well_ord_def tot_ord_def, blast) |
106 |
106 |
107 |
107 |
108 (** Derived rules for pred(A,x,r) **) |
108 (** Derived rules for pred(A,x,r) **) |
109 |
109 |
110 lemma pred_iff: "y \<in> pred(A,x,r) \<longleftrightarrow> <y,x>:r & y:A" |
110 lemma pred_iff: "y \<in> pred(A,x,r) \<longleftrightarrow> <y,x>:r & y \<in> A" |
111 by (unfold pred_def, blast) |
111 by (unfold pred_def, blast) |
112 |
112 |
113 lemmas predI = conjI [THEN pred_iff [THEN iffD2]] |
113 lemmas predI = conjI [THEN pred_iff [THEN iffD2]] |
114 |
114 |
115 lemma predE: "[| y: pred(A,x,r); [| y:A; <y,x>:r |] ==> P |] ==> P" |
115 lemma predE: "[| y \<in> pred(A,x,r); [| y \<in> A; <y,x>:r |] ==> P |] ==> P" |
116 by (simp add: pred_def) |
116 by (simp add: pred_def) |
117 |
117 |
118 lemma pred_subset_under: "pred(A,x,r) \<subseteq> r -`` {x}" |
118 lemma pred_subset_under: "pred(A,x,r) \<subseteq> r -`` {x}" |
119 by (simp add: pred_def, blast) |
119 by (simp add: pred_def, blast) |
120 |
120 |
124 lemma pred_pred_eq: |
124 lemma pred_pred_eq: |
125 "pred(pred(A,x,r), y, r) = pred(A,x,r) \<inter> pred(A,y,r)" |
125 "pred(pred(A,x,r), y, r) = pred(A,x,r) \<inter> pred(A,y,r)" |
126 by (simp add: pred_def, blast) |
126 by (simp add: pred_def, blast) |
127 |
127 |
128 lemma trans_pred_pred_eq: |
128 lemma trans_pred_pred_eq: |
129 "[| trans[A](r); <y,x>:r; x:A; y:A |] |
129 "[| trans[A](r); <y,x>:r; x \<in> A; y \<in> A |] |
130 ==> pred(pred(A,x,r), y, r) = pred(A,y,r)" |
130 ==> pred(pred(A,x,r), y, r) = pred(A,y,r)" |
131 by (unfold trans_on_def pred_def, blast) |
131 by (unfold trans_on_def pred_def, blast) |
132 |
132 |
133 |
133 |
134 subsection{*Restricting an Ordering's Domain*} |
134 subsection{*Restricting an Ordering's Domain*} |
242 |
242 |
243 text{*Suppes calls them "similarities"*} |
243 text{*Suppes calls them "similarities"*} |
244 |
244 |
245 (** Order-preserving (monotone) maps **) |
245 (** Order-preserving (monotone) maps **) |
246 |
246 |
247 lemma mono_map_is_fun: "f: mono_map(A,r,B,s) ==> f: A->B" |
247 lemma mono_map_is_fun: "f \<in> mono_map(A,r,B,s) ==> f \<in> A->B" |
248 by (simp add: mono_map_def) |
248 by (simp add: mono_map_def) |
249 |
249 |
250 lemma mono_map_is_inj: |
250 lemma mono_map_is_inj: |
251 "[| linear(A,r); wf[B](s); f: mono_map(A,r,B,s) |] ==> f: inj(A,B)" |
251 "[| linear(A,r); wf[B](s); f \<in> mono_map(A,r,B,s) |] ==> f \<in> inj(A,B)" |
252 apply (unfold mono_map_def inj_def, clarify) |
252 apply (unfold mono_map_def inj_def, clarify) |
253 apply (erule_tac x=w and y=x in linearE, assumption+) |
253 apply (erule_tac x=w and y=x in linearE, assumption+) |
254 apply (force intro: apply_type dest: wf_on_not_refl)+ |
254 apply (force intro: apply_type dest: wf_on_not_refl)+ |
255 done |
255 done |
256 |
256 |
257 lemma ord_isoI: |
257 lemma ord_isoI: |
258 "[| f: bij(A, B); |
258 "[| f \<in> bij(A, B); |
259 !!x y. [| x:A; y:A |] ==> <x, y> \<in> r \<longleftrightarrow> <f`x, f`y> \<in> s |] |
259 !!x y. [| x \<in> A; y \<in> A |] ==> <x, y> \<in> r \<longleftrightarrow> <f`x, f`y> \<in> s |] |
260 ==> f: ord_iso(A,r,B,s)" |
260 ==> f \<in> ord_iso(A,r,B,s)" |
261 by (simp add: ord_iso_def) |
261 by (simp add: ord_iso_def) |
262 |
262 |
263 lemma ord_iso_is_mono_map: |
263 lemma ord_iso_is_mono_map: |
264 "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)" |
264 "f \<in> ord_iso(A,r,B,s) ==> f \<in> mono_map(A,r,B,s)" |
265 apply (simp add: ord_iso_def mono_map_def) |
265 apply (simp add: ord_iso_def mono_map_def) |
266 apply (blast dest!: bij_is_fun) |
266 apply (blast dest!: bij_is_fun) |
267 done |
267 done |
268 |
268 |
269 lemma ord_iso_is_bij: |
269 lemma ord_iso_is_bij: |
270 "f: ord_iso(A,r,B,s) ==> f: bij(A,B)" |
270 "f \<in> ord_iso(A,r,B,s) ==> f \<in> bij(A,B)" |
271 by (simp add: ord_iso_def) |
271 by (simp add: ord_iso_def) |
272 |
272 |
273 (*Needed? But ord_iso_converse is!*) |
273 (*Needed? But ord_iso_converse is!*) |
274 lemma ord_iso_apply: |
274 lemma ord_iso_apply: |
275 "[| f: ord_iso(A,r,B,s); <x,y>: r; x:A; y:A |] ==> <f`x, f`y> \<in> s" |
275 "[| f \<in> ord_iso(A,r,B,s); <x,y>: r; x \<in> A; y \<in> A |] ==> <f`x, f`y> \<in> s" |
276 by (simp add: ord_iso_def) |
276 by (simp add: ord_iso_def) |
277 |
277 |
278 lemma ord_iso_converse: |
278 lemma ord_iso_converse: |
279 "[| f: ord_iso(A,r,B,s); <x,y>: s; x:B; y:B |] |
279 "[| f \<in> ord_iso(A,r,B,s); <x,y>: s; x \<in> B; y \<in> B |] |
280 ==> <converse(f) ` x, converse(f) ` y> \<in> r" |
280 ==> <converse(f) ` x, converse(f) ` y> \<in> r" |
281 apply (simp add: ord_iso_def, clarify) |
281 apply (simp add: ord_iso_def, clarify) |
282 apply (erule bspec [THEN bspec, THEN iffD2]) |
282 apply (erule bspec [THEN bspec, THEN iffD2]) |
283 apply (erule asm_rl bij_converse_bij [THEN bij_is_fun, THEN apply_type])+ |
283 apply (erule asm_rl bij_converse_bij [THEN bij_is_fun, THEN apply_type])+ |
284 apply (auto simp add: right_inverse_bij) |
284 apply (auto simp add: right_inverse_bij) |
290 (*Reflexivity of similarity*) |
290 (*Reflexivity of similarity*) |
291 lemma ord_iso_refl: "id(A): ord_iso(A,r,A,r)" |
291 lemma ord_iso_refl: "id(A): ord_iso(A,r,A,r)" |
292 by (rule id_bij [THEN ord_isoI], simp) |
292 by (rule id_bij [THEN ord_isoI], simp) |
293 |
293 |
294 (*Symmetry of similarity*) |
294 (*Symmetry of similarity*) |
295 lemma ord_iso_sym: "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)" |
295 lemma ord_iso_sym: "f \<in> ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)" |
296 apply (simp add: ord_iso_def) |
296 apply (simp add: ord_iso_def) |
297 apply (auto simp add: right_inverse_bij bij_converse_bij |
297 apply (auto simp add: right_inverse_bij bij_converse_bij |
298 bij_is_fun [THEN apply_funtype]) |
298 bij_is_fun [THEN apply_funtype]) |
299 done |
299 done |
300 |
300 |
301 (*Transitivity of similarity*) |
301 (*Transitivity of similarity*) |
302 lemma mono_map_trans: |
302 lemma mono_map_trans: |
303 "[| g: mono_map(A,r,B,s); f: mono_map(B,s,C,t) |] |
303 "[| g \<in> mono_map(A,r,B,s); f \<in> mono_map(B,s,C,t) |] |
304 ==> (f O g): mono_map(A,r,C,t)" |
304 ==> (f O g): mono_map(A,r,C,t)" |
305 apply (unfold mono_map_def) |
305 apply (unfold mono_map_def) |
306 apply (auto simp add: comp_fun) |
306 apply (auto simp add: comp_fun) |
307 done |
307 done |
308 |
308 |
309 (*Transitivity of similarity: the order-isomorphism relation*) |
309 (*Transitivity of similarity: the order-isomorphism relation*) |
310 lemma ord_iso_trans: |
310 lemma ord_iso_trans: |
311 "[| g: ord_iso(A,r,B,s); f: ord_iso(B,s,C,t) |] |
311 "[| g \<in> ord_iso(A,r,B,s); f \<in> ord_iso(B,s,C,t) |] |
312 ==> (f O g): ord_iso(A,r,C,t)" |
312 ==> (f O g): ord_iso(A,r,C,t)" |
313 apply (unfold ord_iso_def, clarify) |
313 apply (unfold ord_iso_def, clarify) |
314 apply (frule bij_is_fun [of f]) |
314 apply (frule bij_is_fun [of f]) |
315 apply (frule bij_is_fun [of g]) |
315 apply (frule bij_is_fun [of g]) |
316 apply (auto simp add: comp_bij) |
316 apply (auto simp add: comp_bij) |
317 done |
317 done |
318 |
318 |
319 (** Two monotone maps can make an order-isomorphism **) |
319 (** Two monotone maps can make an order-isomorphism **) |
320 |
320 |
321 lemma mono_ord_isoI: |
321 lemma mono_ord_isoI: |
322 "[| f: mono_map(A,r,B,s); g: mono_map(B,s,A,r); |
322 "[| f \<in> mono_map(A,r,B,s); g \<in> mono_map(B,s,A,r); |
323 f O g = id(B); g O f = id(A) |] ==> f: ord_iso(A,r,B,s)" |
323 f O g = id(B); g O f = id(A) |] ==> f \<in> ord_iso(A,r,B,s)" |
324 apply (simp add: ord_iso_def mono_map_def, safe) |
324 apply (simp add: ord_iso_def mono_map_def, safe) |
325 apply (intro fg_imp_bijective, auto) |
325 apply (intro fg_imp_bijective, auto) |
326 apply (subgoal_tac "<g` (f`x), g` (f`y) > \<in> r") |
326 apply (subgoal_tac "<g` (f`x), g` (f`y) > \<in> r") |
327 apply (simp add: comp_eq_id_iff [THEN iffD1]) |
327 apply (simp add: comp_eq_id_iff [THEN iffD1]) |
328 apply (blast intro: apply_funtype) |
328 apply (blast intro: apply_funtype) |
329 done |
329 done |
330 |
330 |
331 lemma well_ord_mono_ord_isoI: |
331 lemma well_ord_mono_ord_isoI: |
332 "[| well_ord(A,r); well_ord(B,s); |
332 "[| well_ord(A,r); well_ord(B,s); |
333 f: mono_map(A,r,B,s); converse(f): mono_map(B,s,A,r) |] |
333 f \<in> mono_map(A,r,B,s); converse(f): mono_map(B,s,A,r) |] |
334 ==> f: ord_iso(A,r,B,s)" |
334 ==> f \<in> ord_iso(A,r,B,s)" |
335 apply (intro mono_ord_isoI, auto) |
335 apply (intro mono_ord_isoI, auto) |
336 apply (frule mono_map_is_fun [THEN fun_is_rel]) |
336 apply (frule mono_map_is_fun [THEN fun_is_rel]) |
337 apply (erule converse_converse [THEN subst], rule left_comp_inverse) |
337 apply (erule converse_converse [THEN subst], rule left_comp_inverse) |
338 apply (blast intro: left_comp_inverse mono_map_is_inj well_ord_is_linear |
338 apply (blast intro: left_comp_inverse mono_map_is_inj well_ord_is_linear |
339 well_ord_is_wf)+ |
339 well_ord_is_wf)+ |
341 |
341 |
342 |
342 |
343 (** Order-isomorphisms preserve the ordering's properties **) |
343 (** Order-isomorphisms preserve the ordering's properties **) |
344 |
344 |
345 lemma part_ord_ord_iso: |
345 lemma part_ord_ord_iso: |
346 "[| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)" |
346 "[| part_ord(B,s); f \<in> ord_iso(A,r,B,s) |] ==> part_ord(A,r)" |
347 apply (simp add: part_ord_def irrefl_def trans_on_def ord_iso_def) |
347 apply (simp add: part_ord_def irrefl_def trans_on_def ord_iso_def) |
348 apply (fast intro: bij_is_fun [THEN apply_type]) |
348 apply (fast intro: bij_is_fun [THEN apply_type]) |
349 done |
349 done |
350 |
350 |
351 lemma linear_ord_iso: |
351 lemma linear_ord_iso: |
352 "[| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)" |
352 "[| linear(B,s); f \<in> ord_iso(A,r,B,s) |] ==> linear(A,r)" |
353 apply (simp add: linear_def ord_iso_def, safe) |
353 apply (simp add: linear_def ord_iso_def, safe) |
354 apply (drule_tac x1 = "f`x" and x = "f`y" in bspec [THEN bspec]) |
354 apply (drule_tac x1 = "f`x" and x = "f`y" in bspec [THEN bspec]) |
355 apply (safe elim!: bij_is_fun [THEN apply_type]) |
355 apply (safe elim!: bij_is_fun [THEN apply_type]) |
356 apply (drule_tac t = "op ` (converse (f))" in subst_context) |
356 apply (drule_tac t = "op ` (converse (f))" in subst_context) |
357 apply (simp add: left_inverse_bij) |
357 apply (simp add: left_inverse_bij) |
358 done |
358 done |
359 |
359 |
360 lemma wf_on_ord_iso: |
360 lemma wf_on_ord_iso: |
361 "[| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)" |
361 "[| wf[B](s); f \<in> ord_iso(A,r,B,s) |] ==> wf[A](r)" |
362 apply (simp add: wf_on_def wf_def ord_iso_def, safe) |
362 apply (simp add: wf_on_def wf_def ord_iso_def, safe) |
363 apply (drule_tac x = "{f`z. z:Z \<inter> A}" in spec) |
363 apply (drule_tac x = "{f`z. z \<in> Z \<inter> A}" in spec) |
364 apply (safe intro!: equalityI) |
364 apply (safe intro!: equalityI) |
365 apply (blast dest!: equalityD1 intro: bij_is_fun [THEN apply_type])+ |
365 apply (blast dest!: equalityD1 intro: bij_is_fun [THEN apply_type])+ |
366 done |
366 done |
367 |
367 |
368 lemma well_ord_ord_iso: |
368 lemma well_ord_ord_iso: |
369 "[| well_ord(B,s); f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)" |
369 "[| well_ord(B,s); f \<in> ord_iso(A,r,B,s) |] ==> well_ord(A,r)" |
370 apply (unfold well_ord_def tot_ord_def) |
370 apply (unfold well_ord_def tot_ord_def) |
371 apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso) |
371 apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso) |
372 done |
372 done |
373 |
373 |
374 |
374 |
375 subsection{*Main results of Kunen, Chapter 1 section 6*} |
375 subsection{*Main results of Kunen, Chapter 1 section 6*} |
376 |
376 |
377 (*Inductive argument for Kunen's Lemma 6.1, etc. |
377 (*Inductive argument for Kunen's Lemma 6.1, etc. |
378 Simple proof from Halmos, page 72*) |
378 Simple proof from Halmos, page 72*) |
379 lemma well_ord_iso_subset_lemma: |
379 lemma well_ord_iso_subset_lemma: |
380 "[| well_ord(A,r); f: ord_iso(A,r, A',r); A'<= A; y: A |] |
380 "[| well_ord(A,r); f \<in> ord_iso(A,r, A',r); A'<= A; y \<in> A |] |
381 ==> ~ <f`y, y>: r" |
381 ==> ~ <f`y, y>: r" |
382 apply (simp add: well_ord_def ord_iso_def) |
382 apply (simp add: well_ord_def ord_iso_def) |
383 apply (elim conjE CollectE) |
383 apply (elim conjE CollectE) |
384 apply (rule_tac a=y in wf_on_induct, assumption+) |
384 apply (rule_tac a=y in wf_on_induct, assumption+) |
385 apply (blast dest: bij_is_fun [THEN apply_type]) |
385 apply (blast dest: bij_is_fun [THEN apply_type]) |
386 done |
386 done |
387 |
387 |
388 (*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment |
388 (*Kunen's Lemma 6.1 \<in> there's no order-isomorphism to an initial segment |
389 of a well-ordering*) |
389 of a well-ordering*) |
390 lemma well_ord_iso_predE: |
390 lemma well_ord_iso_predE: |
391 "[| well_ord(A,r); f \<in> ord_iso(A, r, pred(A,x,r), r); x:A |] ==> P" |
391 "[| well_ord(A,r); f \<in> ord_iso(A, r, pred(A,x,r), r); x \<in> A |] ==> P" |
392 apply (insert well_ord_iso_subset_lemma [of A r f "pred(A,x,r)" x]) |
392 apply (insert well_ord_iso_subset_lemma [of A r f "pred(A,x,r)" x]) |
393 apply (simp add: pred_subset) |
393 apply (simp add: pred_subset) |
394 (*Now we know f`x < x *) |
394 (*Now we know f`x < x *) |
395 apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) |
395 apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) |
396 (*Now we also know @{term"f`x \<in> pred(A,x,r)"}: contradiction! *) |
396 (*Now we also know @{term"f`x \<in> pred(A,x,r)"}: contradiction! *) |
398 done |
398 done |
399 |
399 |
400 (*Simple consequence of Lemma 6.1*) |
400 (*Simple consequence of Lemma 6.1*) |
401 lemma well_ord_iso_pred_eq: |
401 lemma well_ord_iso_pred_eq: |
402 "[| well_ord(A,r); f \<in> ord_iso(pred(A,a,r), r, pred(A,c,r), r); |
402 "[| well_ord(A,r); f \<in> ord_iso(pred(A,a,r), r, pred(A,c,r), r); |
403 a:A; c:A |] ==> a=c" |
403 a \<in> A; c \<in> A |] ==> a=c" |
404 apply (frule well_ord_is_trans_on) |
404 apply (frule well_ord_is_trans_on) |
405 apply (frule well_ord_is_linear) |
405 apply (frule well_ord_is_linear) |
406 apply (erule_tac x=a and y=c in linearE, assumption+) |
406 apply (erule_tac x=a and y=c in linearE, assumption+) |
407 apply (drule ord_iso_sym) |
407 apply (drule ord_iso_sym) |
408 (*two symmetric cases*) |
408 (*two symmetric cases*) |
411 simp add: trans_pred_pred_eq) |
411 simp add: trans_pred_pred_eq) |
412 done |
412 done |
413 |
413 |
414 (*Does not assume r is a wellordering!*) |
414 (*Does not assume r is a wellordering!*) |
415 lemma ord_iso_image_pred: |
415 lemma ord_iso_image_pred: |
416 "[|f \<in> ord_iso(A,r,B,s); a:A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)" |
416 "[|f \<in> ord_iso(A,r,B,s); a \<in> A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)" |
417 apply (unfold ord_iso_def pred_def) |
417 apply (unfold ord_iso_def pred_def) |
418 apply (erule CollectE) |
418 apply (erule CollectE) |
419 apply (simp (no_asm_simp) add: image_fun [OF bij_is_fun Collect_subset]) |
419 apply (simp (no_asm_simp) add: image_fun [OF bij_is_fun Collect_subset]) |
420 apply (rule equalityI) |
420 apply (rule equalityI) |
421 apply (safe elim!: bij_is_fun [THEN apply_type]) |
421 apply (safe elim!: bij_is_fun [THEN apply_type]) |
432 done |
432 done |
433 |
433 |
434 (*But in use, A and B may themselves be initial segments. Then use |
434 (*But in use, A and B may themselves be initial segments. Then use |
435 trans_pred_pred_eq to simplify the pred(pred...) terms. See just below.*) |
435 trans_pred_pred_eq to simplify the pred(pred...) terms. See just below.*) |
436 lemma ord_iso_restrict_pred: |
436 lemma ord_iso_restrict_pred: |
437 "[| f \<in> ord_iso(A,r,B,s); a:A |] |
437 "[| f \<in> ord_iso(A,r,B,s); a \<in> A |] |
438 ==> restrict(f, pred(A,a,r)) \<in> ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)" |
438 ==> restrict(f, pred(A,a,r)) \<in> ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)" |
439 apply (simp add: ord_iso_image_pred [symmetric]) |
439 apply (simp add: ord_iso_image_pred [symmetric]) |
440 apply (blast intro: ord_iso_restrict_image elim: predE) |
440 apply (blast intro: ord_iso_restrict_image elim: predE) |
441 done |
441 done |
442 |
442 |
443 (*Tricky; a lot of forward proof!*) |
443 (*Tricky; a lot of forward proof!*) |
444 lemma well_ord_iso_preserving: |
444 lemma well_ord_iso_preserving: |
445 "[| well_ord(A,r); well_ord(B,s); <a,c>: r; |
445 "[| well_ord(A,r); well_ord(B,s); <a,c>: r; |
446 f \<in> ord_iso(pred(A,a,r), r, pred(B,b,s), s); |
446 f \<in> ord_iso(pred(A,a,r), r, pred(B,b,s), s); |
447 g \<in> ord_iso(pred(A,c,r), r, pred(B,d,s), s); |
447 g \<in> ord_iso(pred(A,c,r), r, pred(B,d,s), s); |
448 a:A; c:A; b:B; d:B |] ==> <b,d>: s" |
448 a \<in> A; c \<in> A; b \<in> B; d \<in> B |] ==> <b,d>: s" |
449 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], (erule asm_rl predI predE)+) |
449 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], (erule asm_rl predI predE)+) |
450 apply (subgoal_tac "b = g`a") |
450 apply (subgoal_tac "b = g`a") |
451 apply (simp (no_asm_simp)) |
451 apply (simp (no_asm_simp)) |
452 apply (rule well_ord_iso_pred_eq, auto) |
452 apply (rule well_ord_iso_pred_eq, auto) |
453 apply (frule ord_iso_restrict_pred, (erule asm_rl predI)+) |
453 apply (frule ord_iso_restrict_pred, (erule asm_rl predI)+) |
520 \<in> mono_map(domain(ord_iso_map(A,r,B,s)), r, |
520 \<in> mono_map(domain(ord_iso_map(A,r,B,s)), r, |
521 range(ord_iso_map(A,r,B,s)), s)" |
521 range(ord_iso_map(A,r,B,s)), s)" |
522 apply (unfold mono_map_def) |
522 apply (unfold mono_map_def) |
523 apply (simp (no_asm_simp) add: ord_iso_map_fun) |
523 apply (simp (no_asm_simp) add: ord_iso_map_fun) |
524 apply safe |
524 apply safe |
525 apply (subgoal_tac "x:A & ya:A & y:B & yb:B") |
525 apply (subgoal_tac "x \<in> A & ya:A & y \<in> B & yb:B") |
526 apply (simp add: apply_equality [OF _ ord_iso_map_fun]) |
526 apply (simp add: apply_equality [OF _ ord_iso_map_fun]) |
527 apply (unfold ord_iso_map_def) |
527 apply (unfold ord_iso_map_def) |
528 apply (blast intro: well_ord_iso_preserving, blast) |
528 apply (blast intro: well_ord_iso_preserving, blast) |
529 done |
529 done |
530 |
530 |
543 |
543 |
544 |
544 |
545 (*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*) |
545 (*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*) |
546 lemma domain_ord_iso_map_subset: |
546 lemma domain_ord_iso_map_subset: |
547 "[| well_ord(A,r); well_ord(B,s); |
547 "[| well_ord(A,r); well_ord(B,s); |
548 a: A; a \<notin> domain(ord_iso_map(A,r,B,s)) |] |
548 a \<in> A; a \<notin> domain(ord_iso_map(A,r,B,s)) |] |
549 ==> domain(ord_iso_map(A,r,B,s)) \<subseteq> pred(A, a, r)" |
549 ==> domain(ord_iso_map(A,r,B,s)) \<subseteq> pred(A, a, r)" |
550 apply (unfold ord_iso_map_def) |
550 apply (unfold ord_iso_map_def) |
551 apply (safe intro!: predI) |
551 apply (safe intro!: predI) |
552 (*Case analysis on xa vs a in r *) |
552 (*Case analysis on xa vs a in r *) |
553 apply (simp (no_asm_simp)) |
553 apply (simp (no_asm_simp)) |