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