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.128 +by (simp add: pred_def)
   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.249 +by (simp add: mono_map_def)
   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.265 +by (simp add: ord_iso_def)
   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.275 +by (simp add: ord_iso_def)
   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.300 +apply (simp add: ord_iso_def)
   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.361 +apply (simp add: left_inverse_bij)
   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.397 +apply (simp add: pred_subset)
   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.415 +            simp add: trans_pred_pred_eq)
   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.595 +apply (simp add: domain_ord_iso_map_cases)
   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