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