src/ZF/Constructible/Relative.thy
 changeset 13634 99a593b49b04 parent 13628 87482b5e3f2e child 13687 22dce9134953
```     1.1 --- a/src/ZF/Constructible/Relative.thy	Tue Oct 08 14:09:18 2002 +0200
1.2 +++ b/src/ZF/Constructible/Relative.thy	Wed Oct 09 11:07:13 2002 +0200
1.3 @@ -1,7 +1,6 @@
1.4  (*  Title:      ZF/Constructible/Relative.thy
1.5      ID:         \$Id\$
1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 -    Copyright   2002  University of Cambridge
1.8  *)
1.9
1.11 @@ -197,43 +196,43 @@
1.12         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
1.13         (is_quasinat(M,k) | empty(M,z))"
1.14
1.15 -  relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o"
1.16 -    "relativize1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
1.17 +  relation1 :: "[i=>o, [i,i]=>o, i=>i] => o"
1.18 +    "relation1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
1.19
1.20 -  Relativize1 :: "[i=>o, i, [i,i]=>o, i=>i] => o"
1.21 +  Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o"
1.22      --{*as above, but typed*}
1.23 -    "Relativize1(M,A,is_f,f) ==
1.24 +    "Relation1(M,A,is_f,f) ==
1.25          \<forall>x[M]. \<forall>y[M]. x\<in>A --> is_f(x,y) <-> y = f(x)"
1.26
1.27 -  relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
1.28 -    "relativize2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
1.29 +  relation2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
1.30 +    "relation2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
1.31
1.32 -  Relativize2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o"
1.33 -    "Relativize2(M,A,B,is_f,f) ==
1.34 +  Relation2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o"
1.35 +    "Relation2(M,A,B,is_f,f) ==
1.36          \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. x\<in>A --> y\<in>B --> is_f(x,y,z) <-> z = f(x,y)"
1.37
1.38 -  relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
1.39 -    "relativize3(M,is_f,f) ==
1.40 +  relation3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
1.41 +    "relation3(M,is_f,f) ==
1.42         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
1.43
1.44 -  Relativize3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o"
1.45 -    "Relativize3(M,A,B,C,is_f,f) ==
1.46 +  Relation3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o"
1.47 +    "Relation3(M,A,B,C,is_f,f) ==
1.48         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M].
1.49           x\<in>A --> y\<in>B --> z\<in>C --> is_f(x,y,z,u) <-> u = f(x,y,z)"
1.50
1.51 -  relativize4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o"
1.52 -    "relativize4(M,is_f,f) ==
1.53 +  relation4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o"
1.54 +    "relation4(M,is_f,f) ==
1.55         \<forall>u[M]. \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>a[M]. is_f(u,x,y,z,a) <-> a = f(u,x,y,z)"
1.56
1.57
1.58  text{*Useful when absoluteness reasoning has replaced the predicates by terms*}
1.59 -lemma triv_Relativize1:
1.60 -     "Relativize1(M, A, \<lambda>x y. y = f(x), f)"
1.62 +lemma triv_Relation1:
1.63 +     "Relation1(M, A, \<lambda>x y. y = f(x), f)"
1.65
1.66 -lemma triv_Relativize2:
1.67 -     "Relativize2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
1.69 +lemma triv_Relation2:
1.70 +     "Relation2(M, A, B, \<lambda>x y a. a = f(x,y), f)"
1.72
1.73
1.74  subsection {*The relativized ZF axioms*}
1.75 @@ -730,9 +729,9 @@
1.76
1.77  lemma (in M_trivial) lambda_abs2 [simp]:
1.78       "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
1.79 -         Relativize1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
1.80 +         Relation1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
1.81        ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
1.82 -apply (simp add: Relativize1_def is_lambda_def)
1.83 +apply (simp add: Relation1_def is_lambda_def)
1.84  apply (rule iffI)
1.85   prefer 2 apply (simp add: lam_def)
1.86  apply (rule M_equalityI)
1.87 @@ -787,7 +786,7 @@
1.88  by (auto simp add: is_quasinat_def quasinat_def)
1.89
1.90  lemma (in M_trivial) nat_case_abs [simp]:
1.91 -     "[| relativize1(M,is_b,b); M(k); M(z) |]
1.92 +     "[| relation1(M,is_b,b); M(k); M(z) |]
1.93        ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
1.94  apply (case_tac "quasinat(k)")
1.95   prefer 2
1.96 @@ -795,7 +794,7 @@
1.97   apply (force simp add: quasinat_def)
1.98  apply (simp add: quasinat_def is_nat_case_def)
1.99  apply (elim disjE exE)
1.100 - apply (simp_all add: relativize1_def)
1.101 + apply (simp_all add: relation1_def)
1.102  done
1.103
1.104  (*NOT for the simplifier.  The assumption M(z') is apparently necessary, but
1.105 @@ -929,30 +928,8 @@
1.106        strong_replacement(M, \<lambda>p z. \<exists>f[M]. \<exists>b[M]. \<exists>nb[M]. \<exists>cnbf[M].
1.107                  pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) &
1.108                  upair(M,cnbf,cnbf,z))"
1.109 -  and well_ord_iso_separation:
1.110 -     "[| M(A); M(f); M(r) |]
1.111 -      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y[M]. (\<exists>p[M].
1.112 -		     fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
1.113 -  and obase_separation:
1.114 -     --{*part of the order type formalization*}
1.115 -     "[| M(A); M(r) |]
1.116 -      ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
1.117 -	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
1.118 -	     order_isomorphism(M,par,r,x,mx,g))"
1.119 -  and obase_equals_separation:
1.120 -     "[| M(A); M(r) |]
1.121 -      ==> separation (M, \<lambda>x. x\<in>A --> ~(\<exists>y[M]. \<exists>g[M].
1.122 -			      ordinal(M,y) & (\<exists>my[M]. \<exists>pxr[M].
1.123 -			      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
1.124 -			      order_isomorphism(M,pxr,r,y,my,g))))"
1.125 -  and omap_replacement:
1.126 -     "[| M(A); M(r) |]
1.127 -      ==> strong_replacement(M,
1.128 -             \<lambda>a z. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
1.129 -	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
1.130 -	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
1.131    and is_recfun_separation:
1.132 -     --{*for well-founded recursion*}
1.133 +     --{*for well-founded recursion: used to prove @{text is_recfun_equal}*}
1.134       "[| M(r); M(f); M(g); M(a); M(b) |]
1.135       ==> separation(M,
1.136              \<lambda>x. \<exists>xa[M]. \<exists>xb[M].
1.137 @@ -1490,7 +1467,7 @@
1.138  by (auto simp add: is_quasilist_def quasilist_def)
1.139
1.140  lemma (in M_trivial) list_case_abs [simp]:
1.141 -     "[| relativize2(M,is_b,b); M(k); M(z) |]
1.142 +     "[| relation2(M,is_b,b); M(k); M(z) |]
1.143        ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
1.144  apply (case_tac "quasilist(k)")
1.145   prefer 2
1.146 @@ -1498,7 +1475,7 @@
1.147   apply (force simp add: quasilist_def)
1.148  apply (simp add: quasilist_def is_list_case_def)
1.149  apply (elim disjE exE)
1.150 - apply (simp_all add: relativize2_def)
1.151 + apply (simp_all add: relation2_def)
1.152  done
1.153
1.154
1.155 @@ -1536,8 +1513,8 @@
1.156  apply (elim disjE exE, auto)
1.157  done
1.158
1.159 -lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')"