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
   1.522       --{* @{term "tl([]) = []"}; see comments about @{term is_hd}*}
   1.523      "is_tl(M,xs,T) ==
   1.524         (is_Nil(M,xs) --> T=xs) &