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.53  by (simp add: pred_def)
    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.71  by (simp add: mono_map_def)
    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.88  by (simp add: ord_iso_def)
    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.100  by (simp add: ord_iso_def)
   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.106  by (simp add: ord_iso_def)
   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.120  apply (simp add: ord_iso_def)
   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.218  apply (simp add: pred_subset)
   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: