src/ZF/Constructible/Wellorderings.thy
changeset 13293 09276ee04361
parent 13269 3ba9be497c33
child 13295 ca2e9b273472
equal deleted 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) |]