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.4  
     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.9  
    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.14  
    1.15  definition
    1.16    pair :: "[i=>o,i,i,i] => o" where
    1.17 @@ -28,7 +28,7 @@
    1.18  
    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.23  
    1.24  definition
    1.25    is_cons :: "[i=>o,i,i,i] => o" where
    1.26 @@ -52,38 +52,38 @@
    1.27  
    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.32  
    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.37  
    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.42  
    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.47  
    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.52  
    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.57  
    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.65  
    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.71  
    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.81  
    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.87  
    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.93  
    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.99  
   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.108  
   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.117  
   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.124  
   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.133  
   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.139  
   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.154  
   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.161  
   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.170  
   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.175  
   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.181  
   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.189  
   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.198  
   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.204  
   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.216  
   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.221  
   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.228  
   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.233  
   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.239  
   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.245  
   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.252  
   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.258  
   1.259  
   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.267  
   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.276  
   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.285  
   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.293  
   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.301  
   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.307  
   1.308  
   1.309  subsection{*A trivial consistency proof for $V_\omega$ *}
   1.310 @@ -348,22 +348,22 @@
   1.311  done
   1.312  
   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.317  
   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.322  
   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.329  by (simp add: separation_def)
   1.330  
   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.336  by (simp add: univalent_def)
   1.337  
   1.338  lemma univalent_triv [intro,simp]:
   1.339 @@ -376,8 +376,8 @@
   1.340  
   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.348  by (simp add: strong_replacement_def)
   1.349  
   1.350 @@ -457,13 +457,13 @@
   1.351  subsection{*Lemmas Needed to Reduce Some Set Constructions to Instances
   1.352        of Separation*}
   1.353  
   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.359  
   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.367  
   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.372  by (simp add: replacement_def)
   1.373  
   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.378  by (simp add: strong_replacement_def)
   1.379  
   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.383  by (simp add: separation_def)
   1.384  
   1.385  
   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.397  
   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.403  
   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.409  
   1.410  
   1.411  subsection{*Introducing a Transitive Class Model*}
   1.412 @@ -540,65 +540,65 @@
   1.413  by (blast intro: transM)
   1.414  
   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.419  
   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.424  
   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.431  
   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.441  
   1.442  
   1.443  subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*}
   1.444  
   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.448  apply (simp add: empty_def)
   1.449  apply (blast intro: transM)
   1.450  done
   1.451  
   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.455  apply (simp add: subset_def)
   1.456  apply (blast intro: transM)
   1.457  done
   1.458  
   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.462  apply (simp add: upair_def)
   1.463  apply (blast intro: transM)
   1.464  done
   1.465  
   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.472  
   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.477  
   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.484  
   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.488  by (simp add: ZF.Pair_def)
   1.489  
   1.490  lemma (in M_trivial) pair_components_in_M:
   1.491 @@ -608,7 +608,7 @@
   1.492  done
   1.493  
   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.497  apply (simp add: cartprod_def)
   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.502  
   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.506  apply (simp add: union_def)
   1.507  apply (blast intro: transM)
   1.508  done
   1.509  
   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.513  apply (simp add: inter_def)
   1.514  apply (blast intro: transM)
   1.515  done
   1.516  
   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.520  apply (simp add: setdiff_def)
   1.521  apply (blast intro: transM)
   1.522  done
   1.523  
   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.527  apply (simp add: big_union_def)
   1.528  apply (blast intro!: equalityI dest: transM)
   1.529  done
   1.530  
   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.535  
   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.540  
   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.544  
   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.549  
   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.554  
   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.558  apply (simp add: succ_def)
   1.559  apply (blast intro: transM)
   1.560  done
   1.561 @@ -678,11 +678,11 @@
   1.562  done
   1.563  
   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.568  
   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.572  apply (simp add: is_Collect_def)
   1.573  apply (blast intro!: equalityI dest: transM)
   1.574  done
   1.575 @@ -703,16 +703,16 @@
   1.576  
   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.585  by (simp add: is_Replace_def)
   1.586  
   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.597  
   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.604  apply (simp add: is_Replace_def)
   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.611  
   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.628  
   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.636  apply (simp add: lam_def)
   1.637  apply (blast intro: RepFun_closed2 dest: transM)
   1.638  done
   1.639  
   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.649 -apply (simp add: lam_def) 
   1.650 -apply (rule iffI) 
   1.651 - apply (blast dest: transM) 
   1.652 -apply (auto simp add: transM [of _ A]) 
   1.653 +apply (simp add: lam_def)
   1.654 +apply (rule iffI)
   1.655 + apply (blast dest: transM)
   1.656 +apply (auto simp add: transM [of _ A])
   1.657  done
   1.658  
   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.666  by (simp add: is_lambda_def)
   1.667  
   1.668  lemma (in M_trivial) image_abs [simp]:
   1.669 -     "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   1.670 +     "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) \<longleftrightarrow> z = r``A"
   1.671  apply (simp add: image_def)
   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.680  apply (simp add: powerset_def)
   1.681  apply (blast dest: transM)
   1.682  done
   1.683 @@ -847,12 +847,12 @@
   1.684  done
   1.685  
   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.690  
   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.706  by (simp add: is_nat_case_def)
   1.707  
   1.708  
   1.709 @@ -880,22 +880,22 @@
   1.710  by (blast dest: ltD intro: transM)
   1.711  
   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.716  
   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.721  
   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.726  apply (simp add: Ord_0_lt_iff)
   1.727  apply (simp add: lt_def, blast)
   1.728  done
   1.729  
   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.738  
   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.742  apply (simp add: finite_ordinal_def)
   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.747  
   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.751  apply (simp add: omega_def)
   1.752  apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   1.753  done
   1.754  
   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.758  by (simp add: number1_def)
   1.759  
   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.763  by (simp add: number2_def)
   1.764  
   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.768  by (simp add: number3_def)
   1.769  
   1.770  text{*Kunen continued to 20...*}
   1.771 @@ -965,7 +965,7 @@
   1.772  
   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.782  
   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.788  apply (simp add: powerset_def)
   1.789 @@ -1017,8 +1017,8 @@
   1.790  
   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.819  by (simp add: sum_def)
   1.820  
   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.825  
   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.829  by (simp add: Inl_def)
   1.830  
   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.835  
   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.839  by (simp add: Inr_def)
   1.840  
   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.845  
   1.846  
   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.858  
   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.862  apply (simp add: is_converse_def)
   1.863  apply (rule iffI)
   1.864   prefer 2 apply blast
   1.865 @@ -1114,7 +1114,7 @@
   1.866  done
   1.867  
   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.871  apply (simp add: pre_image_def)
   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.876  
   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.880  apply (simp add: is_domain_def)
   1.881  apply (blast intro!: equalityI dest: transM)
   1.882  done
   1.883 @@ -1139,7 +1139,7 @@
   1.884  done
   1.885  
   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.889  apply (simp add: is_range_def)
   1.890  apply (blast intro!: equalityI dest: transM)
   1.891  done
   1.892 @@ -1150,7 +1150,7 @@
   1.893  done
   1.894  
   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.899  
   1.900  lemma (in M_basic) field_closed [intro,simp]:
   1.901 @@ -1161,13 +1161,13 @@
   1.902  subsubsection{*Relations, functions and application*}
   1.903  
   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.910  
   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.918  by (simp add: apply_def)
   1.919  
   1.920  lemma (in M_basic) apply_abs [simp]:
   1.921 -     "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
   1.922 +     "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) \<longleftrightarrow> f`x = y"
   1.923  apply (simp add: fun_apply_def apply_def, blast)
   1.924  done
   1.925  
   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.932  
   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.939  
   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.944  
   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.949  
   1.950  
   1.951 @@ -1224,7 +1224,7 @@
   1.952  done
   1.953  
   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.961  
   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.971  
   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.978  
   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.983  
   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.991  
   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.997  
   1.998  lemma Diff_Collect_eq:
   1.999 @@ -1299,7 +1299,7 @@
  1.1000  by blast
  1.1001  
  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.1009  
  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.1015  
  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.1024           add: separation_iff Collect_rall_eq)
  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.1032  apply (simp add: is_funspace_def)
  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.1037  
  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.1042  
  1.1043  
  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.1048  
  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.1053  
  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.1058  
  1.1059  
  1.1060 @@ -1442,14 +1442,14 @@
  1.1061  lemma (in M_trivial) Nil_in_M [intro,simp]: "M(Nil)"
  1.1062  by (simp add: Nil_def)
  1.1063  
  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.1067  
  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.1070  by (simp add: Cons_def)
  1.1071  
  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.1076  
  1.1077  
  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.1087  
  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.1097  
  1.1098 @@ -1498,7 +1498,7 @@
  1.1099    is_tl :: "[i=>o,i,i] => o" where
  1.1100       --{* @{term "tl([]) = []"}; see comments about @{term is_hd}*}
  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.1106  
  1.1107 @@ -1536,12 +1536,12 @@
  1.1108  done
  1.1109  
  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.1114  
  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.1123  
  1.1124  subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
  1.1125  
  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.1128  by (simp add: is_hd_def)
  1.1129  
  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.1134  
  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.1138  apply (simp add: hd'_def)
  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.1144  
  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 = []"
  1.1147  by (simp add: is_tl_def)
  1.1148  
  1.1149  lemma (in M_trivial) is_tl_Cons:
  1.1150 -     "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
  1.1151 +     "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) \<longleftrightarrow> Z = l"
  1.1152  by (force simp add: is_tl_def)
  1.1153  
  1.1154  lemma (in M_trivial) tl_abs [simp]:
  1.1155 -     "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
  1.1156 +     "[|M(x); M(y)|] ==> is_tl(M,x,y) \<longleftrightarrow> y = tl'(x)"
  1.1157  apply (simp add: tl'_def)
  1.1158  apply (intro impI conjI)
  1.1159   prefer 2 apply (force simp add: is_tl_def)