src/ZF/Order.ML
 author nipkow Tue Sep 21 19:11:07 1999 +0200 (1999-09-21) changeset 7570 a9391550eea1 parent 7499 23e090051cb8 child 8201 a81d18b0a9b1 permissions -rw-r--r--
Mod because of new solver interface.
 clasohm@1461 ` 1` ```(* Title: ZF/Order.ML ``` lcp@435 ` 2` ``` ID: \$Id\$ ``` clasohm@1461 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` lcp@435 ` 4` ``` Copyright 1994 University of Cambridge ``` lcp@435 ` 5` lcp@789 ` 6` ```Orders in Zermelo-Fraenkel Set Theory ``` lcp@789 ` 7` lcp@789 ` 8` ```Results from the book "Set Theory: an Introduction to Independence Proofs" ``` clasohm@1461 ` 9` ``` by Ken Kunen. Chapter 1, section 6. ``` lcp@435 ` 10` ```*) ``` lcp@435 ` 11` lcp@435 ` 12` ```open Order; ``` lcp@435 ` 13` lcp@435 ` 14` ```(** Basic properties of the definitions **) ``` lcp@435 ` 15` lcp@789 ` 16` ```(*needed?*) ``` wenzelm@5067 ` 17` ```Goalw [part_ord_def, irrefl_def, trans_on_def, asym_def] ``` paulson@5147 ` 18` ``` "part_ord(A,r) ==> asym(r Int A*A)"; ``` paulson@2925 ` 19` ```by (Blast_tac 1); ``` clasohm@760 ` 20` ```qed "part_ord_Imp_asym"; ``` lcp@435 ` 21` paulson@5268 ` 22` ```val major::premx::premy::prems = Goalw [linear_def] ``` lcp@789 ` 23` ``` "[| linear(A,r); x:A; y:A; \ ``` lcp@789 ` 24` ```\ :r ==> P; x=y ==> P; :r ==> P |] ==> P"; ``` lcp@789 ` 25` ```by (cut_facts_tac [major,premx,premy] 1); ``` lcp@789 ` 26` ```by (REPEAT_FIRST (eresolve_tac [ballE,disjE])); ``` lcp@789 ` 27` ```by (EVERY1 (map etac prems)); ``` lcp@789 ` 28` ```by (ALLGOALS contr_tac); ``` lcp@789 ` 29` ```qed "linearE"; ``` lcp@789 ` 30` lcp@789 ` 31` ```(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*) ``` lcp@789 ` 32` ```val linear_case_tac = ``` lcp@789 ` 33` ``` SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1, ``` clasohm@1461 ` 34` ``` REPEAT_SOME (assume_tac ORELSE' contr_tac)]); ``` lcp@789 ` 35` lcp@789 ` 36` ```(** General properties of well_ord **) ``` lcp@789 ` 37` wenzelm@5067 ` 38` ```Goalw [irrefl_def, part_ord_def, tot_ord_def, ``` clasohm@1461 ` 39` ``` trans_on_def, well_ord_def] ``` paulson@5147 ` 40` ``` "[| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"; ``` wenzelm@4091 ` 41` ```by (asm_simp_tac (simpset() addsimps [wf_on_not_refl]) 1); ``` wenzelm@4091 ` 42` ```by (fast_tac (claset() addEs [linearE, wf_on_asym, wf_on_chain3]) 1); ``` lcp@789 ` 43` ```qed "well_ordI"; ``` lcp@789 ` 44` wenzelm@5067 ` 45` ```Goalw [well_ord_def] ``` paulson@5147 ` 46` ``` "well_ord(A,r) ==> wf[A](r)"; ``` paulson@4152 ` 47` ```by Safe_tac; ``` lcp@789 ` 48` ```qed "well_ord_is_wf"; ``` lcp@789 ` 49` wenzelm@5067 ` 50` ```Goalw [well_ord_def, tot_ord_def, part_ord_def] ``` paulson@5147 ` 51` ``` "well_ord(A,r) ==> trans[A](r)"; ``` paulson@4152 ` 52` ```by Safe_tac; ``` lcp@789 ` 53` ```qed "well_ord_is_trans_on"; ``` lcp@484 ` 54` wenzelm@5067 ` 55` ```Goalw [well_ord_def, tot_ord_def] ``` paulson@5147 ` 56` ``` "well_ord(A,r) ==> linear(A,r)"; ``` paulson@2925 ` 57` ```by (Blast_tac 1); ``` lcp@789 ` 58` ```qed "well_ord_is_linear"; ``` lcp@789 ` 59` lcp@789 ` 60` lcp@789 ` 61` ```(** Derived rules for pred(A,x,r) **) ``` lcp@789 ` 62` wenzelm@5067 ` 63` ```Goalw [pred_def] "y : pred(A,x,r) <-> :r & y:A"; ``` paulson@2925 ` 64` ```by (Blast_tac 1); ``` lcp@789 ` 65` ```qed "pred_iff"; ``` lcp@789 ` 66` lcp@789 ` 67` ```bind_thm ("predI", conjI RS (pred_iff RS iffD2)); ``` lcp@789 ` 68` paulson@5268 ` 69` ```val [major,minor] = Goalw [pred_def] ``` lcp@789 ` 70` ``` "[| y: pred(A,x,r); [| y:A; :r |] ==> P |] ==> P"; ``` lcp@789 ` 71` ```by (rtac (major RS CollectE) 1); ``` lcp@789 ` 72` ```by (REPEAT (ares_tac [minor] 1)); ``` lcp@789 ` 73` ```qed "predE"; ``` lcp@789 ` 74` wenzelm@5067 ` 75` ```Goalw [pred_def] "pred(A,x,r) <= r -`` {x}"; ``` paulson@2925 ` 76` ```by (Blast_tac 1); ``` lcp@789 ` 77` ```qed "pred_subset_under"; ``` lcp@789 ` 78` wenzelm@5067 ` 79` ```Goalw [pred_def] "pred(A,x,r) <= A"; ``` paulson@2925 ` 80` ```by (Blast_tac 1); ``` lcp@789 ` 81` ```qed "pred_subset"; ``` lcp@789 ` 82` wenzelm@5067 ` 83` ```Goalw [pred_def] ``` lcp@789 ` 84` ``` "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)"; ``` paulson@2925 ` 85` ```by (Blast_tac 1); ``` lcp@789 ` 86` ```qed "pred_pred_eq"; ``` lcp@789 ` 87` wenzelm@5067 ` 88` ```Goalw [trans_on_def, pred_def] ``` paulson@5147 ` 89` ``` "[| trans[A](r); :r; x:A; y:A \ ``` lcp@789 ` 90` ```\ |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"; ``` paulson@2925 ` 91` ```by (Blast_tac 1); ``` lcp@789 ` 92` ```qed "trans_pred_pred_eq"; ``` lcp@789 ` 93` lcp@836 ` 94` lcp@789 ` 95` ```(** The ordering's properties hold over all subsets of its domain ``` lcp@789 ` 96` ``` [including initial segments of the form pred(A,x,r) **) ``` lcp@484 ` 97` lcp@484 ` 98` ```(*Note: a relation s such that s<=r need not be a partial ordering*) ``` wenzelm@5067 ` 99` ```Goalw [part_ord_def, irrefl_def, trans_on_def] ``` paulson@5147 ` 100` ``` "[| part_ord(A,r); B<=A |] ==> part_ord(B,r)"; ``` paulson@2925 ` 101` ```by (Blast_tac 1); ``` clasohm@760 ` 102` ```qed "part_ord_subset"; ``` lcp@484 ` 103` wenzelm@5067 ` 104` ```Goalw [linear_def] ``` paulson@5147 ` 105` ``` "[| linear(A,r); B<=A |] ==> linear(B,r)"; ``` paulson@2925 ` 106` ```by (Blast_tac 1); ``` clasohm@760 ` 107` ```qed "linear_subset"; ``` lcp@484 ` 108` wenzelm@5067 ` 109` ```Goalw [tot_ord_def] ``` paulson@5147 ` 110` ``` "[| tot_ord(A,r); B<=A |] ==> tot_ord(B,r)"; ``` wenzelm@4091 ` 111` ```by (fast_tac (claset() addSEs [part_ord_subset, linear_subset]) 1); ``` clasohm@760 ` 112` ```qed "tot_ord_subset"; ``` lcp@484 ` 113` wenzelm@5067 ` 114` ```Goalw [well_ord_def] ``` paulson@5147 ` 115` ``` "[| well_ord(A,r); B<=A |] ==> well_ord(B,r)"; ``` wenzelm@4091 ` 116` ```by (fast_tac (claset() addSEs [tot_ord_subset, wf_on_subset_A]) 1); ``` clasohm@760 ` 117` ```qed "well_ord_subset"; ``` lcp@484 ` 118` lcp@484 ` 119` lcp@836 ` 120` ```(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **) ``` lcp@836 ` 121` wenzelm@5067 ` 122` ```Goalw [irrefl_def] "irrefl(A,r Int A*A) <-> irrefl(A,r)"; ``` paulson@2925 ` 123` ```by (Blast_tac 1); ``` lcp@836 ` 124` ```qed "irrefl_Int_iff"; ``` lcp@836 ` 125` wenzelm@5067 ` 126` ```Goalw [trans_on_def] "trans[A](r Int A*A) <-> trans[A](r)"; ``` paulson@2925 ` 127` ```by (Blast_tac 1); ``` lcp@836 ` 128` ```qed "trans_on_Int_iff"; ``` lcp@836 ` 129` wenzelm@5067 ` 130` ```Goalw [part_ord_def] "part_ord(A,r Int A*A) <-> part_ord(A,r)"; ``` wenzelm@4091 ` 131` ```by (simp_tac (simpset() addsimps [irrefl_Int_iff, trans_on_Int_iff]) 1); ``` lcp@836 ` 132` ```qed "part_ord_Int_iff"; ``` lcp@836 ` 133` wenzelm@5067 ` 134` ```Goalw [linear_def] "linear(A,r Int A*A) <-> linear(A,r)"; ``` paulson@2925 ` 135` ```by (Blast_tac 1); ``` lcp@836 ` 136` ```qed "linear_Int_iff"; ``` lcp@836 ` 137` wenzelm@5067 ` 138` ```Goalw [tot_ord_def] "tot_ord(A,r Int A*A) <-> tot_ord(A,r)"; ``` wenzelm@4091 ` 139` ```by (simp_tac (simpset() addsimps [part_ord_Int_iff, linear_Int_iff]) 1); ``` lcp@836 ` 140` ```qed "tot_ord_Int_iff"; ``` lcp@836 ` 141` wenzelm@5067 ` 142` ```Goalw [wf_on_def, wf_def] "wf[A](r Int A*A) <-> wf[A](r)"; ``` paulson@4311 ` 143` ```by (Fast_tac 1); (*10 times faster than Blast_tac!*) ``` lcp@836 ` 144` ```qed "wf_on_Int_iff"; ``` lcp@836 ` 145` wenzelm@5067 ` 146` ```Goalw [well_ord_def] "well_ord(A,r Int A*A) <-> well_ord(A,r)"; ``` wenzelm@4091 ` 147` ```by (simp_tac (simpset() addsimps [tot_ord_Int_iff, wf_on_Int_iff]) 1); ``` lcp@836 ` 148` ```qed "well_ord_Int_iff"; ``` lcp@836 ` 149` lcp@836 ` 150` lcp@848 ` 151` ```(** Relations over the Empty Set **) ``` lcp@848 ` 152` wenzelm@5067 ` 153` ```Goalw [irrefl_def] "irrefl(0,r)"; ``` paulson@2925 ` 154` ```by (Blast_tac 1); ``` lcp@848 ` 155` ```qed "irrefl_0"; ``` lcp@848 ` 156` wenzelm@5067 ` 157` ```Goalw [trans_on_def] "trans[0](r)"; ``` paulson@2925 ` 158` ```by (Blast_tac 1); ``` lcp@848 ` 159` ```qed "trans_on_0"; ``` lcp@848 ` 160` wenzelm@5067 ` 161` ```Goalw [part_ord_def] "part_ord(0,r)"; ``` wenzelm@4091 ` 162` ```by (simp_tac (simpset() addsimps [irrefl_0, trans_on_0]) 1); ``` lcp@848 ` 163` ```qed "part_ord_0"; ``` lcp@848 ` 164` wenzelm@5067 ` 165` ```Goalw [linear_def] "linear(0,r)"; ``` paulson@2925 ` 166` ```by (Blast_tac 1); ``` lcp@848 ` 167` ```qed "linear_0"; ``` lcp@848 ` 168` wenzelm@5067 ` 169` ```Goalw [tot_ord_def] "tot_ord(0,r)"; ``` wenzelm@4091 ` 170` ```by (simp_tac (simpset() addsimps [part_ord_0, linear_0]) 1); ``` lcp@848 ` 171` ```qed "tot_ord_0"; ``` lcp@848 ` 172` wenzelm@5067 ` 173` ```Goalw [wf_on_def, wf_def] "wf[0](r)"; ``` paulson@2925 ` 174` ```by (Blast_tac 1); ``` lcp@848 ` 175` ```qed "wf_on_0"; ``` lcp@848 ` 176` wenzelm@5067 ` 177` ```Goalw [well_ord_def] "well_ord(0,r)"; ``` wenzelm@4091 ` 178` ```by (simp_tac (simpset() addsimps [tot_ord_0, wf_on_0]) 1); ``` lcp@848 ` 179` ```qed "well_ord_0"; ``` lcp@836 ` 180` lcp@836 ` 181` paulson@5262 ` 182` ```(** The unit set is well-ordered by the empty relation (Grabczewski) **) ``` paulson@5262 ` 183` paulson@5262 ` 184` ```Goalw [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def] ``` paulson@5262 ` 185` ``` "tot_ord({a},0)"; ``` paulson@5262 ` 186` ```by (Simp_tac 1); ``` paulson@5262 ` 187` ```qed "tot_ord_unit"; ``` paulson@5262 ` 188` paulson@5262 ` 189` ```Goalw [wf_on_def, wf_def] "wf[{a}](0)"; ``` paulson@5262 ` 190` ```by (Fast_tac 1); ``` paulson@5262 ` 191` ```qed "wf_on_unit"; ``` paulson@5262 ` 192` paulson@5262 ` 193` ```Goalw [well_ord_def] "well_ord({a},0)"; ``` paulson@5262 ` 194` ```by (simp_tac (simpset() addsimps [tot_ord_unit, wf_on_unit]) 1); ``` paulson@5262 ` 195` ```qed "well_ord_unit"; ``` paulson@5262 ` 196` paulson@5262 ` 197` lcp@789 ` 198` ```(** Order-preserving (monotone) maps **) ``` lcp@789 ` 199` wenzelm@5067 ` 200` ```Goalw [mono_map_def] ``` paulson@5147 ` 201` ``` "f: mono_map(A,r,B,s) ==> f: A->B"; ``` lcp@789 ` 202` ```by (etac CollectD1 1); ``` lcp@789 ` 203` ```qed "mono_map_is_fun"; ``` lcp@789 ` 204` wenzelm@5067 ` 205` ```Goalw [mono_map_def, inj_def] ``` paulson@5147 ` 206` ``` "[| linear(A,r); wf[B](s); f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"; ``` paulson@3736 ` 207` ```by (Clarify_tac 1); ``` lcp@789 ` 208` ```by (linear_case_tac 1); ``` lcp@789 ` 209` ```by (REPEAT ``` lcp@789 ` 210` ``` (EVERY [eresolve_tac [wf_on_not_refl RS notE] 1, ``` clasohm@1461 ` 211` ``` etac ssubst 2, ``` paulson@2469 ` 212` ``` Fast_tac 2, ``` clasohm@1461 ` 213` ``` REPEAT (ares_tac [apply_type] 1)])); ``` lcp@789 ` 214` ```qed "mono_map_is_inj"; ``` lcp@789 ` 215` lcp@789 ` 216` lcp@789 ` 217` ```(** Order-isomorphisms -- or similarities, as Suppes calls them **) ``` lcp@789 ` 218` paulson@5268 ` 219` ```val prems = Goalw [ord_iso_def] ``` clasohm@1461 ` 220` ``` "[| f: bij(A, B); \ ``` clasohm@1461 ` 221` ```\ !!x y. [| x:A; y:A |] ==> : r <-> : s \ ``` lcp@848 ` 222` ```\ |] ==> f: ord_iso(A,r,B,s)"; ``` wenzelm@4091 ` 223` ```by (blast_tac (claset() addSIs prems) 1); ``` lcp@848 ` 224` ```qed "ord_isoI"; ``` lcp@848 ` 225` wenzelm@5067 ` 226` ```Goalw [ord_iso_def, mono_map_def] ``` paulson@5147 ` 227` ``` "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)"; ``` wenzelm@4091 ` 228` ```by (blast_tac (claset() addSDs [bij_is_fun]) 1); ``` lcp@789 ` 229` ```qed "ord_iso_is_mono_map"; ``` lcp@435 ` 230` wenzelm@5067 ` 231` ```Goalw [ord_iso_def] ``` paulson@5147 ` 232` ``` "f: ord_iso(A,r,B,s) ==> f: bij(A,B)"; ``` lcp@435 ` 233` ```by (etac CollectD1 1); ``` clasohm@760 ` 234` ```qed "ord_iso_is_bij"; ``` lcp@435 ` 235` lcp@789 ` 236` ```(*Needed? But ord_iso_converse is!*) ``` wenzelm@5067 ` 237` ```Goalw [ord_iso_def] ``` paulson@5147 ` 238` ``` "[| f: ord_iso(A,r,B,s); : r; x:A; y:A |] ==> \ ``` lcp@435 ` 239` ```\ : s"; ``` paulson@2925 ` 240` ```by (Blast_tac 1); ``` clasohm@760 ` 241` ```qed "ord_iso_apply"; ``` lcp@435 ` 242` paulson@6176 ` 243` ```(*Rewriting with bijections and converse (function inverse)*) ``` paulson@6176 ` 244` ```val bij_inverse_ss = ``` nipkow@7570 ` 245` ``` simpset() setSolver (mk_solver "" ``` nipkow@7570 ` 246` ``` (type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj, ``` nipkow@7570 ` 247` ``` inj_is_fun, comp_fun, comp_bij]))) ``` paulson@6176 ` 248` ``` addsimps [right_inverse_bij]; ``` paulson@6176 ` 249` wenzelm@5067 ` 250` ```Goalw [ord_iso_def] ``` paulson@5147 ` 251` ``` "[| f: ord_iso(A,r,B,s); : s; x:B; y:B |] ==> \ ``` lcp@435 ` 252` ```\ : r"; ``` lcp@437 ` 253` ```by (etac CollectE 1); ``` lcp@437 ` 254` ```by (etac (bspec RS bspec RS iffD2) 1); ``` lcp@435 ` 255` ```by (REPEAT (eresolve_tac [asm_rl, ``` clasohm@1461 ` 256` ``` bij_converse_bij RS bij_is_fun RS apply_type] 1)); ``` paulson@6176 ` 257` ```by (asm_simp_tac bij_inverse_ss 1); ``` clasohm@760 ` 258` ```qed "ord_iso_converse"; ``` lcp@435 ` 259` lcp@812 ` 260` lcp@812 ` 261` ```(** Symmetry and Transitivity Rules **) ``` lcp@812 ` 262` lcp@848 ` 263` ```(*Reflexivity of similarity*) ``` wenzelm@5067 ` 264` ```Goal "id(A): ord_iso(A,r,A,r)"; ``` lcp@848 ` 265` ```by (resolve_tac [id_bij RS ord_isoI] 1); ``` paulson@2469 ` 266` ```by (Asm_simp_tac 1); ``` lcp@848 ` 267` ```qed "ord_iso_refl"; ``` lcp@848 ` 268` lcp@848 ` 269` ```(*Symmetry of similarity*) ``` paulson@6153 ` 270` ```Goalw [ord_iso_def] "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"; ``` paulson@6153 ` 271` ```by (force_tac (claset(), bij_inverse_ss) 1); ``` clasohm@782 ` 272` ```qed "ord_iso_sym"; ``` lcp@769 ` 273` lcp@848 ` 274` ```(*Transitivity of similarity*) ``` wenzelm@5067 ` 275` ```Goalw [mono_map_def] ``` paulson@5147 ` 276` ``` "[| g: mono_map(A,r,B,s); f: mono_map(B,s,C,t) |] ==> \ ``` lcp@812 ` 277` ```\ (f O g): mono_map(A,r,C,t)"; ``` paulson@6153 ` 278` ```by (force_tac (claset(), bij_inverse_ss) 1); ``` lcp@812 ` 279` ```qed "mono_map_trans"; ``` lcp@812 ` 280` lcp@812 ` 281` ```(*Transitivity of similarity: the order-isomorphism relation*) ``` wenzelm@5067 ` 282` ```Goalw [ord_iso_def] ``` paulson@5147 ` 283` ``` "[| g: ord_iso(A,r,B,s); f: ord_iso(B,s,C,t) |] ==> \ ``` lcp@789 ` 284` ```\ (f O g): ord_iso(A,r,C,t)"; ``` paulson@6153 ` 285` ```by (force_tac (claset(), bij_inverse_ss) 1); ``` lcp@789 ` 286` ```qed "ord_iso_trans"; ``` lcp@789 ` 287` lcp@789 ` 288` ```(** Two monotone maps can make an order-isomorphism **) ``` lcp@789 ` 289` wenzelm@5067 ` 290` ```Goalw [ord_iso_def, mono_map_def] ``` paulson@5147 ` 291` ``` "[| f: mono_map(A,r,B,s); g: mono_map(B,s,A,r); \ ``` lcp@789 ` 292` ```\ f O g = id(B); g O f = id(A) |] ==> f: ord_iso(A,r,B,s)"; ``` paulson@4152 ` 293` ```by Safe_tac; ``` lcp@789 ` 294` ```by (REPEAT_FIRST (ares_tac [fg_imp_bijective])); ``` paulson@2925 ` 295` ```by (Blast_tac 1); ``` lcp@789 ` 296` ```by (subgoal_tac " : r" 1); ``` wenzelm@4091 ` 297` ```by (blast_tac (claset() addIs [apply_funtype]) 2); ``` wenzelm@4091 ` 298` ```by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff RS iffD1]) 1); ``` lcp@789 ` 299` ```qed "mono_ord_isoI"; ``` lcp@789 ` 300` paulson@5268 ` 301` ```Goal "[| well_ord(A,r); well_ord(B,s); \ ``` clasohm@1461 ` 302` ```\ f: mono_map(A,r,B,s); converse(f): mono_map(B,s,A,r) \ ``` lcp@789 ` 303` ```\ |] ==> f: ord_iso(A,r,B,s)"; ``` lcp@789 ` 304` ```by (REPEAT (ares_tac [mono_ord_isoI] 1)); ``` lcp@789 ` 305` ```by (forward_tac [mono_map_is_fun RS fun_is_rel] 1); ``` lcp@789 ` 306` ```by (etac (converse_converse RS subst) 1 THEN rtac left_comp_inverse 1); ``` lcp@789 ` 307` ```by (DEPTH_SOLVE (ares_tac [mono_map_is_inj, left_comp_inverse] 1 ``` lcp@789 ` 308` ``` ORELSE eresolve_tac [well_ord_is_linear, well_ord_is_wf] 1)); ``` lcp@789 ` 309` ```qed "well_ord_mono_ord_isoI"; ``` lcp@789 ` 310` lcp@789 ` 311` lcp@789 ` 312` ```(** Order-isomorphisms preserve the ordering's properties **) ``` lcp@789 ` 313` wenzelm@5067 ` 314` ```Goalw [part_ord_def, irrefl_def, trans_on_def, ord_iso_def] ``` paulson@5147 ` 315` ``` "[| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)"; ``` paulson@2469 ` 316` ```by (Asm_simp_tac 1); ``` wenzelm@4091 ` 317` ```by (fast_tac (claset() addIs [bij_is_fun RS apply_type]) 1); ``` lcp@789 ` 318` ```qed "part_ord_ord_iso"; ``` lcp@435 ` 319` wenzelm@5067 ` 320` ```Goalw [linear_def, ord_iso_def] ``` paulson@5147 ` 321` ``` "[| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)"; ``` paulson@2469 ` 322` ```by (Asm_simp_tac 1); ``` paulson@4152 ` 323` ```by Safe_tac; ``` lcp@789 ` 324` ```by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1); ``` wenzelm@4091 ` 325` ```by (safe_tac (claset() addSEs [bij_is_fun RS apply_type])); ``` lcp@789 ` 326` ```by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); ``` paulson@6176 ` 327` ```by (asm_full_simp_tac bij_inverse_ss 1); ``` lcp@789 ` 328` ```qed "linear_ord_iso"; ``` lcp@789 ` 329` wenzelm@5067 ` 330` ```Goalw [wf_on_def, wf_def, ord_iso_def] ``` paulson@5147 ` 331` ``` "[| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)"; ``` lcp@789 ` 332` ```(*reversed &-congruence rule handles context of membership in A*) ``` wenzelm@4091 ` 333` ```by (asm_full_simp_tac (simpset() addcongs [conj_cong2]) 1); ``` paulson@4152 ` 334` ```by Safe_tac; ``` lcp@789 ` 335` ```by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1); ``` wenzelm@4091 ` 336` ```by (safe_tac (claset() addSIs [equalityI])); ``` paulson@2925 ` 337` ```by (ALLGOALS (blast_tac ``` wenzelm@4091 ` 338` ``` (claset() addSDs [equalityD1] addIs [bij_is_fun RS apply_type]))); ``` lcp@789 ` 339` ```qed "wf_on_ord_iso"; ``` lcp@789 ` 340` wenzelm@5067 ` 341` ```Goalw [well_ord_def, tot_ord_def] ``` paulson@5147 ` 342` ``` "[| well_ord(B,s); f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)"; ``` lcp@789 ` 343` ```by (fast_tac ``` wenzelm@4091 ` 344` ``` (claset() addSEs [part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso]) 1); ``` lcp@789 ` 345` ```qed "well_ord_ord_iso"; ``` lcp@789 ` 346` lcp@789 ` 347` lcp@789 ` 348` ```(*** Main results of Kunen, Chapter 1 section 6 ***) ``` lcp@435 ` 349` lcp@812 ` 350` ```(*Inductive argument for Kunen's Lemma 6.1, etc. ``` lcp@812 ` 351` ``` Simple proof from Halmos, page 72*) ``` wenzelm@5067 ` 352` ```Goalw [well_ord_def, ord_iso_def] ``` paulson@5147 ` 353` ``` "[| well_ord(A,r); f: ord_iso(A,r, A',r); A'<= A; y: A |] \ ``` lcp@812 ` 354` ```\ ==> ~ : r"; ``` lcp@812 ` 355` ```by (REPEAT (eresolve_tac [conjE, CollectE] 1)); ``` lcp@435 ` 356` ```by (wf_on_ind_tac "y" [] 1); ``` lcp@812 ` 357` ```by (dres_inst_tac [("a","y1")] (bij_is_fun RS apply_type) 1); ``` lcp@812 ` 358` ```by (assume_tac 1); ``` paulson@2925 ` 359` ```by (Blast_tac 1); ``` lcp@812 ` 360` ```qed "well_ord_iso_subset_lemma"; ``` lcp@435 ` 361` lcp@435 ` 362` ```(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment ``` lcp@435 ` 363` ``` of a well-ordering*) ``` paulson@5268 ` 364` ```Goal "[| well_ord(A,r); f : ord_iso(A, r, pred(A,x,r), r); x:A |] ==> P"; ``` lcp@812 ` 365` ```by (metacut_tac well_ord_iso_subset_lemma 1); ``` lcp@812 ` 366` ```by (REPEAT_FIRST (ares_tac [pred_subset])); ``` lcp@812 ` 367` ```(*Now we know f`x < x *) ``` lcp@435 ` 368` ```by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type), ``` clasohm@1461 ` 369` ``` assume_tac]); ``` lcp@812 ` 370` ```(*Now we also know f`x : pred(A,x,r); contradiction! *) ``` wenzelm@4091 ` 371` ```by (asm_full_simp_tac (simpset() addsimps [well_ord_def, pred_def]) 1); ``` lcp@789 ` 372` ```qed "well_ord_iso_predE"; ``` lcp@789 ` 373` lcp@789 ` 374` ```(*Simple consequence of Lemma 6.1*) ``` paulson@5268 ` 375` ```Goal "[| well_ord(A,r); f : ord_iso(pred(A,a,r), r, pred(A,c,r), r); \ ``` paulson@6153 ` 376` ```\ a:A; c:A |] ==> a=c"; ``` wenzelm@7499 ` 377` ```by (ftac well_ord_is_trans_on 1); ``` wenzelm@7499 ` 378` ```by (ftac well_ord_is_linear 1); ``` lcp@789 ` 379` ```by (linear_case_tac 1); ``` lcp@789 ` 380` ```by (dtac ord_iso_sym 1); ``` paulson@6153 ` 381` ```(*two symmetric cases*) ``` paulson@6153 ` 382` ```by (auto_tac (claset() addSEs [pred_subset RSN (2, well_ord_subset) RS ``` paulson@6153 ` 383` ``` well_ord_iso_predE] ``` paulson@6153 ` 384` ``` addSIs [predI], ``` paulson@6153 ` 385` ``` simpset() addsimps [trans_pred_pred_eq])); ``` lcp@789 ` 386` ```qed "well_ord_iso_pred_eq"; ``` lcp@789 ` 387` lcp@789 ` 388` ```(*Does not assume r is a wellordering!*) ``` wenzelm@5067 ` 389` ```Goalw [ord_iso_def, pred_def] ``` paulson@5147 ` 390` ``` "[| f : ord_iso(A,r,B,s); a:A |] ==> \ ``` lcp@789 ` 391` ```\ f `` pred(A,a,r) = pred(B, f`a, s)"; ``` lcp@789 ` 392` ```by (etac CollectE 1); ``` lcp@789 ` 393` ```by (asm_simp_tac ``` wenzelm@4091 ` 394` ``` (simpset() addsimps [[bij_is_fun, Collect_subset] MRS image_fun]) 1); ``` paulson@2493 ` 395` ```by (rtac equalityI 1); ``` wenzelm@4091 ` 396` ```by (safe_tac (claset() addSEs [bij_is_fun RS apply_type])); ``` clasohm@1461 ` 397` ```by (rtac RepFun_eqI 1); ``` wenzelm@4091 ` 398` ```by (blast_tac (claset() addSIs [right_inverse_bij RS sym]) 1); ``` lcp@812 ` 399` ```by (asm_simp_tac bij_inverse_ss 1); ``` lcp@789 ` 400` ```qed "ord_iso_image_pred"; ``` lcp@435 ` 401` lcp@789 ` 402` ```(*But in use, A and B may themselves be initial segments. Then use ``` lcp@789 ` 403` ``` trans_pred_pred_eq to simplify the pred(pred...) terms. See just below.*) ``` paulson@5268 ` 404` ```Goal "[| f : ord_iso(A,r,B,s); a:A |] ==> \ ``` lcp@789 ` 405` ```\ restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"; ``` wenzelm@4091 ` 406` ```by (asm_simp_tac (simpset() addsimps [ord_iso_image_pred RS sym]) 1); ``` clasohm@1461 ` 407` ```by (rewtac ord_iso_def); ``` lcp@848 ` 408` ```by (etac CollectE 1); ``` lcp@848 ` 409` ```by (rtac CollectI 1); ``` wenzelm@4091 ` 410` ```by (asm_full_simp_tac (simpset() addsimps [pred_def]) 2); ``` lcp@789 ` 411` ```by (eresolve_tac [[bij_is_inj, pred_subset] MRS restrict_bij] 1); ``` lcp@789 ` 412` ```qed "ord_iso_restrict_pred"; ``` lcp@789 ` 413` lcp@789 ` 414` ```(*Tricky; a lot of forward proof!*) ``` paulson@5268 ` 415` ```Goal "[| well_ord(A,r); well_ord(B,s); : r; \ ``` clasohm@1461 ` 416` ```\ f : ord_iso(pred(A,a,r), r, pred(B,b,s), s); \ ``` clasohm@1461 ` 417` ```\ g : ord_iso(pred(A,c,r), r, pred(B,d,s), s); \ ``` lcp@789 ` 418` ```\ a:A; c:A; b:B; d:B |] ==> : s"; ``` lcp@789 ` 419` ```by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1 THEN ``` lcp@789 ` 420` ``` REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1)); ``` lcp@789 ` 421` ```by (subgoal_tac "b = g`a" 1); ``` paulson@2469 ` 422` ```by (Asm_simp_tac 1); ``` clasohm@1461 ` 423` ```by (rtac well_ord_iso_pred_eq 1); ``` lcp@789 ` 424` ```by (REPEAT_SOME assume_tac); ``` wenzelm@7499 ` 425` ```by (ftac ord_iso_restrict_pred 1 THEN ``` lcp@789 ` 426` ``` REPEAT1 (eresolve_tac [asm_rl, predI] 1)); ``` lcp@789 ` 427` ```by (asm_full_simp_tac ``` wenzelm@4091 ` 428` ``` (simpset() addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1); ``` lcp@789 ` 429` ```by (eresolve_tac [ord_iso_sym RS ord_iso_trans] 1); ``` lcp@789 ` 430` ```by (assume_tac 1); ``` lcp@789 ` 431` ```qed "well_ord_iso_preserving"; ``` lcp@435 ` 432` wenzelm@4091 ` 433` ```val bij_apply_cs = claset() addSIs [bij_converse_bij] ``` paulson@2925 ` 434` ``` addIs [ord_iso_is_bij, bij_is_fun, apply_funtype]; ``` paulson@2469 ` 435` lcp@812 ` 436` ```(*See Halmos, page 72*) ``` paulson@5268 ` 437` ```Goal "[| well_ord(A,r); \ ``` lcp@435 ` 438` ```\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s); y: A |] \ ``` lcp@812 ` 439` ```\ ==> ~ : s"; ``` wenzelm@7499 ` 440` ```by (ftac well_ord_iso_subset_lemma 1); ``` lcp@812 ` 441` ```by (res_inst_tac [("f","converse(f)"), ("g","g")] ord_iso_trans 1); ``` lcp@812 ` 442` ```by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym])); ``` paulson@4152 ` 443` ```by Safe_tac; ``` wenzelm@7499 ` 444` ```by (ftac ord_iso_converse 1); ``` paulson@2925 ` 445` ```by (EVERY (map (blast_tac bij_apply_cs) [1,1,1])); ``` lcp@435 ` 446` ```by (asm_full_simp_tac bij_inverse_ss 1); ``` clasohm@760 ` 447` ```qed "well_ord_iso_unique_lemma"; ``` lcp@435 ` 448` lcp@435 ` 449` ```(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*) ``` paulson@5268 ` 450` ```Goal "[| well_ord(A,r); \ ``` lcp@435 ` 451` ```\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s) |] ==> f = g"; ``` lcp@437 ` 452` ```by (rtac fun_extension 1); ``` lcp@812 ` 453` ```by (REPEAT (etac (ord_iso_is_bij RS bij_is_fun) 1)); ``` lcp@812 ` 454` ```by (subgoals_tac ["f`x : B", "g`x : B", "linear(B,s)"] 1); ``` paulson@2925 ` 455` ```by (REPEAT (blast_tac bij_apply_cs 3)); ``` lcp@812 ` 456` ```by (dtac well_ord_ord_iso 2 THEN etac ord_iso_sym 2); ``` wenzelm@4091 ` 457` ```by (asm_full_simp_tac (simpset() addsimps [tot_ord_def, well_ord_def]) 2); ``` lcp@812 ` 458` ```by (linear_case_tac 1); ``` lcp@812 ` 459` ```by (DEPTH_SOLVE (eresolve_tac [asm_rl, well_ord_iso_unique_lemma RS notE] 1)); ``` clasohm@760 ` 460` ```qed "well_ord_iso_unique"; ``` lcp@435 ` 461` lcp@435 ` 462` lcp@789 ` 463` ```(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **) ``` lcp@789 ` 464` wenzelm@5067 ` 465` ```Goalw [ord_iso_map_def] "ord_iso_map(A,r,B,s) <= A*B"; ``` paulson@2925 ` 466` ```by (Blast_tac 1); ``` lcp@789 ` 467` ```qed "ord_iso_map_subset"; ``` lcp@789 ` 468` wenzelm@5067 ` 469` ```Goalw [ord_iso_map_def] "domain(ord_iso_map(A,r,B,s)) <= A"; ``` paulson@2925 ` 470` ```by (Blast_tac 1); ``` lcp@789 ` 471` ```qed "domain_ord_iso_map"; ``` lcp@789 ` 472` wenzelm@5067 ` 473` ```Goalw [ord_iso_map_def] "range(ord_iso_map(A,r,B,s)) <= B"; ``` paulson@2925 ` 474` ```by (Blast_tac 1); ``` lcp@789 ` 475` ```qed "range_ord_iso_map"; ``` lcp@789 ` 476` wenzelm@5067 ` 477` ```Goalw [ord_iso_map_def] ``` lcp@789 ` 478` ``` "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)"; ``` wenzelm@4091 ` 479` ```by (blast_tac (claset() addIs [ord_iso_sym]) 1); ``` lcp@789 ` 480` ```qed "converse_ord_iso_map"; ``` lcp@789 ` 481` wenzelm@5067 ` 482` ```Goalw [ord_iso_map_def, function_def] ``` paulson@5147 ` 483` ``` "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))"; ``` wenzelm@4091 ` 484` ```by (blast_tac (claset() addIs [well_ord_iso_pred_eq, ``` paulson@2925 ` 485` ``` ord_iso_sym, ord_iso_trans]) 1); ``` lcp@789 ` 486` ```qed "function_ord_iso_map"; ``` lcp@789 ` 487` paulson@5268 ` 488` ```Goal "well_ord(B,s) ==> ord_iso_map(A,r,B,s) \ ``` lcp@789 ` 489` ```\ : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))"; ``` lcp@789 ` 490` ```by (asm_simp_tac ``` wenzelm@4091 ` 491` ``` (simpset() addsimps [Pi_iff, function_ord_iso_map, ``` clasohm@1461 ` 492` ``` ord_iso_map_subset RS domain_times_range]) 1); ``` lcp@789 ` 493` ```qed "ord_iso_map_fun"; ``` lcp@435 ` 494` wenzelm@5067 ` 495` ```Goalw [mono_map_def] ``` paulson@5147 ` 496` ``` "[| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ ``` clasohm@1461 ` 497` ```\ : mono_map(domain(ord_iso_map(A,r,B,s)), r, \ ``` clasohm@1461 ` 498` ```\ range(ord_iso_map(A,r,B,s)), s)"; ``` wenzelm@4091 ` 499` ```by (asm_simp_tac (simpset() addsimps [ord_iso_map_fun]) 1); ``` paulson@4152 ` 500` ```by Safe_tac; ``` lcp@789 ` 501` ```by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1); ``` lcp@789 ` 502` ```by (REPEAT ``` wenzelm@4091 ` 503` ``` (blast_tac (claset() addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2)); ``` paulson@2925 ` 504` ```by (asm_simp_tac ``` wenzelm@4091 ` 505` ``` (simpset() addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1); ``` clasohm@1461 ` 506` ```by (rewtac ord_iso_map_def); ``` paulson@5488 ` 507` ```by Safe_tac; ``` clasohm@1461 ` 508` ```by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac); ``` lcp@789 ` 509` ```qed "ord_iso_map_mono_map"; ``` lcp@435 ` 510` wenzelm@5067 ` 511` ```Goalw [mono_map_def] ``` paulson@5147 ` 512` ``` "[| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ ``` clasohm@1461 ` 513` ```\ : ord_iso(domain(ord_iso_map(A,r,B,s)), r, \ ``` clasohm@1461 ` 514` ```\ range(ord_iso_map(A,r,B,s)), s)"; ``` clasohm@1461 ` 515` ```by (rtac well_ord_mono_ord_isoI 1); ``` lcp@789 ` 516` ```by (resolve_tac [converse_ord_iso_map RS subst] 4); ``` lcp@789 ` 517` ```by (asm_simp_tac ``` wenzelm@4091 ` 518` ``` (simpset() addsimps [ord_iso_map_subset RS converse_converse]) 4); ``` lcp@789 ` 519` ```by (REPEAT (ares_tac [ord_iso_map_mono_map] 3)); ``` lcp@789 ` 520` ```by (ALLGOALS (etac well_ord_subset)); ``` lcp@789 ` 521` ```by (ALLGOALS (resolve_tac [domain_ord_iso_map, range_ord_iso_map])); ``` lcp@789 ` 522` ```qed "ord_iso_map_ord_iso"; ``` lcp@467 ` 523` lcp@789 ` 524` ```(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*) ``` wenzelm@5067 ` 525` ```Goalw [ord_iso_map_def] ``` paulson@5147 ` 526` ``` "[| well_ord(A,r); well_ord(B,s); \ ``` clasohm@1461 ` 527` ```\ a: A; a ~: domain(ord_iso_map(A,r,B,s)) \ ``` lcp@1015 ` 528` ```\ |] ==> domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)"; ``` wenzelm@4091 ` 529` ```by (safe_tac (claset() addSIs [predI])); ``` lcp@1015 ` 530` ```(*Case analysis on xaa vs a in r *) ``` lcp@789 ` 531` ```by (forw_inst_tac [("A","A")] well_ord_is_linear 1); ``` lcp@789 ` 532` ```by (linear_case_tac 1); ``` lcp@1015 ` 533` ```(*Trivial case: a=xa*) ``` paulson@2925 ` 534` ```by (Blast_tac 2); ``` lcp@1015 ` 535` ```(*Harder case: : r*) ``` lcp@789 ` 536` ```by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1 THEN ``` lcp@789 ` 537` ``` REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1)); ``` wenzelm@7499 ` 538` ```by (ftac ord_iso_restrict_pred 1 THEN ``` lcp@789 ` 539` ``` REPEAT1 (eresolve_tac [asm_rl, predI] 1)); ``` lcp@789 ` 540` ```by (asm_full_simp_tac ``` wenzelm@4091 ` 541` ``` (simpset() addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1); ``` paulson@2925 ` 542` ```by (Blast_tac 1); ``` lcp@789 ` 543` ```qed "domain_ord_iso_map_subset"; ``` lcp@435 ` 544` lcp@789 ` 545` ```(*For the 4-way case analysis in the main result*) ``` paulson@5268 ` 546` ```Goal "[| well_ord(A,r); well_ord(B,s) |] ==> \ ``` clasohm@1461 ` 547` ```\ domain(ord_iso_map(A,r,B,s)) = A | \ ``` lcp@789 ` 548` ```\ (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))"; ``` wenzelm@7499 ` 549` ```by (ftac well_ord_is_wf 1); ``` lcp@789 ` 550` ```by (rewrite_goals_tac [wf_on_def, wf_def]); ``` lcp@789 ` 551` ```by (dres_inst_tac [("x", "A-domain(ord_iso_map(A,r,B,s))")] spec 1); ``` paulson@3736 ` 552` ```by Safe_tac; ``` lcp@789 ` 553` ```(*The first case: the domain equals A*) ``` lcp@789 ` 554` ```by (rtac (domain_ord_iso_map RS equalityI) 1); ``` lcp@789 ` 555` ```by (etac (Diff_eq_0_iff RS iffD1) 1); ``` lcp@789 ` 556` ```(*The other case: the domain equals an initial segment*) ``` lcp@789 ` 557` ```by (swap_res_tac [bexI] 1); ``` lcp@789 ` 558` ```by (assume_tac 2); ``` lcp@789 ` 559` ```by (rtac equalityI 1); ``` wenzelm@4091 ` 560` ```(*not (claset()) below; that would use rules like domainE!*) ``` wenzelm@4091 ` 561` ```by (blast_tac (claset() addSEs [predE]) 2); ``` lcp@789 ` 562` ```by (REPEAT (ares_tac [domain_ord_iso_map_subset] 1)); ``` lcp@789 ` 563` ```qed "domain_ord_iso_map_cases"; ``` lcp@467 ` 564` lcp@789 ` 565` ```(*As above, by duality*) ``` paulson@5268 ` 566` ```Goal "[| well_ord(A,r); well_ord(B,s) |] ==> \ ``` clasohm@1461 ` 567` ```\ range(ord_iso_map(A,r,B,s)) = B | \ ``` lcp@789 ` 568` ```\ (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))"; ``` lcp@789 ` 569` ```by (resolve_tac [converse_ord_iso_map RS subst] 1); ``` lcp@789 ` 570` ```by (asm_simp_tac ``` wenzelm@4091 ` 571` ``` (simpset() addsimps [range_converse, domain_ord_iso_map_cases]) 1); ``` lcp@789 ` 572` ```qed "range_ord_iso_map_cases"; ``` lcp@789 ` 573` lcp@789 ` 574` ```(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*) ``` paulson@5268 ` 575` ```Goal "[| well_ord(A,r); well_ord(B,s) |] ==> \ ``` clasohm@1461 ` 576` ```\ ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) | \ ``` lcp@789 ` 577` ```\ (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | \ ``` lcp@789 ` 578` ```\ (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))"; ``` lcp@789 ` 579` ```by (forw_inst_tac [("B","B")] domain_ord_iso_map_cases 1); ``` lcp@789 ` 580` ```by (forw_inst_tac [("B","B")] range_ord_iso_map_cases 2); ``` lcp@789 ` 581` ```by (REPEAT_FIRST (eresolve_tac [asm_rl, disjE, bexE])); ``` clasohm@1461 ` 582` ```by (ALLGOALS (dtac ord_iso_map_ord_iso THEN' assume_tac THEN' ``` wenzelm@4091 ` 583` ``` asm_full_simp_tac (simpset() addsimps [bexI]))); ``` lcp@789 ` 584` ```by (resolve_tac [wf_on_not_refl RS notE] 1); ``` clasohm@1461 ` 585` ```by (etac well_ord_is_wf 1); ``` lcp@789 ` 586` ```by (assume_tac 1); ``` lcp@789 ` 587` ```by (subgoal_tac ": ord_iso_map(A,r,B,s)" 1); ``` clasohm@1461 ` 588` ```by (dtac rangeI 1); ``` wenzelm@4091 ` 589` ```by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1); ``` clasohm@1461 ` 590` ```by (rewtac ord_iso_map_def); ``` paulson@2925 ` 591` ```by (Blast_tac 1); ``` lcp@789 ` 592` ```qed "well_ord_trichotomy"; ``` lcp@467 ` 593` lcp@836 ` 594` lcp@836 ` 595` ```(*** Properties of converse(r), by Krzysztof Grabczewski ***) ``` lcp@836 ` 596` wenzelm@5067 ` 597` ```Goalw [irrefl_def] ``` paulson@5147 ` 598` ``` "irrefl(A,r) ==> irrefl(A,converse(r))"; ``` paulson@4311 ` 599` ```by (Blast_tac 1); ``` lcp@836 ` 600` ```qed "irrefl_converse"; ``` lcp@836 ` 601` wenzelm@5067 ` 602` ```Goalw [trans_on_def] ``` paulson@5147 ` 603` ``` "trans[A](r) ==> trans[A](converse(r))"; ``` paulson@4311 ` 604` ```by (Blast_tac 1); ``` lcp@836 ` 605` ```qed "trans_on_converse"; ``` lcp@836 ` 606` wenzelm@5067 ` 607` ```Goalw [part_ord_def] ``` paulson@5147 ` 608` ``` "part_ord(A,r) ==> part_ord(A,converse(r))"; ``` wenzelm@4091 ` 609` ```by (blast_tac (claset() addSIs [irrefl_converse, trans_on_converse]) 1); ``` lcp@836 ` 610` ```qed "part_ord_converse"; ``` lcp@836 ` 611` wenzelm@5067 ` 612` ```Goalw [linear_def] ``` paulson@5147 ` 613` ``` "linear(A,r) ==> linear(A,converse(r))"; ``` paulson@4311 ` 614` ```by (Blast_tac 1); ``` lcp@836 ` 615` ```qed "linear_converse"; ``` lcp@836 ` 616` wenzelm@5067 ` 617` ```Goalw [tot_ord_def] ``` paulson@5147 ` 618` ``` "tot_ord(A,r) ==> tot_ord(A,converse(r))"; ``` wenzelm@4091 ` 619` ```by (blast_tac (claset() addSIs [part_ord_converse, linear_converse]) 1); ``` lcp@836 ` 620` ```qed "tot_ord_converse"; ``` paulson@2469 ` 621` paulson@2469 ` 622` paulson@2469 ` 623` ```(** By Krzysztof Grabczewski. ``` paulson@2469 ` 624` ``` Lemmas involving the first element of a well ordered set **) ``` paulson@2469 ` 625` paulson@5137 ` 626` ```Goalw [first_def] "first(b,B,r) ==> b:B"; ``` paulson@2925 ` 627` ```by (Blast_tac 1); ``` paulson@2469 ` 628` ```qed "first_is_elem"; ``` paulson@2469 ` 629` wenzelm@5067 ` 630` ```Goalw [well_ord_def, wf_on_def, wf_def, first_def] ``` paulson@5147 ` 631` ``` "[| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"; ``` paulson@2469 ` 632` ```by (REPEAT (eresolve_tac [conjE,allE,disjE] 1)); ``` paulson@2469 ` 633` ```by (contr_tac 1); ``` paulson@2469 ` 634` ```by (etac bexE 1); ``` paulson@2469 ` 635` ```by (res_inst_tac [("a","x")] ex1I 1); ``` paulson@2925 ` 636` ```by (Blast_tac 2); ``` paulson@2469 ` 637` ```by (rewrite_goals_tac [tot_ord_def, linear_def]); ``` wenzelm@4091 ` 638` ```by (Blast.depth_tac (claset()) 7 1); ``` paulson@2469 ` 639` ```qed "well_ord_imp_ex1_first"; ``` paulson@2469 ` 640` paulson@5137 ` 641` ```Goal "[| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B"; ``` paulson@2469 ` 642` ```by (dtac well_ord_imp_ex1_first 1 THEN REPEAT (assume_tac 1)); ``` paulson@2469 ` 643` ```by (rtac first_is_elem 1); ``` paulson@2469 ` 644` ```by (etac theI 1); ``` paulson@2469 ` 645` ```qed "the_first_in"; ```