src/ZF/Constructible/Relative.thy
 changeset 21404 eb85850d3eb7 parent 21233 5a5c8ea5f66a child 22710 f44439cdce77
```     1.1 --- a/src/ZF/Constructible/Relative.thy	Fri Nov 17 02:19:55 2006 +0100
1.2 +++ b/src/ZF/Constructible/Relative.thy	Fri Nov 17 02:20:03 2006 +0100
1.3 @@ -10,95 +10,120 @@
1.4  subsection{* Relativized versions of standard set-theoretic concepts *}
1.5
1.6  definition
1.7 -  empty :: "[i=>o,i] => o"
1.8 +  empty :: "[i=>o,i] => o" where
1.9      "empty(M,z) == \<forall>x[M]. x \<notin> z"
1.10
1.11 -  subset :: "[i=>o,i,i] => o"
1.12 +definition
1.13 +  subset :: "[i=>o,i,i] => o" where
1.14      "subset(M,A,B) == \<forall>x[M]. x\<in>A --> x \<in> B"
1.15
1.16 -  upair :: "[i=>o,i,i,i] => o"
1.17 +definition
1.18 +  upair :: "[i=>o,i,i,i] => o" where
1.19      "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z --> x = a | x = b)"
1.20
1.21 -  pair :: "[i=>o,i,i,i] => o"
1.22 +definition
1.23 +  pair :: "[i=>o,i,i,i] => o" where
1.24      "pair(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) &
1.25 -                          (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
1.26 +                     (\<exists>y[M]. upair(M,a,b,y) & upair(M,x,y,z))"
1.27
1.28
1.29 -  union :: "[i=>o,i,i,i] => o"
1.30 +definition
1.31 +  union :: "[i=>o,i,i,i] => o" where
1.32      "union(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a | x \<in> b"
1.33
1.34 -  is_cons :: "[i=>o,i,i,i] => o"
1.35 +definition
1.36 +  is_cons :: "[i=>o,i,i,i] => o" where
1.37      "is_cons(M,a,b,z) == \<exists>x[M]. upair(M,a,a,x) & union(M,x,b,z)"
1.38
1.39 -  successor :: "[i=>o,i,i] => o"
1.40 +definition
1.41 +  successor :: "[i=>o,i,i] => o" where
1.42      "successor(M,a,z) == is_cons(M,a,a,z)"
1.43
1.44 -  number1 :: "[i=>o,i] => o"
1.45 +definition
1.46 +  number1 :: "[i=>o,i] => o" where
1.47      "number1(M,a) == \<exists>x[M]. empty(M,x) & successor(M,x,a)"
1.48
1.49 -  number2 :: "[i=>o,i] => o"
1.50 +definition
1.51 +  number2 :: "[i=>o,i] => o" where
1.52      "number2(M,a) == \<exists>x[M]. number1(M,x) & successor(M,x,a)"
1.53
1.54 -  number3 :: "[i=>o,i] => o"
1.55 +definition
1.56 +  number3 :: "[i=>o,i] => o" where
1.57      "number3(M,a) == \<exists>x[M]. number2(M,x) & successor(M,x,a)"
1.58
1.59 -  powerset :: "[i=>o,i,i] => o"
1.60 +definition
1.61 +  powerset :: "[i=>o,i,i] => o" where
1.62      "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
1.63
1.64 -  is_Collect :: "[i=>o,i,i=>o,i] => o"
1.65 +definition
1.66 +  is_Collect :: "[i=>o,i,i=>o,i] => o" where
1.67      "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)"
1.68
1.69 -  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
1.70 +definition
1.71 +  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o" where
1.72      "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))"
1.73
1.74 -  inter :: "[i=>o,i,i,i] => o"
1.75 +definition
1.76 +  inter :: "[i=>o,i,i,i] => o" where
1.77      "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
1.78
1.79 -  setdiff :: "[i=>o,i,i,i] => o"
1.80 +definition
1.81 +  setdiff :: "[i=>o,i,i,i] => o" where
1.82      "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"
1.83
1.84 -  big_union :: "[i=>o,i,i] => o"
1.85 +definition
1.86 +  big_union :: "[i=>o,i,i] => o" where
1.87      "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)"
1.88
1.89 -  big_inter :: "[i=>o,i,i] => o"
1.90 +definition
1.91 +  big_inter :: "[i=>o,i,i] => o" where
1.92      "big_inter(M,A,z) ==
1.93               (A=0 --> z=0) &
1.94  	     (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y[M]. y\<in>A --> x \<in> y)))"
1.95
1.96 -  cartprod :: "[i=>o,i,i,i] => o"
1.97 +definition
1.98 +  cartprod :: "[i=>o,i,i,i] => o" where
1.99      "cartprod(M,A,B,z) ==
1.100  	\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
1.101
1.102 -  is_sum :: "[i=>o,i,i,i] => o"
1.103 +definition
1.104 +  is_sum :: "[i=>o,i,i,i] => o" where
1.105      "is_sum(M,A,B,Z) ==
1.106         \<exists>A0[M]. \<exists>n1[M]. \<exists>s1[M]. \<exists>B1[M].
1.107         number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
1.108         cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
1.109
1.110 -  is_Inl :: "[i=>o,i,i] => o"
1.111 +definition
1.112 +  is_Inl :: "[i=>o,i,i] => o" where
1.113      "is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z)"
1.114
1.115 -  is_Inr :: "[i=>o,i,i] => o"
1.116 +definition
1.117 +  is_Inr :: "[i=>o,i,i] => o" where
1.118      "is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z)"
1.119
1.120 -  is_converse :: "[i=>o,i,i] => o"
1.121 +definition
1.122 +  is_converse :: "[i=>o,i,i] => o" where
1.123      "is_converse(M,r,z) ==
1.124  	\<forall>x[M]. x \<in> z <->
1.125               (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))"
1.126
1.127 -  pre_image :: "[i=>o,i,i,i] => o"
1.128 +definition
1.129 +  pre_image :: "[i=>o,i,i,i] => o" where
1.130      "pre_image(M,r,A,z) ==
1.131  	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
1.132
1.133 -  is_domain :: "[i=>o,i,i] => o"
1.134 +definition
1.135 +  is_domain :: "[i=>o,i,i] => o" where
1.136      "is_domain(M,r,z) ==
1.137  	\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w)))"
1.138
1.139 -  image :: "[i=>o,i,i,i] => o"
1.140 +definition
1.141 +  image :: "[i=>o,i,i,i] => o" where
1.142      "image(M,r,A,z) ==
1.143          \<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w)))"
1.144
1.145 -  is_range :: "[i=>o,i,i] => o"
1.146 +definition
1.147 +  is_range :: "[i=>o,i,i] => o" where
1.148      --{*the cleaner
1.149        @{term "\<exists>r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"}
1.150        unfortunately needs an instance of separation in order to prove
1.151 @@ -106,121 +131,147 @@
1.152      "is_range(M,r,z) ==
1.153  	\<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w)))"
1.154
1.155 -  is_field :: "[i=>o,i,i] => o"
1.156 +definition
1.157 +  is_field :: "[i=>o,i,i] => o" where
1.158      "is_field(M,r,z) ==
1.159  	\<exists>dr[M]. \<exists>rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) &
1.160                          union(M,dr,rr,z)"
1.161
1.162 -  is_relation :: "[i=>o,i] => o"
1.163 +definition
1.164 +  is_relation :: "[i=>o,i] => o" where
1.165      "is_relation(M,r) ==
1.166          (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
1.167
1.168 -  is_function :: "[i=>o,i] => o"
1.169 +definition
1.170 +  is_function :: "[i=>o,i] => o" where
1.171      "is_function(M,r) ==
1.172  	\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
1.173             pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'"
1.174
1.175 -  fun_apply :: "[i=>o,i,i,i] => o"
1.176 +definition
1.177 +  fun_apply :: "[i=>o,i,i,i] => o" where
1.178      "fun_apply(M,f,x,y) ==
1.179          (\<exists>xs[M]. \<exists>fxs[M].
1.180           upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))"
1.181
1.182 -  typed_function :: "[i=>o,i,i,i] => o"
1.183 +definition
1.184 +  typed_function :: "[i=>o,i,i,i] => o" where
1.185      "typed_function(M,A,B,r) ==
1.186          is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
1.187          (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))"
1.188
1.189 -  is_funspace :: "[i=>o,i,i,i] => o"
1.190 +definition
1.191 +  is_funspace :: "[i=>o,i,i,i] => o" where
1.192      "is_funspace(M,A,B,F) ==
1.193          \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"
1.194
1.195 -  composition :: "[i=>o,i,i,i] => o"
1.196 +definition
1.197 +  composition :: "[i=>o,i,i,i] => o" where
1.198      "composition(M,r,s,t) ==
1.199          \<forall>p[M]. p \<in> t <->
1.200                 (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
1.201                  pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
1.202                  xy \<in> s & yz \<in> r)"
1.203
1.204 -  injection :: "[i=>o,i,i,i] => o"
1.205 +definition
1.206 +  injection :: "[i=>o,i,i,i] => o" where
1.207      "injection(M,A,B,f) ==
1.208  	typed_function(M,A,B,f) &
1.209          (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
1.210            pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')"
1.211
1.212 -  surjection :: "[i=>o,i,i,i] => o"
1.213 +definition
1.214 +  surjection :: "[i=>o,i,i,i] => o" where
1.215      "surjection(M,A,B,f) ==
1.216          typed_function(M,A,B,f) &
1.217          (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))"
1.218
1.219 -  bijection :: "[i=>o,i,i,i] => o"
1.220 +definition
1.221 +  bijection :: "[i=>o,i,i,i] => o" where
1.222      "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
1.223
1.224 -  restriction :: "[i=>o,i,i,i] => o"
1.225 +definition
1.226 +  restriction :: "[i=>o,i,i,i] => o" where
1.227      "restriction(M,r,A,z) ==
1.228  	\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))"
1.229
1.230 -  transitive_set :: "[i=>o,i] => o"
1.231 +definition
1.232 +  transitive_set :: "[i=>o,i] => o" where
1.233      "transitive_set(M,a) == \<forall>x[M]. x\<in>a --> subset(M,x,a)"
1.234
1.235 -  ordinal :: "[i=>o,i] => o"
1.236 +definition
1.237 +  ordinal :: "[i=>o,i] => o" where
1.238       --{*an ordinal is a transitive set of transitive sets*}
1.239      "ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a --> transitive_set(M,x))"
1.240
1.241 -  limit_ordinal :: "[i=>o,i] => o"
1.242 +definition
1.243 +  limit_ordinal :: "[i=>o,i] => o" where
1.244      --{*a limit ordinal is a non-empty, successor-closed ordinal*}
1.245      "limit_ordinal(M,a) ==
1.246  	ordinal(M,a) & ~ empty(M,a) &
1.247          (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
1.248
1.249 -  successor_ordinal :: "[i=>o,i] => o"
1.250 +definition
1.251 +  successor_ordinal :: "[i=>o,i] => o" where
1.252      --{*a successor ordinal is any ordinal that is neither empty nor limit*}
1.253      "successor_ordinal(M,a) ==
1.254  	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
1.255
1.256 -  finite_ordinal :: "[i=>o,i] => o"
1.257 +definition
1.258 +  finite_ordinal :: "[i=>o,i] => o" where
1.259      --{*an ordinal is finite if neither it nor any of its elements are limit*}
1.260      "finite_ordinal(M,a) ==
1.261  	ordinal(M,a) & ~ limit_ordinal(M,a) &
1.262          (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
1.263
1.264 -  omega :: "[i=>o,i] => o"
1.265 +definition
1.266 +  omega :: "[i=>o,i] => o" where
1.267      --{*omega is a limit ordinal none of whose elements are limit*}
1.268      "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
1.269
1.270 -  is_quasinat :: "[i=>o,i] => o"
1.271 +definition
1.272 +  is_quasinat :: "[i=>o,i] => o" where
1.273      "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))"
1.274
1.275 -  is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
1.276 +definition
1.277 +  is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" where
1.278      "is_nat_case(M, a, is_b, k, z) ==
1.279         (empty(M,k) --> z=a) &
1.280         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
1.281         (is_quasinat(M,k) | empty(M,z))"
1.282
1.283 -  relation1 :: "[i=>o, [i,i]=>o, i=>i] => o"
1.284 +definition
1.285 +  relation1 :: "[i=>o, [i,i]=>o, i=>i] => o" where
1.286      "relation1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
1.287
1.288 -  Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o"
1.289 +definition
1.290 +  Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o" where
1.291      --{*as above, but typed*}
1.292      "Relation1(M,A,is_f,f) ==
1.293          \<forall>x[M]. \<forall>y[M]. x\<in>A --> is_f(x,y) <-> y = f(x)"
1.294
1.295 -  relation2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o"
1.296 +definition
1.297 +  relation2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o" where
1.298      "relation2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
1.299
1.300 -  Relation2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o"
1.301 +definition
1.302 +  Relation2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o" where
1.303      "Relation2(M,A,B,is_f,f) ==
1.304          \<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.305
1.306 -  relation3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o"
1.307 +definition
1.308 +  relation3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o" where
1.309      "relation3(M,is_f,f) ==
1.310         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
1.311
1.312 -  Relation3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o"
1.313 +definition
1.314 +  Relation3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o" where
1.315      "Relation3(M,A,B,C,is_f,f) ==
1.316         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M].
1.317           x\<in>A --> y\<in>B --> z\<in>C --> is_f(x,y,z,u) <-> u = f(x,y,z)"
1.318
1.319 -  relation4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o"
1.320 +definition
1.321 +  relation4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o" where
1.322      "relation4(M,is_f,f) ==
1.323         \<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.324
1.325 @@ -236,13 +287,14 @@
1.326
1.327
1.328  subsection {*The relativized ZF axioms*}
1.329 +
1.330  definition
1.331 -
1.332 -  extensionality :: "(i=>o) => o"
1.333 +  extensionality :: "(i=>o) => o" where
1.334      "extensionality(M) ==
1.335  	\<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x <-> z \<in> y) --> x=y"
1.336
1.337 -  separation :: "[i=>o, i=>o] => o"
1.338 +definition
1.339 +  separation :: "[i=>o, i=>o] => o" where
1.340      --{*The formula @{text P} should only involve parameters
1.341          belonging to @{text M} and all its quantifiers must be relativized
1.342          to @{text M}.  We do not have separation as a scheme; every instance
1.343 @@ -250,30 +302,37 @@
1.344      "separation(M,P) ==
1.345  	\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
1.346
1.347 -  upair_ax :: "(i=>o) => o"
1.348 +definition
1.349 +  upair_ax :: "(i=>o) => o" where
1.350      "upair_ax(M) == \<forall>x[M]. \<forall>y[M]. \<exists>z[M]. upair(M,x,y,z)"
1.351
1.352 -  Union_ax :: "(i=>o) => o"
1.353 +definition
1.354 +  Union_ax :: "(i=>o) => o" where
1.355      "Union_ax(M) == \<forall>x[M]. \<exists>z[M]. big_union(M,x,z)"
1.356
1.357 -  power_ax :: "(i=>o) => o"
1.358 +definition
1.359 +  power_ax :: "(i=>o) => o" where
1.360      "power_ax(M) == \<forall>x[M]. \<exists>z[M]. powerset(M,x,z)"
1.361
1.362 -  univalent :: "[i=>o, i, [i,i]=>o] => o"
1.363 +definition
1.364 +  univalent :: "[i=>o, i, [i,i]=>o] => o" where
1.365      "univalent(M,A,P) ==
1.366  	\<forall>x[M]. x\<in>A --> (\<forall>y[M]. \<forall>z[M]. P(x,y) & P(x,z) --> y=z)"
1.367
1.368 -  replacement :: "[i=>o, [i,i]=>o] => o"
1.369 +definition
1.370 +  replacement :: "[i=>o, [i,i]=>o] => o" where
1.371      "replacement(M,P) ==
1.372        \<forall>A[M]. univalent(M,A,P) -->
1.373        (\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)"
1.374
1.375 -  strong_replacement :: "[i=>o, [i,i]=>o] => o"
1.376 +definition
1.377 +  strong_replacement :: "[i=>o, [i,i]=>o] => o" where
1.378      "strong_replacement(M,P) ==
1.379        \<forall>A[M]. univalent(M,A,P) -->
1.380        (\<exists>Y[M]. \<forall>b[M]. b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))"
1.381
1.382 -  foundation_ax :: "(i=>o) => o"
1.383 +definition
1.384 +  foundation_ax :: "(i=>o) => o" where
1.385      "foundation_ax(M) ==
1.386  	\<forall>x[M]. (\<exists>y[M]. y\<in>x) --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
1.387
1.388 @@ -441,9 +500,9 @@
1.389
1.390
1.391  text{*More constants, for order types*}
1.392 +
1.393  definition
1.394 -
1.395 -  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
1.396 +  order_isomorphism :: "[i=>o,i,i,i,i,i] => o" where
1.397      "order_isomorphism(M,A,r,B,s,f) ==
1.398          bijection(M,A,B,f) &
1.399          (\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->
1.400 @@ -451,11 +510,13 @@
1.401              pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->
1.402              pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
1.403
1.404 -  pred_set :: "[i=>o,i,i,i,i] => o"
1.405 +definition
1.406 +  pred_set :: "[i=>o,i,i,i,i] => o" where
1.407      "pred_set(M,A,x,r,B) ==
1.408  	\<forall>y[M]. y \<in> B <-> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
1.409
1.410 -  membership :: "[i=>o,i,i] => o" --{*membership relation*}
1.411 +definition
1.412 +  membership :: "[i=>o,i,i] => o" where --{*membership relation*}
1.413      "membership(M,A,r) ==
1.414  	\<forall>p[M]. p \<in> r <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>A & x\<in>y & pair(M,x,y,p)))"
1.415
1.416 @@ -713,7 +774,7 @@
1.417  subsubsection {*Absoluteness for @{term Lambda}*}
1.418
1.419  definition
1.420 - is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
1.421 + is_lambda :: "[i=>o, i, [i,i]=>o, i] => o" where
1.422      "is_lambda(M, A, is_b, z) ==
1.423         \<forall>p[M]. p \<in> z <->
1.424          (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))"
1.425 @@ -1313,18 +1374,21 @@
1.426  subsection{*Relativization and Absoluteness for Boolean Operators*}
1.427
1.428  definition
1.429 -  is_bool_of_o :: "[i=>o, o, i] => o"
1.430 +  is_bool_of_o :: "[i=>o, o, i] => o" where
1.431     "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))"
1.432
1.433 -  is_not :: "[i=>o, i, i] => o"
1.434 +definition
1.435 +  is_not :: "[i=>o, i, i] => o" where
1.436     "is_not(M,a,z) == (number1(M,a)  & empty(M,z)) |
1.437                       (~number1(M,a) & number1(M,z))"
1.438
1.439 -  is_and :: "[i=>o, i, i, i] => o"
1.440 +definition
1.441 +  is_and :: "[i=>o, i, i, i] => o" where
1.442     "is_and(M,a,b,z) == (number1(M,a)  & z=b) |
1.443                         (~number1(M,a) & empty(M,z))"
1.444
1.445 -  is_or :: "[i=>o, i, i, i] => o"
1.446 +definition
1.447 +  is_or :: "[i=>o, i, i, i] => o" where
1.448     "is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) |
1.449                        (~number1(M,a) & z=b)"
1.450
1.451 @@ -1366,12 +1430,12 @@
1.452  subsection{*Relativization and Absoluteness for List Operators*}
1.453
1.454  definition
1.455 -
1.456 -  is_Nil :: "[i=>o, i] => o"
1.457 +  is_Nil :: "[i=>o, i] => o" where
1.458       --{* because @{term "[] \<equiv> Inl(0)"}*}
1.459      "is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
1.460
1.461 -  is_Cons :: "[i=>o,i,i,i] => o"
1.462 +definition
1.463 +  is_Cons :: "[i=>o,i,i,i] => o" where
1.464       --{* because @{term "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
1.465      "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
1.466
1.467 @@ -1391,34 +1455,39 @@
1.468
1.469
1.470  definition
1.471 -
1.472 -  quasilist :: "i => o"
1.473 +  quasilist :: "i => o" where
1.474      "quasilist(xs) == xs=Nil | (\<exists>x l. xs = Cons(x,l))"
1.475
1.476 -  is_quasilist :: "[i=>o,i] => o"
1.477 +definition
1.478 +  is_quasilist :: "[i=>o,i] => o" where
1.479      "is_quasilist(M,z) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))"
1.480
1.481 -  list_case' :: "[i, [i,i]=>i, i] => i"
1.482 +definition
1.483 +  list_case' :: "[i, [i,i]=>i, i] => i" where
1.484      --{*A version of @{term list_case} that's always defined.*}
1.485      "list_case'(a,b,xs) ==
1.486         if quasilist(xs) then list_case(a,b,xs) else 0"
1.487
1.488 -  is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
1.489 +definition
1.490 +  is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o" where
1.491      --{*Returns 0 for non-lists*}
1.492      "is_list_case(M, a, is_b, xs, z) ==
1.493         (is_Nil(M,xs) --> z=a) &
1.494         (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) &
1.495         (is_quasilist(M,xs) | empty(M,z))"
1.496
1.497 -  hd' :: "i => i"
1.498 +definition
1.499 +  hd' :: "i => i" where
1.500      --{*A version of @{term hd} that's always defined.*}
1.501      "hd'(xs) == if quasilist(xs) then hd(xs) else 0"
1.502
1.503 -  tl' :: "i => i"
1.504 +definition
1.505 +  tl' :: "i => i" where
1.506      --{*A version of @{term tl} that's always defined.*}
1.507      "tl'(xs) == if quasilist(xs) then tl(xs) else 0"
1.508
1.509 -  is_hd :: "[i=>o,i,i] => o"
1.510 +definition
1.511 +  is_hd :: "[i=>o,i,i] => o" where
1.512       --{* @{term "hd([]) = 0"} no constraints if not a list.
1.513            Avoiding implication prevents the simplifier's looping.*}
1.514      "is_hd(M,xs,H) ==
1.515 @@ -1426,7 +1495,8 @@
1.516         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
1.517         (is_quasilist(M,xs) | empty(M,H))"
1.518
1.519 -  is_tl :: "[i=>o,i,i] => o"
1.520 +definition
1.521 +  is_tl :: "[i=>o,i,i] => o" where