src/ZF/Constructible/Relative.thy
 changeset 46823 57bf0cecb366 parent 32960 69916a850301 child 46953 2b6e55924af3
1.1 --- a/src/ZF/Constructible/Relative.thy	Tue Mar 06 16:46:27 2012 +0000
1.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Mar 06 17:01:37 2012 +0000
1.3 @@ -14,11 +14,11 @@
1.5  definition
1.6    subset :: "[i=>o,i,i] => o" where
1.7 -    "subset(M,A,B) == \<forall>x[M]. x\<in>A --> x \<in> B"
1.8 +    "subset(M,A,B) == \<forall>x[M]. x\<in>A \<longrightarrow> x \<in> B"
1.10  definition
1.11    upair :: "[i=>o,i,i,i] => o" where
1.12 -    "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z --> x = a | x = b)"
1.13 +    "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x[M]. x\<in>z \<longrightarrow> x = a | x = b)"
1.15  definition
1.16    pair :: "[i=>o,i,i,i] => o" where
1.17 @@ -28,7 +28,7 @@
1.19  definition
1.20    union :: "[i=>o,i,i,i] => o" where
1.21 -    "union(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a | x \<in> b"
1.22 +    "union(M,a,b,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a | x \<in> b"
1.24  definition
1.25    is_cons :: "[i=>o,i,i,i] => o" where
1.26 @@ -52,38 +52,38 @@
1.28  definition
1.29    powerset :: "[i=>o,i,i] => o" where
1.30 -    "powerset(M,A,z) == \<forall>x[M]. x \<in> z <-> subset(M,x,A)"
1.31 +    "powerset(M,A,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> subset(M,x,A)"
1.33  definition
1.34    is_Collect :: "[i=>o,i,i=>o,i] => o" where
1.35 -    "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)"
1.36 +    "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> A & P(x)"
1.38  definition
1.39    is_Replace :: "[i=>o,i,[i,i]=>o,i] => o" where
1.40 -    "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))"
1.41 +    "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,u))"
1.43  definition
1.44    inter :: "[i=>o,i,i,i] => o" where
1.45 -    "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
1.46 +    "inter(M,a,b,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a & x \<in> b"
1.48  definition
1.49    setdiff :: "[i=>o,i,i,i] => o" where
1.50 -    "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<notin> b"
1.51 +    "setdiff(M,a,b,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> x \<in> a & x \<notin> b"
1.53  definition
1.54    big_union :: "[i=>o,i,i] => o" where
1.55 -    "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)"
1.56 +    "big_union(M,A,z) == \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>y[M]. y\<in>A & x \<in> y)"
1.58  definition
1.59    big_inter :: "[i=>o,i,i] => o" where
1.60      "big_inter(M,A,z) ==
1.61 -             (A=0 --> z=0) &
1.62 -             (A\<noteq>0 --> (\<forall>x[M]. x \<in> z <-> (\<forall>y[M]. y\<in>A --> x \<in> y)))"
1.63 +             (A=0 \<longrightarrow> z=0) &
1.64 +             (A\<noteq>0 \<longrightarrow> (\<forall>x[M]. x \<in> z \<longleftrightarrow> (\<forall>y[M]. y\<in>A \<longrightarrow> x \<in> y)))"
1.66  definition
1.67    cartprod :: "[i=>o,i,i,i] => o" where
1.68      "cartprod(M,A,B,z) ==
1.69 -        \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
1.70 +        \<forall>u[M]. u \<in> z \<longleftrightarrow> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))"
1.72  definition
1.73    is_sum :: "[i=>o,i,i,i] => o" where
1.74 @@ -103,23 +103,23 @@
1.75  definition
1.76    is_converse :: "[i=>o,i,i] => o" where
1.77      "is_converse(M,r,z) ==
1.78 -        \<forall>x[M]. x \<in> z <->
1.79 +        \<forall>x[M]. x \<in> z \<longleftrightarrow>
1.80               (\<exists>w[M]. w\<in>r & (\<exists>u[M]. \<exists>v[M]. pair(M,u,v,w) & pair(M,v,u,x)))"
1.82  definition
1.83    pre_image :: "[i=>o,i,i,i] => o" where
1.84      "pre_image(M,r,A,z) ==
1.85 -        \<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
1.86 +        \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))"
1.88  definition
1.89    is_domain :: "[i=>o,i,i] => o" where
1.90      "is_domain(M,r,z) ==
1.91 -        \<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w)))"
1.92 +        \<forall>x[M]. x \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w)))"
1.94  definition
1.95    image :: "[i=>o,i,i,i] => o" where
1.96      "image(M,r,A,z) ==
1.97 -        \<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w)))"
1.98 +        \<forall>y[M]. y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w)))"
1.100  definition
1.101    is_range :: "[i=>o,i,i] => o" where
1.102 @@ -128,7 +128,7 @@
1.103        unfortunately needs an instance of separation in order to prove
1.104          @{term "M(converse(r))"}.*}
1.105      "is_range(M,r,z) ==
1.106 -        \<forall>y[M]. y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w)))"
1.107 +        \<forall>y[M]. y \<in> z \<longleftrightarrow> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w)))"
1.109  definition
1.110    is_field :: "[i=>o,i,i] => o" where
1.111 @@ -139,13 +139,13 @@
1.112  definition
1.113    is_relation :: "[i=>o,i] => o" where
1.114      "is_relation(M,r) ==
1.115 -        (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
1.116 +        (\<forall>z[M]. z\<in>r \<longrightarrow> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))"
1.118  definition
1.119    is_function :: "[i=>o,i] => o" where
1.120      "is_function(M,r) ==
1.121          \<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
1.122 -           pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'"
1.123 +           pair(M,x,y,p) \<longrightarrow> pair(M,x,y',p') \<longrightarrow> p\<in>r \<longrightarrow> p'\<in>r \<longrightarrow> y=y'"
1.125  definition
1.126    fun_apply :: "[i=>o,i,i,i] => o" where
1.127 @@ -157,17 +157,17 @@
1.128    typed_function :: "[i=>o,i,i,i] => o" where
1.129      "typed_function(M,A,B,r) ==
1.130          is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
1.131 -        (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))"
1.132 +        (\<forall>u[M]. u\<in>r \<longrightarrow> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) \<longrightarrow> y\<in>B))"
1.134  definition
1.135    is_funspace :: "[i=>o,i,i,i] => o" where
1.136      "is_funspace(M,A,B,F) ==
1.137 -        \<forall>f[M]. f \<in> F <-> typed_function(M,A,B,f)"
1.138 +        \<forall>f[M]. f \<in> F \<longleftrightarrow> typed_function(M,A,B,f)"
1.140  definition
1.141    composition :: "[i=>o,i,i,i] => o" where
1.142      "composition(M,r,s,t) ==
1.143 -        \<forall>p[M]. p \<in> t <->
1.144 +        \<forall>p[M]. p \<in> t \<longleftrightarrow>
1.145                 (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
1.146                  pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
1.147                  xy \<in> s & yz \<in> r)"
1.148 @@ -177,13 +177,13 @@
1.149      "injection(M,A,B,f) ==
1.150          typed_function(M,A,B,f) &
1.151          (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
1.152 -          pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')"
1.153 +          pair(M,x,y,p) \<longrightarrow> pair(M,x',y,p') \<longrightarrow> p\<in>f \<longrightarrow> p'\<in>f \<longrightarrow> x=x')"
1.155  definition
1.156    surjection :: "[i=>o,i,i,i] => o" where
1.157      "surjection(M,A,B,f) ==
1.158          typed_function(M,A,B,f) &
1.159 -        (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))"
1.160 +        (\<forall>y[M]. y\<in>B \<longrightarrow> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))"
1.162  definition
1.163    bijection :: "[i=>o,i,i,i] => o" where
1.164 @@ -192,23 +192,23 @@
1.165  definition
1.166    restriction :: "[i=>o,i,i,i] => o" where
1.167      "restriction(M,r,A,z) ==
1.168 -        \<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))"
1.169 +        \<forall>x[M]. x \<in> z \<longleftrightarrow> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))"
1.171  definition
1.172    transitive_set :: "[i=>o,i] => o" where
1.173 -    "transitive_set(M,a) == \<forall>x[M]. x\<in>a --> subset(M,x,a)"
1.174 +    "transitive_set(M,a) == \<forall>x[M]. x\<in>a \<longrightarrow> subset(M,x,a)"
1.176  definition
1.177    ordinal :: "[i=>o,i] => o" where
1.178       --{*an ordinal is a transitive set of transitive sets*}
1.179 -    "ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a --> transitive_set(M,x))"
1.180 +    "ordinal(M,a) == transitive_set(M,a) & (\<forall>x[M]. x\<in>a \<longrightarrow> transitive_set(M,x))"
1.182  definition
1.183    limit_ordinal :: "[i=>o,i] => o" where
1.184      --{*a limit ordinal is a non-empty, successor-closed ordinal*}
1.185      "limit_ordinal(M,a) ==
1.186          ordinal(M,a) & ~ empty(M,a) &
1.187 -        (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
1.188 +        (\<forall>x[M]. x\<in>a \<longrightarrow> (\<exists>y[M]. y\<in>a & successor(M,x,y)))"
1.190  definition
1.191    successor_ordinal :: "[i=>o,i] => o" where
1.192 @@ -221,12 +221,12 @@
1.193      --{*an ordinal is finite if neither it nor any of its elements are limit*}
1.194      "finite_ordinal(M,a) ==
1.195          ordinal(M,a) & ~ limit_ordinal(M,a) &
1.196 -        (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
1.197 +        (\<forall>x[M]. x\<in>a \<longrightarrow> ~ limit_ordinal(M,x))"
1.199  definition
1.200    omega :: "[i=>o,i] => o" where
1.201      --{*omega is a limit ordinal none of whose elements are limit*}
1.202 -    "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))"
1.203 +    "omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a \<longrightarrow> ~ limit_ordinal(M,x))"
1.205  definition
1.206    is_quasinat :: "[i=>o,i] => o" where
1.207 @@ -235,44 +235,44 @@
1.208  definition
1.209    is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" where
1.210      "is_nat_case(M, a, is_b, k, z) ==
1.211 -       (empty(M,k) --> z=a) &
1.212 -       (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
1.213 +       (empty(M,k) \<longrightarrow> z=a) &
1.214 +       (\<forall>m[M]. successor(M,m,k) \<longrightarrow> is_b(m,z)) &
1.215         (is_quasinat(M,k) | empty(M,z))"
1.217  definition
1.218    relation1 :: "[i=>o, [i,i]=>o, i=>i] => o" where
1.219 -    "relation1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) <-> y = f(x)"
1.220 +    "relation1(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. is_f(x,y) \<longleftrightarrow> y = f(x)"
1.222  definition
1.223    Relation1 :: "[i=>o, i, [i,i]=>o, i=>i] => o" where
1.224      --{*as above, but typed*}
1.225      "Relation1(M,A,is_f,f) ==
1.226 -        \<forall>x[M]. \<forall>y[M]. x\<in>A --> is_f(x,y) <-> y = f(x)"
1.227 +        \<forall>x[M]. \<forall>y[M]. x\<in>A \<longrightarrow> is_f(x,y) \<longleftrightarrow> y = f(x)"
1.229  definition
1.230    relation2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o" where
1.231 -    "relation2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) <-> z = f(x,y)"
1.232 +    "relation2(M,is_f,f) == \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. is_f(x,y,z) \<longleftrightarrow> z = f(x,y)"
1.234  definition
1.235    Relation2 :: "[i=>o, i, i, [i,i,i]=>o, [i,i]=>i] => o" where
1.236      "Relation2(M,A,B,is_f,f) ==
1.237 -        \<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.238 +        \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. x\<in>A \<longrightarrow> y\<in>B \<longrightarrow> is_f(x,y,z) \<longleftrightarrow> z = f(x,y)"
1.240  definition
1.241    relation3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o" where
1.242      "relation3(M,is_f,f) ==
1.243 -       \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)"
1.244 +       \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M]. is_f(x,y,z,u) \<longleftrightarrow> u = f(x,y,z)"
1.246  definition
1.247    Relation3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o" where
1.248      "Relation3(M,A,B,C,is_f,f) ==
1.249         \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>u[M].
1.250 -         x\<in>A --> y\<in>B --> z\<in>C --> is_f(x,y,z,u) <-> u = f(x,y,z)"
1.251 +         x\<in>A \<longrightarrow> y\<in>B \<longrightarrow> z\<in>C \<longrightarrow> is_f(x,y,z,u) \<longleftrightarrow> u = f(x,y,z)"
1.253  definition
1.254    relation4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o" where
1.255      "relation4(M,is_f,f) ==
1.256 -       \<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.257 +       \<forall>u[M]. \<forall>x[M]. \<forall>y[M]. \<forall>z[M]. \<forall>a[M]. is_f(u,x,y,z,a) \<longleftrightarrow> a = f(u,x,y,z)"
1.260  text{*Useful when absoluteness reasoning has replaced the predicates by terms*}
1.261 @@ -290,7 +290,7 @@
1.262  definition
1.263    extensionality :: "(i=>o) => o" where
1.264      "extensionality(M) ==
1.265 -        \<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x <-> z \<in> y) --> x=y"
1.266 +        \<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x \<longleftrightarrow> z \<in> y) \<longrightarrow> x=y"
1.268  definition
1.269    separation :: "[i=>o, i=>o] => o" where
1.270 @@ -299,7 +299,7 @@
1.271          to @{text M}.  We do not have separation as a scheme; every instance
1.272          that we need must be assumed (and later proved) separately.*}
1.273      "separation(M,P) ==
1.274 -        \<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
1.275 +        \<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y \<longleftrightarrow> x \<in> z & P(x)"
1.277  definition
1.278    upair_ax :: "(i=>o) => o" where
1.279 @@ -316,24 +316,24 @@
1.280  definition
1.281    univalent :: "[i=>o, i, [i,i]=>o] => o" where
1.282      "univalent(M,A,P) ==
1.283 -        \<forall>x[M]. x\<in>A --> (\<forall>y[M]. \<forall>z[M]. P(x,y) & P(x,z) --> y=z)"
1.284 +        \<forall>x[M]. x\<in>A \<longrightarrow> (\<forall>y[M]. \<forall>z[M]. P(x,y) & P(x,z) \<longrightarrow> y=z)"
1.286  definition
1.287    replacement :: "[i=>o, [i,i]=>o] => o" where
1.288      "replacement(M,P) ==
1.289 -      \<forall>A[M]. univalent(M,A,P) -->
1.290 -      (\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y)"
1.291 +      \<forall>A[M]. univalent(M,A,P) \<longrightarrow>
1.292 +      (\<exists>Y[M]. \<forall>b[M]. (\<exists>x[M]. x\<in>A & P(x,b)) \<longrightarrow> b \<in> Y)"
1.294  definition
1.295    strong_replacement :: "[i=>o, [i,i]=>o] => o" where
1.296      "strong_replacement(M,P) ==
1.297 -      \<forall>A[M]. univalent(M,A,P) -->
1.298 -      (\<exists>Y[M]. \<forall>b[M]. b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b)))"
1.299 +      \<forall>A[M]. univalent(M,A,P) \<longrightarrow>
1.300 +      (\<exists>Y[M]. \<forall>b[M]. b \<in> Y \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,b)))"
1.302  definition
1.303    foundation_ax :: "(i=>o) => o" where
1.304      "foundation_ax(M) ==
1.305 -        \<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.306 +        \<forall>x[M]. (\<exists>y[M]. y\<in>x) \<longrightarrow> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
1.309  subsection{*A trivial consistency proof for $V_\omega$ *}
1.310 @@ -348,22 +348,22 @@
1.311  done
1.313  lemma univ0_Ball_abs [simp]:
1.314 -     "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))"
1.315 +     "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(x))"
1.316  by (blast intro: univ0_downwards_mem)
1.318  lemma univ0_Bex_abs [simp]:
1.319 -     "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))"
1.320 +     "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(x))"
1.321  by (blast intro: univ0_downwards_mem)
1.323  text{*Congruence rule for separation: can assume the variable is in @{text M}*}
1.324  lemma separation_cong [cong]:
1.325 -     "(!!x. M(x) ==> P(x) <-> P'(x))
1.326 -      ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))"
1.327 +     "(!!x. M(x) ==> P(x) \<longleftrightarrow> P'(x))
1.328 +      ==> separation(M, %x. P(x)) \<longleftrightarrow> separation(M, %x. P'(x))"
1.331  lemma univalent_cong [cong]:
1.332 -     "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
1.333 -      ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))"
1.334 +     "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) \<longleftrightarrow> P'(x,y) |]
1.335 +      ==> univalent(M, A, %x y. P(x,y)) \<longleftrightarrow> univalent(M, A', %x y. P'(x,y))"
1.338  lemma univalent_triv [intro,simp]:
1.339 @@ -376,8 +376,8 @@
1.341  text{*Congruence rule for replacement*}
1.342  lemma strong_replacement_cong [cong]:
1.343 -     "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
1.344 -      ==> strong_replacement(M, %x y. P(x,y)) <->
1.345 +     "[| !!x y. [| M(x); M(y) |] ==> P(x,y) \<longleftrightarrow> P'(x,y) |]
1.346 +      ==> strong_replacement(M, %x y. P(x,y)) \<longleftrightarrow>
1.347            strong_replacement(M, %x y. P'(x,y))"
1.350 @@ -457,13 +457,13 @@
1.351  subsection{*Lemmas Needed to Reduce Some Set Constructions to Instances
1.352        of Separation*}
1.354 -lemma image_iff_Collect: "r  A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
1.355 +lemma image_iff_Collect: "r  A = {y \<in> \<Union>(\<Union>(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
1.356  apply (rule equalityI, auto)
1.357  apply (simp add: Pair_def, blast)
1.358  done
1.360  lemma vimage_iff_Collect:
1.361 -     "r - A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
1.362 +     "r - A = {x \<in> \<Union>(\<Union>(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
1.363  apply (rule equalityI, auto)
1.364  apply (simp add: Pair_def, blast)
1.365  done
1.366 @@ -485,16 +485,16 @@
1.368  lemma replacementD:
1.369      "[| replacement(M,P); M(A);  univalent(M,A,P) |]
1.370 -     ==> \<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) --> b \<in> Y))"
1.371 +     ==> \<exists>Y[M]. (\<forall>b[M]. ((\<exists>x[M]. x\<in>A & P(x,b)) \<longrightarrow> b \<in> Y))"
1.374  lemma strong_replacementD:
1.375      "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]
1.376 -     ==> \<exists>Y[M]. (\<forall>b[M]. (b \<in> Y <-> (\<exists>x[M]. x\<in>A & P(x,b))))"
1.377 +     ==> \<exists>Y[M]. (\<forall>b[M]. (b \<in> Y \<longleftrightarrow> (\<exists>x[M]. x\<in>A & P(x,b))))"
1.380  lemma separationD:
1.381 -    "[| separation(M,P); M(z) |] ==> \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
1.382 +    "[| separation(M,P); M(z) |] ==> \<exists>y[M]. \<forall>x[M]. x \<in> y \<longleftrightarrow> x \<in> z & P(x)"
1.386 @@ -504,20 +504,20 @@
1.387    order_isomorphism :: "[i=>o,i,i,i,i,i] => o" where
1.388      "order_isomorphism(M,A,r,B,s,f) ==
1.389          bijection(M,A,B,f) &
1.390 -        (\<forall>x[M]. x\<in>A --> (\<forall>y[M]. y\<in>A -->
1.391 +        (\<forall>x[M]. x\<in>A \<longrightarrow> (\<forall>y[M]. y\<in>A \<longrightarrow>
1.392            (\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].
1.393 -            pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->
1.394 -            pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
1.395 +            pair(M,x,y,p) \<longrightarrow> fun_apply(M,f,x,fx) \<longrightarrow> fun_apply(M,f,y,fy) \<longrightarrow>
1.396 +            pair(M,fx,fy,q) \<longrightarrow> (p\<in>r \<longleftrightarrow> q\<in>s))))"
1.398  definition
1.399    pred_set :: "[i=>o,i,i,i,i] => o" where
1.400      "pred_set(M,A,x,r,B) ==
1.401 -        \<forall>y[M]. y \<in> B <-> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
1.402 +        \<forall>y[M]. y \<in> B \<longleftrightarrow> (\<exists>p[M]. p\<in>r & y \<in> A & pair(M,y,x,p))"
1.404  definition
1.405    membership :: "[i=>o,i,i] => o" where --{*membership relation*}
1.406      "membership(M,A,r) ==
1.407 -        \<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.408 +        \<forall>p[M]. p \<in> r \<longleftrightarrow> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>A & x\<in>y & pair(M,x,y,p)))"
1.411  subsection{*Introducing a Transitive Class Model*}
1.412 @@ -540,65 +540,65 @@
1.413  by (blast intro: transM)
1.415  lemma (in M_trivial) rall_abs [simp]:
1.416 -     "M(A) ==> (\<forall>x[M]. x\<in>A --> P(x)) <-> (\<forall>x\<in>A. P(x))"
1.417 +     "M(A) ==> (\<forall>x[M]. x\<in>A \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(x))"
1.418  by (blast intro: transM)
1.420  lemma (in M_trivial) rex_abs [simp]:
1.421 -     "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) <-> (\<exists>x\<in>A. P(x))"
1.422 +     "M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(x))"
1.423  by (blast intro: transM)
1.425  lemma (in M_trivial) ball_iff_equiv:
1.426 -     "M(A) ==> (\<forall>x[M]. (x\<in>A <-> P(x))) <->
1.427 -               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)"
1.428 +     "M(A) ==> (\<forall>x[M]. (x\<in>A \<longleftrightarrow> P(x))) \<longleftrightarrow>
1.429 +               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) \<longrightarrow> M(x) \<longrightarrow> x\<in>A)"
1.430  by (blast intro: transM)
1.432  text{*Simplifies proofs of equalities when there's an iff-equality
1.433 -      available for rewriting, universally quantified over M.
1.434 +      available for rewriting, universally quantified over M.
1.435        But it's not the only way to prove such equalities: its
1.436        premises @{term "M(A)"} and  @{term "M(B)"} can be too strong.*}
1.437  lemma (in M_trivial) M_equalityI:
1.438 -     "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
1.439 +     "[| !!x. M(x) ==> x\<in>A \<longleftrightarrow> x\<in>B; M(A); M(B) |] ==> A=B"
1.440  by (blast intro!: equalityI dest: transM)
1.443  subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*}
1.445  lemma (in M_trivial) empty_abs [simp]:
1.446 -     "M(z) ==> empty(M,z) <-> z=0"
1.447 +     "M(z) ==> empty(M,z) \<longleftrightarrow> z=0"
1.449  apply (blast intro: transM)
1.450  done
1.452  lemma (in M_trivial) subset_abs [simp]:
1.453 -     "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
1.454 +     "M(A) ==> subset(M,A,B) \<longleftrightarrow> A \<subseteq> B"
1.456  apply (blast intro: transM)
1.457  done
1.459  lemma (in M_trivial) upair_abs [simp]:
1.460 -     "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
1.461 +     "M(z) ==> upair(M,a,b,z) \<longleftrightarrow> z={a,b}"
1.463  apply (blast intro: transM)
1.464  done
1.466  lemma (in M_trivial) upair_in_M_iff [iff]:
1.467 -     "M({a,b}) <-> M(a) & M(b)"
1.468 +     "M({a,b}) \<longleftrightarrow> M(a) & M(b)"
1.469  apply (insert upair_ax, simp add: upair_ax_def)
1.470  apply (blast intro: transM)
1.471  done
1.473  lemma (in M_trivial) singleton_in_M_iff [iff]:
1.474 -     "M({a}) <-> M(a)"
1.475 +     "M({a}) \<longleftrightarrow> M(a)"
1.476  by (insert upair_in_M_iff [of a a], simp)
1.478  lemma (in M_trivial) pair_abs [simp]:
1.479 -     "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
1.480 +     "M(z) ==> pair(M,a,b,z) \<longleftrightarrow> z=<a,b>"
1.481  apply (simp add: pair_def ZF.Pair_def)
1.482  apply (blast intro: transM)
1.483  done
1.485  lemma (in M_trivial) pair_in_M_iff [iff]:
1.486 -     "M(<a,b>) <-> M(a) & M(b)"
1.487 +     "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
1.490  lemma (in M_trivial) pair_components_in_M:
1.491 @@ -608,7 +608,7 @@
1.492  done
1.494  lemma (in M_trivial) cartprod_abs [simp]:
1.495 -     "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
1.496 +     "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) \<longleftrightarrow> z = A*B"
1.498  apply (rule iffI)
1.499   apply (blast intro!: equalityI intro: transM dest!: rspec)
1.500 @@ -618,35 +618,35 @@
1.501  subsubsection{*Absoluteness for Unions and Intersections*}
1.503  lemma (in M_trivial) union_abs [simp]:
1.504 -     "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
1.505 +     "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) \<longleftrightarrow> z = a \<union> b"
1.507  apply (blast intro: transM)
1.508  done
1.510  lemma (in M_trivial) inter_abs [simp]:
1.511 -     "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
1.512 +     "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) \<longleftrightarrow> z = a \<inter> b"
1.514  apply (blast intro: transM)
1.515  done
1.517  lemma (in M_trivial) setdiff_abs [simp]:
1.518 -     "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
1.519 +     "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) \<longleftrightarrow> z = a-b"
1.521  apply (blast intro: transM)
1.522  done
1.524  lemma (in M_trivial) Union_abs [simp]:
1.525 -     "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
1.526 +     "[| M(A); M(z) |] ==> big_union(M,A,z) \<longleftrightarrow> z = \<Union>(A)"
1.528  apply (blast intro!: equalityI dest: transM)
1.529  done
1.531  lemma (in M_trivial) Union_closed [intro,simp]:
1.532 -     "M(A) ==> M(Union(A))"
1.533 +     "M(A) ==> M(\<Union>(A))"
1.534  by (insert Union_ax, simp add: Union_ax_def)
1.536  lemma (in M_trivial) Un_closed [intro,simp]:
1.537 -     "[| M(A); M(B) |] ==> M(A Un B)"
1.538 +     "[| M(A); M(B) |] ==> M(A \<union> B)"
1.539  by (simp only: Un_eq_Union, blast)
1.541  lemma (in M_trivial) cons_closed [intro,simp]:
1.542 @@ -654,15 +654,15 @@
1.543  by (subst cons_eq [symmetric], blast)
1.545  lemma (in M_trivial) cons_abs [simp]:
1.546 -     "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)"
1.547 +     "[| M(b); M(z) |] ==> is_cons(M,a,b,z) \<longleftrightarrow> z = cons(a,b)"
1.548  by (simp add: is_cons_def, blast intro: transM)
1.550  lemma (in M_trivial) successor_abs [simp]:
1.551 -     "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)"
1.552 +     "[| M(a); M(z) |] ==> successor(M,a,z) \<longleftrightarrow> z = succ(a)"
1.553  by (simp add: successor_def, blast)
1.555  lemma (in M_trivial) succ_in_M_iff [iff]:
1.556 -     "M(succ(a)) <-> M(a)"
1.557 +     "M(succ(a)) \<longleftrightarrow> M(a)"
1.559  apply (blast intro: transM)
1.560  done
1.561 @@ -678,11 +678,11 @@
1.562  done
1.564  lemma separation_iff:
1.565 -     "separation(M,P) <-> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
1.566 +     "separation(M,P) \<longleftrightarrow> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
1.567  by (simp add: separation_def is_Collect_def)
1.569  lemma (in M_trivial) Collect_abs [simp]:
1.570 -     "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) <-> z = Collect(A,P)"
1.571 +     "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) \<longleftrightarrow> z = Collect(A,P)"
1.573  apply (blast intro!: equalityI dest: transM)
1.574  done
1.575 @@ -703,16 +703,16 @@
1.577  lemma is_Replace_cong [cong]:
1.578       "[| A=A';
1.579 -         !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y);
1.580 +         !!x y. [| M(x); M(y) |] ==> P(x,y) \<longleftrightarrow> P'(x,y);
1.581           z=z' |]
1.582 -      ==> is_Replace(M, A, %x y. P(x,y), z) <->
1.583 +      ==> is_Replace(M, A, %x y. P(x,y), z) \<longleftrightarrow>
1.584            is_Replace(M, A', %x y. P'(x,y), z')"
1.587  lemma (in M_trivial) univalent_Replace_iff:
1.588       "[| M(A); univalent(M,A,P);
1.589           !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
1.590 -      ==> u \<in> Replace(A,P) <-> (\<exists>x. x\<in>A & P(x,u))"
1.591 +      ==> u \<in> Replace(A,P) \<longleftrightarrow> (\<exists>x. x\<in>A & P(x,u))"
1.592  apply (simp add: Replace_iff univalent_def)
1.593  apply (blast dest: transM)
1.594  done
1.595 @@ -731,13 +731,13 @@
1.596  done
1.598  lemma (in M_trivial) Replace_abs:
1.599 -     "[| M(A); M(z); univalent(M,A,P);
1.600 +     "[| M(A); M(z); univalent(M,A,P);
1.601           !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |]
1.602 -      ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)"
1.603 +      ==> is_Replace(M,A,P,z) \<longleftrightarrow> z = Replace(A,P)"
1.605  apply (rule iffI)
1.606   apply (rule equality_iffI)
1.607 - apply (simp_all add: univalent_Replace_iff)
1.608 + apply (simp_all add: univalent_Replace_iff)
1.609   apply (blast dest: transM)+
1.610  done
1.612 @@ -747,7 +747,7 @@
1.613    Let K be a nonconstructible subset of nat and define
1.614    f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a
1.615    nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
1.616 -  even for f : M -> M.
1.617 +  even for f \<in> M -> M.
1.618  *)
1.619  lemma (in M_trivial) RepFun_closed:
1.620       "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
1.621 @@ -775,7 +775,7 @@
1.622  definition
1.623   is_lambda :: "[i=>o, i, [i,i]=>o, i] => o" where
1.624      "is_lambda(M, A, is_b, z) ==
1.625 -       \<forall>p[M]. p \<in> z <->
1.626 +       \<forall>p[M]. p \<in> z \<longleftrightarrow>
1.627          (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))"
1.629  lemma (in M_trivial) lam_closed:
1.630 @@ -786,33 +786,33 @@
1.631  text{*Better than @{text lam_closed}: has the formula @{term "x\<in>A"}*}
1.632  lemma (in M_trivial) lam_closed2:
1.633    "[|strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
1.634 -     M(A); \<forall>m[M]. m\<in>A --> M(b(m))|] ==> M(Lambda(A,b))"
1.635 +     M(A); \<forall>m[M]. m\<in>A \<longrightarrow> M(b(m))|] ==> M(Lambda(A,b))"
1.637  apply (blast intro: RepFun_closed2 dest: transM)
1.638  done
1.640  lemma (in M_trivial) lambda_abs2:
1.641 -     "[| Relation1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
1.642 -      ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
1.643 +     "[| Relation1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A \<longrightarrow> M(b(m)); M(z) |]
1.644 +      ==> is_lambda(M,A,is_b,z) \<longleftrightarrow> z = Lambda(A,b)"
1.645  apply (simp add: Relation1_def is_lambda_def)
1.646  apply (rule iffI)
1.647   prefer 2 apply (simp add: lam_def)
1.648  apply (rule equality_iffI)
1.650 -apply (rule iffI)
1.651 - apply (blast dest: transM)
1.652 -apply (auto simp add: transM [of _ A])
1.654 +apply (rule iffI)
1.655 + apply (blast dest: transM)
1.656 +apply (auto simp add: transM [of _ A])
1.657  done
1.659  lemma is_lambda_cong [cong]:
1.660       "[| A=A';  z=z';
1.661 -         !!x y. [| x\<in>A; M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
1.662 -      ==> is_lambda(M, A, %x y. is_b(x,y), z) <->
1.663 +         !!x y. [| x\<in>A; M(x); M(y) |] ==> is_b(x,y) \<longleftrightarrow> is_b'(x,y) |]
1.664 +      ==> is_lambda(M, A, %x y. is_b(x,y), z) \<longleftrightarrow>
1.665            is_lambda(M, A', %x y. is_b'(x,y), z')"
1.668  lemma (in M_trivial) image_abs [simp]:
1.669 -     "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = rA"
1.670 +     "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) \<longleftrightarrow> z = rA"
1.672  apply (rule iffI)
1.673   apply (blast intro!: equalityI dest: transM, blast)
1.674 @@ -828,7 +828,7 @@
1.675  text{*But we can't prove that the powerset in @{text M} includes the
1.676        real powerset.*}
1.677  lemma (in M_trivial) powerset_imp_subset_Pow:
1.678 -     "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
1.679 +     "[| powerset(M,x,y); M(y) |] ==> y \<subseteq> Pow(x)"
1.681  apply (blast dest: transM)
1.682  done
1.683 @@ -847,12 +847,12 @@
1.684  done
1.686  lemma (in M_trivial) quasinat_abs [simp]:
1.687 -     "M(z) ==> is_quasinat(M,z) <-> quasinat(z)"
1.688 +     "M(z) ==> is_quasinat(M,z) \<longleftrightarrow> quasinat(z)"
1.689  by (auto simp add: is_quasinat_def quasinat_def)
1.691  lemma (in M_trivial) nat_case_abs [simp]:
1.692       "[| relation1(M,is_b,b); M(k); M(z) |]
1.693 -      ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)"
1.694 +      ==> is_nat_case(M,a,is_b,k,z) \<longleftrightarrow> z = nat_case(a,b,k)"
1.695  apply (case_tac "quasinat(k)")
1.696   prefer 2
1.697   apply (simp add: is_nat_case_def non_nat_case)
1.698 @@ -867,8 +867,8 @@
1.699    is_nat_case by nat_case before attempting congruence reasoning.*)
1.700  lemma is_nat_case_cong:
1.701       "[| a = a'; k = k';  z = z';  M(z');
1.702 -       !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
1.703 -      ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
1.704 +       !!x y. [| M(x); M(y) |] ==> is_b(x,y) \<longleftrightarrow> is_b'(x,y) |]
1.705 +      ==> is_nat_case(M, a, is_b, k, z) \<longleftrightarrow> is_nat_case(M, a', is_b', k', z')"
1.709 @@ -880,22 +880,22 @@
1.710  by (blast dest: ltD intro: transM)
1.712  lemma (in M_trivial) transitive_set_abs [simp]:
1.713 -     "M(a) ==> transitive_set(M,a) <-> Transset(a)"
1.714 +     "M(a) ==> transitive_set(M,a) \<longleftrightarrow> Transset(a)"
1.715  by (simp add: transitive_set_def Transset_def)
1.717  lemma (in M_trivial) ordinal_abs [simp]:
1.718 -     "M(a) ==> ordinal(M,a) <-> Ord(a)"
1.719 +     "M(a) ==> ordinal(M,a) \<longleftrightarrow> Ord(a)"
1.720  by (simp add: ordinal_def Ord_def)
1.722  lemma (in M_trivial) limit_ordinal_abs [simp]:
1.723 -     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
1.724 +     "M(a) ==> limit_ordinal(M,a) \<longleftrightarrow> Limit(a)"
1.725  apply (unfold Limit_def limit_ordinal_def)
1.727  apply (simp add: lt_def, blast)
1.728  done
1.730  lemma (in M_trivial) successor_ordinal_abs [simp]:
1.731 -     "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b[M]. a = succ(b))"
1.732 +     "M(a) ==> successor_ordinal(M,a) \<longleftrightarrow> Ord(a) & (\<exists>b[M]. a = succ(b))"
1.733  apply (simp add: successor_ordinal_def, safe)
1.734  apply (drule Ord_cases_disj, auto)
1.735  done
1.736 @@ -905,7 +905,7 @@
1.737  by (induct a rule: trans_induct3, simp_all)
1.739  lemma (in M_trivial) finite_ordinal_abs [simp]:
1.740 -     "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
1.741 +     "M(a) ==> finite_ordinal(M,a) \<longleftrightarrow> a \<in> nat"
1.743  apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord
1.744               dest: Ord_trans naturals_not_limit)
1.745 @@ -921,21 +921,21 @@
1.746  done
1.748  lemma (in M_trivial) omega_abs [simp]:
1.749 -     "M(a) ==> omega(M,a) <-> a = nat"
1.750 +     "M(a) ==> omega(M,a) \<longleftrightarrow> a = nat"
1.752  apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
1.753  done
1.755  lemma (in M_trivial) number1_abs [simp]:
1.756 -     "M(a) ==> number1(M,a) <-> a = 1"
1.757 +     "M(a) ==> number1(M,a) \<longleftrightarrow> a = 1"
1.760  lemma (in M_trivial) number2_abs [simp]:
1.761 -     "M(a) ==> number2(M,a) <-> a = succ(1)"
1.762 +     "M(a) ==> number2(M,a) \<longleftrightarrow> a = succ(1)"
1.765  lemma (in M_trivial) number3_abs [simp]:
1.766 -     "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
1.767 +     "M(a) ==> number3(M,a) \<longleftrightarrow> a = succ(succ(1))"
1.770  text{*Kunen continued to 20...*}
1.771 @@ -965,7 +965,7 @@
1.773  locale M_basic = M_trivial +
1.774  assumes Inter_separation:
1.775 -     "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A --> x\<in>y)"
1.776 +     "M(A) ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>A \<longrightarrow> x\<in>y)"
1.777    and Diff_separation:
1.778       "M(B) ==> separation(M, \<lambda>x. x \<notin> B)"
1.779    and cartprod_separation:
1.780 @@ -1003,7 +1003,7 @@
1.781                                     fx \<noteq> gx))"
1.783  lemma (in M_basic) cartprod_iff_lemma:
1.784 -     "[| M(C);  \<forall>u[M]. u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
1.785 +     "[| M(C);  \<forall>u[M]. u \<in> C \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
1.786           powerset(M, A \<union> B, p1); powerset(M, p1, p2);  M(p2) |]
1.787         ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
1.789 @@ -1017,8 +1017,8 @@
1.791  lemma (in M_basic) cartprod_iff:
1.792       "[| M(A); M(B); M(C) |]
1.793 -      ==> cartprod(M,A,B,C) <->
1.794 -          (\<exists>p1[M]. \<exists>p2[M]. powerset(M,A Un B,p1) & powerset(M,p1,p2) &
1.795 +      ==> cartprod(M,A,B,C) \<longleftrightarrow>
1.796 +          (\<exists>p1[M]. \<exists>p2[M]. powerset(M,A \<union> B,p1) & powerset(M,p1,p2) &
1.797                     C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
1.798  apply (simp add: Pair_def cartprod_def, safe)
1.799  defer 1
1.800 @@ -1026,7 +1026,7 @@
1.801   apply blast
1.802  txt{*Final, difficult case: the left-to-right direction of the theorem.*}
1.803  apply (insert power_ax, simp add: power_ax_def)
1.804 -apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
1.805 +apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
1.806  apply (blast, clarify)
1.807  apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
1.808  apply assumption
1.809 @@ -1037,7 +1037,7 @@
1.810       "[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
1.811  apply (simp del: cartprod_abs add: cartprod_iff)
1.812  apply (insert power_ax, simp add: power_ax_def)
1.813 -apply (frule_tac x="A Un B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
1.814 +apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
1.815  apply (blast, clarify)
1.816  apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec, auto)
1.817  apply (intro rexI conjI, simp+)
1.818 @@ -1055,23 +1055,23 @@
1.821  lemma (in M_basic) sum_abs [simp]:
1.822 -     "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
1.823 +     "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) \<longleftrightarrow> (Z = A+B)"
1.824  by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
1.826  lemma (in M_trivial) Inl_in_M_iff [iff]:
1.827 -     "M(Inl(a)) <-> M(a)"
1.828 +     "M(Inl(a)) \<longleftrightarrow> M(a)"
1.831  lemma (in M_trivial) Inl_abs [simp]:
1.832 -     "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
1.833 +     "M(Z) ==> is_Inl(M,a,Z) \<longleftrightarrow> (Z = Inl(a))"
1.834  by (simp add: is_Inl_def Inl_def)
1.836  lemma (in M_trivial) Inr_in_M_iff [iff]:
1.837 -     "M(Inr(a)) <-> M(a)"
1.838 +     "M(Inr(a)) \<longleftrightarrow> M(a)"
1.841  lemma (in M_trivial) Inr_abs [simp]:
1.842 -     "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
1.843 +     "M(Z) ==> is_Inr(M,a,Z) \<longleftrightarrow> (Z = Inr(a))"
1.844  by (simp add: is_Inr_def Inr_def)
1.847 @@ -1080,7 +1080,7 @@
1.848  lemma (in M_basic) M_converse_iff:
1.849       "M(r) ==>
1.850        converse(r) =
1.851 -      {z \<in> Union(Union(r)) * Union(Union(r)).
1.852 +      {z \<in> \<Union>(\<Union>(r)) * \<Union>(\<Union>(r)).
1.853         \<exists>p\<in>r. \<exists>x[M]. \<exists>y[M]. p = \<langle>x,y\<rangle> & z = \<langle>y,x\<rangle>}"
1.854  apply (rule equalityI)
1.855   prefer 2 apply (blast dest: transM, clarify, simp)
1.856 @@ -1095,7 +1095,7 @@
1.857  done
1.859  lemma (in M_basic) converse_abs [simp]:
1.860 -     "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
1.861 +     "[| M(r); M(z) |] ==> is_converse(M,r,z) \<longleftrightarrow> z = converse(r)"
1.863  apply (rule iffI)
1.864   prefer 2 apply blast
1.865 @@ -1114,7 +1114,7 @@
1.866  done
1.868  lemma (in M_basic) vimage_abs [simp]:
1.869 -     "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-A"
1.870 +     "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) \<longleftrightarrow> z = r-A"
1.872  apply (rule iffI)
1.873   apply (blast intro!: equalityI dest: transM, blast)
1.874 @@ -1128,7 +1128,7 @@
1.875  subsubsection{*Domain, range and field*}
1.877  lemma (in M_basic) domain_abs [simp]:
1.878 -     "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
1.879 +     "[| M(r); M(z) |] ==> is_domain(M,r,z) \<longleftrightarrow> z = domain(r)"
1.881  apply (blast intro!: equalityI dest: transM)
1.882  done
1.883 @@ -1139,7 +1139,7 @@
1.884  done
1.886  lemma (in M_basic) range_abs [simp]:
1.887 -     "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
1.888 +     "[| M(r); M(z) |] ==> is_range(M,r,z) \<longleftrightarrow> z = range(r)"
1.890  apply (blast intro!: equalityI dest: transM)
1.891  done
1.892 @@ -1150,7 +1150,7 @@
1.893  done
1.895  lemma (in M_basic) field_abs [simp]:
1.896 -     "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)"
1.897 +     "[| M(r); M(z) |] ==> is_field(M,r,z) \<longleftrightarrow> z = field(r)"
1.898  by (simp add: domain_closed range_closed is_field_def field_def)
1.900  lemma (in M_basic) field_closed [intro,simp]:
1.901 @@ -1161,13 +1161,13 @@
1.902  subsubsection{*Relations, functions and application*}
1.904  lemma (in M_basic) relation_abs [simp]:
1.905 -     "M(r) ==> is_relation(M,r) <-> relation(r)"
1.906 +     "M(r) ==> is_relation(M,r) \<longleftrightarrow> relation(r)"
1.907  apply (simp add: is_relation_def relation_def)
1.908  apply (blast dest!: bspec dest: pair_components_in_M)+
1.909  done
1.911  lemma (in M_basic) function_abs [simp]:
1.912 -     "M(r) ==> is_function(M,r) <-> function(r)"
1.913 +     "M(r) ==> is_function(M,r) \<longleftrightarrow> function(r)"
1.914  apply (simp add: is_function_def function_def, safe)
1.915     apply (frule transM, assumption)
1.916    apply (blast dest: pair_components_in_M)+
1.917 @@ -1178,28 +1178,28 @@
1.920  lemma (in M_basic) apply_abs [simp]:
1.921 -     "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> fx = y"
1.922 +     "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) \<longleftrightarrow> fx = y"
1.923  apply (simp add: fun_apply_def apply_def, blast)
1.924  done
1.926  lemma (in M_basic) typed_function_abs [simp]:
1.927 -     "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
1.928 +     "[| M(A); M(f) |] ==> typed_function(M,A,B,f) \<longleftrightarrow> f \<in> A -> B"
1.929  apply (auto simp add: typed_function_def relation_def Pi_iff)
1.930  apply (blast dest: pair_components_in_M)+
1.931  done
1.933  lemma (in M_basic) injection_abs [simp]:
1.934 -     "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
1.935 +     "[| M(A); M(f) |] ==> injection(M,A,B,f) \<longleftrightarrow> f \<in> inj(A,B)"
1.936  apply (simp add: injection_def apply_iff inj_def apply_closed)
1.937  apply (blast dest: transM [of _ A])
1.938  done
1.940  lemma (in M_basic) surjection_abs [simp]:
1.941 -     "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
1.942 +     "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) \<longleftrightarrow> f \<in> surj(A,B)"
1.943  by (simp add: surjection_def surj_def)
1.945  lemma (in M_basic) bijection_abs [simp]:
1.946 -     "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
1.947 +     "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) \<longleftrightarrow> f \<in> bij(A,B)"
1.948  by (simp add: bijection_def bij_def)
1.951 @@ -1224,7 +1224,7 @@
1.952  done
1.954  lemma (in M_basic) composition_abs [simp]:
1.955 -     "[| M(r); M(s); M(t) |] ==> composition(M,r,s,t) <-> t = r O s"
1.956 +     "[| M(r); M(s); M(t) |] ==> composition(M,r,s,t) \<longleftrightarrow> t = r O s"
1.957  apply safe
1.958   txt{*Proving @{term "composition(M, r, s, r O s)"}*}
1.959   prefer 2
1.960 @@ -1246,7 +1246,7 @@
1.962  lemma (in M_basic) restriction_abs [simp]:
1.963       "[| M(f); M(A); M(z) |]
1.964 -      ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
1.965 +      ==> restriction(M,f,A,z) \<longleftrightarrow> z = restrict(f,A)"
1.966  apply (simp add: ball_iff_equiv restriction_def restrict_def)
1.967  apply (blast intro!: equalityI dest: transM)
1.968  done
1.969 @@ -1263,17 +1263,17 @@
1.970  done
1.972  lemma (in M_basic) Inter_abs [simp]:
1.973 -     "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
1.974 +     "[| M(A); M(z) |] ==> big_inter(M,A,z) \<longleftrightarrow> z = \<Inter>(A)"
1.975  apply (simp add: big_inter_def Inter_def)
1.976  apply (blast intro!: equalityI dest: transM)
1.977  done
1.979  lemma (in M_basic) Inter_closed [intro,simp]:
1.980 -     "M(A) ==> M(Inter(A))"
1.981 +     "M(A) ==> M(\<Inter>(A))"
1.982  by (insert Inter_separation, simp add: Inter_def)
1.984  lemma (in M_basic) Int_closed [intro,simp]:
1.985 -     "[| M(A); M(B) |] ==> M(A Int B)"
1.986 +     "[| M(A); M(B) |] ==> M(A \<inter> B)"
1.987  apply (subgoal_tac "M({A,B})")
1.988  apply (frule Inter_closed, force+)
1.989  done
1.990 @@ -1291,7 +1291,7 @@
1.992  (*???equalities*)
1.993  lemma Collect_Un_Collect_eq:
1.994 -     "Collect(A,P) Un Collect(A,Q) = Collect(A, %x. P(x) | Q(x))"
1.995 +     "Collect(A,P) \<union> Collect(A,Q) = Collect(A, %x. P(x) | Q(x))"
1.996  by blast
1.998  lemma Diff_Collect_eq:
1.999 @@ -1299,7 +1299,7 @@
1.1000  by blast
1.1002  lemma (in M_trivial) Collect_rall_eq:
1.1003 -     "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y --> P(x,y)) =
1.1004 +     "M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y \<longrightarrow> P(x,y)) =
1.1005                 (if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
1.1006  apply simp
1.1007  apply (blast intro!: equalityI dest: transM)
1.1008 @@ -1317,7 +1317,7 @@
1.1010  lemma (in M_basic) separation_imp:
1.1011       "[|separation(M,P); separation(M,Q)|]
1.1012 -      ==> separation(M, \<lambda>z. P(z) --> Q(z))"
1.1013 +      ==> separation(M, \<lambda>z. P(z) \<longrightarrow> Q(z))"
1.1014  by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric])
1.1016  text{*This result is a hint of how little can be done without the Reflection
1.1017 @@ -1326,7 +1326,7 @@
1.1018  lemma (in M_basic) separation_rall:
1.1019       "[|M(Y); \<forall>y[M]. separation(M, \<lambda>x. P(x,y));
1.1020          \<forall>z[M]. strong_replacement(M, \<lambda>x y. y = {u \<in> z . P(u,x)})|]
1.1021 -      ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y --> P(x,y))"
1.1022 +      ==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y \<longrightarrow> P(x,y))"
1.1023  apply (simp del: separation_closed rall_abs
1.1025  apply (blast intro!: Inter_closed RepFun_closed dest: transM)
1.1026 @@ -1338,7 +1338,7 @@
1.1027  text{*The assumption @{term "M(A->B)"} is unusual, but essential: in
1.1028  all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
1.1029  lemma (in M_basic) is_funspace_abs [simp]:
1.1030 -     "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B";
1.1031 +     "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) \<longleftrightarrow> F = A->B";
1.1033  apply (rule iffI)
1.1034   prefer 2 apply blast
1.1035 @@ -1392,20 +1392,20 @@
1.1036                        (~number1(M,a) & z=b)"
1.1038  lemma (in M_trivial) bool_of_o_abs [simp]:
1.1039 -     "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)"
1.1040 +     "M(z) ==> is_bool_of_o(M,P,z) \<longleftrightarrow> z = bool_of_o(P)"
1.1041  by (simp add: is_bool_of_o_def bool_of_o_def)
1.1044  lemma (in M_trivial) not_abs [simp]:
1.1045 -     "[| M(a); M(z)|] ==> is_not(M,a,z) <-> z = not(a)"
1.1046 +     "[| M(a); M(z)|] ==> is_not(M,a,z) \<longleftrightarrow> z = not(a)"
1.1047  by (simp add: Bool.not_def cond_def is_not_def)
1.1049  lemma (in M_trivial) and_abs [simp]:
1.1050 -     "[| M(a); M(b); M(z)|] ==> is_and(M,a,b,z) <-> z = a and b"
1.1051 +     "[| M(a); M(b); M(z)|] ==> is_and(M,a,b,z) \<longleftrightarrow> z = a and b"
1.1052  by (simp add: Bool.and_def cond_def is_and_def)
1.1054  lemma (in M_trivial) or_abs [simp]:
1.1055 -     "[| M(a); M(b); M(z)|] ==> is_or(M,a,b,z) <-> z = a or b"
1.1056 +     "[| M(a); M(b); M(z)|] ==> is_or(M,a,b,z) \<longleftrightarrow> z = a or b"
1.1057  by (simp add: Bool.or_def cond_def is_or_def)
1.1060 @@ -1442,14 +1442,14 @@
1.1061  lemma (in M_trivial) Nil_in_M [intro,simp]: "M(Nil)"
1.1064 -lemma (in M_trivial) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
1.1065 +lemma (in M_trivial) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) \<longleftrightarrow> (Z = Nil)"
1.1066  by (simp add: is_Nil_def Nil_def)
1.1068 -lemma (in M_trivial) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
1.1069 +lemma (in M_trivial) Cons_in_M_iff [iff]: "M(Cons(a,l)) \<longleftrightarrow> M(a) & M(l)"
1.1072  lemma (in M_trivial) Cons_abs [simp]:
1.1073 -     "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
1.1074 +     "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) \<longleftrightarrow> (Z = Cons(a,l))"
1.1075  by (simp add: is_Cons_def Cons_def)
1.1078 @@ -1471,8 +1471,8 @@
1.1079    is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o" where
1.1080      --{*Returns 0 for non-lists*}
1.1081      "is_list_case(M, a, is_b, xs, z) ==
1.1082 -       (is_Nil(M,xs) --> z=a) &
1.1083 -       (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) &
1.1084 +       (is_Nil(M,xs) \<longrightarrow> z=a) &
1.1085 +       (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) \<longrightarrow> is_b(x,l,z)) &
1.1086         (is_quasilist(M,xs) | empty(M,z))"
1.1088  definition
1.1089 @@ -1490,7 +1490,7 @@
1.1090       --{* @{term "hd([]) = 0"} no constraints if not a list.
1.1091            Avoiding implication prevents the simplifier's looping.*}
1.1092      "is_hd(M,xs,H) ==
1.1093 -       (is_Nil(M,xs) --> empty(M,H)) &
1.1094 +       (is_Nil(M,xs) \<longrightarrow> empty(M,H)) &
1.1095         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
1.1096         (is_quasilist(M,xs) | empty(M,H))"
1.1098 @@ -1498,7 +1498,7 @@
1.1099    is_tl :: "[i=>o,i,i] => o" where
1.1101      "is_tl(M,xs,T) ==
1.1102 -       (is_Nil(M,xs) --> T=xs) &
1.1103 +       (is_Nil(M,xs) \<longrightarrow> T=xs) &
1.1104         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
1.1105         (is_quasilist(M,xs) | empty(M,T))"
1.1107 @@ -1536,12 +1536,12 @@
1.1108  done
1.1110  lemma (in M_trivial) quasilist_abs [simp]:
1.1111 -     "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
1.1112 +     "M(z) ==> is_quasilist(M,z) \<longleftrightarrow> quasilist(z)"
1.1113  by (auto simp add: is_quasilist_def quasilist_def)
1.1115  lemma (in M_trivial) list_case_abs [simp]:
1.1116       "[| relation2(M,is_b,b); M(k); M(z) |]
1.1117 -      ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
1.1118 +      ==> is_list_case(M,a,is_b,k,z) \<longleftrightarrow> z = list_case'(a,b,k)"
1.1119  apply (case_tac "quasilist(k)")
1.1120   prefer 2
1.1121   apply (simp add: is_list_case_def non_list_case)
1.1122 @@ -1554,15 +1554,15 @@
1.1124  subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
1.1126 -lemma (in M_trivial) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
1.1127 +lemma (in M_trivial) is_hd_Nil: "is_hd(M,[],Z) \<longleftrightarrow> empty(M,Z)"
1.1130  lemma (in M_trivial) is_hd_Cons:
1.1131 -     "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
1.1132 +     "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) \<longleftrightarrow> Z = a"
1.1133  by (force simp add: is_hd_def)
1.1135  lemma (in M_trivial) hd_abs [simp]:
1.1136 -     "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
1.1137 +     "[|M(x); M(y)|] ==> is_hd(M,x,y) \<longleftrightarrow> y = hd'(x)"
1.1139  apply (intro impI conjI)
1.1140   prefer 2 apply (force simp add: is_hd_def)
1.1141 @@ -1570,15 +1570,15 @@
1.1142  apply (elim disjE exE, auto)
1.1143  done
1.1145 -lemma (in M_trivial) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
1.1146 +lemma (in M_trivial) is_tl_Nil: "is_tl(M,[],Z) \<longleftrightarrow> Z = []"