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