47 transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)" |
47 transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)" |
48 |
48 |
49 |
49 |
50 subsubsection {*Trivial absoluteness proofs*} |
50 subsubsection {*Trivial absoluteness proofs*} |
51 |
51 |
52 lemma (in M_axioms) irreflexive_abs [simp]: |
52 lemma (in M_basic) irreflexive_abs [simp]: |
53 "M(A) ==> irreflexive(M,A,r) <-> irrefl(A,r)" |
53 "M(A) ==> irreflexive(M,A,r) <-> irrefl(A,r)" |
54 by (simp add: irreflexive_def irrefl_def) |
54 by (simp add: irreflexive_def irrefl_def) |
55 |
55 |
56 lemma (in M_axioms) transitive_rel_abs [simp]: |
56 lemma (in M_basic) transitive_rel_abs [simp]: |
57 "M(A) ==> transitive_rel(M,A,r) <-> trans[A](r)" |
57 "M(A) ==> transitive_rel(M,A,r) <-> trans[A](r)" |
58 by (simp add: transitive_rel_def trans_on_def) |
58 by (simp add: transitive_rel_def trans_on_def) |
59 |
59 |
60 lemma (in M_axioms) linear_rel_abs [simp]: |
60 lemma (in M_basic) linear_rel_abs [simp]: |
61 "M(A) ==> linear_rel(M,A,r) <-> linear(A,r)" |
61 "M(A) ==> linear_rel(M,A,r) <-> linear(A,r)" |
62 by (simp add: linear_rel_def linear_def) |
62 by (simp add: linear_rel_def linear_def) |
63 |
63 |
64 lemma (in M_axioms) wellordered_is_trans_on: |
64 lemma (in M_basic) wellordered_is_trans_on: |
65 "[| wellordered(M,A,r); M(A) |] ==> trans[A](r)" |
65 "[| wellordered(M,A,r); M(A) |] ==> trans[A](r)" |
66 by (auto simp add: wellordered_def) |
66 by (auto simp add: wellordered_def) |
67 |
67 |
68 lemma (in M_axioms) wellordered_is_linear: |
68 lemma (in M_basic) wellordered_is_linear: |
69 "[| wellordered(M,A,r); M(A) |] ==> linear(A,r)" |
69 "[| wellordered(M,A,r); M(A) |] ==> linear(A,r)" |
70 by (auto simp add: wellordered_def) |
70 by (auto simp add: wellordered_def) |
71 |
71 |
72 lemma (in M_axioms) wellordered_is_wellfounded_on: |
72 lemma (in M_basic) wellordered_is_wellfounded_on: |
73 "[| wellordered(M,A,r); M(A) |] ==> wellfounded_on(M,A,r)" |
73 "[| wellordered(M,A,r); M(A) |] ==> wellfounded_on(M,A,r)" |
74 by (auto simp add: wellordered_def) |
74 by (auto simp add: wellordered_def) |
75 |
75 |
76 lemma (in M_axioms) wellfounded_imp_wellfounded_on: |
76 lemma (in M_basic) wellfounded_imp_wellfounded_on: |
77 "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)" |
77 "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)" |
78 by (auto simp add: wellfounded_def wellfounded_on_def) |
78 by (auto simp add: wellfounded_def wellfounded_on_def) |
79 |
79 |
80 lemma (in M_axioms) wellfounded_on_subset_A: |
80 lemma (in M_basic) wellfounded_on_subset_A: |
81 "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)" |
81 "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)" |
82 by (simp add: wellfounded_on_def, blast) |
82 by (simp add: wellfounded_on_def, blast) |
83 |
83 |
84 |
84 |
85 subsubsection {*Well-founded relations*} |
85 subsubsection {*Well-founded relations*} |
86 |
86 |
87 lemma (in M_axioms) wellfounded_on_iff_wellfounded: |
87 lemma (in M_basic) wellfounded_on_iff_wellfounded: |
88 "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)" |
88 "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)" |
89 apply (simp add: wellfounded_on_def wellfounded_def, safe) |
89 apply (simp add: wellfounded_on_def wellfounded_def, safe) |
90 apply blast |
90 apply blast |
91 apply (drule_tac x=x in rspec, assumption, blast) |
91 apply (drule_tac x=x in rspec, assumption, blast) |
92 done |
92 done |
93 |
93 |
94 lemma (in M_axioms) wellfounded_on_imp_wellfounded: |
94 lemma (in M_basic) wellfounded_on_imp_wellfounded: |
95 "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)" |
95 "[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)" |
96 by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff) |
96 by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff) |
97 |
97 |
98 lemma (in M_axioms) wellfounded_on_field_imp_wellfounded: |
98 lemma (in M_basic) wellfounded_on_field_imp_wellfounded: |
99 "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)" |
99 "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)" |
100 by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast) |
100 by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast) |
101 |
101 |
102 lemma (in M_axioms) wellfounded_iff_wellfounded_on_field: |
102 lemma (in M_basic) wellfounded_iff_wellfounded_on_field: |
103 "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)" |
103 "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)" |
104 by (blast intro: wellfounded_imp_wellfounded_on |
104 by (blast intro: wellfounded_imp_wellfounded_on |
105 wellfounded_on_field_imp_wellfounded) |
105 wellfounded_on_field_imp_wellfounded) |
106 |
106 |
107 (*Consider the least z in domain(r) such that P(z) does not hold...*) |
107 (*Consider the least z in domain(r) such that P(z) does not hold...*) |
108 lemma (in M_axioms) wellfounded_induct: |
108 lemma (in M_basic) wellfounded_induct: |
109 "[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x)); |
109 "[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x)); |
110 \<forall>x. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |] |
110 \<forall>x. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |] |
111 ==> P(a)"; |
111 ==> P(a)"; |
112 apply (simp (no_asm_use) add: wellfounded_def) |
112 apply (simp (no_asm_use) add: wellfounded_def) |
113 apply (drule_tac x="{z \<in> domain(r). ~P(z)}" in rspec) |
113 apply (drule_tac x="{z \<in> domain(r). ~P(z)}" in rspec) |
114 apply (blast dest: transM)+ |
114 apply (blast dest: transM)+ |
115 done |
115 done |
116 |
116 |
117 lemma (in M_axioms) wellfounded_on_induct: |
117 lemma (in M_basic) wellfounded_on_induct: |
118 "[| a\<in>A; wellfounded_on(M,A,r); M(A); |
118 "[| a\<in>A; wellfounded_on(M,A,r); M(A); |
119 separation(M, \<lambda>x. x\<in>A --> ~P(x)); |
119 separation(M, \<lambda>x. x\<in>A --> ~P(x)); |
120 \<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r --> P(y)) --> P(x) |] |
120 \<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r --> P(y)) --> P(x) |] |
121 ==> P(a)"; |
121 ==> P(a)"; |
122 apply (simp (no_asm_use) add: wellfounded_on_def) |
122 apply (simp (no_asm_use) add: wellfounded_on_def) |
124 apply (blast intro: transM)+ |
124 apply (blast intro: transM)+ |
125 done |
125 done |
126 |
126 |
127 text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction |
127 text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction |
128 hypothesis by removing the restriction to @{term A}.*} |
128 hypothesis by removing the restriction to @{term A}.*} |
129 lemma (in M_axioms) wellfounded_on_induct2: |
129 lemma (in M_basic) wellfounded_on_induct2: |
130 "[| a\<in>A; wellfounded_on(M,A,r); M(A); r \<subseteq> A*A; |
130 "[| a\<in>A; wellfounded_on(M,A,r); M(A); r \<subseteq> A*A; |
131 separation(M, \<lambda>x. x\<in>A --> ~P(x)); |
131 separation(M, \<lambda>x. x\<in>A --> ~P(x)); |
132 \<forall>x\<in>A. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |] |
132 \<forall>x\<in>A. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |] |
133 ==> P(a)"; |
133 ==> P(a)"; |
134 by (rule wellfounded_on_induct, assumption+, blast) |
134 by (rule wellfounded_on_induct, assumption+, blast) |
135 |
135 |
136 |
136 |
137 subsubsection {*Kunen's lemma IV 3.14, page 123*} |
137 subsubsection {*Kunen's lemma IV 3.14, page 123*} |
138 |
138 |
139 lemma (in M_axioms) linear_imp_relativized: |
139 lemma (in M_basic) linear_imp_relativized: |
140 "linear(A,r) ==> linear_rel(M,A,r)" |
140 "linear(A,r) ==> linear_rel(M,A,r)" |
141 by (simp add: linear_def linear_rel_def) |
141 by (simp add: linear_def linear_rel_def) |
142 |
142 |
143 lemma (in M_axioms) trans_on_imp_relativized: |
143 lemma (in M_basic) trans_on_imp_relativized: |
144 "trans[A](r) ==> transitive_rel(M,A,r)" |
144 "trans[A](r) ==> transitive_rel(M,A,r)" |
145 by (unfold transitive_rel_def trans_on_def, blast) |
145 by (unfold transitive_rel_def trans_on_def, blast) |
146 |
146 |
147 lemma (in M_axioms) wf_on_imp_relativized: |
147 lemma (in M_basic) wf_on_imp_relativized: |
148 "wf[A](r) ==> wellfounded_on(M,A,r)" |
148 "wf[A](r) ==> wellfounded_on(M,A,r)" |
149 apply (simp add: wellfounded_on_def wf_def wf_on_def, clarify) |
149 apply (simp add: wellfounded_on_def wf_def wf_on_def, clarify) |
150 apply (drule_tac x=x in spec, blast) |
150 apply (drule_tac x=x in spec, blast) |
151 done |
151 done |
152 |
152 |
153 lemma (in M_axioms) wf_imp_relativized: |
153 lemma (in M_basic) wf_imp_relativized: |
154 "wf(r) ==> wellfounded(M,r)" |
154 "wf(r) ==> wellfounded(M,r)" |
155 apply (simp add: wellfounded_def wf_def, clarify) |
155 apply (simp add: wellfounded_def wf_def, clarify) |
156 apply (drule_tac x=x in spec, blast) |
156 apply (drule_tac x=x in spec, blast) |
157 done |
157 done |
158 |
158 |
159 lemma (in M_axioms) well_ord_imp_relativized: |
159 lemma (in M_basic) well_ord_imp_relativized: |
160 "well_ord(A,r) ==> wellordered(M,A,r)" |
160 "well_ord(A,r) ==> wellordered(M,A,r)" |
161 by (simp add: wellordered_def well_ord_def tot_ord_def part_ord_def |
161 by (simp add: wellordered_def well_ord_def tot_ord_def part_ord_def |
162 linear_imp_relativized trans_on_imp_relativized wf_on_imp_relativized) |
162 linear_imp_relativized trans_on_imp_relativized wf_on_imp_relativized) |
163 |
163 |
164 |
164 |
165 subsection{* Relativized versions of order-isomorphisms and order types *} |
165 subsection{* Relativized versions of order-isomorphisms and order types *} |
166 |
166 |
167 lemma (in M_axioms) order_isomorphism_abs [simp]: |
167 lemma (in M_basic) order_isomorphism_abs [simp]: |
168 "[| M(A); M(B); M(f) |] |
168 "[| M(A); M(B); M(f) |] |
169 ==> order_isomorphism(M,A,r,B,s,f) <-> f \<in> ord_iso(A,r,B,s)" |
169 ==> order_isomorphism(M,A,r,B,s,f) <-> f \<in> ord_iso(A,r,B,s)" |
170 by (simp add: apply_closed order_isomorphism_def ord_iso_def) |
170 by (simp add: apply_closed order_isomorphism_def ord_iso_def) |
171 |
171 |
172 lemma (in M_axioms) pred_set_abs [simp]: |
172 lemma (in M_basic) pred_set_abs [simp]: |
173 "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) <-> B = Order.pred(A,x,r)" |
173 "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) <-> B = Order.pred(A,x,r)" |
174 apply (simp add: pred_set_def Order.pred_def) |
174 apply (simp add: pred_set_def Order.pred_def) |
175 apply (blast dest: transM) |
175 apply (blast dest: transM) |
176 done |
176 done |
177 |
177 |
178 lemma (in M_axioms) pred_closed [intro,simp]: |
178 lemma (in M_basic) pred_closed [intro,simp]: |
179 "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))" |
179 "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))" |
180 apply (simp add: Order.pred_def) |
180 apply (simp add: Order.pred_def) |
181 apply (insert pred_separation [of r x], simp) |
181 apply (insert pred_separation [of r x], simp) |
182 done |
182 done |
183 |
183 |
184 lemma (in M_axioms) membership_abs [simp]: |
184 lemma (in M_basic) membership_abs [simp]: |
185 "[| M(r); M(A) |] ==> membership(M,A,r) <-> r = Memrel(A)" |
185 "[| M(r); M(A) |] ==> membership(M,A,r) <-> r = Memrel(A)" |
186 apply (simp add: membership_def Memrel_def, safe) |
186 apply (simp add: membership_def Memrel_def, safe) |
187 apply (rule equalityI) |
187 apply (rule equalityI) |
188 apply clarify |
188 apply clarify |
189 apply (frule transM, assumption) |
189 apply (frule transM, assumption) |
283 apply (drule ord_iso_sym) |
283 apply (drule ord_iso_sym) |
284 (*two symmetric cases*) |
284 (*two symmetric cases*) |
285 apply (blast dest: wellordered_iso_pred_eq_lemma)+ |
285 apply (blast dest: wellordered_iso_pred_eq_lemma)+ |
286 done |
286 done |
287 |
287 |
288 lemma (in M_axioms) wellfounded_on_asym: |
288 lemma (in M_basic) wellfounded_on_asym: |
289 "[| wellfounded_on(M,A,r); <a,x>\<in>r; a\<in>A; x\<in>A; M(A) |] ==> <x,a>\<notin>r" |
289 "[| wellfounded_on(M,A,r); <a,x>\<in>r; a\<in>A; x\<in>A; M(A) |] ==> <x,a>\<notin>r" |
290 apply (simp add: wellfounded_on_def) |
290 apply (simp add: wellfounded_on_def) |
291 apply (drule_tac x="{x,a}" in rspec) |
291 apply (drule_tac x="{x,a}" in rspec) |
292 apply (blast dest: transM)+ |
292 apply (blast dest: transM)+ |
293 done |
293 done |
294 |
294 |
295 lemma (in M_axioms) wellordered_asym: |
295 lemma (in M_basic) wellordered_asym: |
296 "[| wellordered(M,A,r); <a,x>\<in>r; a\<in>A; x\<in>A; M(A) |] ==> <x,a>\<notin>r" |
296 "[| wellordered(M,A,r); <a,x>\<in>r; a\<in>A; x\<in>A; M(A) |] ==> <x,a>\<notin>r" |
297 by (simp add: wellordered_def, blast dest: wellfounded_on_asym) |
297 by (simp add: wellordered_def, blast dest: wellfounded_on_asym) |
298 |
298 |
299 |
299 |
300 text{*Surely a shorter proof using lemmas in @{text Order}? |
300 text{*Surely a shorter proof using lemmas in @{text Order}? |
301 Like @{text well_ord_iso_preserving}?*} |
301 Like @{text well_ord_iso_preserving}?*} |
302 lemma (in M_axioms) ord_iso_pred_imp_lt: |
302 lemma (in M_basic) ord_iso_pred_imp_lt: |
303 "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i)); |
303 "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i)); |
304 g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j)); |
304 g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j)); |
305 wellordered(M,A,r); x \<in> A; y \<in> A; M(A); M(r); M(f); M(g); M(j); |
305 wellordered(M,A,r); x \<in> A; y \<in> A; M(A); M(r); M(f); M(g); M(j); |
306 Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |] |
306 Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |] |
307 ==> i < j" |
307 ==> i < j" |
370 otype :: "[i=>o,i,i,i] => o" --{*the order types themselves*} |
370 otype :: "[i=>o,i,i,i] => o" --{*the order types themselves*} |
371 "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)" |
371 "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)" |
372 |
372 |
373 |
373 |
374 |
374 |
375 lemma (in M_axioms) obase_iff: |
375 lemma (in M_basic) obase_iff: |
376 "[| M(A); M(r); M(z) |] |
376 "[| M(A); M(r); M(z) |] |
377 ==> obase(M,A,r,z) <-> |
377 ==> obase(M,A,r,z) <-> |
378 z = {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & |
378 z = {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & |
379 g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}" |
379 g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}" |
380 apply (simp add: obase_def Memrel_closed pred_closed) |
380 apply (simp add: obase_def Memrel_closed pred_closed) |
398 apply (drule_tac [2] x=z in rspec) |
398 apply (drule_tac [2] x=z in rspec) |
399 apply (drule_tac x=z in rspec) |
399 apply (drule_tac x=z in rspec) |
400 apply (blast dest: transM)+ |
400 apply (blast dest: transM)+ |
401 done |
401 done |
402 |
402 |
403 lemma (in M_axioms) omap_unique: |
403 lemma (in M_basic) omap_unique: |
404 "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" |
404 "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" |
405 apply (rule equality_iffI) |
405 apply (rule equality_iffI) |
406 apply (simp add: omap_iff) |
406 apply (simp add: omap_iff) |
407 done |
407 done |
408 |
408 |
409 lemma (in M_axioms) omap_yields_Ord: |
409 lemma (in M_basic) omap_yields_Ord: |
410 "[| omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) |] ==> Ord(x)" |
410 "[| omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) |] ==> Ord(x)" |
411 apply (simp add: omap_def, blast) |
411 apply (simp add: omap_def, blast) |
412 done |
412 done |
413 |
413 |
414 lemma (in M_axioms) otype_iff: |
414 lemma (in M_basic) otype_iff: |
415 "[| otype(M,A,r,i); M(A); M(r); M(i) |] |
415 "[| otype(M,A,r,i); M(A); M(r); M(i) |] |
416 ==> x \<in> i <-> |
416 ==> x \<in> i <-> |
417 (M(x) & Ord(x) & |
417 (M(x) & Ord(x) & |
418 (\<exists>a\<in>A. \<exists>g[M]. g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))))" |
418 (\<exists>a\<in>A. \<exists>g[M]. g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))))" |
419 apply (auto simp add: omap_iff otype_def) |
419 apply (auto simp add: omap_iff otype_def) |
450 apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption) |
450 apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption) |
451 apply (safe elim!: predE) |
451 apply (safe elim!: predE) |
452 apply (blast intro: restrict_ord_iso ord_iso_sym ltI dest: transM) |
452 apply (blast intro: restrict_ord_iso ord_iso_sym ltI dest: transM) |
453 done |
453 done |
454 |
454 |
455 lemma (in M_axioms) domain_omap: |
455 lemma (in M_basic) domain_omap: |
456 "[| omap(M,A,r,f); obase(M,A,r,B); M(A); M(r); M(B); M(f) |] |
456 "[| omap(M,A,r,f); obase(M,A,r,B); M(A); M(r); M(B); M(f) |] |
457 ==> domain(f) = B" |
457 ==> domain(f) = B" |
458 apply (rotate_tac 2) |
458 apply (rotate_tac 2) |
459 apply (simp add: domain_closed obase_iff) |
459 apply (simp add: domain_closed obase_iff) |
460 apply (rule equality_iffI) |
460 apply (rule equality_iffI) |
461 apply (simp add: domain_iff omap_iff, blast) |
461 apply (simp add: domain_iff omap_iff, blast) |
462 done |
462 done |
463 |
463 |
464 lemma (in M_axioms) omap_subset: |
464 lemma (in M_basic) omap_subset: |
465 "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
465 "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
466 M(A); M(r); M(f); M(B); M(i) |] ==> f \<subseteq> B * i" |
466 M(A); M(r); M(f); M(B); M(i) |] ==> f \<subseteq> B * i" |
467 apply (rotate_tac 3, clarify) |
467 apply (rotate_tac 3, clarify) |
468 apply (simp add: omap_iff obase_iff) |
468 apply (simp add: omap_iff obase_iff) |
469 apply (force simp add: otype_iff) |
469 apply (force simp add: otype_iff) |
470 done |
470 done |
471 |
471 |
472 lemma (in M_axioms) omap_funtype: |
472 lemma (in M_basic) omap_funtype: |
473 "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
473 "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
474 M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> B -> i" |
474 M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> B -> i" |
475 apply (rotate_tac 3) |
475 apply (rotate_tac 3) |
476 apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) |
476 apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) |
477 apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) |
477 apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) |
478 done |
478 done |
479 |
479 |
480 |
480 |
481 lemma (in M_axioms) wellordered_omap_bij: |
481 lemma (in M_basic) wellordered_omap_bij: |
482 "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
482 "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
483 M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> bij(B,i)" |
483 M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> bij(B,i)" |
484 apply (insert omap_funtype [of A r f B i]) |
484 apply (insert omap_funtype [of A r f B i]) |
485 apply (auto simp add: bij_def inj_def) |
485 apply (auto simp add: bij_def inj_def) |
486 prefer 2 apply (blast intro: fun_is_surj dest: otype_eq_range) |
486 prefer 2 apply (blast intro: fun_is_surj dest: otype_eq_range) |
537 apply (erule_tac b=c in trans_onD) |
537 apply (erule_tac b=c in trans_onD) |
538 apply (rule ord_iso_converse1 [OF omap_ord_iso [of A r f B i]]) |
538 apply (rule ord_iso_converse1 [OF omap_ord_iso [of A r f B i]]) |
539 apply (auto simp add: obase_iff) |
539 apply (auto simp add: obase_iff) |
540 done |
540 done |
541 |
541 |
542 lemma (in M_axioms) restrict_omap_ord_iso: |
542 lemma (in M_basic) restrict_omap_ord_iso: |
543 "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
543 "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
544 D \<subseteq> B; M(A); M(r); M(f); M(B); M(i) |] |
544 D \<subseteq> B; M(A); M(r); M(f); M(B); M(i) |] |
545 ==> restrict(f,D) \<in> (\<langle>D,r\<rangle> \<cong> \<langle>f``D, Memrel(f``D)\<rangle>)" |
545 ==> restrict(f,D) \<in> (\<langle>D,r\<rangle> \<cong> \<langle>f``D, Memrel(f``D)\<rangle>)" |
546 apply (frule ord_iso_restrict_image [OF omap_ord_iso [of A r f B i]], |
546 apply (frule ord_iso_restrict_image [OF omap_ord_iso [of A r f B i]], |
547 assumption+) |
547 assumption+) |
548 apply (drule ord_iso_sym [THEN subset_ord_iso_Memrel]) |
548 apply (drule ord_iso_sym [THEN subset_ord_iso_Memrel]) |
549 apply (blast dest: subsetD [OF omap_subset]) |
549 apply (blast dest: subsetD [OF omap_subset]) |
550 apply (drule ord_iso_sym, simp) |
550 apply (drule ord_iso_sym, simp) |
551 done |
551 done |
552 |
552 |
553 lemma (in M_axioms) obase_equals: |
553 lemma (in M_basic) obase_equals: |
554 "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
554 "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
555 M(A); M(r); M(f); M(B); M(i) |] ==> B = A" |
555 M(A); M(r); M(f); M(B); M(i) |] ==> B = A" |
556 apply (rotate_tac 4) |
556 apply (rotate_tac 4) |
557 apply (rule equalityI, force simp add: obase_iff, clarify) |
557 apply (rule equalityI, force simp add: obase_iff, clarify) |
558 apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp) |
558 apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp) |
568 |
568 |
569 |
569 |
570 |
570 |
571 text{*Main result: @{term om} gives the order-isomorphism |
571 text{*Main result: @{term om} gives the order-isomorphism |
572 @{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"} *} |
572 @{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"} *} |
573 theorem (in M_axioms) omap_ord_iso_otype: |
573 theorem (in M_basic) omap_ord_iso_otype: |
574 "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
574 "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); |
575 M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))" |
575 M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))" |
576 apply (frule omap_ord_iso, assumption+) |
576 apply (frule omap_ord_iso, assumption+) |
577 apply (frule obase_equals, assumption+, blast) |
577 apply (frule obase_equals, assumption+, blast) |
578 done |
578 done |
579 |
579 |
580 lemma (in M_axioms) obase_exists: |
580 lemma (in M_basic) obase_exists: |
581 "[| M(A); M(r) |] ==> \<exists>z[M]. obase(M,A,r,z)" |
581 "[| M(A); M(r) |] ==> \<exists>z[M]. obase(M,A,r,z)" |
582 apply (simp add: obase_def) |
582 apply (simp add: obase_def) |
583 apply (insert obase_separation [of A r]) |
583 apply (insert obase_separation [of A r]) |
584 apply (simp add: separation_def) |
584 apply (simp add: separation_def) |
585 done |
585 done |
586 |
586 |
587 lemma (in M_axioms) omap_exists: |
587 lemma (in M_basic) omap_exists: |
588 "[| M(A); M(r) |] ==> \<exists>z[M]. omap(M,A,r,z)" |
588 "[| M(A); M(r) |] ==> \<exists>z[M]. omap(M,A,r,z)" |
589 apply (insert obase_exists [of A r]) |
589 apply (insert obase_exists [of A r]) |
590 apply (simp add: omap_def) |
590 apply (simp add: omap_def) |
591 apply (insert omap_replacement [of A r]) |
591 apply (insert omap_replacement [of A r]) |
592 apply (simp add: strong_replacement_def, clarify) |
592 apply (simp add: strong_replacement_def, clarify) |
599 apply (simp add: Memrel_closed pred_closed obase_iff, blast, assumption) |
599 apply (simp add: Memrel_closed pred_closed obase_iff, blast, assumption) |
600 done |
600 done |
601 |
601 |
602 declare rall_simps [simp] rex_simps [simp] |
602 declare rall_simps [simp] rex_simps [simp] |
603 |
603 |
604 lemma (in M_axioms) otype_exists: |
604 lemma (in M_basic) otype_exists: |
605 "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i[M]. otype(M,A,r,i)" |
605 "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i[M]. otype(M,A,r,i)" |
606 apply (insert omap_exists [of A r]) |
606 apply (insert omap_exists [of A r]) |
607 apply (simp add: otype_def, safe) |
607 apply (simp add: otype_def, safe) |
608 apply (rule_tac x="range(x)" in rexI) |
608 apply (rule_tac x="range(x)" in rexI) |
609 apply blast+ |
609 apply blast+ |
610 done |
610 done |
611 |
611 |
612 theorem (in M_axioms) omap_ord_iso_otype': |
612 theorem (in M_basic) omap_ord_iso_otype': |
613 "[| wellordered(M,A,r); M(A); M(r) |] |
613 "[| wellordered(M,A,r); M(A); M(r) |] |
614 ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))" |
614 ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))" |
615 apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify) |
615 apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify) |
616 apply (rename_tac i) |
616 apply (rename_tac i) |
617 apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) |
617 apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) |
618 apply (rule Ord_otype) |
618 apply (rule Ord_otype) |
619 apply (force simp add: otype_def range_closed) |
619 apply (force simp add: otype_def range_closed) |
620 apply (simp_all add: wellordered_is_trans_on) |
620 apply (simp_all add: wellordered_is_trans_on) |
621 done |
621 done |
622 |
622 |
623 lemma (in M_axioms) ordertype_exists: |
623 lemma (in M_basic) ordertype_exists: |
624 "[| wellordered(M,A,r); M(A); M(r) |] |
624 "[| wellordered(M,A,r); M(A); M(r) |] |
625 ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))" |
625 ==> \<exists>f[M]. (\<exists>i[M]. Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))" |
626 apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify) |
626 apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify) |
627 apply (rename_tac i) |
627 apply (rename_tac i) |
628 apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype') |
628 apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype') |
630 apply (force simp add: otype_def range_closed) |
630 apply (force simp add: otype_def range_closed) |
631 apply (simp_all add: wellordered_is_trans_on) |
631 apply (simp_all add: wellordered_is_trans_on) |
632 done |
632 done |
633 |
633 |
634 |
634 |
635 lemma (in M_axioms) relativized_imp_well_ord: |
635 lemma (in M_basic) relativized_imp_well_ord: |
636 "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" |
636 "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" |
637 apply (insert ordertype_exists [of A r], simp) |
637 apply (insert ordertype_exists [of A r], simp) |
638 apply (blast intro: well_ord_ord_iso well_ord_Memrel) |
638 apply (blast intro: well_ord_ord_iso well_ord_Memrel) |
639 done |
639 done |
640 |
640 |
641 subsection {*Kunen's theorem 5.4, poage 127*} |
641 subsection {*Kunen's theorem 5.4, poage 127*} |
642 |
642 |
643 text{*(a) The notion of Wellordering is absolute*} |
643 text{*(a) The notion of Wellordering is absolute*} |
644 theorem (in M_axioms) well_ord_abs [simp]: |
644 theorem (in M_basic) well_ord_abs [simp]: |
645 "[| M(A); M(r) |] ==> wellordered(M,A,r) <-> well_ord(A,r)" |
645 "[| M(A); M(r) |] ==> wellordered(M,A,r) <-> well_ord(A,r)" |
646 by (blast intro: well_ord_imp_relativized relativized_imp_well_ord) |
646 by (blast intro: well_ord_imp_relativized relativized_imp_well_ord) |
647 |
647 |
648 |
648 |
649 text{*(b) Order types are absolute*} |
649 text{*(b) Order types are absolute*} |
650 lemma (in M_axioms) |
650 lemma (in M_basic) |
651 "[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i)); |
651 "[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i)); |
652 M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)" |
652 M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)" |
653 by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso |
653 by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso |
654 Ord_iso_implies_eq ord_iso_sym ord_iso_trans) |
654 Ord_iso_implies_eq ord_iso_sym ord_iso_trans) |
655 |
655 |