author | clasohm |
Wed, 14 Dec 1994 11:41:49 +0100 | |
changeset 782 | 200a16083201 |
parent 769 | 66cdfde4ec5d |
child 789 | 30bdc59198ff |
permissions | -rw-r--r-- |
435 | 1 |
(* Title: ZF/Order.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
6 |
For Order.thy. Orders in Zermelo-Fraenkel Set Theory |
|
7 |
*) |
|
8 |
||
9 |
||
10 |
open Order; |
|
11 |
||
12 |
val bij_apply_cs = ZF_cs addSEs [bij_converse_bij] |
|
13 |
addIs [bij_is_fun, apply_type]; |
|
14 |
||
15 |
val bij_inverse_ss = |
|
16 |
ZF_ss addsimps [bij_is_fun RS apply_type, |
|
17 |
bij_converse_bij RS bij_is_fun RS apply_type, |
|
18 |
left_inverse_bij, right_inverse_bij]; |
|
19 |
||
20 |
(** Basic properties of the definitions **) |
|
21 |
||
22 |
(*needed????*) |
|
23 |
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, asym_def] |
|
24 |
"!!r. part_ord(A,r) ==> asym(r Int A*A)"; |
|
25 |
by (fast_tac ZF_cs 1); |
|
760 | 26 |
qed "part_ord_Imp_asym"; |
435 | 27 |
|
484 | 28 |
(** Subset properties for the various forms of relation **) |
29 |
||
30 |
||
31 |
(*Note: a relation s such that s<=r need not be a partial ordering*) |
|
32 |
goalw Order.thy [part_ord_def, irrefl_def, trans_on_def] |
|
33 |
"!!A B r. [| part_ord(A,r); B<=A |] ==> part_ord(B,r)"; |
|
34 |
by (fast_tac ZF_cs 1); |
|
760 | 35 |
qed "part_ord_subset"; |
484 | 36 |
|
37 |
goalw Order.thy [linear_def] |
|
38 |
"!!A B r. [| linear(A,r); B<=A |] ==> linear(B,r)"; |
|
39 |
by (fast_tac ZF_cs 1); |
|
760 | 40 |
qed "linear_subset"; |
484 | 41 |
|
42 |
goalw Order.thy [tot_ord_def] |
|
43 |
"!!A B r. [| tot_ord(A,r); B<=A |] ==> tot_ord(B,r)"; |
|
44 |
by (fast_tac (ZF_cs addSEs [part_ord_subset, linear_subset]) 1); |
|
760 | 45 |
qed "tot_ord_subset"; |
484 | 46 |
|
47 |
goalw Order.thy [well_ord_def] |
|
48 |
"!!A B r. [| well_ord(A,r); B<=A |] ==> well_ord(B,r)"; |
|
49 |
by (fast_tac (ZF_cs addSEs [tot_ord_subset, wf_on_subset_A]) 1); |
|
760 | 50 |
qed "well_ord_subset"; |
484 | 51 |
|
52 |
||
435 | 53 |
(** Order-isomorphisms **) |
54 |
||
55 |
goalw Order.thy [ord_iso_def] |
|
56 |
"!!f. f: ord_iso(A,r,B,s) ==> f: bij(A,B)"; |
|
57 |
by (etac CollectD1 1); |
|
760 | 58 |
qed "ord_iso_is_bij"; |
435 | 59 |
|
60 |
goalw Order.thy [ord_iso_def] |
|
61 |
"!!f. [| f: ord_iso(A,r,B,s); <x,y>: r; x:A; y:A |] ==> \ |
|
62 |
\ <f`x, f`y> : s"; |
|
63 |
by (fast_tac ZF_cs 1); |
|
760 | 64 |
qed "ord_iso_apply"; |
435 | 65 |
|
66 |
goalw Order.thy [ord_iso_def] |
|
67 |
"!!f. [| f: ord_iso(A,r,B,s); <x,y>: s; x:B; y:B |] ==> \ |
|
68 |
\ <converse(f) ` x, converse(f) ` y> : r"; |
|
437 | 69 |
by (etac CollectE 1); |
70 |
by (etac (bspec RS bspec RS iffD2) 1); |
|
435 | 71 |
by (REPEAT (eresolve_tac [asm_rl, |
72 |
bij_converse_bij RS bij_is_fun RS apply_type] 1)); |
|
73 |
by (asm_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1); |
|
760 | 74 |
qed "ord_iso_converse"; |
435 | 75 |
|
769 | 76 |
(*Rewriting with bijections and converse (function inverse)*) |
77 |
val bij_ss = ZF_ss setsolver (type_auto_tac [bij_is_fun RS apply_type, |
|
78 |
bij_converse_bij]) |
|
79 |
addsimps [right_inverse_bij, left_inverse_bij]; |
|
80 |
||
81 |
(*Symmetry of the order-isomorphism relation*) |
|
82 |
goalw Order.thy [ord_iso_def] |
|
83 |
"!!f. f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"; |
|
84 |
by (safe_tac ZF_cs); |
|
85 |
by (ALLGOALS (asm_full_simp_tac bij_ss)); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
769
diff
changeset
|
86 |
qed "ord_iso_sym"; |
769 | 87 |
|
435 | 88 |
val major::premx::premy::prems = goalw Order.thy [linear_def] |
89 |
"[| linear(A,r); x:A; y:A; \ |
|
90 |
\ <x,y>:r ==> P; x=y ==> P; <y,x>:r ==> P |] ==> P"; |
|
91 |
by (cut_facts_tac [major,premx,premy] 1); |
|
92 |
by (REPEAT_FIRST (eresolve_tac [ballE,disjE])); |
|
93 |
by (EVERY1 (map etac prems)); |
|
94 |
by (ALLGOALS contr_tac); |
|
760 | 95 |
qed "linearE"; |
435 | 96 |
|
97 |
(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*) |
|
98 |
val linear_case_tac = |
|
99 |
SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1, |
|
100 |
REPEAT_SOME assume_tac]); |
|
101 |
||
102 |
(*Inductive argument for proving Kunen's Lemma 6.1*) |
|
103 |
goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def, pred_def] |
|
104 |
"!!r. [| well_ord(A,r); x: A; f: ord_iso(A, r, pred(A,x,r), r); y: A |] \ |
|
105 |
\ ==> f`y = y"; |
|
106 |
by (safe_tac ZF_cs); |
|
107 |
by (wf_on_ind_tac "y" [] 1); |
|
108 |
by (forward_tac [ord_iso_is_bij] 1); |
|
109 |
by (subgoal_tac "f`y1 : {y: A . <y, x> : r}" 1); |
|
110 |
by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type]) 2); |
|
111 |
(*Now we know f`y1 : A and <f`y1, x> : r *) |
|
112 |
by (etac CollectE 1); |
|
113 |
by (linear_case_tac 1); |
|
114 |
(*Case <f`y1, y1> : r *) (*use induction hyp*) |
|
115 |
by (dtac bspec 1 THEN mp_tac 2 THEN assume_tac 1); |
|
116 |
by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); |
|
117 |
by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
118 |
(*The case <y1, f`y1> : r *) |
|
119 |
by (subgoal_tac "<y1,x> : r" 1); |
|
120 |
by (fast_tac (ZF_cs addSEs [trans_onD]) 2); |
|
121 |
by (dtac ord_iso_converse 1 THEN assume_tac 1 THEN fast_tac ZF_cs 2); |
|
122 |
by (fast_tac ZF_cs 1); |
|
123 |
by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
124 |
(*now use induction hyp*) |
|
125 |
by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); |
|
126 |
by (dres_inst_tac [("t", "op `(f)")] subst_context 1); |
|
127 |
by (asm_full_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1); |
|
760 | 128 |
qed "not_well_ord_iso_pred_lemma"; |
435 | 129 |
|
130 |
||
131 |
(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment |
|
132 |
of a well-ordering*) |
|
133 |
goal Order.thy |
|
769 | 134 |
"!!r. [| well_ord(A,r); x:A |] ==> f ~: ord_iso(A, r, pred(A,x,r), r)"; |
435 | 135 |
by (safe_tac ZF_cs); |
136 |
by (metacut_tac not_well_ord_iso_pred_lemma 1); |
|
137 |
by (REPEAT_SOME assume_tac); |
|
138 |
(*Now we know f`x = x*) |
|
139 |
by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type), |
|
140 |
assume_tac]); |
|
141 |
(*Now we know f`x : pred(A,x,r) *) |
|
142 |
by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, pred_def]) 1); |
|
143 |
by (fast_tac (ZF_cs addSEs [wf_on_not_refl RS notE]) 1); |
|
760 | 144 |
qed "not_well_ord_iso_pred"; |
435 | 145 |
|
146 |
||
147 |
(*Inductive argument for proving Kunen's Lemma 6.2*) |
|
148 |
goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def] |
|
149 |
"!!r. [| well_ord(A,r); well_ord(B,s); \ |
|
150 |
\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s); y: A |] \ |
|
151 |
\ ==> f`y = g`y"; |
|
152 |
by (safe_tac ZF_cs); |
|
153 |
by (wf_on_ind_tac "y" [] 1); |
|
154 |
by (subgoals_tac ["f: bij(A,B)", "g: bij(A,B)", "f`y1 : B", "g`y1 : B"] 1); |
|
155 |
by (REPEAT (fast_tac (bij_apply_cs addSEs [ord_iso_is_bij]) 2)); |
|
156 |
by (linear_case_tac 1); |
|
157 |
(*The case <f`y1, g`y1> : s *) |
|
158 |
by (forw_inst_tac [("f","g")] ord_iso_converse 1 THEN REPEAT (assume_tac 1)); |
|
159 |
by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
160 |
by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); |
|
161 |
by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); |
|
162 |
by (dres_inst_tac [("t", "op `(g)")] subst_context 1); |
|
163 |
by (asm_full_simp_tac bij_inverse_ss 1); |
|
164 |
(*The case <g`y1, f`y1> : s *) |
|
165 |
by (forw_inst_tac [("f","f")] ord_iso_converse 1 THEN REPEAT (assume_tac 1)); |
|
166 |
by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
167 |
by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); |
|
168 |
by (dres_inst_tac [("t", "op `(converse(g))")] subst_context 1); |
|
169 |
by (dres_inst_tac [("t", "op `(f)")] subst_context 1); |
|
170 |
by (asm_full_simp_tac bij_inverse_ss 1); |
|
760 | 171 |
qed "well_ord_iso_unique_lemma"; |
435 | 172 |
|
173 |
||
174 |
(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*) |
|
175 |
goal Order.thy |
|
176 |
"!!r. [| well_ord(A,r); well_ord(B,s); \ |
|
177 |
\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s) |] ==> f = g"; |
|
437 | 178 |
by (rtac fun_extension 1); |
179 |
by (etac (ord_iso_is_bij RS bij_is_fun) 1); |
|
180 |
by (etac (ord_iso_is_bij RS bij_is_fun) 1); |
|
181 |
by (rtac well_ord_iso_unique_lemma 1); |
|
435 | 182 |
by (REPEAT_SOME assume_tac); |
760 | 183 |
qed "well_ord_iso_unique"; |
435 | 184 |
|
185 |
||
186 |
goalw Order.thy [irrefl_def, part_ord_def, tot_ord_def, |
|
187 |
trans_on_def, well_ord_def] |
|
188 |
"!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"; |
|
189 |
by (asm_simp_tac (ZF_ss addsimps [wf_on_not_refl]) 1); |
|
190 |
by (safe_tac ZF_cs); |
|
191 |
by (linear_case_tac 1); |
|
192 |
(*case x=xb*) |
|
437 | 193 |
by (fast_tac (ZF_cs addSEs [wf_on_asym]) 1); |
435 | 194 |
(*case x<xb*) |
195 |
by (fast_tac (ZF_cs addSEs [wf_on_chain3]) 1); |
|
760 | 196 |
qed "well_ordI"; |
435 | 197 |
|
198 |
goalw Order.thy [well_ord_def] |
|
199 |
"!!r. well_ord(A,r) ==> wf[A](r)"; |
|
200 |
by (safe_tac ZF_cs); |
|
760 | 201 |
qed "well_ord_is_wf"; |
435 | 202 |
|
467 | 203 |
goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def] |
204 |
"!!r. well_ord(A,r) ==> trans[A](r)"; |
|
205 |
by (safe_tac ZF_cs); |
|
760 | 206 |
qed "well_ord_is_trans_on"; |
467 | 207 |
|
435 | 208 |
(*** Derived rules for pred(A,x,r) ***) |
209 |
||
210 |
val [major,minor] = goalw Order.thy [pred_def] |
|
211 |
"[| y: pred(A,x,r); [| y:A; <y,x>:r |] ==> P |] ==> P"; |
|
437 | 212 |
by (rtac (major RS CollectE) 1); |
435 | 213 |
by (REPEAT (ares_tac [minor] 1)); |
760 | 214 |
qed "predE"; |
435 | 215 |
|
216 |
goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}"; |
|
217 |
by (fast_tac ZF_cs 1); |
|
760 | 218 |
qed "pred_subset_under"; |
435 | 219 |
|
220 |
goalw Order.thy [pred_def] "pred(A,x,r) <= A"; |
|
221 |
by (fast_tac ZF_cs 1); |
|
760 | 222 |
qed "pred_subset"; |
467 | 223 |
|
224 |
goalw Order.thy [pred_def] "y : pred(A,x,r) <-> <y,x>:r & y:A"; |
|
225 |
by (fast_tac ZF_cs 1); |
|
760 | 226 |
qed "pred_iff"; |
467 | 227 |
|
228 |
goalw Order.thy [pred_def] |
|
229 |
"pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)"; |
|
230 |
by (fast_tac eq_cs 1); |
|
760 | 231 |
qed "pred_pred_eq"; |