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
```