src/ZF/Constructible/Wellorderings.thy
 changeset 13293 09276ee04361 parent 13269 3ba9be497c33 child 13295 ca2e9b273472
```     1.1 --- a/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 10:53:52 2002 +0200
1.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Thu Jul 04 10:54:04 2002 +0200
1.3 @@ -346,23 +346,23 @@
1.4    obase :: "[i=>o,i,i,i] => o"
1.5         --{*the domain of @{text om}, eventually shown to equal @{text A}*}
1.6     "obase(M,A,r,z) ==
1.7 -	\<forall>a. M(a) -->
1.8 -         (a \<in> z <->
1.9 +	\<forall>a[M].
1.10 +         a \<in> z <->
1.11            (a\<in>A & (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) &
1.12                                 membership(M,x,mx) & pred_set(M,A,a,r,par) &
1.13 -                               order_isomorphism(M,par,r,x,mx,g))))"
1.14 +                               order_isomorphism(M,par,r,x,mx,g)))"
1.15
1.16
1.17    omap :: "[i=>o,i,i,i] => o"
1.18      --{*the function that maps wosets to order types*}
1.19     "omap(M,A,r,f) ==
1.20 -	\<forall>z. M(z) -->
1.21 -         (z \<in> f <->
1.22 +	\<forall>z[M].
1.23 +         z \<in> f <->
1.24            (\<exists>a\<in>A. M(a) &
1.25             (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) &
1.26                           pair(M,a,x,z) & membership(M,x,mx) &
1.27                           pred_set(M,A,a,r,par) &
1.28 -                         order_isomorphism(M,par,r,x,mx,g))))"
1.29 +                         order_isomorphism(M,par,r,x,mx,g)))"
1.30
1.31
1.32    otype :: "[i=>o,i,i,i] => o"  --{*the order types themselves*}
1.33 @@ -392,8 +392,10 @@
1.34                     g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
1.35  apply (rotate_tac 1)
1.36  apply (simp add: omap_def Memrel_closed pred_closed)
1.37 -apply (rule iffI)
1.38 -apply (drule_tac x=z in spec, blast dest: transM)+
1.39 +apply (rule iffI)
1.40 + apply (drule_tac [2] x=z in rspec)
1.41 + apply (drule_tac x=z in rspec)
1.42 + apply (blast dest: transM)+
1.43  done
1.44
1.45  lemma (in M_axioms) omap_unique:
1.46 @@ -576,35 +578,37 @@
1.47         M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"
1.48  apply (frule omap_ord_iso, assumption+)
1.49  apply (frule obase_equals, assumption+, blast)
1.50 -done
1.51 +done
1.52
1.53  lemma (in M_axioms) obase_exists:
1.54 -     "[| M(A); M(r) |] ==> \<exists>z. M(z) & obase(M,A,r,z)"
1.55 +     "[| M(A); M(r) |] ==> \<exists>z[M]. obase(M,A,r,z)"
1.57  apply (insert obase_separation [of A r])
1.59  done
1.60
1.61  lemma (in M_axioms) omap_exists:
1.62 -     "[| M(A); M(r) |] ==> \<exists>z. M(z) & omap(M,A,r,z)"
1.63 +     "[| M(A); M(r) |] ==> \<exists>z[M]. omap(M,A,r,z)"
1.64  apply (insert obase_exists [of A r])
1.66  apply (insert omap_replacement [of A r])
1.67  apply (simp add: strong_replacement_def, clarify)
1.68 -apply (drule_tac x=z in spec, clarify)
1.69 +apply (drule_tac x=x in spec, clarify)
1.70  apply (simp add: Memrel_closed pred_closed obase_iff)
1.71  apply (erule impE)
1.72   apply (clarsimp simp add: univalent_def)
1.73   apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)
1.74 -apply (rule_tac x=Y in exI)
1.75 -apply (simp add: Memrel_closed pred_closed obase_iff, blast)
1.76 +apply (rule_tac x=Y in rexI)
1.77 +apply (simp add: Memrel_closed pred_closed obase_iff, blast, assumption)
1.78  done
1.79
1.80 +declare rall_simps [simp] rex_simps [simp]
1.81 +
1.82  lemma (in M_axioms) otype_exists:
1.83       "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i. M(i) & otype(M,A,r,i)"
1.84 -apply (insert omap_exists [of A r])
1.85 -apply (simp add: otype_def, clarify)
1.86 -apply (rule_tac x="range(z)" in exI)
1.87 +apply (insert omap_exists [of A r])
1.88 +apply (simp add: otype_def, safe)
1.89 +apply (rule_tac x="range(x)" in exI)
1.90  apply blast
1.91  done
1.92
```