src/ZF/Constructible/Wellorderings.thy
 changeset 13293 09276ee04361 parent 13269 3ba9be497c33 child 13295 ca2e9b273472
equal inserted replaced
13292:f504f5d284d3 13293:09276ee04361
`   344 constdefs`
`   344 constdefs`
`   345   `
`   345   `
`   346   obase :: "[i=>o,i,i,i] => o"`
`   346   obase :: "[i=>o,i,i,i] => o"`
`   347        --{*the domain of @{text om}, eventually shown to equal @{text A}*}`
`   347        --{*the domain of @{text om}, eventually shown to equal @{text A}*}`
`   348    "obase(M,A,r,z) == `
`   348    "obase(M,A,r,z) == `
`   349 	\<forall>a. M(a) --> `
`   349 	\<forall>a[M]. `
`   350          (a \<in> z <-> `
`   350          a \<in> z <-> `
`   351           (a\<in>A & (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & `
`   351           (a\<in>A & (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & `
`   352                                membership(M,x,mx) & pred_set(M,A,a,r,par) &  `
`   352                                membership(M,x,mx) & pred_set(M,A,a,r,par) &  `
`   353                                order_isomorphism(M,par,r,x,mx,g))))"`
`   353                                order_isomorphism(M,par,r,x,mx,g)))"`
`   354 `
`   354 `
`   355 `
`   355 `
`   356   omap :: "[i=>o,i,i,i] => o"  `
`   356   omap :: "[i=>o,i,i,i] => o"  `
`   357     --{*the function that maps wosets to order types*}`
`   357     --{*the function that maps wosets to order types*}`
`   358    "omap(M,A,r,f) == `
`   358    "omap(M,A,r,f) == `
`   359 	\<forall>z. M(z) --> `
`   359 	\<forall>z[M].`
`   360          (z \<in> f <-> `
`   360          z \<in> f <-> `
`   361           (\<exists>a\<in>A. M(a) & `
`   361           (\<exists>a\<in>A. M(a) & `
`   362            (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & `
`   362            (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & `
`   363                          pair(M,a,x,z) & membership(M,x,mx) & `
`   363                          pair(M,a,x,z) & membership(M,x,mx) & `
`   364                          pred_set(M,A,a,r,par) &  `
`   364                          pred_set(M,A,a,r,par) &  `
`   365                          order_isomorphism(M,par,r,x,mx,g))))"`
`   365                          order_isomorphism(M,par,r,x,mx,g)))"`
`   366 `
`   366 `
`   367 `
`   367 `
`   368   otype :: "[i=>o,i,i,i] => o"  --{*the order types themselves*}`
`   368   otype :: "[i=>o,i,i,i] => o"  --{*the order types themselves*}`
`   369    "otype(M,A,r,i) == \<exists>f. M(f) & omap(M,A,r,f) & is_range(M,f,i)"`
`   369    "otype(M,A,r,i) == \<exists>f. M(f) & omap(M,A,r,f) & is_range(M,f,i)"`
`   370 `
`   370 `
`   390       ==> z \<in> f <->`
`   390       ==> z \<in> f <->`
`   391       (\<exists>a\<in>A. \<exists>x g. M(x) & M(g) & z = <a,x> & Ord(x) & `
`   391       (\<exists>a\<in>A. \<exists>x g. M(x) & M(g) & z = <a,x> & Ord(x) & `
`   392                    g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"`
`   392                    g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"`
`   393 apply (rotate_tac 1) `
`   393 apply (rotate_tac 1) `
`   394 apply (simp add: omap_def Memrel_closed pred_closed) `
`   394 apply (simp add: omap_def Memrel_closed pred_closed) `
`   395 apply (rule iffI) `
`   395 apply (rule iffI)`
`   396 apply (drule_tac x=z in spec, blast dest: transM)+ `
`   396  apply (drule_tac [2] x=z in rspec)`
`       `
`   397  apply (drule_tac x=z in rspec)`
`       `
`   398  apply (blast dest: transM)+`
`   397 done`
`   399 done`
`   398 `
`   400 `
`   399 lemma (in M_axioms) omap_unique:`
`   401 lemma (in M_axioms) omap_unique:`
`   400      "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" `
`   402      "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" `
`   401 apply (rule equality_iffI) `
`   403 apply (rule equality_iffI) `
`   574 theorem (in M_axioms) omap_ord_iso_otype:`
`   576 theorem (in M_axioms) omap_ord_iso_otype:`
`   575      "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);`
`   577      "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);`
`   576        M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"`
`   578        M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"`
`   577 apply (frule omap_ord_iso, assumption+) `
`   579 apply (frule omap_ord_iso, assumption+) `
`   578 apply (frule obase_equals, assumption+, blast) `
`   580 apply (frule obase_equals, assumption+, blast) `
`   579 done`
`   581 done `
`   580 `
`   582 `
`   581 lemma (in M_axioms) obase_exists:`
`   583 lemma (in M_axioms) obase_exists:`
`   582      "[| M(A); M(r) |] ==> \<exists>z. M(z) & obase(M,A,r,z)"`
`   584      "[| M(A); M(r) |] ==> \<exists>z[M]. obase(M,A,r,z)"`
`   583 apply (simp add: obase_def) `
`   585 apply (simp add: obase_def) `
`   584 apply (insert obase_separation [of A r])`
`   586 apply (insert obase_separation [of A r])`
`   585 apply (simp add: separation_def)  `
`   587 apply (simp add: separation_def)  `
`   586 done`
`   588 done`
`   587 `
`   589 `
`   588 lemma (in M_axioms) omap_exists:`
`   590 lemma (in M_axioms) omap_exists:`
`   589      "[| M(A); M(r) |] ==> \<exists>z. M(z) & omap(M,A,r,z)"`
`   591      "[| M(A); M(r) |] ==> \<exists>z[M]. omap(M,A,r,z)"`
`   590 apply (insert obase_exists [of A r]) `
`   592 apply (insert obase_exists [of A r]) `
`   591 apply (simp add: omap_def) `
`   593 apply (simp add: omap_def) `
`   592 apply (insert omap_replacement [of A r])`
`   594 apply (insert omap_replacement [of A r])`
`   593 apply (simp add: strong_replacement_def, clarify) `
`   595 apply (simp add: strong_replacement_def, clarify) `
`   594 apply (drule_tac x=z in spec, clarify) `
`   596 apply (drule_tac x=x in spec, clarify) `
`   595 apply (simp add: Memrel_closed pred_closed obase_iff)`
`   597 apply (simp add: Memrel_closed pred_closed obase_iff)`
`   596 apply (erule impE) `
`   598 apply (erule impE) `
`   597  apply (clarsimp simp add: univalent_def)`
`   599  apply (clarsimp simp add: univalent_def)`
`   598  apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)  `
`   600  apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)  `
`   599 apply (rule_tac x=Y in exI) `
`   601 apply (rule_tac x=Y in rexI) `
`   600 apply (simp add: Memrel_closed pred_closed obase_iff, blast)   `
`   602 apply (simp add: Memrel_closed pred_closed obase_iff, blast, assumption)`
`   601 done`
`   603 done`
`       `
`   604 `
`       `
`   605 declare rall_simps [simp] rex_simps [simp]`
`   602 `
`   606 `
`   603 lemma (in M_axioms) otype_exists:`
`   607 lemma (in M_axioms) otype_exists:`
`   604      "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i. M(i) & otype(M,A,r,i)"`
`   608      "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i. M(i) & otype(M,A,r,i)"`
`   605 apply (insert omap_exists [of A r]) `
`   609 apply (insert omap_exists [of A r])  `
`   606 apply (simp add: otype_def, clarify) `
`   610 apply (simp add: otype_def, safe)`
`   607 apply (rule_tac x="range(z)" in exI) `
`   611 apply (rule_tac x="range(x)" in exI) `
`   608 apply blast `
`   612 apply blast `
`   609 done`
`   613 done`
`   610 `
`   614 `
`   611 theorem (in M_axioms) omap_ord_iso_otype:`
`   615 theorem (in M_axioms) omap_ord_iso_otype:`
`   612      "[| wellordered(M,A,r); M(A); M(r) |]`
`   616      "[| wellordered(M,A,r); M(A); M(r) |]`