src/ZF/Constructible/Relative.thy
changeset 13247 e3c289f0724b
parent 13245 714f7a423a15
child 13251 74cb2af8811e
     1.1 --- a/src/ZF/Constructible/Relative.thy	Mon Jun 24 16:33:43 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Wed Jun 26 10:25:36 2002 +0200
     1.3 @@ -569,16 +569,12 @@
     1.4  lemma (in M_axioms) strong_replacementI [rule_format]:
     1.5      "[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
     1.6       ==> strong_replacement(M,P)"
     1.7 -apply (simp add: strong_replacement_def) 
     1.8 -apply (clarify ); 
     1.9 -apply (frule replacementD [OF replacement]) 
    1.10 -apply assumption
    1.11 -apply (clarify ); 
    1.12 -apply (drule_tac x=A in spec)
    1.13 -apply (clarify );  
    1.14 -apply (drule_tac z=Y in separationD) 
    1.15 -apply assumption; 
    1.16 -apply (clarify ); 
    1.17 +apply (simp add: strong_replacement_def, clarify) 
    1.18 +apply (frule replacementD [OF replacement], assumption)
    1.19 +apply clarify 
    1.20 +apply (drule_tac x=A in spec, clarify)  
    1.21 +apply (drule_tac z=Y in separationD, assumption)
    1.22 +apply clarify 
    1.23  apply (blast dest: transM) 
    1.24  done
    1.25  
    1.26 @@ -586,17 +582,16 @@
    1.27  (*The last premise expresses that P takes M to M*)
    1.28  lemma (in M_axioms) strong_replacement_closed [intro,simp]:
    1.29       "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
    1.30 -       !!x y. [| P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
    1.31 +       !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
    1.32  apply (simp add: strong_replacement_def) 
    1.33  apply (drule spec [THEN mp], auto) 
    1.34  apply (subgoal_tac "Replace(A,P) = Y")
    1.35 - apply (simp add: ); 
    1.36 + apply simp 
    1.37  apply (rule equality_iffI) 
    1.38 -apply (simp add: Replace_iff) 
    1.39 -apply safe;
    1.40 +apply (simp add: Replace_iff, safe)
    1.41   apply (blast dest: transM) 
    1.42  apply (frule transM, assumption) 
    1.43 - apply (simp add: univalent_def);
    1.44 + apply (simp add: univalent_def)
    1.45   apply (drule spec [THEN mp, THEN iffD1], assumption, assumption)
    1.46   apply (blast dest: transM) 
    1.47  done
    1.48 @@ -609,13 +604,18 @@
    1.49    even for f : M -> M.
    1.50  *)
    1.51  lemma (in M_axioms) RepFun_closed [intro,simp]:
    1.52 -     "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x. M(x) --> M(f(x)) |]
    1.53 +     "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
    1.54        ==> M(RepFun(A,f))"
    1.55  apply (simp add: RepFun_def) 
    1.56  apply (rule strong_replacement_closed) 
    1.57  apply (auto dest: transM  simp add: univalent_def) 
    1.58  done
    1.59  
    1.60 +lemma (in M_axioms) lam_closed [intro,simp]:
    1.61 +     "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
    1.62 +      ==> M(\<lambda>x\<in>A. b(x))"
    1.63 +by (simp add: lam_def, blast dest: transM) 
    1.64 +
    1.65  lemma (in M_axioms) converse_abs [simp]: 
    1.66       "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
    1.67  apply (simp add: is_converse_def)
    1.68 @@ -800,7 +800,7 @@
    1.69  lemma (in M_axioms) injection_abs [simp]: 
    1.70       "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
    1.71  apply (simp add: injection_def apply_iff inj_def apply_closed)
    1.72 -apply (blast dest: transM [of _ A]); 
    1.73 +apply (blast dest: transM [of _ A]) 
    1.74  done
    1.75  
    1.76  lemma (in M_axioms) surjection_abs [simp]: 
    1.77 @@ -846,8 +846,8 @@
    1.78                  xz = \<langle>x,z\<rangle> & \<langle>x,y\<rangle> \<in> s & \<langle>y,z\<rangle> \<in> r))}"
    1.79  apply (simp add: comp_def)
    1.80  apply (rule equalityI) 
    1.81 - apply (clarify ); 
    1.82 - apply (simp add: ); 
    1.83 + apply clarify 
    1.84 + apply simp 
    1.85   apply  (blast dest:  transM)+
    1.86  done
    1.87  
    1.88 @@ -860,7 +860,7 @@
    1.89  lemma (in M_axioms) composition_abs [simp]: 
    1.90       "[| M(r); M(s); M(t) |] 
    1.91        ==> composition(M,r,s,t) <-> t = r O s"
    1.92 -apply safe;
    1.93 +apply safe
    1.94   txt{*Proving @{term "composition(M, r, s, r O s)"}*}
    1.95   prefer 2 
    1.96   apply (simp add: composition_def comp_def)
    1.97 @@ -896,7 +896,7 @@
    1.98  lemma (in M_axioms) Int_closed [intro,simp]:
    1.99       "[| M(A); M(B) |] ==> M(A Int B)"
   1.100  apply (subgoal_tac "M({A,B})")
   1.101 -apply (frule Inter_closed, force+); 
   1.102 +apply (frule Inter_closed, force+) 
   1.103  done
   1.104  
   1.105  text{*M contains all finite functions*}