src/ZF/Constructible/Relative.thy
changeset 13353 1800e7134d2e
parent 13352 3cd767f8d78b
child 13363 c26eeb000470
     1.1 --- a/src/ZF/Constructible/Relative.thy	Fri Jul 12 11:24:40 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Fri Jul 12 16:41:39 2002 +0200
     1.3 @@ -179,6 +179,16 @@
     1.4         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
     1.5         (is_quasinat(M,k) | z=0)"
     1.6  
     1.7 +  relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o"
     1.8 +    "relativize1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
     1.9 +
    1.10 +  relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
    1.11 +    "relativize2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
    1.12 +
    1.13 +  relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
    1.14 +    "relativize3(M,is_f,f) == 
    1.15 +       \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
    1.16 +
    1.17  
    1.18  subsection {*The relativized ZF axioms*}
    1.19  constdefs
    1.20 @@ -584,7 +594,7 @@
    1.21    nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
    1.22    even for f : M -> M.
    1.23  *)
    1.24 -lemma (in M_triv_axioms) RepFun_closed [intro,simp]:
    1.25 +lemma (in M_triv_axioms) RepFun_closed:
    1.26       "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
    1.27        ==> M(RepFun(A,f))"
    1.28  apply (simp add: RepFun_def) 
    1.29 @@ -592,10 +602,23 @@
    1.30  apply (auto dest: transM  simp add: univalent_def) 
    1.31  done
    1.32  
    1.33 +lemma Replace_conj_eq: "{y . x \<in> A, x\<in>A & y=f(x)} = {y . x\<in>A, y=f(x)}"
    1.34 +by simp
    1.35 +
    1.36 +text{*Better than @{text RepFun_closed} when having the formula @{term "x\<in>A"}
    1.37 +      makes relativization easier.*}
    1.38 +lemma (in M_triv_axioms) RepFun_closed2:
    1.39 +     "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
    1.40 +      ==> M(RepFun(A, %x. f(x)))"
    1.41 +apply (simp add: RepFun_def)
    1.42 +apply (frule strong_replacement_closed, assumption)
    1.43 +apply (auto dest: transM  simp add: Replace_conj_eq univalent_def) 
    1.44 +done
    1.45 +
    1.46  lemma (in M_triv_axioms) lam_closed [intro,simp]:
    1.47       "[| strong_replacement(M, \<lambda>x y. y = <x,b(x)>); M(A); \<forall>x\<in>A. M(b(x)) |]
    1.48        ==> M(\<lambda>x\<in>A. b(x))"
    1.49 -by (simp add: lam_def, blast dest: transM) 
    1.50 +by (simp add: lam_def, blast intro: RepFun_closed dest: transM) 
    1.51  
    1.52  lemma (in M_triv_axioms) image_abs [simp]: 
    1.53       "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
    1.54 @@ -635,19 +658,18 @@
    1.55  by (auto simp add: is_quasinat_def quasinat_def)
    1.56  
    1.57  lemma (in M_triv_axioms) nat_case_abs [simp]: 
    1.58 -  assumes b_abs: "!!x y. M(x) --> M(y) --> (is_b(x,y) <-> y = b(x))"
    1.59 -  shows
    1.60 -     "[| M(k); M(z) |] ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
    1.61 +     "[| relativize1(M,is_b,b); M(k); M(z) |] 
    1.62 +      ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
    1.63  apply (case_tac "quasinat(k)") 
    1.64   prefer 2 
    1.65   apply (simp add: is_nat_case_def non_nat_case) 
    1.66   apply (force simp add: quasinat_def) 
    1.67  apply (simp add: quasinat_def is_nat_case_def)
    1.68  apply (elim disjE exE) 
    1.69 - apply (simp_all add: b_abs) 
    1.70 + apply (simp_all add: relativize1_def) 
    1.71  done
    1.72  
    1.73 -(*Needed?  surely better to replace by nat_case?*)
    1.74 +(*Needed?  surely better to replace is_nat_case by nat_case?*)
    1.75  lemma (in M_triv_axioms) is_nat_case_cong [cong]:
    1.76       "[| a = a'; k = k';  z = z';  M(z');
    1.77         !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
    1.78 @@ -980,8 +1002,7 @@
    1.79  
    1.80  lemma (in M_axioms) apply_abs [simp]: 
    1.81       "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
    1.82 -apply (simp add: fun_apply_def apply_def)
    1.83 -apply (blast intro: elim:); 
    1.84 +apply (simp add: fun_apply_def apply_def, blast) 
    1.85  done
    1.86  
    1.87  lemma (in M_axioms) typed_function_abs [simp]: