|
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 (*TO PURE/TACTIC.ML*) |
|
10 fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops); |
|
11 |
|
12 |
|
13 open Order; |
|
14 |
|
15 val bij_apply_cs = ZF_cs addSEs [bij_converse_bij] |
|
16 addIs [bij_is_fun, apply_type]; |
|
17 |
|
18 val bij_inverse_ss = |
|
19 ZF_ss addsimps [bij_is_fun RS apply_type, |
|
20 bij_converse_bij RS bij_is_fun RS apply_type, |
|
21 left_inverse_bij, right_inverse_bij]; |
|
22 |
|
23 (** Basic properties of the definitions **) |
|
24 |
|
25 (*needed????*) |
|
26 goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, asym_def] |
|
27 "!!r. part_ord(A,r) ==> asym(r Int A*A)"; |
|
28 by (fast_tac ZF_cs 1); |
|
29 val part_ord_Imp_asym = result(); |
|
30 |
|
31 (** Order-isomorphisms **) |
|
32 |
|
33 goalw Order.thy [ord_iso_def] |
|
34 "!!f. f: ord_iso(A,r,B,s) ==> f: bij(A,B)"; |
|
35 by (etac CollectD1 1); |
|
36 val ord_iso_is_bij = result(); |
|
37 |
|
38 goalw Order.thy [ord_iso_def] |
|
39 "!!f. [| f: ord_iso(A,r,B,s); <x,y>: r; x:A; y:A |] ==> \ |
|
40 \ <f`x, f`y> : s"; |
|
41 by (fast_tac ZF_cs 1); |
|
42 val ord_iso_apply = result(); |
|
43 |
|
44 goalw Order.thy [ord_iso_def] |
|
45 "!!f. [| f: ord_iso(A,r,B,s); <x,y>: s; x:B; y:B |] ==> \ |
|
46 \ <converse(f) ` x, converse(f) ` y> : r"; |
|
47 be CollectE 1; |
|
48 be (bspec RS bspec RS iffD2) 1; |
|
49 by (REPEAT (eresolve_tac [asm_rl, |
|
50 bij_converse_bij RS bij_is_fun RS apply_type] 1)); |
|
51 by (asm_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1); |
|
52 val ord_iso_converse = result(); |
|
53 |
|
54 val major::premx::premy::prems = goalw Order.thy [linear_def] |
|
55 "[| linear(A,r); x:A; y:A; \ |
|
56 \ <x,y>:r ==> P; x=y ==> P; <y,x>:r ==> P |] ==> P"; |
|
57 by (cut_facts_tac [major,premx,premy] 1); |
|
58 by (REPEAT_FIRST (eresolve_tac [ballE,disjE])); |
|
59 by (EVERY1 (map etac prems)); |
|
60 by (ALLGOALS contr_tac); |
|
61 val linearE = result(); |
|
62 |
|
63 (*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*) |
|
64 val linear_case_tac = |
|
65 SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1, |
|
66 REPEAT_SOME assume_tac]); |
|
67 |
|
68 (*Inductive argument for proving Kunen's Lemma 6.1*) |
|
69 goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def, pred_def] |
|
70 "!!r. [| well_ord(A,r); x: A; f: ord_iso(A, r, pred(A,x,r), r); y: A |] \ |
|
71 \ ==> f`y = y"; |
|
72 by (safe_tac ZF_cs); |
|
73 by (wf_on_ind_tac "y" [] 1); |
|
74 by (forward_tac [ord_iso_is_bij] 1); |
|
75 by (subgoal_tac "f`y1 : {y: A . <y, x> : r}" 1); |
|
76 by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type]) 2); |
|
77 (*Now we know f`y1 : A and <f`y1, x> : r *) |
|
78 by (etac CollectE 1); |
|
79 by (linear_case_tac 1); |
|
80 (*Case <f`y1, y1> : r *) (*use induction hyp*) |
|
81 by (dtac bspec 1 THEN mp_tac 2 THEN assume_tac 1); |
|
82 by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); |
|
83 by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
84 (*The case <y1, f`y1> : r *) |
|
85 by (subgoal_tac "<y1,x> : r" 1); |
|
86 by (fast_tac (ZF_cs addSEs [trans_onD]) 2); |
|
87 by (dtac ord_iso_converse 1 THEN assume_tac 1 THEN fast_tac ZF_cs 2); |
|
88 by (fast_tac ZF_cs 1); |
|
89 by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
90 (*now use induction hyp*) |
|
91 by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); |
|
92 by (dres_inst_tac [("t", "op `(f)")] subst_context 1); |
|
93 by (asm_full_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1); |
|
94 val not_well_ord_iso_pred_lemma = result(); |
|
95 |
|
96 |
|
97 (*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment |
|
98 of a well-ordering*) |
|
99 goal Order.thy |
|
100 "!!r. [| well_ord(A,r); x:A |] ==> \ |
|
101 \ ALL f. f ~: ord_iso(A, r, pred(A,x,r), r)"; |
|
102 by (safe_tac ZF_cs); |
|
103 by (metacut_tac not_well_ord_iso_pred_lemma 1); |
|
104 by (REPEAT_SOME assume_tac); |
|
105 (*Now we know f`x = x*) |
|
106 by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type), |
|
107 assume_tac]); |
|
108 (*Now we know f`x : pred(A,x,r) *) |
|
109 by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, pred_def]) 1); |
|
110 by (fast_tac (ZF_cs addSEs [wf_on_not_refl RS notE]) 1); |
|
111 val not_well_ord_iso_pred = result(); |
|
112 |
|
113 |
|
114 (*Inductive argument for proving Kunen's Lemma 6.2*) |
|
115 goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def] |
|
116 "!!r. [| well_ord(A,r); well_ord(B,s); \ |
|
117 \ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s); y: A |] \ |
|
118 \ ==> f`y = g`y"; |
|
119 by (safe_tac ZF_cs); |
|
120 by (wf_on_ind_tac "y" [] 1); |
|
121 by (subgoals_tac ["f: bij(A,B)", "g: bij(A,B)", "f`y1 : B", "g`y1 : B"] 1); |
|
122 by (REPEAT (fast_tac (bij_apply_cs addSEs [ord_iso_is_bij]) 2)); |
|
123 by (linear_case_tac 1); |
|
124 (*The case <f`y1, g`y1> : s *) |
|
125 by (forw_inst_tac [("f","g")] ord_iso_converse 1 THEN REPEAT (assume_tac 1)); |
|
126 by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
127 by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); |
|
128 by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); |
|
129 by (dres_inst_tac [("t", "op `(g)")] subst_context 1); |
|
130 by (asm_full_simp_tac bij_inverse_ss 1); |
|
131 (*The case <g`y1, f`y1> : s *) |
|
132 by (forw_inst_tac [("f","f")] ord_iso_converse 1 THEN REPEAT (assume_tac 1)); |
|
133 by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); |
|
134 by (dtac bspec 1 THEN mp_tac 2 THEN fast_tac bij_apply_cs 1); |
|
135 by (dres_inst_tac [("t", "op `(converse(g))")] subst_context 1); |
|
136 by (dres_inst_tac [("t", "op `(f)")] subst_context 1); |
|
137 by (asm_full_simp_tac bij_inverse_ss 1); |
|
138 val well_ord_iso_unique_lemma = result(); |
|
139 |
|
140 |
|
141 (*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*) |
|
142 goal Order.thy |
|
143 "!!r. [| well_ord(A,r); well_ord(B,s); \ |
|
144 \ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s) |] ==> f = g"; |
|
145 br fun_extension 1; |
|
146 be (ord_iso_is_bij RS bij_is_fun) 1; |
|
147 be (ord_iso_is_bij RS bij_is_fun) 1; |
|
148 br well_ord_iso_unique_lemma 1; |
|
149 by (REPEAT_SOME assume_tac); |
|
150 val well_ord_iso_unique = result(); |
|
151 |
|
152 |
|
153 goalw Order.thy [irrefl_def, part_ord_def, tot_ord_def, |
|
154 trans_on_def, well_ord_def] |
|
155 "!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"; |
|
156 by (asm_simp_tac (ZF_ss addsimps [wf_on_not_refl]) 1); |
|
157 by (safe_tac ZF_cs); |
|
158 by (linear_case_tac 1); |
|
159 (*case x=xb*) |
|
160 by (fast_tac (ZF_cs addSEs [wf_on_anti_sym]) 1); |
|
161 (*case x<xb*) |
|
162 by (fast_tac (ZF_cs addSEs [wf_on_chain3]) 1); |
|
163 val well_ordI = result(); |
|
164 |
|
165 goalw Order.thy [well_ord_def] |
|
166 "!!r. well_ord(A,r) ==> wf[A](r)"; |
|
167 by (safe_tac ZF_cs); |
|
168 val well_ord_is_wf = result(); |
|
169 |
|
170 |
|
171 (*** Derived rules for pred(A,x,r) ***) |
|
172 |
|
173 val [major,minor] = goalw Order.thy [pred_def] |
|
174 "[| y: pred(A,x,r); [| y:A; <y,x>:r |] ==> P |] ==> P"; |
|
175 br (major RS CollectE) 1; |
|
176 by (REPEAT (ares_tac [minor] 1)); |
|
177 val predE = result(); |
|
178 |
|
179 goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}"; |
|
180 by (fast_tac ZF_cs 1); |
|
181 val pred_subset_under = result(); |
|
182 |
|
183 goalw Order.thy [pred_def] "pred(A,x,r) <= A"; |
|
184 by (fast_tac ZF_cs 1); |
|
185 val pred_subset = result(); |