134 apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype]) |
134 apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype]) |
135 apply (simp add: left_inverse_bij [OF ord_iso_is_bij]) |
135 apply (simp add: left_inverse_bij [OF ord_iso_is_bij]) |
136 done |
136 done |
137 |
137 |
138 |
138 |
139 definition |
139 definition |
140 |
140 obase :: "[i=>o,i,i] => i" where |
141 obase :: "[i=>o,i,i] => i" |
|
142 --{*the domain of @{text om}, eventually shown to equal @{text A}*} |
141 --{*the domain of @{text om}, eventually shown to equal @{text A}*} |
143 "obase(M,A,r) == {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & |
142 "obase(M,A,r) == {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & |
144 g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}" |
143 g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}" |
145 |
144 |
146 omap :: "[i=>o,i,i,i] => o" |
145 definition |
|
146 omap :: "[i=>o,i,i,i] => o" where |
147 --{*the function that maps wosets to order types*} |
147 --{*the function that maps wosets to order types*} |
148 "omap(M,A,r,f) == |
148 "omap(M,A,r,f) == |
149 \<forall>z[M]. |
149 \<forall>z[M]. |
150 z \<in> f <-> (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & |
150 z \<in> f <-> (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & |
151 g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))" |
151 g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))" |
152 |
152 |
153 |
153 definition |
154 otype :: "[i=>o,i,i,i] => o" --{*the order types themselves*} |
154 otype :: "[i=>o,i,i,i] => o" where --{*the order types themselves*} |
155 "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)" |
155 "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)" |
156 |
156 |
157 |
157 |
158 text{*Can also be proved with the premise @{term "M(z)"} instead of |
158 text{*Can also be proved with the premise @{term "M(z)"} instead of |
159 @{term "M(f)"}, but that version is less useful. This lemma |
159 @{term "M(f)"}, but that version is less useful. This lemma |
412 text{*Note: the remainder of this theory is not needed elsewhere.*} |
412 text{*Note: the remainder of this theory is not needed elsewhere.*} |
413 |
413 |
414 subsubsection{*Ordinal Addition*} |
414 subsubsection{*Ordinal Addition*} |
415 |
415 |
416 (*FIXME: update to use new techniques!!*) |
416 (*FIXME: update to use new techniques!!*) |
417 definition |
|
418 (*This expresses ordinal addition in the language of ZF. It also |
417 (*This expresses ordinal addition in the language of ZF. It also |
419 provides an abbreviation that can be used in the instance of strong |
418 provides an abbreviation that can be used in the instance of strong |
420 replacement below. Here j is used to define the relation, namely |
419 replacement below. Here j is used to define the relation, namely |
421 Memrel(succ(j)), while x determines the domain of f.*) |
420 Memrel(succ(j)), while x determines the domain of f.*) |
422 is_oadd_fun :: "[i=>o,i,i,i,i] => o" |
421 definition |
|
422 is_oadd_fun :: "[i=>o,i,i,i,i] => o" where |
423 "is_oadd_fun(M,i,j,x,f) == |
423 "is_oadd_fun(M,i,j,x,f) == |
424 (\<forall>sj msj. M(sj) --> M(msj) --> |
424 (\<forall>sj msj. M(sj) --> M(msj) --> |
425 successor(M,j,sj) --> membership(M,sj,msj) --> |
425 successor(M,j,sj) --> membership(M,sj,msj) --> |
426 M_is_recfun(M, |
426 M_is_recfun(M, |
427 %x g y. \<exists>gx[M]. image(M,g,x,gx) & union(M,i,gx,y), |
427 %x g y. \<exists>gx[M]. image(M,g,x,gx) & union(M,i,gx,y), |
428 msj, x, f))" |
428 msj, x, f))" |
429 |
429 |
430 is_oadd :: "[i=>o,i,i,i] => o" |
430 definition |
|
431 is_oadd :: "[i=>o,i,i,i] => o" where |
431 "is_oadd(M,i,j,k) == |
432 "is_oadd(M,i,j,k) == |
432 (~ ordinal(M,i) & ~ ordinal(M,j) & k=0) | |
433 (~ ordinal(M,i) & ~ ordinal(M,j) & k=0) | |
433 (~ ordinal(M,i) & ordinal(M,j) & k=j) | |
434 (~ ordinal(M,i) & ordinal(M,j) & k=j) | |
434 (ordinal(M,i) & ~ ordinal(M,j) & k=i) | |
435 (ordinal(M,i) & ~ ordinal(M,j) & k=i) | |
435 (ordinal(M,i) & ordinal(M,j) & |
436 (ordinal(M,i) & ordinal(M,j) & |
436 (\<exists>f fj sj. M(f) & M(fj) & M(sj) & |
437 (\<exists>f fj sj. M(f) & M(fj) & M(sj) & |
437 successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) & |
438 successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) & |
438 fun_apply(M,f,j,fj) & fj = k))" |
439 fun_apply(M,f,j,fj) & fj = k))" |
439 |
440 |
|
441 definition |
440 (*NEEDS RELATIVIZATION*) |
442 (*NEEDS RELATIVIZATION*) |
441 omult_eqns :: "[i,i,i,i] => o" |
443 omult_eqns :: "[i,i,i,i] => o" where |
442 "omult_eqns(i,x,g,z) == |
444 "omult_eqns(i,x,g,z) == |
443 Ord(x) & |
445 Ord(x) & |
444 (x=0 --> z=0) & |
446 (x=0 --> z=0) & |
445 (\<forall>j. x = succ(j) --> z = g`j ++ i) & |
447 (\<forall>j. x = succ(j) --> z = g`j ++ i) & |
446 (Limit(x) --> z = \<Union>(g``x))" |
448 (Limit(x) --> z = \<Union>(g``x))" |
447 |
449 |
448 is_omult_fun :: "[i=>o,i,i,i] => o" |
450 definition |
|
451 is_omult_fun :: "[i=>o,i,i,i] => o" where |
449 "is_omult_fun(M,i,j,f) == |
452 "is_omult_fun(M,i,j,f) == |
450 (\<exists>df. M(df) & is_function(M,f) & |
453 (\<exists>df. M(df) & is_function(M,f) & |
451 is_domain(M,f,df) & subset(M, j, df)) & |
454 is_domain(M,f,df) & subset(M, j, df)) & |
452 (\<forall>x\<in>j. omult_eqns(i,x,f,f`x))" |
455 (\<forall>x\<in>j. omult_eqns(i,x,f,f`x))" |
453 |
456 |
454 is_omult :: "[i=>o,i,i,i] => o" |
457 definition |
|
458 is_omult :: "[i=>o,i,i,i] => o" where |
455 "is_omult(M,i,j,k) == |
459 "is_omult(M,i,j,k) == |
456 \<exists>f fj sj. M(f) & M(fj) & M(sj) & |
460 \<exists>f fj sj. M(f) & M(fj) & M(sj) & |
457 successor(M,j,sj) & is_omult_fun(M,i,sj,f) & |
461 successor(M,j,sj) & is_omult_fun(M,i,sj,f) & |
458 fun_apply(M,f,j,fj) & fj = k" |
462 fun_apply(M,f,j,fj) & fj = k" |
459 |
463 |