src/ZF/Order.thy
 changeset 46953 2b6e55924af3 parent 46821 ff6b0c1087f2 child 58871 c399ae4b836f
```     1.1 --- a/src/ZF/Order.thy	Thu Mar 15 15:54:22 2012 +0000
1.2 +++ b/src/ZF/Order.thy	Thu Mar 15 16:35:02 2012 +0000
1.3 @@ -46,16 +46,16 @@
1.4  definition
1.5    mono_map :: "[i,i,i,i]=>i"            (*Order-preserving maps*)  where
1.6     "mono_map(A,r,B,s) ==
1.7 -              {f: A->B. \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longrightarrow> <f`x,f`y>:s}"
1.8 +              {f \<in> A->B. \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longrightarrow> <f`x,f`y>:s}"
1.9
1.10  definition
1.11    ord_iso  :: "[i,i,i,i]=>i"            (*Order isomorphisms*)  where
1.12     "ord_iso(A,r,B,s) ==
1.13 -              {f: bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longleftrightarrow> <f`x,f`y>:s}"
1.14 +              {f \<in> bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longleftrightarrow> <f`x,f`y>:s}"
1.15
1.16  definition
1.17    pred     :: "[i,i,i]=>i"              (*Set of predecessors*)  where
1.18 -   "pred(A,x,r) == {y:A. <y,x>:r}"
1.19 +   "pred(A,x,r) == {y \<in> A. <y,x>:r}"
1.20
1.21  definition
1.22    ord_iso_map :: "[i,i,i,i]=>i"         (*Construction for linearity theorem*)  where
1.23 @@ -64,7 +64,7 @@
1.24
1.25  definition
1.26    first :: "[i, i, i] => o"  where
1.27 -    "first(u, X, R) == u:X & (\<forall>v\<in>X. v\<noteq>u \<longrightarrow> <u,v> \<in> R)"
1.28 +    "first(u, X, R) == u \<in> X & (\<forall>v\<in>X. v\<noteq>u \<longrightarrow> <u,v> \<in> R)"
1.29
1.30
1.31  notation (xsymbols)
1.32 @@ -78,7 +78,7 @@
1.33  by (unfold part_ord_def irrefl_def trans_on_def asym_def, blast)
1.34
1.35  lemma linearE:
1.36 -    "[| linear(A,r);  x:A;  y:A;
1.37 +    "[| linear(A,r);  x \<in> A;  y \<in> A;
1.38          <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |]
1.39       ==> P"
1.40  by (simp add: linear_def, blast)
1.41 @@ -107,12 +107,12 @@
1.42
1.43  (** Derived rules for pred(A,x,r) **)
1.44
1.45 -lemma pred_iff: "y \<in> pred(A,x,r) \<longleftrightarrow> <y,x>:r & y:A"
1.46 +lemma pred_iff: "y \<in> pred(A,x,r) \<longleftrightarrow> <y,x>:r & y \<in> A"
1.47  by (unfold pred_def, blast)
1.48
1.49  lemmas predI = conjI [THEN pred_iff [THEN iffD2]]
1.50
1.51 -lemma predE: "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P"
1.52 +lemma predE: "[| y \<in> pred(A,x,r);  [| y \<in> A; <y,x>:r |] ==> P |] ==> P"
1.54
1.55  lemma pred_subset_under: "pred(A,x,r) \<subseteq> r -`` {x}"
1.56 @@ -126,7 +126,7 @@
1.57  by (simp add: pred_def, blast)
1.58
1.59  lemma trans_pred_pred_eq:
1.60 -    "[| trans[A](r);  <y,x>:r;  x:A;  y:A |]
1.61 +    "[| trans[A](r);  <y,x>:r;  x \<in> A;  y \<in> A |]
1.62       ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"
1.63  by (unfold trans_on_def pred_def, blast)
1.64
1.65 @@ -244,39 +244,39 @@
1.66
1.67  (** Order-preserving (monotone) maps **)
1.68
1.69 -lemma mono_map_is_fun: "f: mono_map(A,r,B,s) ==> f: A->B"
1.70 +lemma mono_map_is_fun: "f \<in> mono_map(A,r,B,s) ==> f \<in> A->B"
1.72
1.73  lemma mono_map_is_inj:
1.74 -    "[| linear(A,r);  wf[B](s);  f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"
1.75 +    "[| linear(A,r);  wf[B](s);  f \<in> mono_map(A,r,B,s) |] ==> f \<in> inj(A,B)"
1.76  apply (unfold mono_map_def inj_def, clarify)
1.77  apply (erule_tac x=w and y=x in linearE, assumption+)
1.78  apply (force intro: apply_type dest: wf_on_not_refl)+
1.79  done
1.80
1.81  lemma ord_isoI:
1.82 -    "[| f: bij(A, B);
1.83 -        !!x y. [| x:A; y:A |] ==> <x, y> \<in> r \<longleftrightarrow> <f`x, f`y> \<in> s |]
1.84 -     ==> f: ord_iso(A,r,B,s)"
1.85 +    "[| f \<in> bij(A, B);
1.86 +        !!x y. [| x \<in> A; y \<in> A |] ==> <x, y> \<in> r \<longleftrightarrow> <f`x, f`y> \<in> s |]
1.87 +     ==> f \<in> ord_iso(A,r,B,s)"
1.89
1.90  lemma ord_iso_is_mono_map:
1.91 -    "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)"
1.92 +    "f \<in> ord_iso(A,r,B,s) ==> f \<in> mono_map(A,r,B,s)"
1.93  apply (simp add: ord_iso_def mono_map_def)
1.94  apply (blast dest!: bij_is_fun)
1.95  done
1.96
1.97  lemma ord_iso_is_bij:
1.98 -    "f: ord_iso(A,r,B,s) ==> f: bij(A,B)"
1.99 +    "f \<in> ord_iso(A,r,B,s) ==> f \<in> bij(A,B)"
1.101
1.102  (*Needed?  But ord_iso_converse is!*)
1.103  lemma ord_iso_apply:
1.104 -    "[| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> <f`x, f`y> \<in> s"
1.105 +    "[| f \<in> ord_iso(A,r,B,s);  <x,y>: r;  x \<in> A;  y \<in> A |] ==> <f`x, f`y> \<in> s"
1.107
1.108  lemma ord_iso_converse:
1.109 -    "[| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |]
1.110 +    "[| f \<in> ord_iso(A,r,B,s);  <x,y>: s;  x \<in> B;  y \<in> B |]
1.111       ==> <converse(f) ` x, converse(f) ` y> \<in> r"
1.112  apply (simp add: ord_iso_def, clarify)
1.113  apply (erule bspec [THEN bspec, THEN iffD2])
1.114 @@ -292,7 +292,7 @@
1.115  by (rule id_bij [THEN ord_isoI], simp)
1.116
1.117  (*Symmetry of similarity*)
1.118 -lemma ord_iso_sym: "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"
1.119 +lemma ord_iso_sym: "f \<in> ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"
1.121  apply (auto simp add: right_inverse_bij bij_converse_bij
1.122                        bij_is_fun [THEN apply_funtype])
1.123 @@ -300,7 +300,7 @@
1.124
1.125  (*Transitivity of similarity*)
1.126  lemma mono_map_trans:
1.127 -    "[| g: mono_map(A,r,B,s);  f: mono_map(B,s,C,t) |]
1.128 +    "[| g \<in> mono_map(A,r,B,s);  f \<in> mono_map(B,s,C,t) |]
1.129       ==> (f O g): mono_map(A,r,C,t)"
1.130  apply (unfold mono_map_def)
1.131  apply (auto simp add: comp_fun)
1.132 @@ -308,7 +308,7 @@
1.133
1.134  (*Transitivity of similarity: the order-isomorphism relation*)
1.135  lemma ord_iso_trans:
1.136 -    "[| g: ord_iso(A,r,B,s);  f: ord_iso(B,s,C,t) |]
1.137 +    "[| g \<in> ord_iso(A,r,B,s);  f \<in> ord_iso(B,s,C,t) |]
1.138       ==> (f O g): ord_iso(A,r,C,t)"
1.139  apply (unfold ord_iso_def, clarify)
1.140  apply (frule bij_is_fun [of f])
1.141 @@ -319,8 +319,8 @@
1.142  (** Two monotone maps can make an order-isomorphism **)
1.143
1.144  lemma mono_ord_isoI:
1.145 -    "[| f: mono_map(A,r,B,s);  g: mono_map(B,s,A,r);
1.146 -        f O g = id(B);  g O f = id(A) |] ==> f: ord_iso(A,r,B,s)"
1.147 +    "[| f \<in> mono_map(A,r,B,s);  g \<in> mono_map(B,s,A,r);
1.148 +        f O g = id(B);  g O f = id(A) |] ==> f \<in> ord_iso(A,r,B,s)"
1.149  apply (simp add: ord_iso_def mono_map_def, safe)
1.150  apply (intro fg_imp_bijective, auto)
1.151  apply (subgoal_tac "<g` (f`x), g` (f`y) > \<in> r")
1.152 @@ -330,8 +330,8 @@
1.153
1.154  lemma well_ord_mono_ord_isoI:
1.155       "[| well_ord(A,r);  well_ord(B,s);
1.156 -         f: mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r) |]
1.157 -      ==> f: ord_iso(A,r,B,s)"
1.158 +         f \<in> mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r) |]
1.159 +      ==> f \<in> ord_iso(A,r,B,s)"
1.160  apply (intro mono_ord_isoI, auto)
1.161  apply (frule mono_map_is_fun [THEN fun_is_rel])
1.162  apply (erule converse_converse [THEN subst], rule left_comp_inverse)
1.163 @@ -343,13 +343,13 @@
1.164  (** Order-isomorphisms preserve the ordering's properties **)
1.165
1.166  lemma part_ord_ord_iso:
1.167 -    "[| part_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)"
1.168 +    "[| part_ord(B,s);  f \<in> ord_iso(A,r,B,s) |] ==> part_ord(A,r)"
1.169  apply (simp add: part_ord_def irrefl_def trans_on_def ord_iso_def)
1.170  apply (fast intro: bij_is_fun [THEN apply_type])
1.171  done
1.172
1.173  lemma linear_ord_iso:
1.174 -    "[| linear(B,s);  f: ord_iso(A,r,B,s) |] ==> linear(A,r)"
1.175 +    "[| linear(B,s);  f \<in> ord_iso(A,r,B,s) |] ==> linear(A,r)"
1.176  apply (simp add: linear_def ord_iso_def, safe)
1.177  apply (drule_tac x1 = "f`x" and x = "f`y" in bspec [THEN bspec])
1.178  apply (safe elim!: bij_is_fun [THEN apply_type])
1.179 @@ -358,15 +358,15 @@
1.180  done
1.181
1.182  lemma wf_on_ord_iso:
1.183 -    "[| wf[B](s);  f: ord_iso(A,r,B,s) |] ==> wf[A](r)"
1.184 +    "[| wf[B](s);  f \<in> ord_iso(A,r,B,s) |] ==> wf[A](r)"
1.185  apply (simp add: wf_on_def wf_def ord_iso_def, safe)
1.186 -apply (drule_tac x = "{f`z. z:Z \<inter> A}" in spec)
1.187 +apply (drule_tac x = "{f`z. z \<in> Z \<inter> A}" in spec)
1.188  apply (safe intro!: equalityI)
1.189  apply (blast dest!: equalityD1 intro: bij_is_fun [THEN apply_type])+
1.190  done
1.191
1.192  lemma well_ord_ord_iso:
1.193 -    "[| well_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)"
1.194 +    "[| well_ord(B,s);  f \<in> ord_iso(A,r,B,s) |] ==> well_ord(A,r)"
1.195  apply (unfold well_ord_def tot_ord_def)
1.196  apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso)
1.197  done
1.198 @@ -377,7 +377,7 @@
1.199  (*Inductive argument for Kunen's Lemma 6.1, etc.
1.200    Simple proof from Halmos, page 72*)
1.201  lemma well_ord_iso_subset_lemma:
1.202 -     "[| well_ord(A,r);  f: ord_iso(A,r, A',r);  A'<= A;  y: A |]
1.203 +     "[| well_ord(A,r);  f \<in> ord_iso(A,r, A',r);  A'<= A;  y \<in> A |]
1.204        ==> ~ <f`y, y>: r"
1.205  apply (simp add: well_ord_def ord_iso_def)
1.206  apply (elim conjE CollectE)
1.207 @@ -385,10 +385,10 @@
1.208  apply (blast dest: bij_is_fun [THEN apply_type])
1.209  done
1.210
1.211 -(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
1.212 +(*Kunen's Lemma 6.1 \<in> there's no order-isomorphism to an initial segment
1.213                       of a well-ordering*)
1.214  lemma well_ord_iso_predE:
1.215 -     "[| well_ord(A,r);  f \<in> ord_iso(A, r, pred(A,x,r), r);  x:A |] ==> P"
1.216 +     "[| well_ord(A,r);  f \<in> ord_iso(A, r, pred(A,x,r), r);  x \<in> A |] ==> P"
1.217  apply (insert well_ord_iso_subset_lemma [of A r f "pred(A,x,r)" x])
1.219  (*Now we know  f`x < x *)
1.220 @@ -400,7 +400,7 @@
1.221  (*Simple consequence of Lemma 6.1*)
1.222  lemma well_ord_iso_pred_eq:
1.223       "[| well_ord(A,r);  f \<in> ord_iso(pred(A,a,r), r, pred(A,c,r), r);
1.224 -         a:A;  c:A |] ==> a=c"
1.225 +         a \<in> A;  c \<in> A |] ==> a=c"
1.226  apply (frule well_ord_is_trans_on)
1.227  apply (frule well_ord_is_linear)
1.228  apply (erule_tac x=a and y=c in linearE, assumption+)
1.229 @@ -413,7 +413,7 @@
1.230
1.231  (*Does not assume r is a wellordering!*)
1.232  lemma ord_iso_image_pred:
1.233 -     "[|f \<in> ord_iso(A,r,B,s);  a:A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)"
1.234 +     "[|f \<in> ord_iso(A,r,B,s);  a \<in> A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)"
1.235  apply (unfold ord_iso_def pred_def)
1.236  apply (erule CollectE)
1.237  apply (simp (no_asm_simp) add: image_fun [OF bij_is_fun Collect_subset])
1.238 @@ -434,7 +434,7 @@
1.239  (*But in use, A and B may themselves be initial segments.  Then use
1.240    trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
1.241  lemma ord_iso_restrict_pred:
1.242 -   "[| f \<in> ord_iso(A,r,B,s);   a:A |]
1.243 +   "[| f \<in> ord_iso(A,r,B,s);   a \<in> A |]
1.244      ==> restrict(f, pred(A,a,r)) \<in> ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"
1.245  apply (simp add: ord_iso_image_pred [symmetric])
1.246  apply (blast intro: ord_iso_restrict_image elim: predE)
1.247 @@ -445,7 +445,7 @@
1.248       "[| well_ord(A,r);  well_ord(B,s);  <a,c>: r;
1.249           f \<in> ord_iso(pred(A,a,r), r, pred(B,b,s), s);
1.250           g \<in> ord_iso(pred(A,c,r), r, pred(B,d,s), s);
1.251 -         a:A;  c:A;  b:B;  d:B |] ==> <b,d>: s"
1.252 +         a \<in> A;  c \<in> A;  b \<in> B;  d \<in> B |] ==> <b,d>: s"
1.253  apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], (erule asm_rl predI predE)+)
1.254  apply (subgoal_tac "b = g`a")
1.255  apply (simp (no_asm_simp))
1.256 @@ -458,7 +458,7 @@
1.257  (*See Halmos, page 72*)
1.258  lemma well_ord_iso_unique_lemma:
1.259       "[| well_ord(A,r);
1.260 -         f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |]
1.261 +         f \<in> ord_iso(A,r, B,s);  g \<in> ord_iso(A,r, B,s);  y \<in> A |]
1.262        ==> ~ <g`y, f`y> \<in> s"
1.263  apply (frule well_ord_iso_subset_lemma)
1.264  apply (rule_tac f = "converse (f) " and g = g in ord_iso_trans)
1.265 @@ -476,7 +476,7 @@
1.266
1.267  (*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
1.268  lemma well_ord_iso_unique: "[| well_ord(A,r);
1.269 -         f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g"
1.270 +         f \<in> ord_iso(A,r, B,s);  g \<in> ord_iso(A,r, B,s) |] ==> f = g"
1.271  apply (rule fun_extension)
1.272  apply (erule ord_iso_is_bij [THEN bij_is_fun])+
1.273  apply (subgoal_tac "f`x \<in> B & g`x \<in> B & linear(B,s)")
1.274 @@ -522,7 +522,7 @@
1.275  apply (unfold mono_map_def)
1.276  apply (simp (no_asm_simp) add: ord_iso_map_fun)
1.277  apply safe
1.278 -apply (subgoal_tac "x:A & ya:A & y:B & yb:B")
1.279 +apply (subgoal_tac "x \<in> A & ya:A & y \<in> B & yb:B")
1.280   apply (simp add: apply_equality [OF _  ord_iso_map_fun])
1.281   apply (unfold ord_iso_map_def)
1.282   apply (blast intro: well_ord_iso_preserving, blast)
1.283 @@ -545,7 +545,7 @@
1.284  (*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*)
1.285  lemma domain_ord_iso_map_subset:
1.286       "[| well_ord(A,r);  well_ord(B,s);
1.287 -         a: A;  a \<notin> domain(ord_iso_map(A,r,B,s)) |]
1.288 +         a \<in> A;  a \<notin> domain(ord_iso_map(A,r,B,s)) |]
1.289        ==>  domain(ord_iso_map(A,r,B,s)) \<subseteq> pred(A, a, r)"
1.290  apply (unfold ord_iso_map_def)
1.291  apply (safe intro!: predI)
1.292 @@ -642,7 +642,7 @@
1.293  (** By Krzysztof Grabczewski.
1.294      Lemmas involving the first element of a well ordered set **)
1.295
1.296 -lemma first_is_elem: "first(b,B,r) ==> b:B"
1.297 +lemma first_is_elem: "first(b,B,r) ==> b \<in> B"
1.298  by (unfold first_def, blast)
1.299
1.300  lemma well_ord_imp_ex1_first:
```