src/ZF/Order.thy
 author paulson Tue May 28 11:07:36 2002 +0200 (2002-05-28) changeset 13185 da61bfa0a391 parent 13176 312bd350579b child 13212 ba84715f6785 permissions -rw-r--r--
deleted some useless ML bindings
 clasohm@1478 ` 1` ```(* Title: ZF/Order.thy ``` lcp@435 ` 2` ``` ID: \$Id\$ ``` clasohm@1478 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` lcp@435 ` 4` ``` Copyright 1994 University of Cambridge ``` lcp@435 ` 5` paulson@13140 ` 6` ```Orders in Zermelo-Fraenkel Set Theory ``` paulson@13140 ` 7` paulson@13140 ` 8` ```Results from the book "Set Theory: an Introduction to Independence Proofs" ``` paulson@13140 ` 9` ``` by Kenneth Kunen. Chapter 1, section 6. ``` lcp@435 ` 10` ```*) ``` lcp@435 ` 11` paulson@13140 ` 12` ```theory Order = WF + Perm: ``` lcp@786 ` 13` paulson@2469 ` 14` ```constdefs ``` paulson@2469 ` 15` paulson@13140 ` 16` ``` part_ord :: "[i,i]=>o" (*Strict partial ordering*) ``` paulson@13140 ` 17` ``` "part_ord(A,r) == irrefl(A,r) & trans[A](r)" ``` paulson@13140 ` 18` paulson@13140 ` 19` ``` linear :: "[i,i]=>o" (*Strict total ordering*) ``` paulson@13140 ` 20` ``` "linear(A,r) == (ALL x:A. ALL y:A. :r | x=y | :r)" ``` paulson@13140 ` 21` paulson@13140 ` 22` ``` tot_ord :: "[i,i]=>o" (*Strict total ordering*) ``` paulson@13140 ` 23` ``` "tot_ord(A,r) == part_ord(A,r) & linear(A,r)" ``` paulson@13140 ` 24` paulson@13140 ` 25` ``` well_ord :: "[i,i]=>o" (*Well-ordering*) ``` paulson@13140 ` 26` ``` "well_ord(A,r) == tot_ord(A,r) & wf[A](r)" ``` paulson@13140 ` 27` paulson@13140 ` 28` ``` mono_map :: "[i,i,i,i]=>i" (*Order-preserving maps*) ``` paulson@13140 ` 29` ``` "mono_map(A,r,B,s) == ``` paulson@13140 ` 30` ``` {f: A->B. ALL x:A. ALL y:A. :r --> :s}" ``` paulson@13140 ` 31` paulson@13140 ` 32` ``` ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*) ``` paulson@13140 ` 33` ``` "ord_iso(A,r,B,s) == ``` paulson@13140 ` 34` ``` {f: bij(A,B). ALL x:A. ALL y:A. :r <-> :s}" ``` paulson@13140 ` 35` paulson@13140 ` 36` ``` pred :: "[i,i,i]=>i" (*Set of predecessors*) ``` paulson@13140 ` 37` ``` "pred(A,x,r) == {y:A. :r}" ``` paulson@13140 ` 38` paulson@13140 ` 39` ``` ord_iso_map :: "[i,i,i,i]=>i" (*Construction for linearity theorem*) ``` paulson@13140 ` 40` ``` "ord_iso_map(A,r,B,s) == ``` paulson@13140 ` 41` ``` UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {}" ``` paulson@13140 ` 42` paulson@13140 ` 43` ``` first :: "[i, i, i] => o" ``` paulson@2469 ` 44` ``` "first(u, X, R) == u:X & (ALL v:X. v~=u --> : R)" ``` paulson@2469 ` 45` paulson@13140 ` 46` paulson@9683 ` 47` ```syntax (xsymbols) ``` paulson@13140 ` 48` ``` ord_iso :: "[i,i,i,i]=>i" ("(\_, _\ \/ \_, _\)" 51) ``` paulson@13140 ` 49` paulson@13140 ` 50` paulson@13140 ` 51` ```(** Basic properties of the definitions **) ``` paulson@13140 ` 52` paulson@13140 ` 53` ```(*needed?*) ``` paulson@13140 ` 54` ```lemma part_ord_Imp_asym: ``` paulson@13140 ` 55` ``` "part_ord(A,r) ==> asym(r Int A*A)" ``` paulson@13140 ` 56` ```by (unfold part_ord_def irrefl_def trans_on_def asym_def, blast) ``` paulson@13140 ` 57` paulson@13140 ` 58` ```lemma linearE: ``` paulson@13140 ` 59` ``` "[| linear(A,r); x:A; y:A; ``` paulson@13140 ` 60` ``` :r ==> P; x=y ==> P; :r ==> P |] ``` paulson@13140 ` 61` ``` ==> P" ``` paulson@13140 ` 62` ```by (simp add: linear_def, blast) ``` paulson@13140 ` 63` paulson@13140 ` 64` paulson@13140 ` 65` ```(** General properties of well_ord **) ``` paulson@13140 ` 66` paulson@13140 ` 67` ```lemma well_ordI: ``` paulson@13140 ` 68` ``` "[| wf[A](r); linear(A,r) |] ==> well_ord(A,r)" ``` paulson@13140 ` 69` ```apply (simp add: irrefl_def part_ord_def tot_ord_def ``` paulson@13140 ` 70` ``` trans_on_def well_ord_def wf_on_not_refl) ``` paulson@13140 ` 71` ```apply (fast elim: linearE wf_on_asym wf_on_chain3) ``` paulson@13140 ` 72` ```done ``` paulson@13140 ` 73` paulson@13140 ` 74` ```lemma well_ord_is_wf: ``` paulson@13140 ` 75` ``` "well_ord(A,r) ==> wf[A](r)" ``` paulson@13140 ` 76` ```by (unfold well_ord_def, safe) ``` paulson@13140 ` 77` paulson@13140 ` 78` ```lemma well_ord_is_trans_on: ``` paulson@13140 ` 79` ``` "well_ord(A,r) ==> trans[A](r)" ``` paulson@13140 ` 80` ```by (unfold well_ord_def tot_ord_def part_ord_def, safe) ``` paulson@13140 ` 81` paulson@13140 ` 82` ```lemma well_ord_is_linear: "well_ord(A,r) ==> linear(A,r)" ``` paulson@13140 ` 83` ```by (unfold well_ord_def tot_ord_def, blast) ``` paulson@13140 ` 84` paulson@13140 ` 85` paulson@13140 ` 86` ```(** Derived rules for pred(A,x,r) **) ``` paulson@13140 ` 87` paulson@13140 ` 88` ```lemma pred_iff: "y : pred(A,x,r) <-> :r & y:A" ``` paulson@13140 ` 89` ```by (unfold pred_def, blast) ``` paulson@13140 ` 90` paulson@13140 ` 91` ```lemmas predI = conjI [THEN pred_iff [THEN iffD2]] ``` paulson@13140 ` 92` paulson@13140 ` 93` ```lemma predE: "[| y: pred(A,x,r); [| y:A; :r |] ==> P |] ==> P" ``` paulson@13140 ` 94` ```by (simp add: pred_def) ``` paulson@13140 ` 95` paulson@13140 ` 96` ```lemma pred_subset_under: "pred(A,x,r) <= r -`` {x}" ``` paulson@13140 ` 97` ```by (simp add: pred_def, blast) ``` paulson@13140 ` 98` paulson@13140 ` 99` ```lemma pred_subset: "pred(A,x,r) <= A" ``` paulson@13140 ` 100` ```by (simp add: pred_def, blast) ``` paulson@13140 ` 101` paulson@13140 ` 102` ```lemma pred_pred_eq: ``` paulson@13140 ` 103` ``` "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)" ``` paulson@13140 ` 104` ```by (simp add: pred_def, blast) ``` paulson@13140 ` 105` paulson@13140 ` 106` ```lemma trans_pred_pred_eq: ``` paulson@13140 ` 107` ``` "[| trans[A](r); :r; x:A; y:A |] ``` paulson@13140 ` 108` ``` ==> pred(pred(A,x,r), y, r) = pred(A,y,r)" ``` paulson@13140 ` 109` ```by (unfold trans_on_def pred_def, blast) ``` paulson@13140 ` 110` paulson@13140 ` 111` paulson@13140 ` 112` ```(** The ordering's properties hold over all subsets of its domain ``` paulson@13140 ` 113` ``` [including initial segments of the form pred(A,x,r) **) ``` paulson@13140 ` 114` paulson@13140 ` 115` ```(*Note: a relation s such that s<=r need not be a partial ordering*) ``` paulson@13140 ` 116` ```lemma part_ord_subset: ``` paulson@13140 ` 117` ``` "[| part_ord(A,r); B<=A |] ==> part_ord(B,r)" ``` paulson@13140 ` 118` ```by (unfold part_ord_def irrefl_def trans_on_def, blast) ``` paulson@13140 ` 119` paulson@13140 ` 120` ```lemma linear_subset: ``` paulson@13140 ` 121` ``` "[| linear(A,r); B<=A |] ==> linear(B,r)" ``` paulson@13140 ` 122` ```by (unfold linear_def, blast) ``` paulson@13140 ` 123` paulson@13140 ` 124` ```lemma tot_ord_subset: ``` paulson@13140 ` 125` ``` "[| tot_ord(A,r); B<=A |] ==> tot_ord(B,r)" ``` paulson@13140 ` 126` ```apply (unfold tot_ord_def) ``` paulson@13140 ` 127` ```apply (fast elim!: part_ord_subset linear_subset) ``` paulson@13140 ` 128` ```done ``` paulson@13140 ` 129` paulson@13140 ` 130` ```lemma well_ord_subset: ``` paulson@13140 ` 131` ``` "[| well_ord(A,r); B<=A |] ==> well_ord(B,r)" ``` paulson@13140 ` 132` ```apply (unfold well_ord_def) ``` paulson@13140 ` 133` ```apply (fast elim!: tot_ord_subset wf_on_subset_A) ``` paulson@13140 ` 134` ```done ``` paulson@13140 ` 135` paulson@13140 ` 136` paulson@13140 ` 137` ```(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **) ``` paulson@13140 ` 138` paulson@13140 ` 139` ```lemma irrefl_Int_iff: "irrefl(A,r Int A*A) <-> irrefl(A,r)" ``` paulson@13140 ` 140` ```by (unfold irrefl_def, blast) ``` paulson@13140 ` 141` paulson@13140 ` 142` ```lemma trans_on_Int_iff: "trans[A](r Int A*A) <-> trans[A](r)" ``` paulson@13140 ` 143` ```by (unfold trans_on_def, blast) ``` paulson@13140 ` 144` paulson@13140 ` 145` ```lemma part_ord_Int_iff: "part_ord(A,r Int A*A) <-> part_ord(A,r)" ``` paulson@13140 ` 146` ```apply (unfold part_ord_def) ``` paulson@13140 ` 147` ```apply (simp add: irrefl_Int_iff trans_on_Int_iff) ``` paulson@13140 ` 148` ```done ``` paulson@13140 ` 149` paulson@13140 ` 150` ```lemma linear_Int_iff: "linear(A,r Int A*A) <-> linear(A,r)" ``` paulson@13140 ` 151` ```by (unfold linear_def, blast) ``` paulson@13140 ` 152` paulson@13140 ` 153` ```lemma tot_ord_Int_iff: "tot_ord(A,r Int A*A) <-> tot_ord(A,r)" ``` paulson@13140 ` 154` ```apply (unfold tot_ord_def) ``` paulson@13140 ` 155` ```apply (simp add: part_ord_Int_iff linear_Int_iff) ``` paulson@13140 ` 156` ```done ``` paulson@13140 ` 157` paulson@13140 ` 158` ```lemma wf_on_Int_iff: "wf[A](r Int A*A) <-> wf[A](r)" ``` paulson@13140 ` 159` ```apply (unfold wf_on_def wf_def, fast) (*10 times faster than Blast_tac!*) ``` paulson@13140 ` 160` ```done ``` paulson@13140 ` 161` paulson@13140 ` 162` ```lemma well_ord_Int_iff: "well_ord(A,r Int A*A) <-> well_ord(A,r)" ``` paulson@13140 ` 163` ```apply (unfold well_ord_def) ``` paulson@13140 ` 164` ```apply (simp add: tot_ord_Int_iff wf_on_Int_iff) ``` paulson@13140 ` 165` ```done ``` paulson@13140 ` 166` paulson@13140 ` 167` paulson@13140 ` 168` ```(** Relations over the Empty Set **) ``` paulson@13140 ` 169` paulson@13140 ` 170` ```lemma irrefl_0: "irrefl(0,r)" ``` paulson@13140 ` 171` ```by (unfold irrefl_def, blast) ``` paulson@13140 ` 172` paulson@13140 ` 173` ```lemma trans_on_0: "trans[0](r)" ``` paulson@13140 ` 174` ```by (unfold trans_on_def, blast) ``` paulson@13140 ` 175` paulson@13140 ` 176` ```lemma part_ord_0: "part_ord(0,r)" ``` paulson@13140 ` 177` ```apply (unfold part_ord_def) ``` paulson@13140 ` 178` ```apply (simp add: irrefl_0 trans_on_0) ``` paulson@13140 ` 179` ```done ``` paulson@13140 ` 180` paulson@13140 ` 181` ```lemma linear_0: "linear(0,r)" ``` paulson@13140 ` 182` ```by (unfold linear_def, blast) ``` paulson@13140 ` 183` paulson@13140 ` 184` ```lemma tot_ord_0: "tot_ord(0,r)" ``` paulson@13140 ` 185` ```apply (unfold tot_ord_def) ``` paulson@13140 ` 186` ```apply (simp add: part_ord_0 linear_0) ``` paulson@13140 ` 187` ```done ``` paulson@13140 ` 188` paulson@13140 ` 189` ```lemma wf_on_0: "wf[0](r)" ``` paulson@13140 ` 190` ```by (unfold wf_on_def wf_def, blast) ``` paulson@13140 ` 191` paulson@13140 ` 192` ```lemma well_ord_0: "well_ord(0,r)" ``` paulson@13140 ` 193` ```apply (unfold well_ord_def) ``` paulson@13140 ` 194` ```apply (simp add: tot_ord_0 wf_on_0) ``` paulson@13140 ` 195` ```done ``` paulson@13140 ` 196` paulson@13140 ` 197` paulson@13140 ` 198` ```(** The unit set is well-ordered by the empty relation (Grabczewski) **) ``` paulson@13140 ` 199` paulson@13140 ` 200` ```lemma tot_ord_unit: "tot_ord({a},0)" ``` paulson@13140 ` 201` ```by (simp add: irrefl_def trans_on_def part_ord_def linear_def tot_ord_def) ``` paulson@13140 ` 202` paulson@13140 ` 203` ```lemma wf_on_unit: "wf[{a}](0)" ``` paulson@13140 ` 204` ```by (simp add: wf_on_def wf_def, fast) ``` paulson@13140 ` 205` paulson@13140 ` 206` ```lemma well_ord_unit: "well_ord({a},0)" ``` paulson@13140 ` 207` ```apply (unfold well_ord_def) ``` paulson@13140 ` 208` ```apply (simp add: tot_ord_unit wf_on_unit) ``` paulson@13140 ` 209` ```done ``` paulson@13140 ` 210` paulson@13140 ` 211` paulson@13140 ` 212` ```(** Order-preserving (monotone) maps **) ``` paulson@13140 ` 213` paulson@13140 ` 214` ```lemma mono_map_is_fun: "f: mono_map(A,r,B,s) ==> f: A->B" ``` paulson@13140 ` 215` ```by (simp add: mono_map_def) ``` paulson@13140 ` 216` paulson@13140 ` 217` ```lemma mono_map_is_inj: ``` paulson@13140 ` 218` ``` "[| linear(A,r); wf[B](s); f: mono_map(A,r,B,s) |] ==> f: inj(A,B)" ``` paulson@13140 ` 219` ```apply (unfold mono_map_def inj_def, clarify) ``` paulson@13140 ` 220` ```apply (erule_tac x=w and y=x in linearE, assumption+) ``` paulson@13140 ` 221` ```apply (force intro: apply_type dest: wf_on_not_refl)+ ``` paulson@13140 ` 222` ```done ``` paulson@13140 ` 223` paulson@13140 ` 224` paulson@13140 ` 225` ```(** Order-isomorphisms -- or similarities, as Suppes calls them **) ``` paulson@13140 ` 226` paulson@13140 ` 227` ```lemma ord_isoI: ``` paulson@13140 ` 228` ``` "[| f: bij(A, B); ``` paulson@13140 ` 229` ``` !!x y. [| x:A; y:A |] ==> : r <-> : s |] ``` paulson@13140 ` 230` ``` ==> f: ord_iso(A,r,B,s)" ``` paulson@13140 ` 231` ```by (simp add: ord_iso_def) ``` paulson@13140 ` 232` paulson@13140 ` 233` ```lemma ord_iso_is_mono_map: ``` paulson@13140 ` 234` ``` "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)" ``` paulson@13140 ` 235` ```apply (simp add: ord_iso_def mono_map_def) ``` paulson@13140 ` 236` ```apply (blast dest!: bij_is_fun) ``` paulson@13140 ` 237` ```done ``` paulson@13140 ` 238` paulson@13140 ` 239` ```lemma ord_iso_is_bij: ``` paulson@13140 ` 240` ``` "f: ord_iso(A,r,B,s) ==> f: bij(A,B)" ``` paulson@13140 ` 241` ```by (simp add: ord_iso_def) ``` paulson@13140 ` 242` paulson@13140 ` 243` ```(*Needed? But ord_iso_converse is!*) ``` paulson@13140 ` 244` ```lemma ord_iso_apply: ``` paulson@13140 ` 245` ``` "[| f: ord_iso(A,r,B,s); : r; x:A; y:A |] ==> : s" ``` paulson@13140 ` 246` ```by (simp add: ord_iso_def, blast) ``` paulson@13140 ` 247` paulson@13140 ` 248` ```lemma ord_iso_converse: ``` paulson@13140 ` 249` ``` "[| f: ord_iso(A,r,B,s); : s; x:B; y:B |] ``` paulson@13140 ` 250` ``` ==> : r" ``` paulson@13140 ` 251` ```apply (simp add: ord_iso_def, clarify) ``` paulson@13140 ` 252` ```apply (erule bspec [THEN bspec, THEN iffD2]) ``` paulson@13140 ` 253` ```apply (erule asm_rl bij_converse_bij [THEN bij_is_fun, THEN apply_type])+ ``` paulson@13140 ` 254` ```apply (auto simp add: right_inverse_bij) ``` paulson@13140 ` 255` ```done ``` paulson@13140 ` 256` paulson@13140 ` 257` paulson@13140 ` 258` ```(** Symmetry and Transitivity Rules **) ``` paulson@13140 ` 259` paulson@13140 ` 260` ```(*Reflexivity of similarity*) ``` paulson@13140 ` 261` ```lemma ord_iso_refl: "id(A): ord_iso(A,r,A,r)" ``` paulson@13140 ` 262` ```by (rule id_bij [THEN ord_isoI], simp) ``` paulson@13140 ` 263` paulson@13140 ` 264` ```(*Symmetry of similarity*) ``` paulson@13140 ` 265` ```lemma ord_iso_sym: "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)" ``` paulson@13140 ` 266` ```apply (simp add: ord_iso_def) ``` paulson@13140 ` 267` ```apply (auto simp add: right_inverse_bij bij_converse_bij ``` paulson@13140 ` 268` ``` bij_is_fun [THEN apply_funtype]) ``` paulson@13140 ` 269` ```done ``` paulson@13140 ` 270` paulson@13140 ` 271` ```(*Transitivity of similarity*) ``` paulson@13140 ` 272` ```lemma mono_map_trans: ``` paulson@13140 ` 273` ``` "[| g: mono_map(A,r,B,s); f: mono_map(B,s,C,t) |] ``` paulson@13140 ` 274` ``` ==> (f O g): mono_map(A,r,C,t)" ``` paulson@13140 ` 275` ```apply (unfold mono_map_def) ``` paulson@13140 ` 276` ```apply (auto simp add: comp_fun) ``` paulson@13140 ` 277` ```done ``` paulson@13140 ` 278` paulson@13140 ` 279` ```(*Transitivity of similarity: the order-isomorphism relation*) ``` paulson@13140 ` 280` ```lemma ord_iso_trans: ``` paulson@13140 ` 281` ``` "[| g: ord_iso(A,r,B,s); f: ord_iso(B,s,C,t) |] ``` paulson@13140 ` 282` ``` ==> (f O g): ord_iso(A,r,C,t)" ``` paulson@13140 ` 283` ```apply (unfold ord_iso_def, clarify) ``` paulson@13140 ` 284` ```apply (frule bij_is_fun [of f]) ``` paulson@13140 ` 285` ```apply (frule bij_is_fun [of g]) ``` paulson@13140 ` 286` ```apply (auto simp add: comp_bij) ``` paulson@13140 ` 287` ```done ``` paulson@13140 ` 288` paulson@13140 ` 289` ```(** Two monotone maps can make an order-isomorphism **) ``` paulson@13140 ` 290` paulson@13140 ` 291` ```lemma mono_ord_isoI: ``` paulson@13140 ` 292` ``` "[| f: mono_map(A,r,B,s); g: mono_map(B,s,A,r); ``` paulson@13140 ` 293` ``` f O g = id(B); g O f = id(A) |] ==> f: ord_iso(A,r,B,s)" ``` paulson@13140 ` 294` ```apply (simp add: ord_iso_def mono_map_def, safe) ``` paulson@13140 ` 295` ```apply (intro fg_imp_bijective, auto) ``` paulson@13140 ` 296` ```apply (subgoal_tac " : r") ``` paulson@13140 ` 297` ```apply (simp add: comp_eq_id_iff [THEN iffD1]) ``` paulson@13140 ` 298` ```apply (blast intro: apply_funtype) ``` paulson@13140 ` 299` ```done ``` paulson@13140 ` 300` paulson@13140 ` 301` ```lemma well_ord_mono_ord_isoI: ``` paulson@13140 ` 302` ``` "[| well_ord(A,r); well_ord(B,s); ``` paulson@13140 ` 303` ``` f: mono_map(A,r,B,s); converse(f): mono_map(B,s,A,r) |] ``` paulson@13140 ` 304` ``` ==> f: ord_iso(A,r,B,s)" ``` paulson@13140 ` 305` ```apply (intro mono_ord_isoI, auto) ``` paulson@13140 ` 306` ```apply (frule mono_map_is_fun [THEN fun_is_rel]) ``` paulson@13140 ` 307` ```apply (erule converse_converse [THEN subst], rule left_comp_inverse) ``` paulson@13140 ` 308` ```apply (blast intro: left_comp_inverse mono_map_is_inj well_ord_is_linear ``` paulson@13140 ` 309` ``` well_ord_is_wf)+ ``` paulson@13140 ` 310` ```done ``` paulson@13140 ` 311` paulson@13140 ` 312` paulson@13140 ` 313` ```(** Order-isomorphisms preserve the ordering's properties **) ``` paulson@13140 ` 314` paulson@13140 ` 315` ```lemma part_ord_ord_iso: ``` paulson@13140 ` 316` ``` "[| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)" ``` paulson@13140 ` 317` ```apply (simp add: part_ord_def irrefl_def trans_on_def ord_iso_def) ``` paulson@13140 ` 318` ```apply (fast intro: bij_is_fun [THEN apply_type]) ``` paulson@13140 ` 319` ```done ``` paulson@13140 ` 320` paulson@13140 ` 321` ```lemma linear_ord_iso: ``` paulson@13140 ` 322` ``` "[| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)" ``` paulson@13140 ` 323` ```apply (simp add: linear_def ord_iso_def, safe) ``` paulson@13140 ` 324` ```apply (drule_tac x1 = "f`x" and x = "f`xa" in bspec [THEN bspec]) ``` paulson@13140 ` 325` ```apply (safe elim!: bij_is_fun [THEN apply_type]) ``` paulson@13140 ` 326` ```apply (drule_tac t = "op ` (converse (f))" in subst_context) ``` paulson@13140 ` 327` ```apply (simp add: left_inverse_bij) ``` paulson@13140 ` 328` ```done ``` paulson@13140 ` 329` paulson@13140 ` 330` ```lemma wf_on_ord_iso: ``` paulson@13140 ` 331` ``` "[| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)" ``` paulson@13140 ` 332` ```apply (simp add: wf_on_def wf_def ord_iso_def, safe) ``` paulson@13140 ` 333` ```apply (drule_tac x = "{f`z. z:Z Int A}" in spec) ``` paulson@13140 ` 334` ```apply (safe intro!: equalityI) ``` paulson@13140 ` 335` ```apply (blast dest!: equalityD1 intro: bij_is_fun [THEN apply_type])+ ``` paulson@13140 ` 336` ```done ``` paulson@13140 ` 337` paulson@13140 ` 338` ```lemma well_ord_ord_iso: ``` paulson@13140 ` 339` ``` "[| well_ord(B,s); f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)" ``` paulson@13140 ` 340` ```apply (unfold well_ord_def tot_ord_def) ``` paulson@13140 ` 341` ```apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso) ``` paulson@13140 ` 342` ```done ``` paulson@9683 ` 343` paulson@9683 ` 344` paulson@13140 ` 345` ```(*** Main results of Kunen, Chapter 1 section 6 ***) ``` paulson@13140 ` 346` paulson@13140 ` 347` ```(*Inductive argument for Kunen's Lemma 6.1, etc. ``` paulson@13140 ` 348` ``` Simple proof from Halmos, page 72*) ``` paulson@13140 ` 349` ```lemma well_ord_iso_subset_lemma: ``` paulson@13140 ` 350` ``` "[| well_ord(A,r); f: ord_iso(A,r, A',r); A'<= A; y: A |] ``` paulson@13140 ` 351` ``` ==> ~ : r" ``` paulson@13140 ` 352` ```apply (simp add: well_ord_def ord_iso_def) ``` paulson@13140 ` 353` ```apply (elim conjE CollectE) ``` paulson@13140 ` 354` ```apply (rule_tac a=y in wf_on_induct, assumption+) ``` paulson@13140 ` 355` ```apply (blast dest: bij_is_fun [THEN apply_type]) ``` paulson@13140 ` 356` ```done ``` paulson@13140 ` 357` paulson@13140 ` 358` ```(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment ``` paulson@13140 ` 359` ``` of a well-ordering*) ``` paulson@13140 ` 360` ```lemma well_ord_iso_predE: ``` paulson@13140 ` 361` ``` "[| well_ord(A,r); f : ord_iso(A, r, pred(A,x,r), r); x:A |] ==> P" ``` paulson@13140 ` 362` ```apply (insert well_ord_iso_subset_lemma [of A r f "pred(A,x,r)" x]) ``` paulson@13140 ` 363` ```apply (simp add: pred_subset) ``` paulson@13140 ` 364` ```(*Now we know f`x < x *) ``` paulson@13140 ` 365` ```apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) ``` paulson@13140 ` 366` ```(*Now we also know f`x : pred(A,x,r); contradiction! *) ``` paulson@13140 ` 367` ```apply (simp add: well_ord_def pred_def) ``` paulson@13140 ` 368` ```done ``` paulson@13140 ` 369` paulson@13140 ` 370` ```(*Simple consequence of Lemma 6.1*) ``` paulson@13140 ` 371` ```lemma well_ord_iso_pred_eq: ``` paulson@13140 ` 372` ``` "[| well_ord(A,r); f : ord_iso(pred(A,a,r), r, pred(A,c,r), r); ``` paulson@13140 ` 373` ``` a:A; c:A |] ==> a=c" ``` paulson@13140 ` 374` ```apply (frule well_ord_is_trans_on) ``` paulson@13140 ` 375` ```apply (frule well_ord_is_linear) ``` paulson@13140 ` 376` ```apply (erule_tac x=a and y=c in linearE, assumption+) ``` paulson@13140 ` 377` ```apply (drule ord_iso_sym) ``` paulson@13140 ` 378` ```(*two symmetric cases*) ``` paulson@13140 ` 379` ```apply (auto elim!: well_ord_subset [OF _ pred_subset, THEN well_ord_iso_predE] ``` paulson@13140 ` 380` ``` intro!: predI ``` paulson@13140 ` 381` ``` simp add: trans_pred_pred_eq) ``` paulson@13140 ` 382` ```done ``` paulson@13140 ` 383` paulson@13140 ` 384` ```(*Does not assume r is a wellordering!*) ``` paulson@13140 ` 385` ```lemma ord_iso_image_pred: ``` paulson@13140 ` 386` ``` "[|f : ord_iso(A,r,B,s); a:A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)" ``` paulson@13140 ` 387` ```apply (unfold ord_iso_def pred_def) ``` paulson@13140 ` 388` ```apply (erule CollectE) ``` paulson@13140 ` 389` ```apply (simp (no_asm_simp) add: image_fun [OF bij_is_fun Collect_subset]) ``` paulson@13140 ` 390` ```apply (rule equalityI) ``` paulson@13140 ` 391` ```apply (safe elim!: bij_is_fun [THEN apply_type]) ``` paulson@13140 ` 392` ```apply (rule RepFun_eqI) ``` paulson@13140 ` 393` ```apply (blast intro!: right_inverse_bij [symmetric]) ``` paulson@13140 ` 394` ```apply (auto simp add: right_inverse_bij bij_is_fun [THEN apply_funtype]) ``` paulson@13140 ` 395` ```done ``` paulson@13140 ` 396` paulson@13140 ` 397` ```(*But in use, A and B may themselves be initial segments. Then use ``` paulson@13140 ` 398` ``` trans_pred_pred_eq to simplify the pred(pred...) terms. See just below.*) ``` paulson@13140 ` 399` ```lemma ord_iso_restrict_pred: "[| f : ord_iso(A,r,B,s); a:A |] ==> ``` paulson@13140 ` 400` ``` restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)" ``` paulson@13140 ` 401` ```apply (simp add: ord_iso_image_pred [symmetric]) ``` paulson@13140 ` 402` ```apply (simp add: ord_iso_def, clarify) ``` paulson@13140 ` 403` ```apply (rule conjI) ``` paulson@13140 ` 404` ```apply (erule restrict_bij [OF bij_is_inj pred_subset]) ``` paulson@13140 ` 405` ```apply (frule bij_is_fun) ``` paulson@13140 ` 406` ```apply (auto simp add: pred_def) ``` paulson@13140 ` 407` ```done ``` paulson@13140 ` 408` paulson@13140 ` 409` ```(*Tricky; a lot of forward proof!*) ``` paulson@13140 ` 410` ```lemma well_ord_iso_preserving: ``` paulson@13140 ` 411` ``` "[| well_ord(A,r); well_ord(B,s); : r; ``` paulson@13140 ` 412` ``` f : ord_iso(pred(A,a,r), r, pred(B,b,s), s); ``` paulson@13140 ` 413` ``` g : ord_iso(pred(A,c,r), r, pred(B,d,s), s); ``` paulson@13140 ` 414` ``` a:A; c:A; b:B; d:B |] ==> : s" ``` paulson@13140 ` 415` ```apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], (erule asm_rl predI predE)+) ``` paulson@13140 ` 416` ```apply (subgoal_tac "b = g`a") ``` paulson@13140 ` 417` ```apply (simp (no_asm_simp)) ``` paulson@13140 ` 418` ```apply (rule well_ord_iso_pred_eq, auto) ``` paulson@13140 ` 419` ```apply (frule ord_iso_restrict_pred, (erule asm_rl predI)+) ``` paulson@13140 ` 420` ```apply (simp add: well_ord_is_trans_on trans_pred_pred_eq) ``` paulson@13140 ` 421` ```apply (erule ord_iso_sym [THEN ord_iso_trans], assumption) ``` paulson@13140 ` 422` ```done ``` paulson@13140 ` 423` paulson@13140 ` 424` ```(*See Halmos, page 72*) ``` paulson@13140 ` 425` ```lemma well_ord_iso_unique_lemma: ``` paulson@13140 ` 426` ``` "[| well_ord(A,r); ``` paulson@13140 ` 427` ``` f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s); y: A |] ``` paulson@13140 ` 428` ``` ==> ~ : s" ``` paulson@13140 ` 429` ```apply (frule well_ord_iso_subset_lemma) ``` paulson@13140 ` 430` ```apply (rule_tac f = "converse (f) " and g = g in ord_iso_trans) ``` paulson@13140 ` 431` ```apply auto ``` paulson@13140 ` 432` ```apply (blast intro: ord_iso_sym) ``` paulson@13140 ` 433` ```apply (frule ord_iso_is_bij [of f]) ``` paulson@13140 ` 434` ```apply (frule ord_iso_is_bij [of g]) ``` paulson@13140 ` 435` ```apply (frule ord_iso_converse) ``` paulson@13140 ` 436` ```apply (blast intro!: bij_converse_bij ``` paulson@13140 ` 437` ``` intro: bij_is_fun apply_funtype)+ ``` paulson@13140 ` 438` ```apply (erule notE) ``` paulson@13176 ` 439` ```apply (simp add: left_inverse_bij bij_is_fun comp_fun_apply [of _ A B]) ``` paulson@13140 ` 440` ```done ``` paulson@13140 ` 441` paulson@13140 ` 442` paulson@13140 ` 443` ```(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*) ``` paulson@13140 ` 444` ```lemma well_ord_iso_unique: "[| well_ord(A,r); ``` paulson@13140 ` 445` ``` f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s) |] ==> f = g" ``` paulson@13140 ` 446` ```apply (rule fun_extension) ``` paulson@13140 ` 447` ```apply (erule ord_iso_is_bij [THEN bij_is_fun])+ ``` paulson@13140 ` 448` ```apply (subgoal_tac "f`x : B & g`x : B & linear(B,s)") ``` paulson@13140 ` 449` ``` apply (simp add: linear_def) ``` paulson@13140 ` 450` ``` apply (blast dest: well_ord_iso_unique_lemma) ``` paulson@13140 ` 451` ```apply (blast intro: ord_iso_is_bij bij_is_fun apply_funtype ``` paulson@13140 ` 452` ``` well_ord_is_linear well_ord_ord_iso ord_iso_sym) ``` paulson@13140 ` 453` ```done ``` paulson@13140 ` 454` paulson@13140 ` 455` ```(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **) ``` paulson@13140 ` 456` paulson@13140 ` 457` ```lemma ord_iso_map_subset: "ord_iso_map(A,r,B,s) <= A*B" ``` paulson@13140 ` 458` ```by (unfold ord_iso_map_def, blast) ``` paulson@13140 ` 459` paulson@13140 ` 460` ```lemma domain_ord_iso_map: "domain(ord_iso_map(A,r,B,s)) <= A" ``` paulson@13140 ` 461` ```by (unfold ord_iso_map_def, blast) ``` paulson@13140 ` 462` paulson@13140 ` 463` ```lemma range_ord_iso_map: "range(ord_iso_map(A,r,B,s)) <= B" ``` paulson@13140 ` 464` ```by (unfold ord_iso_map_def, blast) ``` paulson@13140 ` 465` paulson@13140 ` 466` ```lemma converse_ord_iso_map: ``` paulson@13140 ` 467` ``` "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)" ``` paulson@13140 ` 468` ```apply (unfold ord_iso_map_def) ``` paulson@13140 ` 469` ```apply (blast intro: ord_iso_sym) ``` paulson@13140 ` 470` ```done ``` paulson@13140 ` 471` paulson@13140 ` 472` ```lemma function_ord_iso_map: ``` paulson@13140 ` 473` ``` "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))" ``` paulson@13140 ` 474` ```apply (unfold ord_iso_map_def function_def) ``` paulson@13140 ` 475` ```apply (blast intro: well_ord_iso_pred_eq ord_iso_sym ord_iso_trans) ``` paulson@13140 ` 476` ```done ``` paulson@13140 ` 477` paulson@13140 ` 478` ```lemma ord_iso_map_fun: "well_ord(B,s) ==> ord_iso_map(A,r,B,s) ``` paulson@13140 ` 479` ``` : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))" ``` paulson@13140 ` 480` ```by (simp add: Pi_iff function_ord_iso_map ``` paulson@13140 ` 481` ``` ord_iso_map_subset [THEN domain_times_range]) ``` paulson@13140 ` 482` paulson@13140 ` 483` ```lemma ord_iso_map_mono_map: ``` paulson@13140 ` 484` ``` "[| well_ord(A,r); well_ord(B,s) |] ``` paulson@13140 ` 485` ``` ==> ord_iso_map(A,r,B,s) ``` paulson@13140 ` 486` ``` : mono_map(domain(ord_iso_map(A,r,B,s)), r, ``` paulson@13140 ` 487` ``` range(ord_iso_map(A,r,B,s)), s)" ``` paulson@13140 ` 488` ```apply (unfold mono_map_def) ``` paulson@13140 ` 489` ```apply (simp (no_asm_simp) add: ord_iso_map_fun) ``` paulson@13140 ` 490` ```apply safe ``` paulson@13140 ` 491` ```apply (subgoal_tac "x:A & ya:A & y:B & yb:B") ``` paulson@13140 ` 492` ``` apply (simp add: apply_equality [OF _ ord_iso_map_fun]) ``` paulson@13140 ` 493` ``` apply (unfold ord_iso_map_def) ``` paulson@13140 ` 494` ``` apply (blast intro: well_ord_iso_preserving, blast) ``` paulson@13140 ` 495` ```done ``` paulson@13140 ` 496` paulson@13140 ` 497` ```lemma ord_iso_map_ord_iso: ``` paulson@13140 ` 498` ``` "[| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) ``` paulson@13140 ` 499` ``` : ord_iso(domain(ord_iso_map(A,r,B,s)), r, ``` paulson@13140 ` 500` ``` range(ord_iso_map(A,r,B,s)), s)" ``` paulson@13140 ` 501` ```apply (rule well_ord_mono_ord_isoI) ``` paulson@13140 ` 502` ``` prefer 4 ``` paulson@13140 ` 503` ``` apply (rule converse_ord_iso_map [THEN subst]) ``` paulson@13140 ` 504` ``` apply (simp add: ord_iso_map_mono_map ``` paulson@13140 ` 505` ``` ord_iso_map_subset [THEN converse_converse]) ``` paulson@13140 ` 506` ```apply (blast intro!: domain_ord_iso_map range_ord_iso_map ``` paulson@13140 ` 507` ``` intro: well_ord_subset ord_iso_map_mono_map)+ ``` paulson@13140 ` 508` ```done ``` paulson@13140 ` 509` paulson@13140 ` 510` paulson@13140 ` 511` ```(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*) ``` paulson@13140 ` 512` ```lemma domain_ord_iso_map_subset: ``` paulson@13140 ` 513` ``` "[| well_ord(A,r); well_ord(B,s); ``` paulson@13140 ` 514` ``` a: A; a ~: domain(ord_iso_map(A,r,B,s)) |] ``` paulson@13140 ` 515` ``` ==> domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)" ``` paulson@13140 ` 516` ```apply (unfold ord_iso_map_def) ``` paulson@13140 ` 517` ```apply (safe intro!: predI) ``` paulson@13140 ` 518` ```(*Case analysis on xa vs a in r *) ``` paulson@13140 ` 519` ```apply (simp (no_asm_simp)) ``` paulson@13140 ` 520` ```apply (frule_tac A = A in well_ord_is_linear) ``` paulson@13140 ` 521` ```apply (rename_tac b y f) ``` paulson@13140 ` 522` ```apply (erule_tac x=b and y=a in linearE, assumption+) ``` paulson@13140 ` 523` ```(*Trivial case: b=a*) ``` paulson@13140 ` 524` ```apply clarify ``` paulson@13140 ` 525` ```apply blast ``` paulson@13140 ` 526` ```(*Harder case: : r*) ``` paulson@13140 ` 527` ```apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], ``` paulson@13140 ` 528` ``` (erule asm_rl predI predE)+) ``` paulson@13140 ` 529` ```apply (frule ord_iso_restrict_pred) ``` paulson@13140 ` 530` ``` apply (simp add: pred_iff) ``` paulson@13140 ` 531` ```apply (simp split: split_if_asm ``` paulson@13140 ` 532` ``` add: well_ord_is_trans_on trans_pred_pred_eq domain_UN domain_Union, blast) ``` paulson@13140 ` 533` ```done ``` paulson@13140 ` 534` paulson@13140 ` 535` ```(*For the 4-way case analysis in the main result*) ``` paulson@13140 ` 536` ```lemma domain_ord_iso_map_cases: ``` paulson@13140 ` 537` ``` "[| well_ord(A,r); well_ord(B,s) |] ``` paulson@13140 ` 538` ``` ==> domain(ord_iso_map(A,r,B,s)) = A | ``` paulson@13140 ` 539` ``` (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))" ``` paulson@13140 ` 540` ```apply (frule well_ord_is_wf) ``` paulson@13140 ` 541` ```apply (unfold wf_on_def wf_def) ``` paulson@13140 ` 542` ```apply (drule_tac x = "A-domain (ord_iso_map (A,r,B,s))" in spec) ``` paulson@13140 ` 543` ```apply safe ``` paulson@13140 ` 544` ```(*The first case: the domain equals A*) ``` paulson@13140 ` 545` ```apply (rule domain_ord_iso_map [THEN equalityI]) ``` paulson@13140 ` 546` ```apply (erule Diff_eq_0_iff [THEN iffD1]) ``` paulson@13140 ` 547` ```(*The other case: the domain equals an initial segment*) ``` paulson@13140 ` 548` ```apply (blast del: domainI subsetI ``` paulson@13140 ` 549` ``` elim!: predE ``` paulson@13140 ` 550` ``` intro!: domain_ord_iso_map_subset ``` paulson@13140 ` 551` ``` intro: subsetI)+ ``` paulson@13140 ` 552` ```done ``` paulson@13140 ` 553` paulson@13140 ` 554` ```(*As above, by duality*) ``` paulson@13140 ` 555` ```lemma range_ord_iso_map_cases: ``` paulson@13140 ` 556` ``` "[| well_ord(A,r); well_ord(B,s) |] ``` paulson@13140 ` 557` ``` ==> range(ord_iso_map(A,r,B,s)) = B | ``` paulson@13140 ` 558` ``` (EX y:B. range(ord_iso_map(A,r,B,s)) = pred(B,y,s))" ``` paulson@13140 ` 559` ```apply (rule converse_ord_iso_map [THEN subst]) ``` paulson@13140 ` 560` ```apply (simp add: domain_ord_iso_map_cases) ``` paulson@13140 ` 561` ```done ``` paulson@13140 ` 562` paulson@13140 ` 563` ```(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*) ``` paulson@13140 ` 564` ```lemma well_ord_trichotomy: ``` paulson@13140 ` 565` ``` "[| well_ord(A,r); well_ord(B,s) |] ``` paulson@13140 ` 566` ``` ==> ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) | ``` paulson@13140 ` 567` ``` (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | ``` paulson@13140 ` 568` ``` (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))" ``` paulson@13140 ` 569` ```apply (frule_tac B = B in domain_ord_iso_map_cases, assumption) ``` paulson@13140 ` 570` ```apply (frule_tac B = B in range_ord_iso_map_cases, assumption) ``` paulson@13140 ` 571` ```apply (drule ord_iso_map_ord_iso, assumption) ``` paulson@13140 ` 572` ```apply (elim disjE bexE) ``` paulson@13140 ` 573` ``` apply (simp_all add: bexI) ``` paulson@13140 ` 574` ```apply (rule wf_on_not_refl [THEN notE]) ``` paulson@13140 ` 575` ``` apply (erule well_ord_is_wf) ``` paulson@13140 ` 576` ``` apply assumption ``` paulson@13140 ` 577` ```apply (subgoal_tac ": ord_iso_map (A,r,B,s) ") ``` paulson@13140 ` 578` ``` apply (drule rangeI) ``` paulson@13140 ` 579` ``` apply (simp add: pred_def) ``` paulson@13140 ` 580` ```apply (unfold ord_iso_map_def, blast) ``` paulson@13140 ` 581` ```done ``` paulson@13140 ` 582` paulson@13140 ` 583` paulson@13140 ` 584` ```(*** Properties of converse(r), by Krzysztof Grabczewski ***) ``` paulson@13140 ` 585` paulson@13140 ` 586` ```lemma irrefl_converse: "irrefl(A,r) ==> irrefl(A,converse(r))" ``` paulson@13140 ` 587` ```by (unfold irrefl_def, blast) ``` paulson@13140 ` 588` paulson@13140 ` 589` ```lemma trans_on_converse: "trans[A](r) ==> trans[A](converse(r))" ``` paulson@13140 ` 590` ```by (unfold trans_on_def, blast) ``` paulson@13140 ` 591` paulson@13140 ` 592` ```lemma part_ord_converse: "part_ord(A,r) ==> part_ord(A,converse(r))" ``` paulson@13140 ` 593` ```apply (unfold part_ord_def) ``` paulson@13140 ` 594` ```apply (blast intro!: irrefl_converse trans_on_converse) ``` paulson@13140 ` 595` ```done ``` paulson@13140 ` 596` paulson@13140 ` 597` ```lemma linear_converse: "linear(A,r) ==> linear(A,converse(r))" ``` paulson@13140 ` 598` ```by (unfold linear_def, blast) ``` paulson@13140 ` 599` paulson@13140 ` 600` ```lemma tot_ord_converse: "tot_ord(A,r) ==> tot_ord(A,converse(r))" ``` paulson@13140 ` 601` ```apply (unfold tot_ord_def) ``` paulson@13140 ` 602` ```apply (blast intro!: part_ord_converse linear_converse) ``` paulson@13140 ` 603` ```done ``` paulson@13140 ` 604` paulson@13140 ` 605` paulson@13140 ` 606` ```(** By Krzysztof Grabczewski. ``` paulson@13140 ` 607` ``` Lemmas involving the first element of a well ordered set **) ``` paulson@13140 ` 608` paulson@13140 ` 609` ```lemma first_is_elem: "first(b,B,r) ==> b:B" ``` paulson@13140 ` 610` ```by (unfold first_def, blast) ``` paulson@13140 ` 611` paulson@13140 ` 612` ```lemma well_ord_imp_ex1_first: ``` paulson@13140 ` 613` ``` "[| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))" ``` paulson@13140 ` 614` ```apply (unfold well_ord_def wf_on_def wf_def first_def) ``` paulson@13140 ` 615` ```apply (elim conjE allE disjE, blast) ``` paulson@13140 ` 616` ```apply (erule bexE) ``` paulson@13140 ` 617` ```apply (rule_tac a = x in ex1I, auto) ``` paulson@13140 ` 618` ```apply (unfold tot_ord_def linear_def, blast) ``` paulson@13140 ` 619` ```done ``` paulson@13140 ` 620` paulson@13140 ` 621` ```lemma the_first_in: ``` paulson@13140 ` 622` ``` "[| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B" ``` paulson@13140 ` 623` ```apply (drule well_ord_imp_ex1_first, assumption+) ``` paulson@13140 ` 624` ```apply (rule first_is_elem) ``` paulson@13140 ` 625` ```apply (erule theI) ``` paulson@13140 ` 626` ```done ``` paulson@13140 ` 627` paulson@13140 ` 628` ```ML {* ``` paulson@13140 ` 629` ```val pred_def = thm "pred_def" ``` paulson@13140 ` 630` ```val linear_def = thm "linear_def" ``` paulson@13140 ` 631` ```val part_ord_def = thm "part_ord_def" ``` paulson@13140 ` 632` ```val tot_ord_def = thm "tot_ord_def" ``` paulson@13140 ` 633` ```val well_ord_def = thm "well_ord_def" ``` paulson@13140 ` 634` ```val ord_iso_def = thm "ord_iso_def" ``` paulson@13140 ` 635` ```val mono_map_def = thm "mono_map_def"; ``` paulson@13140 ` 636` paulson@13140 ` 637` ```val part_ord_Imp_asym = thm "part_ord_Imp_asym"; ``` paulson@13140 ` 638` ```val linearE = thm "linearE"; ``` paulson@13140 ` 639` ```val well_ordI = thm "well_ordI"; ``` paulson@13140 ` 640` ```val well_ord_is_wf = thm "well_ord_is_wf"; ``` paulson@13140 ` 641` ```val well_ord_is_trans_on = thm "well_ord_is_trans_on"; ``` paulson@13140 ` 642` ```val well_ord_is_linear = thm "well_ord_is_linear"; ``` paulson@13140 ` 643` ```val pred_iff = thm "pred_iff"; ``` paulson@13140 ` 644` ```val predI = thm "predI"; ``` paulson@13140 ` 645` ```val predE = thm "predE"; ``` paulson@13140 ` 646` ```val pred_subset_under = thm "pred_subset_under"; ``` paulson@13140 ` 647` ```val pred_subset = thm "pred_subset"; ``` paulson@13140 ` 648` ```val pred_pred_eq = thm "pred_pred_eq"; ``` paulson@13140 ` 649` ```val trans_pred_pred_eq = thm "trans_pred_pred_eq"; ``` paulson@13140 ` 650` ```val part_ord_subset = thm "part_ord_subset"; ``` paulson@13140 ` 651` ```val linear_subset = thm "linear_subset"; ``` paulson@13140 ` 652` ```val tot_ord_subset = thm "tot_ord_subset"; ``` paulson@13140 ` 653` ```val well_ord_subset = thm "well_ord_subset"; ``` paulson@13140 ` 654` ```val irrefl_Int_iff = thm "irrefl_Int_iff"; ``` paulson@13140 ` 655` ```val trans_on_Int_iff = thm "trans_on_Int_iff"; ``` paulson@13140 ` 656` ```val part_ord_Int_iff = thm "part_ord_Int_iff"; ``` paulson@13140 ` 657` ```val linear_Int_iff = thm "linear_Int_iff"; ``` paulson@13140 ` 658` ```val tot_ord_Int_iff = thm "tot_ord_Int_iff"; ``` paulson@13140 ` 659` ```val wf_on_Int_iff = thm "wf_on_Int_iff"; ``` paulson@13140 ` 660` ```val well_ord_Int_iff = thm "well_ord_Int_iff"; ``` paulson@13140 ` 661` ```val irrefl_0 = thm "irrefl_0"; ``` paulson@13140 ` 662` ```val trans_on_0 = thm "trans_on_0"; ``` paulson@13140 ` 663` ```val part_ord_0 = thm "part_ord_0"; ``` paulson@13140 ` 664` ```val linear_0 = thm "linear_0"; ``` paulson@13140 ` 665` ```val tot_ord_0 = thm "tot_ord_0"; ``` paulson@13140 ` 666` ```val wf_on_0 = thm "wf_on_0"; ``` paulson@13140 ` 667` ```val well_ord_0 = thm "well_ord_0"; ``` paulson@13140 ` 668` ```val tot_ord_unit = thm "tot_ord_unit"; ``` paulson@13140 ` 669` ```val wf_on_unit = thm "wf_on_unit"; ``` paulson@13140 ` 670` ```val well_ord_unit = thm "well_ord_unit"; ``` paulson@13140 ` 671` ```val mono_map_is_fun = thm "mono_map_is_fun"; ``` paulson@13140 ` 672` ```val mono_map_is_inj = thm "mono_map_is_inj"; ``` paulson@13140 ` 673` ```val ord_isoI = thm "ord_isoI"; ``` paulson@13140 ` 674` ```val ord_iso_is_mono_map = thm "ord_iso_is_mono_map"; ``` paulson@13140 ` 675` ```val ord_iso_is_bij = thm "ord_iso_is_bij"; ``` paulson@13140 ` 676` ```val ord_iso_apply = thm "ord_iso_apply"; ``` paulson@13140 ` 677` ```val ord_iso_converse = thm "ord_iso_converse"; ``` paulson@13140 ` 678` ```val ord_iso_refl = thm "ord_iso_refl"; ``` paulson@13140 ` 679` ```val ord_iso_sym = thm "ord_iso_sym"; ``` paulson@13140 ` 680` ```val mono_map_trans = thm "mono_map_trans"; ``` paulson@13140 ` 681` ```val ord_iso_trans = thm "ord_iso_trans"; ``` paulson@13140 ` 682` ```val mono_ord_isoI = thm "mono_ord_isoI"; ``` paulson@13140 ` 683` ```val well_ord_mono_ord_isoI = thm "well_ord_mono_ord_isoI"; ``` paulson@13140 ` 684` ```val part_ord_ord_iso = thm "part_ord_ord_iso"; ``` paulson@13140 ` 685` ```val linear_ord_iso = thm "linear_ord_iso"; ``` paulson@13140 ` 686` ```val wf_on_ord_iso = thm "wf_on_ord_iso"; ``` paulson@13140 ` 687` ```val well_ord_ord_iso = thm "well_ord_ord_iso"; ``` paulson@13140 ` 688` ```val well_ord_iso_predE = thm "well_ord_iso_predE"; ``` paulson@13140 ` 689` ```val well_ord_iso_pred_eq = thm "well_ord_iso_pred_eq"; ``` paulson@13140 ` 690` ```val ord_iso_image_pred = thm "ord_iso_image_pred"; ``` paulson@13140 ` 691` ```val ord_iso_restrict_pred = thm "ord_iso_restrict_pred"; ``` paulson@13140 ` 692` ```val well_ord_iso_preserving = thm "well_ord_iso_preserving"; ``` paulson@13140 ` 693` ```val well_ord_iso_unique = thm "well_ord_iso_unique"; ``` paulson@13140 ` 694` ```val ord_iso_map_subset = thm "ord_iso_map_subset"; ``` paulson@13140 ` 695` ```val domain_ord_iso_map = thm "domain_ord_iso_map"; ``` paulson@13140 ` 696` ```val range_ord_iso_map = thm "range_ord_iso_map"; ``` paulson@13140 ` 697` ```val converse_ord_iso_map = thm "converse_ord_iso_map"; ``` paulson@13140 ` 698` ```val function_ord_iso_map = thm "function_ord_iso_map"; ``` paulson@13140 ` 699` ```val ord_iso_map_fun = thm "ord_iso_map_fun"; ``` paulson@13140 ` 700` ```val ord_iso_map_mono_map = thm "ord_iso_map_mono_map"; ``` paulson@13140 ` 701` ```val ord_iso_map_ord_iso = thm "ord_iso_map_ord_iso"; ``` paulson@13140 ` 702` ```val domain_ord_iso_map_subset = thm "domain_ord_iso_map_subset"; ``` paulson@13140 ` 703` ```val domain_ord_iso_map_cases = thm "domain_ord_iso_map_cases"; ``` paulson@13140 ` 704` ```val range_ord_iso_map_cases = thm "range_ord_iso_map_cases"; ``` paulson@13140 ` 705` ```val well_ord_trichotomy = thm "well_ord_trichotomy"; ``` paulson@13140 ` 706` ```val irrefl_converse = thm "irrefl_converse"; ``` paulson@13140 ` 707` ```val trans_on_converse = thm "trans_on_converse"; ``` paulson@13140 ` 708` ```val part_ord_converse = thm "part_ord_converse"; ``` paulson@13140 ` 709` ```val linear_converse = thm "linear_converse"; ``` paulson@13140 ` 710` ```val tot_ord_converse = thm "tot_ord_converse"; ``` paulson@13140 ` 711` ```val first_is_elem = thm "first_is_elem"; ``` paulson@13140 ` 712` ```val well_ord_imp_ex1_first = thm "well_ord_imp_ex1_first"; ``` paulson@13140 ` 713` ```val the_first_in = thm "the_first_in"; ``` paulson@13140 ` 714` ```*} ``` paulson@13140 ` 715` lcp@435 ` 716` ```end ```