src/ZF/Constructible/Wellorderings.thy
changeset 13306 6eebcddee32b
parent 13299 3a932abf97e8
child 13339 0f89104dd377
     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Fri Jul 05 17:48:05 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Fri Jul 05 18:33:50 2002 +0200
     1.3 @@ -347,9 +347,9 @@
     1.4     "obase(M,A,r,z) == 
     1.5  	\<forall>a[M]. 
     1.6           a \<in> z <-> 
     1.7 -          (a\<in>A & (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & 
     1.8 -                               membership(M,x,mx) & pred_set(M,A,a,r,par) &  
     1.9 -                               order_isomorphism(M,par,r,x,mx,g)))"
    1.10 +          (a\<in>A & (\<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
    1.11 +                   ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
    1.12 +                   order_isomorphism(M,par,r,x,mx,g)))"
    1.13  
    1.14  
    1.15    omap :: "[i=>o,i,i,i] => o"  
    1.16 @@ -358,10 +358,9 @@
    1.17  	\<forall>z[M].
    1.18           z \<in> f <-> 
    1.19            (\<exists>a[M]. a\<in>A & 
    1.20 -           (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & 
    1.21 -                         pair(M,a,x,z) & membership(M,x,mx) & 
    1.22 -                         pred_set(M,A,a,r,par) &  
    1.23 -                         order_isomorphism(M,par,r,x,mx,g)))"
    1.24 +           (\<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M]. 
    1.25 +                ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
    1.26 +                pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g)))"
    1.27  
    1.28  
    1.29    otype :: "[i=>o,i,i,i] => o"  --{*the order types themselves*}
    1.30 @@ -372,7 +371,7 @@
    1.31  lemma (in M_axioms) obase_iff:
    1.32       "[| M(A); M(r); M(z) |] 
    1.33        ==> obase(M,A,r,z) <-> 
    1.34 -          z = {a\<in>A. \<exists>x g. M(x) & M(g) & Ord(x) & 
    1.35 +          z = {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & 
    1.36                            g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
    1.37  apply (simp add: obase_def Memrel_closed pred_closed)
    1.38  apply (rule iffI) 
    1.39 @@ -387,8 +386,8 @@
    1.40  lemma (in M_axioms) omap_iff:
    1.41       "[| omap(M,A,r,f); M(A); M(r); M(f) |] 
    1.42        ==> z \<in> f <->
    1.43 -      (\<exists>a\<in>A. \<exists>x g. M(x) & M(g) & z = <a,x> & Ord(x) & 
    1.44 -                   g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
    1.45 +      (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
    1.46 +                        g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
    1.47  apply (rotate_tac 1) 
    1.48  apply (simp add: omap_def Memrel_closed pred_closed) 
    1.49  apply (rule iffI)
    1.50 @@ -411,19 +410,18 @@
    1.51  lemma (in M_axioms) otype_iff:
    1.52       "[| otype(M,A,r,i); M(A); M(r); M(i) |] 
    1.53        ==> x \<in> i <-> 
    1.54 -          (\<exists>a\<in>A. \<exists>g. M(x) & M(g) & Ord(x) & 
    1.55 -                     g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
    1.56 -apply (simp add: otype_def, auto)
    1.57 -  apply (blast dest: transM)
    1.58 - apply (blast dest!: omap_iff intro: transM)
    1.59 -apply (rename_tac a g) 
    1.60 -apply (rule_tac a=a in rangeI) 
    1.61 +          (M(x) & Ord(x) & 
    1.62 +           (\<exists>a\<in>A. \<exists>g[M]. g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))))"
    1.63 +apply (auto simp add: omap_iff otype_def)
    1.64 + apply (blast intro: transM) 
    1.65 +apply (rule rangeI) 
    1.66  apply (frule transM, assumption)
    1.67  apply (simp add: omap_iff, blast)
    1.68  done
    1.69  
    1.70  lemma (in M_axioms) otype_eq_range:
    1.71 -     "[| omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) |] ==> i = range(f)"
    1.72 +     "[| omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) |] 
    1.73 +      ==> i = range(f)"
    1.74  apply (auto simp add: otype_def omap_iff)
    1.75  apply (blast dest: omap_unique) 
    1.76  done
    1.77 @@ -439,18 +437,15 @@
    1.78      apply (frule pair_components_in_M, assumption) 
    1.79      apply blast 
    1.80  apply (auto simp add: Transset_def otype_iff) 
    1.81 - apply (blast intro: transM)
    1.82 +  apply (blast intro: transM)
    1.83 + apply (blast intro: Ord_in_Ord) 
    1.84  apply (rename_tac y a g)
    1.85  apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun, 
    1.86  			  THEN apply_funtype],  assumption)  
    1.87  apply (rule_tac x="converse(g)`y" in bexI)
    1.88   apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption) 
    1.89  apply (safe elim!: predE) 
    1.90 -apply (intro conjI exI) 
    1.91 -prefer 3
    1.92 -  apply (blast intro: restrict_ord_iso ord_iso_sym ltI)
    1.93 - apply (blast intro: transM)
    1.94 - apply (blast intro: Ord_in_Ord)
    1.95 +apply (blast intro: restrict_ord_iso ord_iso_sym ltI dest: transM)
    1.96  done
    1.97  
    1.98  lemma (in M_axioms) domain_omap:
    1.99 @@ -559,14 +554,12 @@
   1.100  apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp) 
   1.101  apply (frule wellordered_is_wellfounded_on, assumption)
   1.102  apply (erule wellfounded_on_induct, assumption+)
   1.103 - apply (insert obase_equals_separation)
   1.104 - apply (simp add: rex_def, clarify) 
   1.105 + apply (frule obase_equals_separation [of A r], assumption) 
   1.106 + apply (simp, clarify) 
   1.107  apply (rename_tac b) 
   1.108  apply (subgoal_tac "Order.pred(A,b,r) <= B") 
   1.109 - prefer 2 apply (force simp add: pred_iff obase_iff)  
   1.110 -apply (intro conjI exI) 
   1.111 -    prefer 4 apply (blast intro: restrict_omap_ord_iso) 
   1.112 -apply (blast intro: Ord_omap_image_pred)+
   1.113 + apply (blast intro!: restrict_omap_ord_iso Ord_omap_image_pred)
   1.114 +apply (force simp add: pred_iff obase_iff)  
   1.115  done
   1.116  
   1.117