15 text {* We adopt the following convention: @{text ord} is used for |
14 text {* We adopt the following convention: @{text ord} is used for |
16 strict orders and @{text order} is used for their reflexive |
15 strict orders and @{text order} is used for their reflexive |
17 counterparts. *} |
16 counterparts. *} |
18 |
17 |
19 definition |
18 definition |
20 part_ord :: "[i,i]=>o" (*Strict partial ordering*) where |
19 part_ord :: "[i,i]=>o" (*Strict partial ordering*) where |
21 "part_ord(A,r) == irrefl(A,r) & trans[A](r)" |
20 "part_ord(A,r) == irrefl(A,r) & trans[A](r)" |
22 |
21 |
23 definition |
22 definition |
24 linear :: "[i,i]=>o" (*Strict total ordering*) where |
23 linear :: "[i,i]=>o" (*Strict total ordering*) where |
25 "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)" |
24 "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)" |
26 |
25 |
27 definition |
26 definition |
28 tot_ord :: "[i,i]=>o" (*Strict total ordering*) where |
27 tot_ord :: "[i,i]=>o" (*Strict total ordering*) where |
29 "tot_ord(A,r) == part_ord(A,r) & linear(A,r)" |
28 "tot_ord(A,r) == part_ord(A,r) & linear(A,r)" |
30 |
29 |
31 definition |
30 definition |
32 "preorder_on(A, r) \<equiv> refl(A, r) \<and> trans[A](r)" |
31 "preorder_on(A, r) \<equiv> refl(A, r) \<and> trans[A](r)" |
33 |
32 |
39 |
38 |
40 abbreviation |
39 abbreviation |
41 "Partial_order(r) \<equiv> partial_order_on(field(r), r)" |
40 "Partial_order(r) \<equiv> partial_order_on(field(r), r)" |
42 |
41 |
43 definition |
42 definition |
44 well_ord :: "[i,i]=>o" (*Well-ordering*) where |
43 well_ord :: "[i,i]=>o" (*Well-ordering*) where |
45 "well_ord(A,r) == tot_ord(A,r) & wf[A](r)" |
44 "well_ord(A,r) == tot_ord(A,r) & wf[A](r)" |
46 |
45 |
47 definition |
46 definition |
48 mono_map :: "[i,i,i,i]=>i" (*Order-preserving maps*) where |
47 mono_map :: "[i,i,i,i]=>i" (*Order-preserving maps*) where |
49 "mono_map(A,r,B,s) == |
48 "mono_map(A,r,B,s) == |
50 {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}" |
49 {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}" |
51 |
50 |
52 definition |
51 definition |
53 ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*) where |
52 ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*) where |
54 "ord_iso(A,r,B,s) == |
53 "ord_iso(A,r,B,s) == |
55 {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}" |
54 {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}" |
56 |
55 |
57 definition |
56 definition |
58 pred :: "[i,i,i]=>i" (*Set of predecessors*) where |
57 pred :: "[i,i,i]=>i" (*Set of predecessors*) where |
59 "pred(A,x,r) == {y:A. <y,x>:r}" |
58 "pred(A,x,r) == {y:A. <y,x>:r}" |
60 |
59 |
61 definition |
60 definition |
62 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 |
63 "ord_iso_map(A,r,B,s) == |
62 "ord_iso_map(A,r,B,s) == |
64 \<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>}" |
65 |
64 |
66 definition |
65 definition |
67 first :: "[i, i, i] => o" where |
66 first :: "[i, i, i] => o" where |
535 range(ord_iso_map(A,r,B,s)), s)" |
534 range(ord_iso_map(A,r,B,s)), s)" |
536 apply (rule well_ord_mono_ord_isoI) |
535 apply (rule well_ord_mono_ord_isoI) |
537 prefer 4 |
536 prefer 4 |
538 apply (rule converse_ord_iso_map [THEN subst]) |
537 apply (rule converse_ord_iso_map [THEN subst]) |
539 apply (simp add: ord_iso_map_mono_map |
538 apply (simp add: ord_iso_map_mono_map |
540 ord_iso_map_subset [THEN converse_converse]) |
539 ord_iso_map_subset [THEN converse_converse]) |
541 apply (blast intro!: domain_ord_iso_map range_ord_iso_map |
540 apply (blast intro!: domain_ord_iso_map range_ord_iso_map |
542 intro: well_ord_subset ord_iso_map_mono_map)+ |
541 intro: well_ord_subset ord_iso_map_mono_map)+ |
543 done |
542 done |
544 |
543 |
545 |
544 |
579 (*The first case: the domain equals A*) |
578 (*The first case: the domain equals A*) |
580 apply (rule domain_ord_iso_map [THEN equalityI]) |
579 apply (rule domain_ord_iso_map [THEN equalityI]) |
581 apply (erule Diff_eq_0_iff [THEN iffD1]) |
580 apply (erule Diff_eq_0_iff [THEN iffD1]) |
582 (*The other case: the domain equals an initial segment*) |
581 (*The other case: the domain equals an initial segment*) |
583 apply (blast del: domainI subsetI |
582 apply (blast del: domainI subsetI |
584 elim!: predE |
583 elim!: predE |
585 intro!: domain_ord_iso_map_subset |
584 intro!: domain_ord_iso_map_subset |
586 intro: subsetI)+ |
585 intro: subsetI)+ |
587 done |
586 done |
588 |
587 |
589 (*As above, by duality*) |
588 (*As above, by duality*) |
590 lemma range_ord_iso_map_cases: |
589 lemma range_ord_iso_map_cases: |