author | lcp |
Tue, 20 Dec 1994 15:58:52 +0100 | |
changeset 814 | a32b420c33d4 |
parent 807 | 3abd026e68a4 |
child 831 | 60d850cc5fe6 |
permissions | -rw-r--r-- |
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 |
||
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
6 |
Order types in Zermelo-Fraenkel Set Theory |
435 | 7 |
*) |
8 |
||
9 |
||
10 |
open OrderType; |
|
11 |
||
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
12 |
(*** Proofs needing the combination of Ordinal.thy and Order.thy ***) |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
13 |
|
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
14 |
goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
15 |
by (rtac well_ordI 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
16 |
by (rtac (wf_Memrel RS wf_imp_wf_on) 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
17 |
by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
18 |
by (REPEAT (resolve_tac [ballI, Ord_linear] 1));; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
19 |
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
20 |
qed "well_ord_Memrel"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
21 |
|
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
22 |
(*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
23 |
The smaller ordinal is an initial segment of the larger *) |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
24 |
goalw OrderType.thy [pred_def, lt_def] |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
25 |
"!!i j. j<i ==> j = pred(i, j, Memrel(i))"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
26 |
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
27 |
by (fast_tac (eq_cs addEs [Ord_trans]) 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
28 |
qed "lt_eq_pred"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
29 |
|
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
30 |
goal OrderType.thy |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
31 |
"!!i. [| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
32 |
by (forward_tac [lt_eq_pred] 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
33 |
by (etac ltE 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
34 |
by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
35 |
assume_tac 3 THEN assume_tac 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
36 |
by (etac subst 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
37 |
by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
38 |
(*Combining the two simplifications causes looping*) |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
39 |
by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
40 |
by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type] addEs [Ord_trans]) 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
41 |
qed "Ord_iso_implies_eq_lemma"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
42 |
|
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
43 |
(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*) |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
44 |
goal OrderType.thy |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
45 |
"!!i. [| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) \ |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
46 |
\ |] ==> i=j"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
47 |
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
48 |
by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1)); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
49 |
qed "Ord_iso_implies_eq"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
50 |
|
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
51 |
(*** Ordermap and ordertype ***) |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
52 |
|
437 | 53 |
goalw OrderType.thy [ordermap_def,ordertype_def] |
54 |
"ordermap(A,r) : A -> ordertype(A,r)"; |
|
55 |
by (rtac lam_type 1); |
|
56 |
by (rtac (lamI RS imageI) 1); |
|
57 |
by (REPEAT (assume_tac 1)); |
|
760 | 58 |
qed "ordermap_type"; |
437 | 59 |
|
435 | 60 |
(** Unfolding of ordermap **) |
61 |
||
437 | 62 |
(*Useful for cardinality reasoning; see CardinalArith.ML*) |
435 | 63 |
goalw OrderType.thy [ordermap_def, pred_def] |
64 |
"!!r. [| wf[A](r); x:A |] ==> \ |
|
437 | 65 |
\ ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"; |
66 |
by (asm_simp_tac ZF_ss 1); |
|
67 |
by (etac (wfrec_on RS trans) 1); |
|
68 |
by (assume_tac 1); |
|
69 |
by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam, |
|
70 |
vimage_singleton_iff]) 1); |
|
760 | 71 |
qed "ordermap_eq_image"; |
437 | 72 |
|
467 | 73 |
(*Useful for rewriting PROVIDED pred is not unfolded until later!*) |
437 | 74 |
goal OrderType.thy |
75 |
"!!r. [| wf[A](r); x:A |] ==> \ |
|
435 | 76 |
\ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"; |
437 | 77 |
by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset, |
78 |
ordermap_type RS image_fun]) 1); |
|
760 | 79 |
qed "ordermap_pred_unfold"; |
435 | 80 |
|
81 |
(*pred-unfolded version. NOT suitable for rewriting -- loops!*) |
|
82 |
val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold; |
|
83 |
||
84 |
(** Showing that ordermap, ordertype yield ordinals **) |
|
85 |
||
86 |
fun ordermap_elim_tac i = |
|
87 |
EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i, |
|
88 |
assume_tac (i+1), |
|
89 |
assume_tac i]; |
|
90 |
||
91 |
goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def] |
|
92 |
"!!r. [| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)"; |
|
93 |
by (safe_tac ZF_cs); |
|
94 |
by (wf_on_ind_tac "x" [] 1); |
|
95 |
by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1); |
|
96 |
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); |
|
437 | 97 |
by (rewrite_goals_tac [pred_def,Transset_def]); |
435 | 98 |
by (fast_tac ZF_cs 2); |
99 |
by (safe_tac ZF_cs); |
|
100 |
by (ordermap_elim_tac 1); |
|
101 |
by (fast_tac (ZF_cs addSEs [trans_onD]) 1); |
|
760 | 102 |
qed "Ord_ordermap"; |
435 | 103 |
|
104 |
goalw OrderType.thy [ordertype_def] |
|
105 |
"!!r. well_ord(A,r) ==> Ord(ordertype(A,r))"; |
|
106 |
by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1); |
|
107 |
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); |
|
108 |
by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2); |
|
437 | 109 |
by (rewrite_goals_tac [Transset_def,well_ord_def]); |
435 | 110 |
by (safe_tac ZF_cs); |
111 |
by (ordermap_elim_tac 1); |
|
112 |
by (fast_tac ZF_cs 1); |
|
760 | 113 |
qed "Ord_ordertype"; |
435 | 114 |
|
115 |
(** ordermap preserves the orderings in both directions **) |
|
116 |
||
117 |
goal OrderType.thy |
|
118 |
"!!r. [| <w,x>: r; wf[A](r); w: A; x: A |] ==> \ |
|
119 |
\ ordermap(A,r)`w : ordermap(A,r)`x"; |
|
120 |
by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1); |
|
437 | 121 |
by (assume_tac 1); |
435 | 122 |
by (fast_tac ZF_cs 1); |
760 | 123 |
qed "ordermap_mono"; |
435 | 124 |
|
125 |
(*linearity of r is crucial here*) |
|
126 |
goalw OrderType.thy [well_ord_def, tot_ord_def] |
|
127 |
"!!r. [| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \ |
|
128 |
\ w: A; x: A |] ==> <w,x>: r"; |
|
129 |
by (safe_tac ZF_cs); |
|
130 |
by (linear_case_tac 1); |
|
131 |
by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1); |
|
467 | 132 |
by (dtac ordermap_mono 1); |
435 | 133 |
by (REPEAT_SOME assume_tac); |
437 | 134 |
by (etac mem_asym 1); |
135 |
by (assume_tac 1); |
|
760 | 136 |
qed "converse_ordermap_mono"; |
435 | 137 |
|
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
788
diff
changeset
|
138 |
bind_thm ("ordermap_surj", |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
788
diff
changeset
|
139 |
rewrite_rule [symmetric ordertype_def] |
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
788
diff
changeset
|
140 |
(ordermap_type RS surj_image)); |
435 | 141 |
|
142 |
goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def] |
|
143 |
"!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"; |
|
144 |
by (safe_tac ZF_cs); |
|
437 | 145 |
by (rtac ordermap_type 1); |
146 |
by (rtac ordermap_surj 2); |
|
435 | 147 |
by (linear_case_tac 1); |
148 |
(*The two cases yield similar contradictions*) |
|
467 | 149 |
by (ALLGOALS (dtac ordermap_mono)); |
435 | 150 |
by (REPEAT_SOME assume_tac); |
151 |
by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl]))); |
|
760 | 152 |
qed "ordermap_bij"; |
435 | 153 |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
154 |
(** Isomorphisms involving ordertype **) |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
155 |
|
435 | 156 |
goalw OrderType.thy [ord_iso_def] |
157 |
"!!r. well_ord(A,r) ==> \ |
|
158 |
\ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"; |
|
159 |
by (safe_tac ZF_cs); |
|
467 | 160 |
by (rtac ordermap_bij 1); |
437 | 161 |
by (assume_tac 1); |
467 | 162 |
by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2); |
437 | 163 |
by (rewtac well_ord_def); |
467 | 164 |
by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono, |
435 | 165 |
ordermap_type RS apply_type]) 1); |
760 | 166 |
qed "ordertype_ord_iso"; |
435 | 167 |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
168 |
goal OrderType.thy |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
169 |
"!!f. [| f: ord_iso(A,r,B,s); well_ord(B,s) |] ==> \ |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
170 |
\ ordertype(A,r) = ordertype(B,s)"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
171 |
by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
172 |
by (resolve_tac [Ord_iso_implies_eq] 1 |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
173 |
THEN REPEAT (eresolve_tac [Ord_ordertype] 1)); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
174 |
by (deepen_tac (ZF_cs addIs [ord_iso_trans, ord_iso_sym] |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
175 |
addSEs [ordertype_ord_iso]) 0 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
176 |
qed "ordertype_eq"; |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
177 |
|
435 | 178 |
|
179 |
(** Unfolding of ordertype **) |
|
180 |
||
181 |
goalw OrderType.thy [ordertype_def] |
|
182 |
"ordertype(A,r) = {ordermap(A,r)`y . y : A}"; |
|
183 |
by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1); |
|
760 | 184 |
qed "ordertype_unfold"; |
467 | 185 |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
186 |
(*Ordertype of Memrel*) |
467 | 187 |
goal OrderType.thy "!!i. Ord(i) ==> ordertype(i,Memrel(i)) = i"; |
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
188 |
by (resolve_tac [Ord_iso_implies_eq RS sym] 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
189 |
by (resolve_tac [ordertype_ord_iso] 3); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
190 |
by (REPEAT (ares_tac [well_ord_Memrel, Ord_ordertype] 1)); |
760 | 191 |
qed "ordertype_Memrel"; |
467 | 192 |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
193 |
(*Ordertype of rvimage*) |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
194 |
bind_thm ("bij_ordertype_vimage", ord_iso_rvimage RS ordertype_eq); |
467 | 195 |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
196 |
(*Ordermap returns the same result if applied to an initial segment*) |
467 | 197 |
goal OrderType.thy |
198 |
"!!r. [| well_ord(A,r); y:A; z: pred(A,y,r) |] ==> \ |
|
199 |
\ ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"; |
|
200 |
by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1); |
|
201 |
by (wf_on_ind_tac "z" [] 1); |
|
202 |
by (safe_tac (ZF_cs addSEs [predE])); |
|
203 |
by (asm_simp_tac |
|
204 |
(ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1); |
|
205 |
(*combining these two simplifications LOOPS! *) |
|
206 |
by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1); |
|
207 |
by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1); |
|
807 | 208 |
by (rtac (refl RSN (2,RepFun_cong)) 1); |
209 |
by (dtac well_ord_is_trans_on 1); |
|
467 | 210 |
by (fast_tac (eq_cs addSEs [trans_onD]) 1); |
760 | 211 |
qed "ordermap_pred_eq_ordermap"; |
467 | 212 |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
213 |
(*Lemma for proving there exist ever larger cardinals*) |
467 | 214 |
goal OrderType.thy |
215 |
"!!r. [| well_ord(A,r); i: ordertype(A,r) |] ==> \ |
|
216 |
\ EX B. B<=A & i = ordertype(B,r)"; |
|
217 |
by (dresolve_tac [ordertype_unfold RS equalityD1 RS subsetD] 1); |
|
814
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
218 |
by (etac RepFunE 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
219 |
by (res_inst_tac [("x", "pred(A,y,r)")] exI 1); |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
220 |
by (asm_simp_tac |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
221 |
(ZF_ss addsimps [pred_subset, well_ord_is_wf RS ordermap_pred_unfold, |
a32b420c33d4
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
lcp
parents:
807
diff
changeset
|
222 |
ordertype_unfold, ordermap_pred_eq_ordermap]) 1); |
760 | 223 |
qed "ordertype_subset"; |
467 | 224 |