src/ZF/Order.thy
 changeset 13140 6d97dbb189a9 parent 13119 6f7526467e5a child 13176 312bd350579b
```     1.1 --- a/src/ZF/Order.thy	Sat May 11 20:40:31 2002 +0200
1.2 +++ b/src/ZF/Order.thy	Mon May 13 09:02:13 2002 +0200
1.3 @@ -3,47 +3,717 @@
1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.5      Copyright   1994  University of Cambridge
1.6
1.7 -Orders in Zermelo-Fraenkel Set Theory
1.8 +Orders in Zermelo-Fraenkel Set Theory
1.9 +
1.10 +Results from the book "Set Theory: an Introduction to Independence Proofs"
1.11 +        by Kenneth Kunen.  Chapter 1, section 6.
1.12  *)
1.13
1.14 -Order = WF + Perm +
1.15 -consts
1.16 -  part_ord        :: [i,i]=>o           (*Strict partial ordering*)
1.17 -  linear, tot_ord :: [i,i]=>o           (*Strict total ordering*)
1.18 -  well_ord        :: [i,i]=>o           (*Well-ordering*)
1.19 -  mono_map        :: [i,i,i,i]=>i       (*Order-preserving maps*)
1.20 -  ord_iso         :: [i,i,i,i]=>i       (*Order isomorphisms*)
1.21 -  pred            :: [i,i,i]=>i		(*Set of predecessors*)
1.22 -  ord_iso_map     :: [i,i,i,i]=>i       (*Construction for linearity theorem*)
1.23 -
1.24 -defs
1.25 -  part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
1.26 -
1.27 -  linear_def   "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
1.28 -
1.29 -  tot_ord_def  "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
1.30 -
1.31 -  well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
1.32 -
1.33 -  mono_map_def "mono_map(A,r,B,s) ==
1.34 -                   {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
1.35 -
1.36 -  ord_iso_def  "ord_iso(A,r,B,s) ==
1.37 -                   {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
1.38 -
1.39 -  pred_def     "pred(A,x,r) == {y:A. <y,x>:r}"
1.40 -
1.41 -  ord_iso_map_def
1.42 -     "ord_iso_map(A,r,B,s) ==
1.43 -       UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
1.44 +theory Order = WF + Perm:
1.45
1.46  constdefs
1.47
1.48 -  first :: [i, i, i] => o
1.49 +  part_ord :: "[i,i]=>o"          	(*Strict partial ordering*)
1.50 +   "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
1.51 +
1.52 +  linear   :: "[i,i]=>o"          	(*Strict total ordering*)
1.53 +   "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
1.54 +
1.55 +  tot_ord  :: "[i,i]=>o"          	(*Strict total ordering*)
1.56 +   "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
1.57 +
1.58 +  well_ord :: "[i,i]=>o"          	(*Well-ordering*)
1.59 +   "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
1.60 +
1.61 +  mono_map :: "[i,i,i,i]=>i"      	(*Order-preserving maps*)
1.62 +   "mono_map(A,r,B,s) ==
1.63 +	      {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
1.64 +
1.65 +  ord_iso  :: "[i,i,i,i]=>i"		(*Order isomorphisms*)
1.66 +   "ord_iso(A,r,B,s) ==
1.67 +	      {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
1.68 +
1.69 +  pred     :: "[i,i,i]=>i"		(*Set of predecessors*)
1.70 +   "pred(A,x,r) == {y:A. <y,x>:r}"
1.71 +
1.72 +  ord_iso_map :: "[i,i,i,i]=>i"      	(*Construction for linearity theorem*)
1.73 +   "ord_iso_map(A,r,B,s) ==
1.74 +     UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
1.75 +
1.76 +  first :: "[i, i, i] => o"
1.77      "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
1.78
1.79 +
1.80  syntax (xsymbols)
1.81 -    ord_iso :: [i,i,i,i]=>i       ("(\\<langle>_, _\\<rangle> \\<cong>/ \\<langle>_, _\\<rangle>)" 51)
1.82 +    ord_iso :: "[i,i,i,i]=>i"      ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)
1.83 +
1.84 +
1.85 +(** Basic properties of the definitions **)
1.86 +
1.87 +(*needed?*)
1.88 +lemma part_ord_Imp_asym:
1.89 +    "part_ord(A,r) ==> asym(r Int A*A)"
1.90 +by (unfold part_ord_def irrefl_def trans_on_def asym_def, blast)
1.91 +
1.92 +lemma linearE:
1.93 +    "[| linear(A,r);  x:A;  y:A;
1.94 +        <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |]
1.95 +     ==> P"
1.96 +by (simp add: linear_def, blast)
1.97 +
1.98 +
1.99 +(** General properties of well_ord **)
1.100 +
1.101 +lemma well_ordI:
1.102 +    "[| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"
1.103 +apply (simp add: irrefl_def part_ord_def tot_ord_def
1.104 +                 trans_on_def well_ord_def wf_on_not_refl)
1.105 +apply (fast elim: linearE wf_on_asym wf_on_chain3)
1.106 +done
1.107 +
1.108 +lemma well_ord_is_wf:
1.109 +    "well_ord(A,r) ==> wf[A](r)"
1.110 +by (unfold well_ord_def, safe)
1.111 +
1.112 +lemma well_ord_is_trans_on:
1.113 +    "well_ord(A,r) ==> trans[A](r)"
1.114 +by (unfold well_ord_def tot_ord_def part_ord_def, safe)
1.115 +
1.116 +lemma well_ord_is_linear: "well_ord(A,r) ==> linear(A,r)"
1.117 +by (unfold well_ord_def tot_ord_def, blast)
1.118 +
1.119 +
1.120 +(** Derived rules for pred(A,x,r) **)
1.121 +
1.122 +lemma pred_iff: "y : pred(A,x,r) <-> <y,x>:r & y:A"
1.123 +by (unfold pred_def, blast)
1.124 +
1.125 +lemmas predI = conjI [THEN pred_iff [THEN iffD2]]
1.126 +
1.127 +lemma predE: "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P"
1.129 +
1.130 +lemma pred_subset_under: "pred(A,x,r) <= r -`` {x}"
1.131 +by (simp add: pred_def, blast)
1.132 +
1.133 +lemma pred_subset: "pred(A,x,r) <= A"
1.134 +by (simp add: pred_def, blast)
1.135 +
1.136 +lemma pred_pred_eq:
1.137 +    "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)"
1.138 +by (simp add: pred_def, blast)
1.139 +
1.140 +lemma trans_pred_pred_eq:
1.141 +    "[| trans[A](r);  <y,x>:r;  x:A;  y:A |]
1.142 +     ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"
1.143 +by (unfold trans_on_def pred_def, blast)
1.144 +
1.145 +
1.146 +(** The ordering's properties hold over all subsets of its domain
1.147 +    [including initial segments of the form pred(A,x,r) **)
1.148 +
1.149 +(*Note: a relation s such that s<=r need not be a partial ordering*)
1.150 +lemma part_ord_subset:
1.151 +    "[| part_ord(A,r);  B<=A |] ==> part_ord(B,r)"
1.152 +by (unfold part_ord_def irrefl_def trans_on_def, blast)
1.153 +
1.154 +lemma linear_subset:
1.155 +    "[| linear(A,r);  B<=A |] ==> linear(B,r)"
1.156 +by (unfold linear_def, blast)
1.157 +
1.158 +lemma tot_ord_subset:
1.159 +    "[| tot_ord(A,r);  B<=A |] ==> tot_ord(B,r)"
1.160 +apply (unfold tot_ord_def)
1.161 +apply (fast elim!: part_ord_subset linear_subset)
1.162 +done
1.163 +
1.164 +lemma well_ord_subset:
1.165 +    "[| well_ord(A,r);  B<=A |] ==> well_ord(B,r)"
1.166 +apply (unfold well_ord_def)
1.167 +apply (fast elim!: tot_ord_subset wf_on_subset_A)
1.168 +done
1.169 +
1.170 +
1.171 +(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
1.172 +
1.173 +lemma irrefl_Int_iff: "irrefl(A,r Int A*A) <-> irrefl(A,r)"
1.174 +by (unfold irrefl_def, blast)
1.175 +
1.176 +lemma trans_on_Int_iff: "trans[A](r Int A*A) <-> trans[A](r)"
1.177 +by (unfold trans_on_def, blast)
1.178 +
1.179 +lemma part_ord_Int_iff: "part_ord(A,r Int A*A) <-> part_ord(A,r)"
1.180 +apply (unfold part_ord_def)
1.181 +apply (simp add: irrefl_Int_iff trans_on_Int_iff)
1.182 +done
1.183 +
1.184 +lemma linear_Int_iff: "linear(A,r Int A*A) <-> linear(A,r)"
1.185 +by (unfold linear_def, blast)
1.186 +
1.187 +lemma tot_ord_Int_iff: "tot_ord(A,r Int A*A) <-> tot_ord(A,r)"
1.188 +apply (unfold tot_ord_def)
1.189 +apply (simp add: part_ord_Int_iff linear_Int_iff)
1.190 +done
1.191 +
1.192 +lemma wf_on_Int_iff: "wf[A](r Int A*A) <-> wf[A](r)"
1.193 +apply (unfold wf_on_def wf_def, fast) (*10 times faster than Blast_tac!*)
1.194 +done
1.195 +
1.196 +lemma well_ord_Int_iff: "well_ord(A,r Int A*A) <-> well_ord(A,r)"
1.197 +apply (unfold well_ord_def)
1.198 +apply (simp add: tot_ord_Int_iff wf_on_Int_iff)
1.199 +done
1.200 +
1.201 +
1.202 +(** Relations over the Empty Set **)
1.203 +
1.204 +lemma irrefl_0: "irrefl(0,r)"
1.205 +by (unfold irrefl_def, blast)
1.206 +
1.207 +lemma trans_on_0: "trans[0](r)"
1.208 +by (unfold trans_on_def, blast)
1.209 +
1.210 +lemma part_ord_0: "part_ord(0,r)"
1.211 +apply (unfold part_ord_def)
1.212 +apply (simp add: irrefl_0 trans_on_0)
1.213 +done
1.214 +
1.215 +lemma linear_0: "linear(0,r)"
1.216 +by (unfold linear_def, blast)
1.217 +
1.218 +lemma tot_ord_0: "tot_ord(0,r)"
1.219 +apply (unfold tot_ord_def)
1.220 +apply (simp add: part_ord_0 linear_0)
1.221 +done
1.222 +
1.223 +lemma wf_on_0: "wf[0](r)"
1.224 +by (unfold wf_on_def wf_def, blast)
1.225 +
1.226 +lemma well_ord_0: "well_ord(0,r)"
1.227 +apply (unfold well_ord_def)
1.228 +apply (simp add: tot_ord_0 wf_on_0)
1.229 +done
1.230 +
1.231 +
1.232 +(** The unit set is well-ordered by the empty relation (Grabczewski) **)
1.233 +
1.234 +lemma tot_ord_unit: "tot_ord({a},0)"
1.235 +by (simp add: irrefl_def trans_on_def part_ord_def linear_def tot_ord_def)
1.236 +
1.237 +lemma wf_on_unit: "wf[{a}](0)"
1.238 +by (simp add: wf_on_def wf_def, fast)
1.239 +
1.240 +lemma well_ord_unit: "well_ord({a},0)"
1.241 +apply (unfold well_ord_def)
1.242 +apply (simp add: tot_ord_unit wf_on_unit)
1.243 +done
1.244 +
1.245 +
1.246 +(** Order-preserving (monotone) maps **)
1.247 +
1.248 +lemma mono_map_is_fun: "f: mono_map(A,r,B,s) ==> f: A->B"
1.250 +
1.251 +lemma mono_map_is_inj:
1.252 +    "[| linear(A,r);  wf[B](s);  f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"
1.253 +apply (unfold mono_map_def inj_def, clarify)
1.254 +apply (erule_tac x=w and y=x in linearE, assumption+)
1.255 +apply (force intro: apply_type dest: wf_on_not_refl)+
1.256 +done
1.257 +
1.258 +
1.259 +(** Order-isomorphisms -- or similarities, as Suppes calls them **)
1.260 +
1.261 +lemma ord_isoI:
1.262 +    "[| f: bij(A, B);
1.263 +        !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s |]
1.264 +     ==> f: ord_iso(A,r,B,s)"
1.266 +
1.267 +lemma ord_iso_is_mono_map:
1.268 +    "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)"
1.269 +apply (simp add: ord_iso_def mono_map_def)
1.270 +apply (blast dest!: bij_is_fun)
1.271 +done
1.272 +
1.273 +lemma ord_iso_is_bij:
1.274 +    "f: ord_iso(A,r,B,s) ==> f: bij(A,B)"
1.276 +
1.277 +(*Needed?  But ord_iso_converse is!*)
1.278 +lemma ord_iso_apply:
1.279 +    "[| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> <f`x, f`y> : s"
1.280 +by (simp add: ord_iso_def, blast)
1.281 +
1.282 +lemma ord_iso_converse:
1.283 +    "[| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |]
1.284 +     ==> <converse(f) ` x, converse(f) ` y> : r"
1.285 +apply (simp add: ord_iso_def, clarify)
1.286 +apply (erule bspec [THEN bspec, THEN iffD2])
1.287 +apply (erule asm_rl bij_converse_bij [THEN bij_is_fun, THEN apply_type])+
1.288 +apply (auto simp add: right_inverse_bij)
1.289 +done
1.290 +
1.291 +
1.292 +(** Symmetry and Transitivity Rules **)
1.293 +
1.294 +(*Reflexivity of similarity*)
1.295 +lemma ord_iso_refl: "id(A): ord_iso(A,r,A,r)"
1.296 +by (rule id_bij [THEN ord_isoI], simp)
1.297 +
1.298 +(*Symmetry of similarity*)
1.299 +lemma ord_iso_sym: "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"
1.301 +apply (auto simp add: right_inverse_bij bij_converse_bij
1.302 +                      bij_is_fun [THEN apply_funtype])
1.303 +done
1.304 +
1.305 +(*Transitivity of similarity*)
1.306 +lemma mono_map_trans:
1.307 +    "[| g: mono_map(A,r,B,s);  f: mono_map(B,s,C,t) |]
1.308 +     ==> (f O g): mono_map(A,r,C,t)"
1.309 +apply (unfold mono_map_def)
1.310 +apply (auto simp add: comp_fun)
1.311 +done
1.312 +
1.313 +(*Transitivity of similarity: the order-isomorphism relation*)
1.314 +lemma ord_iso_trans:
1.315 +    "[| g: ord_iso(A,r,B,s);  f: ord_iso(B,s,C,t) |]
1.316 +     ==> (f O g): ord_iso(A,r,C,t)"
1.317 +apply (unfold ord_iso_def, clarify)
1.318 +apply (frule bij_is_fun [of f])
1.319 +apply (frule bij_is_fun [of g])
1.320 +apply (auto simp add: comp_bij)
1.321 +done
1.322 +
1.323 +(** Two monotone maps can make an order-isomorphism **)
1.324 +
1.325 +lemma mono_ord_isoI:
1.326 +    "[| f: mono_map(A,r,B,s);  g: mono_map(B,s,A,r);
1.327 +        f O g = id(B);  g O f = id(A) |] ==> f: ord_iso(A,r,B,s)"
1.328 +apply (simp add: ord_iso_def mono_map_def, safe)
1.329 +apply (intro fg_imp_bijective, auto)
1.330 +apply (subgoal_tac "<g` (f`x), g` (f`y) > : r")
1.331 +apply (simp add: comp_eq_id_iff [THEN iffD1])
1.332 +apply (blast intro: apply_funtype)
1.333 +done
1.334 +
1.335 +lemma well_ord_mono_ord_isoI:
1.336 +     "[| well_ord(A,r);  well_ord(B,s);
1.337 +         f: mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r) |]
1.338 +      ==> f: ord_iso(A,r,B,s)"
1.339 +apply (intro mono_ord_isoI, auto)
1.340 +apply (frule mono_map_is_fun [THEN fun_is_rel])
1.341 +apply (erule converse_converse [THEN subst], rule left_comp_inverse)
1.342 +apply (blast intro: left_comp_inverse mono_map_is_inj well_ord_is_linear
1.343 +                    well_ord_is_wf)+
1.344 +done
1.345 +
1.346 +
1.347 +(** Order-isomorphisms preserve the ordering's properties **)
1.348 +
1.349 +lemma part_ord_ord_iso:
1.350 +    "[| part_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)"
1.351 +apply (simp add: part_ord_def irrefl_def trans_on_def ord_iso_def)
1.352 +apply (fast intro: bij_is_fun [THEN apply_type])
1.353 +done
1.354 +
1.355 +lemma linear_ord_iso:
1.356 +    "[| linear(B,s);  f: ord_iso(A,r,B,s) |] ==> linear(A,r)"
1.357 +apply (simp add: linear_def ord_iso_def, safe)
1.358 +apply (drule_tac x1 = "f`x" and x = "f`xa" in bspec [THEN bspec])
1.359 +apply (safe elim!: bij_is_fun [THEN apply_type])
1.360 +apply (drule_tac t = "op ` (converse (f))" in subst_context)
1.362 +done
1.363 +
1.364 +lemma wf_on_ord_iso:
1.365 +    "[| wf[B](s);  f: ord_iso(A,r,B,s) |] ==> wf[A](r)"
1.366 +apply (simp add: wf_on_def wf_def ord_iso_def, safe)
1.367 +apply (drule_tac x = "{f`z. z:Z Int A}" in spec)
1.368 +apply (safe intro!: equalityI)
1.369 +apply (blast dest!: equalityD1 intro: bij_is_fun [THEN apply_type])+
1.370 +done
1.371 +
1.372 +lemma well_ord_ord_iso:
1.373 +    "[| well_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)"
1.374 +apply (unfold well_ord_def tot_ord_def)
1.375 +apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso)
1.376 +done
1.377
1.378
1.379 +(*** Main results of Kunen, Chapter 1 section 6 ***)
1.380 +
1.381 +(*Inductive argument for Kunen's Lemma 6.1, etc.
1.382 +  Simple proof from Halmos, page 72*)
1.383 +lemma well_ord_iso_subset_lemma:
1.384 +     "[| well_ord(A,r);  f: ord_iso(A,r, A',r);  A'<= A;  y: A |]
1.385 +      ==> ~ <f`y, y>: r"
1.386 +apply (simp add: well_ord_def ord_iso_def)
1.387 +apply (elim conjE CollectE)
1.388 +apply (rule_tac a=y in wf_on_induct, assumption+)
1.389 +apply (blast dest: bij_is_fun [THEN apply_type])
1.390 +done
1.391 +
1.392 +(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
1.393 +                     of a well-ordering*)
1.394 +lemma well_ord_iso_predE:
1.395 +     "[| well_ord(A,r);  f : ord_iso(A, r, pred(A,x,r), r);  x:A |] ==> P"
1.396 +apply (insert well_ord_iso_subset_lemma [of A r f "pred(A,x,r)" x])
1.398 +(*Now we know  f`x < x *)
1.399 +apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
1.400 +(*Now we also know f`x : pred(A,x,r);  contradiction! *)
1.401 +apply (simp add: well_ord_def pred_def)
1.402 +done
1.403 +
1.404 +(*Simple consequence of Lemma 6.1*)
1.405 +lemma well_ord_iso_pred_eq:
1.406 +     "[| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);
1.407 +         a:A;  c:A |] ==> a=c"
1.408 +apply (frule well_ord_is_trans_on)
1.409 +apply (frule well_ord_is_linear)
1.410 +apply (erule_tac x=a and y=c in linearE, assumption+)
1.411 +apply (drule ord_iso_sym)
1.412 +(*two symmetric cases*)
1.413 +apply (auto elim!: well_ord_subset [OF _ pred_subset, THEN well_ord_iso_predE]
1.414 +            intro!: predI
1.416 +done
1.417 +
1.418 +(*Does not assume r is a wellordering!*)
1.419 +lemma ord_iso_image_pred:
1.420 +     "[|f : ord_iso(A,r,B,s);  a:A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)"
1.421 +apply (unfold ord_iso_def pred_def)
1.422 +apply (erule CollectE)
1.423 +apply (simp (no_asm_simp) add: image_fun [OF bij_is_fun Collect_subset])
1.424 +apply (rule equalityI)
1.425 +apply (safe elim!: bij_is_fun [THEN apply_type])
1.426 +apply (rule RepFun_eqI)
1.427 +apply (blast intro!: right_inverse_bij [symmetric])
1.428 +apply (auto simp add: right_inverse_bij  bij_is_fun [THEN apply_funtype])
1.429 +done
1.430 +
1.431 +(*But in use, A and B may themselves be initial segments.  Then use
1.432 +  trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
1.433 +lemma ord_iso_restrict_pred: "[| f : ord_iso(A,r,B,s);   a:A |] ==>
1.434 +       restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"
1.435 +apply (simp add: ord_iso_image_pred [symmetric])
1.436 +apply (simp add: ord_iso_def, clarify)
1.437 +apply (rule conjI)
1.438 +apply (erule restrict_bij [OF bij_is_inj pred_subset])
1.439 +apply (frule bij_is_fun)
1.440 +apply (auto simp add: pred_def)
1.441 +done
1.442 +
1.443 +(*Tricky; a lot of forward proof!*)
1.444 +lemma well_ord_iso_preserving:
1.445 +     "[| well_ord(A,r);  well_ord(B,s);  <a,c>: r;
1.446 +         f : ord_iso(pred(A,a,r), r, pred(B,b,s), s);
1.447 +         g : ord_iso(pred(A,c,r), r, pred(B,d,s), s);
1.448 +         a:A;  c:A;  b:B;  d:B |] ==> <b,d>: s"
1.449 +apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], (erule asm_rl predI predE)+)
1.450 +apply (subgoal_tac "b = g`a")
1.451 +apply (simp (no_asm_simp))
1.452 +apply (rule well_ord_iso_pred_eq, auto)
1.453 +apply (frule ord_iso_restrict_pred, (erule asm_rl predI)+)
1.454 +apply (simp add: well_ord_is_trans_on trans_pred_pred_eq)
1.455 +apply (erule ord_iso_sym [THEN ord_iso_trans], assumption)
1.456 +done
1.457 +
1.458 +(*See Halmos, page 72*)
1.459 +lemma well_ord_iso_unique_lemma:
1.460 +     "[| well_ord(A,r);
1.461 +         f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |]
1.462 +      ==> ~ <g`y, f`y> : s"
1.463 +apply (frule well_ord_iso_subset_lemma)
1.464 +apply (rule_tac f = "converse (f) " and g = g in ord_iso_trans)
1.465 +apply auto
1.466 +apply (blast intro: ord_iso_sym)
1.467 +apply (frule ord_iso_is_bij [of f])
1.468 +apply (frule ord_iso_is_bij [of g])
1.469 +apply (frule ord_iso_converse)
1.470 +apply (blast intro!: bij_converse_bij
1.471 +             intro: bij_is_fun apply_funtype)+
1.472 +apply (erule notE)
1.473 +apply (simp add: left_inverse_bij bij_converse_bij bij_is_fun
1.474 +                 comp_fun_apply [of _ A B _ A])
1.475 +done
1.476 +
1.477 +
1.478 +(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
1.479 +lemma well_ord_iso_unique: "[| well_ord(A,r);
1.480 +         f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g"
1.481 +apply (rule fun_extension)
1.482 +apply (erule ord_iso_is_bij [THEN bij_is_fun])+
1.483 +apply (subgoal_tac "f`x : B & g`x : B & linear(B,s)")
1.484 + apply (simp add: linear_def)
1.485 + apply (blast dest: well_ord_iso_unique_lemma)
1.486 +apply (blast intro: ord_iso_is_bij bij_is_fun apply_funtype
1.487 +                    well_ord_is_linear well_ord_ord_iso ord_iso_sym)
1.488 +done
1.489 +
1.490 +(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
1.491 +
1.492 +lemma ord_iso_map_subset: "ord_iso_map(A,r,B,s) <= A*B"
1.493 +by (unfold ord_iso_map_def, blast)
1.494 +
1.495 +lemma domain_ord_iso_map: "domain(ord_iso_map(A,r,B,s)) <= A"
1.496 +by (unfold ord_iso_map_def, blast)
1.497 +
1.498 +lemma range_ord_iso_map: "range(ord_iso_map(A,r,B,s)) <= B"
1.499 +by (unfold ord_iso_map_def, blast)
1.500 +
1.501 +lemma converse_ord_iso_map:
1.502 +    "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)"
1.503 +apply (unfold ord_iso_map_def)
1.504 +apply (blast intro: ord_iso_sym)
1.505 +done
1.506 +
1.507 +lemma function_ord_iso_map:
1.508 +    "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))"
1.509 +apply (unfold ord_iso_map_def function_def)
1.510 +apply (blast intro: well_ord_iso_pred_eq ord_iso_sym ord_iso_trans)
1.511 +done
1.512 +
1.513 +lemma ord_iso_map_fun: "well_ord(B,s) ==> ord_iso_map(A,r,B,s)
1.514 +           : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))"
1.515 +by (simp add: Pi_iff function_ord_iso_map
1.516 +                 ord_iso_map_subset [THEN domain_times_range])
1.517 +
1.518 +lemma ord_iso_map_mono_map:
1.519 +    "[| well_ord(A,r);  well_ord(B,s) |]
1.520 +     ==> ord_iso_map(A,r,B,s)
1.521 +           : mono_map(domain(ord_iso_map(A,r,B,s)), r,
1.522 +                      range(ord_iso_map(A,r,B,s)), s)"
1.523 +apply (unfold mono_map_def)
1.524 +apply (simp (no_asm_simp) add: ord_iso_map_fun)
1.525 +apply safe
1.526 +apply (subgoal_tac "x:A & ya:A & y:B & yb:B")
1.527 + apply (simp add: apply_equality [OF _  ord_iso_map_fun])
1.528 + apply (unfold ord_iso_map_def)
1.529 + apply (blast intro: well_ord_iso_preserving, blast)
1.530 +done
1.531 +
1.532 +lemma ord_iso_map_ord_iso:
1.533 +    "[| well_ord(A,r);  well_ord(B,s) |] ==> ord_iso_map(A,r,B,s)
1.534 +           : ord_iso(domain(ord_iso_map(A,r,B,s)), r,
1.535 +                      range(ord_iso_map(A,r,B,s)), s)"
1.536 +apply (rule well_ord_mono_ord_isoI)
1.537 +   prefer 4
1.538 +   apply (rule converse_ord_iso_map [THEN subst])
1.539 +   apply (simp add: ord_iso_map_mono_map
1.540 +		    ord_iso_map_subset [THEN converse_converse])
1.541 +apply (blast intro!: domain_ord_iso_map range_ord_iso_map
1.542 +             intro: well_ord_subset ord_iso_map_mono_map)+
1.543 +done
1.544 +
1.545 +
1.546 +(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*)
1.547 +lemma domain_ord_iso_map_subset:
1.548 +     "[| well_ord(A,r);  well_ord(B,s);
1.549 +         a: A;  a ~: domain(ord_iso_map(A,r,B,s)) |]
1.550 +      ==>  domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)"
1.551 +apply (unfold ord_iso_map_def)
1.552 +apply (safe intro!: predI)
1.553 +(*Case analysis on  xa vs a in r *)
1.554 +apply (simp (no_asm_simp))
1.555 +apply (frule_tac A = A in well_ord_is_linear)
1.556 +apply (rename_tac b y f)
1.557 +apply (erule_tac x=b and y=a in linearE, assumption+)
1.558 +(*Trivial case: b=a*)
1.559 +apply clarify
1.560 +apply blast
1.561 +(*Harder case: <a, xa>: r*)
1.562 +apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type],
1.563 +       (erule asm_rl predI predE)+)
1.564 +apply (frule ord_iso_restrict_pred)
1.565 + apply (simp add: pred_iff)
1.566 +apply (simp split: split_if_asm
1.567 +          add: well_ord_is_trans_on trans_pred_pred_eq domain_UN domain_Union, blast)
1.568 +done
1.569 +
1.570 +(*For the 4-way case analysis in the main result*)
1.571 +lemma domain_ord_iso_map_cases:
1.572 +     "[| well_ord(A,r);  well_ord(B,s) |]
1.573 +      ==> domain(ord_iso_map(A,r,B,s)) = A |
1.574 +          (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))"
1.575 +apply (frule well_ord_is_wf)
1.576 +apply (unfold wf_on_def wf_def)
1.577 +apply (drule_tac x = "A-domain (ord_iso_map (A,r,B,s))" in spec)
1.578 +apply safe
1.579 +(*The first case: the domain equals A*)
1.580 +apply (rule domain_ord_iso_map [THEN equalityI])
1.581 +apply (erule Diff_eq_0_iff [THEN iffD1])
1.582 +(*The other case: the domain equals an initial segment*)
1.583 +apply (blast del: domainI subsetI
1.584 +	     elim!: predE
1.585 +	     intro!: domain_ord_iso_map_subset
1.586 +             intro: subsetI)+
1.587 +done
1.588 +
1.589 +(*As above, by duality*)
1.590 +lemma range_ord_iso_map_cases:
1.591 +    "[| well_ord(A,r);  well_ord(B,s) |]
1.592 +     ==> range(ord_iso_map(A,r,B,s)) = B |
1.593 +         (EX y:B. range(ord_iso_map(A,r,B,s)) = pred(B,y,s))"
1.594 +apply (rule converse_ord_iso_map [THEN subst])
1.596 +done
1.597 +
1.598 +(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
1.599 +lemma well_ord_trichotomy:
1.600 +   "[| well_ord(A,r);  well_ord(B,s) |]
1.601 +    ==> ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) |
1.602 +        (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) |
1.603 +        (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))"
1.604 +apply (frule_tac B = B in domain_ord_iso_map_cases, assumption)
1.605 +apply (frule_tac B = B in range_ord_iso_map_cases, assumption)
1.606 +apply (drule ord_iso_map_ord_iso, assumption)
1.607 +apply (elim disjE bexE)
1.608 +   apply (simp_all add: bexI)
1.609 +apply (rule wf_on_not_refl [THEN notE])
1.610 +  apply (erule well_ord_is_wf)
1.611 + apply assumption
1.612 +apply (subgoal_tac "<x,y>: ord_iso_map (A,r,B,s) ")
1.613 + apply (drule rangeI)
1.614 + apply (simp add: pred_def)
1.615 +apply (unfold ord_iso_map_def, blast)
1.616 +done
1.617 +
1.618 +
1.619 +(*** Properties of converse(r), by Krzysztof Grabczewski ***)
1.620 +
1.621 +lemma irrefl_converse: "irrefl(A,r) ==> irrefl(A,converse(r))"
1.622 +by (unfold irrefl_def, blast)
1.623 +
1.624 +lemma trans_on_converse: "trans[A](r) ==> trans[A](converse(r))"
1.625 +by (unfold trans_on_def, blast)
1.626 +
1.627 +lemma part_ord_converse: "part_ord(A,r) ==> part_ord(A,converse(r))"
1.628 +apply (unfold part_ord_def)
1.629 +apply (blast intro!: irrefl_converse trans_on_converse)
1.630 +done
1.631 +
1.632 +lemma linear_converse: "linear(A,r) ==> linear(A,converse(r))"
1.633 +by (unfold linear_def, blast)
1.634 +
1.635 +lemma tot_ord_converse: "tot_ord(A,r) ==> tot_ord(A,converse(r))"
1.636 +apply (unfold tot_ord_def)
1.637 +apply (blast intro!: part_ord_converse linear_converse)
1.638 +done
1.639 +
1.640 +
1.641 +(** By Krzysztof Grabczewski.
1.642 +    Lemmas involving the first element of a well ordered set **)
1.643 +
1.644 +lemma first_is_elem: "first(b,B,r) ==> b:B"
1.645 +by (unfold first_def, blast)
1.646 +
1.647 +lemma well_ord_imp_ex1_first:
1.648 +        "[| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"
1.649 +apply (unfold well_ord_def wf_on_def wf_def first_def)
1.650 +apply (elim conjE allE disjE, blast)
1.651 +apply (erule bexE)
1.652 +apply (rule_tac a = x in ex1I, auto)
1.653 +apply (unfold tot_ord_def linear_def, blast)
1.654 +done
1.655 +
1.656 +lemma the_first_in:
1.657 +     "[| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B"
1.658 +apply (drule well_ord_imp_ex1_first, assumption+)
1.659 +apply (rule first_is_elem)
1.660 +apply (erule theI)
1.661 +done
1.662 +
1.663 +ML {*
1.664 +val pred_def = thm "pred_def"
1.665 +val linear_def = thm "linear_def"
1.666 +val part_ord_def = thm "part_ord_def"
1.667 +val tot_ord_def = thm "tot_ord_def"
1.668 +val well_ord_def = thm "well_ord_def"
1.669 +val ord_iso_def = thm "ord_iso_def"
1.670 +val mono_map_def = thm "mono_map_def";
1.671 +
1.672 +val part_ord_Imp_asym = thm "part_ord_Imp_asym";
1.673 +val linearE = thm "linearE";
1.674 +val well_ordI = thm "well_ordI";
1.675 +val well_ord_is_wf = thm "well_ord_is_wf";
1.676 +val well_ord_is_trans_on = thm "well_ord_is_trans_on";
1.677 +val well_ord_is_linear = thm "well_ord_is_linear";
1.678 +val pred_iff = thm "pred_iff";
1.679 +val predI = thm "predI";
1.680 +val predE = thm "predE";
1.681 +val pred_subset_under = thm "pred_subset_under";
1.682 +val pred_subset = thm "pred_subset";
1.683 +val pred_pred_eq = thm "pred_pred_eq";
1.684 +val trans_pred_pred_eq = thm "trans_pred_pred_eq";
1.685 +val part_ord_subset = thm "part_ord_subset";
1.686 +val linear_subset = thm "linear_subset";
1.687 +val tot_ord_subset = thm "tot_ord_subset";
1.688 +val well_ord_subset = thm "well_ord_subset";
1.689 +val irrefl_Int_iff = thm "irrefl_Int_iff";
1.690 +val trans_on_Int_iff = thm "trans_on_Int_iff";
1.691 +val part_ord_Int_iff = thm "part_ord_Int_iff";
1.692 +val linear_Int_iff = thm "linear_Int_iff";
1.693 +val tot_ord_Int_iff = thm "tot_ord_Int_iff";
1.694 +val wf_on_Int_iff = thm "wf_on_Int_iff";
1.695 +val well_ord_Int_iff = thm "well_ord_Int_iff";
1.696 +val irrefl_0 = thm "irrefl_0";
1.697 +val trans_on_0 = thm "trans_on_0";
1.698 +val part_ord_0 = thm "part_ord_0";
1.699 +val linear_0 = thm "linear_0";
1.700 +val tot_ord_0 = thm "tot_ord_0";
1.701 +val wf_on_0 = thm "wf_on_0";
1.702 +val well_ord_0 = thm "well_ord_0";
1.703 +val tot_ord_unit = thm "tot_ord_unit";
1.704 +val wf_on_unit = thm "wf_on_unit";
1.705 +val well_ord_unit = thm "well_ord_unit";
1.706 +val mono_map_is_fun = thm "mono_map_is_fun";
1.707 +val mono_map_is_inj = thm "mono_map_is_inj";
1.708 +val ord_isoI = thm "ord_isoI";
1.709 +val ord_iso_is_mono_map = thm "ord_iso_is_mono_map";
1.710 +val ord_iso_is_bij = thm "ord_iso_is_bij";
1.711 +val ord_iso_apply = thm "ord_iso_apply";
1.712 +val ord_iso_converse = thm "ord_iso_converse";
1.713 +val ord_iso_refl = thm "ord_iso_refl";
1.714 +val ord_iso_sym = thm "ord_iso_sym";
1.715 +val mono_map_trans = thm "mono_map_trans";
1.716 +val ord_iso_trans = thm "ord_iso_trans";
1.717 +val mono_ord_isoI = thm "mono_ord_isoI";
1.718 +val well_ord_mono_ord_isoI = thm "well_ord_mono_ord_isoI";
1.719 +val part_ord_ord_iso = thm "part_ord_ord_iso";
1.720 +val linear_ord_iso = thm "linear_ord_iso";
1.721 +val wf_on_ord_iso = thm "wf_on_ord_iso";
1.722 +val well_ord_ord_iso = thm "well_ord_ord_iso";
1.723 +val well_ord_iso_subset_lemma = thm "well_ord_iso_subset_lemma";
1.724 +val well_ord_iso_predE = thm "well_ord_iso_predE";
1.725 +val well_ord_iso_pred_eq = thm "well_ord_iso_pred_eq";
1.726 +val ord_iso_image_pred = thm "ord_iso_image_pred";
1.727 +val ord_iso_restrict_pred = thm "ord_iso_restrict_pred";
1.728 +val well_ord_iso_preserving = thm "well_ord_iso_preserving";
1.729 +val well_ord_iso_unique_lemma = thm "well_ord_iso_unique_lemma";
1.730 +val well_ord_iso_unique = thm "well_ord_iso_unique";
1.731 +val ord_iso_map_subset = thm "ord_iso_map_subset";
1.732 +val domain_ord_iso_map = thm "domain_ord_iso_map";
1.733 +val range_ord_iso_map = thm "range_ord_iso_map";
1.734 +val converse_ord_iso_map = thm "converse_ord_iso_map";
1.735 +val function_ord_iso_map = thm "function_ord_iso_map";
1.736 +val ord_iso_map_fun = thm "ord_iso_map_fun";
1.737 +val ord_iso_map_mono_map = thm "ord_iso_map_mono_map";
1.738 +val ord_iso_map_ord_iso = thm "ord_iso_map_ord_iso";
1.739 +val domain_ord_iso_map_subset = thm "domain_ord_iso_map_subset";
1.740 +val domain_ord_iso_map_cases = thm "domain_ord_iso_map_cases";
1.741 +val range_ord_iso_map_cases = thm "range_ord_iso_map_cases";
1.742 +val well_ord_trichotomy = thm "well_ord_trichotomy";
1.743 +val irrefl_converse = thm "irrefl_converse";
1.744 +val trans_on_converse = thm "trans_on_converse";
1.745 +val part_ord_converse = thm "part_ord_converse";
1.746 +val linear_converse = thm "linear_converse";
1.747 +val tot_ord_converse = thm "tot_ord_converse";
1.748 +val first_is_elem = thm "first_is_elem";
1.749 +val well_ord_imp_ex1_first = thm "well_ord_imp_ex1_first";
1.750 +val the_first_in = thm "the_first_in";
1.751 +*}
1.752 +
1.753  end
```