435
|
1 |
(* Title: ZF/OrderType.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1994 University of Cambridge
|
|
5 |
|
|
6 |
For OrderType.thy. Order types in Zermelo-Fraenkel Set Theory
|
|
7 |
*)
|
|
8 |
|
|
9 |
|
|
10 |
open OrderType;
|
|
11 |
|
437
|
12 |
goalw OrderType.thy [ordermap_def,ordertype_def]
|
|
13 |
"ordermap(A,r) : A -> ordertype(A,r)";
|
|
14 |
by (rtac lam_type 1);
|
|
15 |
by (rtac (lamI RS imageI) 1);
|
|
16 |
by (REPEAT (assume_tac 1));
|
760
|
17 |
qed "ordermap_type";
|
437
|
18 |
|
435
|
19 |
(** Unfolding of ordermap **)
|
|
20 |
|
437
|
21 |
(*Useful for cardinality reasoning; see CardinalArith.ML*)
|
435
|
22 |
goalw OrderType.thy [ordermap_def, pred_def]
|
|
23 |
"!!r. [| wf[A](r); x:A |] ==> \
|
437
|
24 |
\ ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)";
|
|
25 |
by (asm_simp_tac ZF_ss 1);
|
|
26 |
by (etac (wfrec_on RS trans) 1);
|
|
27 |
by (assume_tac 1);
|
|
28 |
by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam,
|
|
29 |
vimage_singleton_iff]) 1);
|
760
|
30 |
qed "ordermap_eq_image";
|
437
|
31 |
|
467
|
32 |
(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
|
437
|
33 |
goal OrderType.thy
|
|
34 |
"!!r. [| wf[A](r); x:A |] ==> \
|
435
|
35 |
\ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
|
437
|
36 |
by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset,
|
|
37 |
ordermap_type RS image_fun]) 1);
|
760
|
38 |
qed "ordermap_pred_unfold";
|
435
|
39 |
|
|
40 |
(*pred-unfolded version. NOT suitable for rewriting -- loops!*)
|
|
41 |
val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
|
|
42 |
|
|
43 |
(** Showing that ordermap, ordertype yield ordinals **)
|
|
44 |
|
|
45 |
fun ordermap_elim_tac i =
|
|
46 |
EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i,
|
|
47 |
assume_tac (i+1),
|
|
48 |
assume_tac i];
|
|
49 |
|
|
50 |
goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def]
|
|
51 |
"!!r. [| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)";
|
|
52 |
by (safe_tac ZF_cs);
|
|
53 |
by (wf_on_ind_tac "x" [] 1);
|
|
54 |
by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1);
|
|
55 |
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
|
437
|
56 |
by (rewrite_goals_tac [pred_def,Transset_def]);
|
435
|
57 |
by (fast_tac ZF_cs 2);
|
|
58 |
by (safe_tac ZF_cs);
|
|
59 |
by (ordermap_elim_tac 1);
|
|
60 |
by (fast_tac (ZF_cs addSEs [trans_onD]) 1);
|
760
|
61 |
qed "Ord_ordermap";
|
435
|
62 |
|
|
63 |
goalw OrderType.thy [ordertype_def]
|
|
64 |
"!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
|
|
65 |
by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1);
|
|
66 |
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
|
|
67 |
by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
|
437
|
68 |
by (rewrite_goals_tac [Transset_def,well_ord_def]);
|
435
|
69 |
by (safe_tac ZF_cs);
|
|
70 |
by (ordermap_elim_tac 1);
|
|
71 |
by (fast_tac ZF_cs 1);
|
760
|
72 |
qed "Ord_ordertype";
|
435
|
73 |
|
|
74 |
(** ordermap preserves the orderings in both directions **)
|
|
75 |
|
|
76 |
goal OrderType.thy
|
|
77 |
"!!r. [| <w,x>: r; wf[A](r); w: A; x: A |] ==> \
|
|
78 |
\ ordermap(A,r)`w : ordermap(A,r)`x";
|
|
79 |
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
|
437
|
80 |
by (assume_tac 1);
|
435
|
81 |
by (fast_tac ZF_cs 1);
|
760
|
82 |
qed "ordermap_mono";
|
435
|
83 |
|
|
84 |
(*linearity of r is crucial here*)
|
|
85 |
goalw OrderType.thy [well_ord_def, tot_ord_def]
|
|
86 |
"!!r. [| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \
|
|
87 |
\ w: A; x: A |] ==> <w,x>: r";
|
|
88 |
by (safe_tac ZF_cs);
|
|
89 |
by (linear_case_tac 1);
|
|
90 |
by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1);
|
467
|
91 |
by (dtac ordermap_mono 1);
|
435
|
92 |
by (REPEAT_SOME assume_tac);
|
437
|
93 |
by (etac mem_asym 1);
|
|
94 |
by (assume_tac 1);
|
760
|
95 |
qed "converse_ordermap_mono";
|
435
|
96 |
|
|
97 |
val ordermap_surj =
|
|
98 |
(ordermap_type RS surj_image) |>
|
|
99 |
rewrite_rule [symmetric ordertype_def] |>
|
|
100 |
standard;
|
|
101 |
|
|
102 |
goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
|
|
103 |
"!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
|
|
104 |
by (safe_tac ZF_cs);
|
437
|
105 |
by (rtac ordermap_type 1);
|
|
106 |
by (rtac ordermap_surj 2);
|
435
|
107 |
by (linear_case_tac 1);
|
|
108 |
(*The two cases yield similar contradictions*)
|
467
|
109 |
by (ALLGOALS (dtac ordermap_mono));
|
435
|
110 |
by (REPEAT_SOME assume_tac);
|
|
111 |
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl])));
|
760
|
112 |
qed "ordermap_bij";
|
435
|
113 |
|
|
114 |
goalw OrderType.thy [ord_iso_def]
|
|
115 |
"!!r. well_ord(A,r) ==> \
|
|
116 |
\ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
|
|
117 |
by (safe_tac ZF_cs);
|
467
|
118 |
by (rtac ordermap_bij 1);
|
437
|
119 |
by (assume_tac 1);
|
467
|
120 |
by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2);
|
437
|
121 |
by (rewtac well_ord_def);
|
467
|
122 |
by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono,
|
435
|
123 |
ordermap_type RS apply_type]) 1);
|
760
|
124 |
qed "ordertype_ord_iso";
|
435
|
125 |
|
|
126 |
|
|
127 |
(** Unfolding of ordertype **)
|
|
128 |
|
|
129 |
goalw OrderType.thy [ordertype_def]
|
|
130 |
"ordertype(A,r) = {ordermap(A,r)`y . y : A}";
|
|
131 |
by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
|
760
|
132 |
qed "ordertype_unfold";
|
467
|
133 |
|
|
134 |
|
|
135 |
(** Ordertype of Memrel **)
|
|
136 |
|
|
137 |
(*Requires Ordinal.thy as parent; otherwise could be in Order.ML*)
|
|
138 |
goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
|
|
139 |
by (rtac well_ordI 1);
|
|
140 |
by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
|
|
141 |
by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1);
|
|
142 |
by (REPEAT (resolve_tac [ballI, Ord_linear] 1));;
|
|
143 |
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));;
|
760
|
144 |
qed "well_ord_Memrel";
|
467
|
145 |
|
|
146 |
goal OrderType.thy "!!i. [| Ord(i); j:i |] ==> ordermap(i,Memrel(i)) ` j = j";
|
|
147 |
by (eresolve_tac [Ord_induct] 1);
|
|
148 |
ba 1;
|
|
149 |
by (asm_simp_tac (ZF_ss addsimps
|
|
150 |
[well_ord_Memrel RS well_ord_is_wf RS ordermap_pred_unfold]) 1);
|
|
151 |
by (asm_simp_tac (ZF_ss addsimps [pred_def, Memrel_iff]) 1);
|
|
152 |
by (dresolve_tac [OrdmemD] 1);
|
|
153 |
by (assume_tac 1);
|
|
154 |
by (fast_tac eq_cs 1);
|
760
|
155 |
qed "ordermap_Memrel";
|
467
|
156 |
|
|
157 |
goal OrderType.thy "!!i. Ord(i) ==> ordertype(i,Memrel(i)) = i";
|
|
158 |
by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, ordermap_Memrel]) 1);
|
760
|
159 |
qed "ordertype_Memrel";
|
467
|
160 |
|
|
161 |
(** Ordertype of rvimage **)
|
|
162 |
|
|
163 |
goal OrderType.thy
|
|
164 |
"!!f. [| f: bij(A,B); well_ord(B,r); x:A |] ==> \
|
|
165 |
\ ordermap(A,rvimage(A,f,r)) ` x = ordermap(B,r) ` (f`x)";
|
|
166 |
by (metacut_tac well_ord_rvimage 1 THEN
|
|
167 |
etac bij_is_inj 2 THEN assume_tac 2);
|
|
168 |
by (res_inst_tac [("A","A"), ("a","x")] wf_on_induct 1 THEN
|
|
169 |
REPEAT (ares_tac [well_ord_is_wf] 1));
|
|
170 |
by (asm_simp_tac
|
|
171 |
(bij_inverse_ss addsimps [ordermap_pred_unfold, well_ord_is_wf]) 1);
|
|
172 |
by (asm_simp_tac (ZF_ss addsimps [pred_def, rvimage_iff]) 1);
|
|
173 |
by (safe_tac eq_cs);
|
|
174 |
by (fast_tac bij_apply_cs 1);
|
|
175 |
by (res_inst_tac [("a", "converse(f)`xb")] RepFun_eqI 1);
|
|
176 |
by (ALLGOALS (asm_simp_tac bij_inverse_ss));
|
760
|
177 |
qed "bij_ordermap_vimage";
|
467
|
178 |
|
|
179 |
goal OrderType.thy
|
|
180 |
"!!f. [| f: bij(A,B); well_ord(B,r) |] ==> \
|
|
181 |
\ ordertype(A,rvimage(A,f,r)) = ordertype(B,r)";
|
|
182 |
by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, bij_ordermap_vimage]) 1);
|
|
183 |
by (safe_tac eq_cs);
|
|
184 |
by (fast_tac bij_apply_cs 1);
|
|
185 |
by (res_inst_tac [("a", "converse(f)`xa")] RepFun_eqI 1);
|
|
186 |
by (ALLGOALS (asm_simp_tac bij_inverse_ss));
|
760
|
187 |
qed "bij_ordertype_vimage";
|
467
|
188 |
|
|
189 |
|
|
190 |
goal OrderType.thy
|
|
191 |
"!!r. [| well_ord(A,r); y:A; z: pred(A,y,r) |] ==> \
|
|
192 |
\ ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
|
|
193 |
by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1);
|
|
194 |
by (wf_on_ind_tac "z" [] 1);
|
|
195 |
by (safe_tac (ZF_cs addSEs [predE]));
|
|
196 |
by (asm_simp_tac
|
|
197 |
(ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
|
|
198 |
(*combining these two simplifications LOOPS! *)
|
|
199 |
by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1);
|
|
200 |
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1);
|
|
201 |
br (refl RSN (2,RepFun_cong)) 1;
|
|
202 |
bd well_ord_is_trans_on 1;
|
|
203 |
by (fast_tac (eq_cs addSEs [trans_onD]) 1);
|
760
|
204 |
qed "ordermap_pred_eq_ordermap";
|
467
|
205 |
|
|
206 |
|
|
207 |
goal OrderType.thy
|
|
208 |
"!!r. [| well_ord(A,r); i: ordertype(A,r) |] ==> \
|
|
209 |
\ EX B. B<=A & i = ordertype(B,r)";
|
|
210 |
by (dresolve_tac [ordertype_unfold RS equalityD1 RS subsetD] 1);
|
|
211 |
by (res_inst_tac [("x", "pred(A, converse(ordermap(A,r))`i, r)")] exI 1);
|
|
212 |
by (safe_tac (ZF_cs addSEs [predE]));
|
|
213 |
by (asm_simp_tac (ZF_ss addsimps [ordermap_bij RS left_inverse_bij]) 1);
|
|
214 |
by (asm_simp_tac (ZF_ss addsimps
|
|
215 |
[well_ord_is_wf RS ordermap_pred_unfold]) 1);
|
|
216 |
by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold,
|
|
217 |
ordermap_pred_eq_ordermap]) 1);
|
760
|
218 |
qed "ordertype_subset";
|
467
|
219 |
|