# HG changeset patch # User lcp # Date 787422263 -3600 # Node ID 30bdc59198ff361ecd5dc19e8a82f6bda46b4e57 # Parent 8acbe6f3de2bf068b189d7d5142d7f0c3f0737b3 well_ord_iso_predE replaces not_well_ord_iso_pred well_ord_iso_unique: eliminated a premise using well_ord_ord_iso Proved well_ord_iso_pred_eq, ord_iso_image_pred, ord_iso_restrict_pred, part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso, well_ord_ord_iso, well_ord_iso_preserving, mono_map_is_fun, mono_map_is_inj, mono_map_trans, mono_ord_isoI, well_ord_mono_ord_isoI, ord_iso_is_mono_map, ord_iso_map_mono_map, ord_iso_map_ord_iso, domain_ord_iso_map_subset, domain_ord_iso_map_cases, range_ord_iso_map_cases, well_ord_trichotomy deleted bij_ss in favour of bij_inverse_ss diff -r 8acbe6f3de2b -r 30bdc59198ff src/ZF/Order.ML --- a/src/ZF/Order.ML Wed Dec 14 17:15:54 1994 +0100 +++ b/src/ZF/Order.ML Wed Dec 14 17:24:23 1994 +0100 @@ -3,30 +3,104 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -For Order.thy. Orders in Zermelo-Fraenkel Set Theory +Orders in Zermelo-Fraenkel Set Theory + +Results from the book "Set Theory: an Introduction to Independence Proofs" + by Ken Kunen. Chapter 1, section 6. *) - open Order; val bij_apply_cs = ZF_cs addSEs [bij_converse_bij] addIs [bij_is_fun, apply_type]; -val bij_inverse_ss = - ZF_ss addsimps [bij_is_fun RS apply_type, - bij_converse_bij RS bij_is_fun RS apply_type, - left_inverse_bij, right_inverse_bij]; - (** Basic properties of the definitions **) -(*needed????*) +(*needed?*) goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, asym_def] "!!r. part_ord(A,r) ==> asym(r Int A*A)"; by (fast_tac ZF_cs 1); qed "part_ord_Imp_asym"; -(** Subset properties for the various forms of relation **) +val major::premx::premy::prems = goalw Order.thy [linear_def] + "[| linear(A,r); x:A; y:A; \ +\ :r ==> P; x=y ==> P; :r ==> P |] ==> P"; +by (cut_facts_tac [major,premx,premy] 1); +by (REPEAT_FIRST (eresolve_tac [ballE,disjE])); +by (EVERY1 (map etac prems)); +by (ALLGOALS contr_tac); +qed "linearE"; + +(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*) +val linear_case_tac = + SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1, + REPEAT_SOME (assume_tac ORELSE' contr_tac)]); + +(** General properties of well_ord **) + +goalw Order.thy [irrefl_def, part_ord_def, tot_ord_def, + trans_on_def, well_ord_def] + "!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"; +by (asm_simp_tac (ZF_ss addsimps [wf_on_not_refl]) 1); +by (safe_tac ZF_cs); +by (linear_case_tac 1); +(*case x=xb*) +by (fast_tac (ZF_cs addSEs [wf_on_asym]) 1); +(*case x wf[A](r)"; +by (safe_tac ZF_cs); +qed "well_ord_is_wf"; + +goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def] + "!!r. well_ord(A,r) ==> trans[A](r)"; +by (safe_tac ZF_cs); +qed "well_ord_is_trans_on"; +goalw Order.thy [well_ord_def, tot_ord_def] + "!!r. well_ord(A,r) ==> linear(A,r)"; +by (fast_tac ZF_cs 1); +qed "well_ord_is_linear"; + + +(** Derived rules for pred(A,x,r) **) + +goalw Order.thy [pred_def] "y : pred(A,x,r) <-> :r & y:A"; +by (fast_tac ZF_cs 1); +qed "pred_iff"; + +bind_thm ("predI", conjI RS (pred_iff RS iffD2)); + +val [major,minor] = goalw Order.thy [pred_def] + "[| y: pred(A,x,r); [| y:A; :r |] ==> P |] ==> P"; +by (rtac (major RS CollectE) 1); +by (REPEAT (ares_tac [minor] 1)); +qed "predE"; + +goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}"; +by (fast_tac ZF_cs 1); +qed "pred_subset_under"; + +goalw Order.thy [pred_def] "pred(A,x,r) <= A"; +by (fast_tac ZF_cs 1); +qed "pred_subset"; + +goalw Order.thy [pred_def] + "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)"; +by (fast_tac eq_cs 1); +qed "pred_pred_eq"; + +goalw Order.thy [trans_on_def, pred_def] + "!!r. [| trans[A](r); :r; x:A; y:A \ +\ |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"; +by (fast_tac eq_cs 1); +qed "trans_pred_pred_eq"; + +(** The ordering's properties hold over all subsets of its domain + [including initial segments of the form pred(A,x,r) **) (*Note: a relation s such that s<=r need not be a partial ordering*) goalw Order.thy [part_ord_def, irrefl_def, trans_on_def] @@ -50,13 +124,52 @@ qed "well_ord_subset"; -(** Order-isomorphisms **) +(** Order-preserving (monotone) maps **) + +(*Rewriting with bijections and converse (function inverse)*) +val bij_inverse_ss = + ZF_ss setsolver (type_auto_tac [bij_is_fun, apply_type, + bij_converse_bij, comp_fun, comp_bij]) + addsimps [right_inverse_bij, left_inverse_bij, comp_fun_apply]; + +goalw Order.thy [mono_map_def] + "!!f. f: mono_map(A,r,B,s) ==> f: A->B"; +by (etac CollectD1 1); +qed "mono_map_is_fun"; + +goalw Order.thy [mono_map_def, inj_def] + "!!f. [| linear(A,r); wf[B](s); f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"; +by (step_tac ZF_cs 1); +by (linear_case_tac 1); +by (REPEAT + (EVERY [eresolve_tac [wf_on_not_refl RS notE] 1, + eresolve_tac [ssubst] 2, + fast_tac ZF_cs 2, + REPEAT (ares_tac [apply_type] 1)])); +qed "mono_map_is_inj"; + +(*Transitivity of similarity: the order-isomorphism relation*) +goalw Order.thy [mono_map_def] + "!!f. [| g: mono_map(A,r,B,s); f: mono_map(B,s,C,t) |] ==> \ +\ (f O g): mono_map(A,r,C,t)"; +by (safe_tac ZF_cs); +by (ALLGOALS (asm_full_simp_tac bij_inverse_ss)); +qed "mono_map_trans"; + + +(** Order-isomorphisms -- or similarities, as Suppes calls them **) + +goalw Order.thy [ord_iso_def, mono_map_def] + "!!f. f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)"; +by (fast_tac (ZF_cs addSDs [bij_is_fun]) 1); +qed "ord_iso_is_mono_map"; goalw Order.thy [ord_iso_def] "!!f. f: ord_iso(A,r,B,s) ==> f: bij(A,B)"; by (etac CollectD1 1); qed "ord_iso_is_bij"; +(*Needed? But ord_iso_converse is!*) goalw Order.thy [ord_iso_def] "!!f. [| f: ord_iso(A,r,B,s); : r; x:A; y:A |] ==> \ \ : s"; @@ -73,31 +186,100 @@ by (asm_simp_tac (ZF_ss addsimps [right_inverse_bij]) 1); qed "ord_iso_converse"; -(*Rewriting with bijections and converse (function inverse)*) -val bij_ss = ZF_ss setsolver (type_auto_tac [bij_is_fun RS apply_type, - bij_converse_bij]) - addsimps [right_inverse_bij, left_inverse_bij]; - -(*Symmetry of the order-isomorphism relation*) +(*Symmetry of similarity: the order-isomorphism relation*) goalw Order.thy [ord_iso_def] "!!f. f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"; by (safe_tac ZF_cs); -by (ALLGOALS (asm_full_simp_tac bij_ss)); +by (ALLGOALS (asm_full_simp_tac bij_inverse_ss)); qed "ord_iso_sym"; -val major::premx::premy::prems = goalw Order.thy [linear_def] - "[| linear(A,r); x:A; y:A; \ -\ :r ==> P; x=y ==> P; :r ==> P |] ==> P"; -by (cut_facts_tac [major,premx,premy] 1); -by (REPEAT_FIRST (eresolve_tac [ballE,disjE])); -by (EVERY1 (map etac prems)); -by (ALLGOALS contr_tac); -qed "linearE"; +(*Transitivity of similarity: the order-isomorphism relation*) +goalw Order.thy [ord_iso_def] + "!!f. [| g: ord_iso(A,r,B,s); f: ord_iso(B,s,C,t) |] ==> \ +\ (f O g): ord_iso(A,r,C,t)"; +by (safe_tac ZF_cs); +by (ALLGOALS (asm_full_simp_tac bij_inverse_ss)); +qed "ord_iso_trans"; + +(** Two monotone maps can make an order-isomorphism **) + +goalw Order.thy [ord_iso_def, mono_map_def] + "!!f g. [| f: mono_map(A,r,B,s); g: mono_map(B,s,A,r); \ +\ f O g = id(B); g O f = id(A) |] ==> f: ord_iso(A,r,B,s)"; +by (safe_tac ZF_cs); +by (REPEAT_FIRST (ares_tac [fg_imp_bijective])); +by (fast_tac ZF_cs 1); +by (subgoal_tac " : r" 1); +by (fast_tac (ZF_cs addIs [apply_type] addSEs [bspec RS bspec RS mp]) 2); +by (asm_full_simp_tac + (ZF_ss addsimps [comp_eq_id_iff RS iffD1]) 1); +qed "mono_ord_isoI"; + +goal Order.thy + "!!B. [| well_ord(A,r); well_ord(B,s); \ +\ f: mono_map(A,r,B,s); converse(f): mono_map(B,s,A,r) \ +\ |] ==> f: ord_iso(A,r,B,s)"; +by (REPEAT (ares_tac [mono_ord_isoI] 1)); +by (forward_tac [mono_map_is_fun RS fun_is_rel] 1); +by (etac (converse_converse RS subst) 1 THEN rtac left_comp_inverse 1); +by (DEPTH_SOLVE (ares_tac [mono_map_is_inj, left_comp_inverse] 1 + ORELSE eresolve_tac [well_ord_is_linear, well_ord_is_wf] 1)); +qed "well_ord_mono_ord_isoI"; + + +(** Order-isomorphisms preserve the ordering's properties **) + +goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, ord_iso_def] + "!!A B r. [| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)"; +by (asm_simp_tac ZF_ss 1); +by (fast_tac (ZF_cs addIs [bij_is_fun RS apply_type]) 1); +qed "part_ord_ord_iso"; -(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*) -val linear_case_tac = - SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1, - REPEAT_SOME assume_tac]); +goalw Order.thy [linear_def, ord_iso_def] + "!!A B r. [| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)"; +by (asm_simp_tac ZF_ss 1); +by (safe_tac ZF_cs); +by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1); +by (safe_tac (ZF_cs addSEs [bij_is_fun RS apply_type])); +by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1); +by (asm_full_simp_tac (ZF_ss addsimps [left_inverse_bij]) 1); +qed "linear_ord_iso"; + +(*FOR FOL/IFOL.ML*) +fun iff_tac prems i = + resolve_tac (prems RL [iffE]) i THEN + REPEAT1 (eresolve_tac [asm_rl,mp] i); + +(*Reversed congruence rule!*) +val conj_cong2 = prove_goal IFOL.thy + "[| P <-> P'; P' ==> Q <-> Q' |] ==> (Q&P) <-> (Q'&P')" + (fn prems => + [ (cut_facts_tac prems 1), + (REPEAT (ares_tac [iffI,conjI] 1 + ORELSE eresolve_tac [iffE,conjE,mp] 1 + ORELSE iff_tac prems 1)) ]); + +goalw Order.thy [wf_on_def, wf_def, ord_iso_def] + "!!A B r. [| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)"; +(*reversed &-congruence rule handles context of membership in A*) +by (asm_full_simp_tac (ZF_ss addcongs [conj_cong2]) 1); +by (safe_tac ZF_cs); +by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1); +by (safe_tac eq_cs); +by (dtac equalityD1 1); +by (fast_tac (ZF_cs addSIs [bexI]) 1); +by (fast_tac (ZF_cs addSIs [bexI] + addIs [bij_is_fun RS apply_type]) 1); +qed "wf_on_ord_iso"; + +goalw Order.thy [well_ord_def, tot_ord_def] + "!!A B r. [| well_ord(B,s); f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)"; +by (fast_tac + (ZF_cs addSEs [part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso]) 1); +qed "well_ord_ord_iso"; + + +(*** Main results of Kunen, Chapter 1 section 6 ***) (*Inductive argument for proving Kunen's Lemma 6.1*) goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def, pred_def] @@ -131,18 +313,80 @@ (*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment of a well-ordering*) goal Order.thy - "!!r. [| well_ord(A,r); x:A |] ==> f ~: ord_iso(A, r, pred(A,x,r), r)"; -by (safe_tac ZF_cs); + "!!r. [| well_ord(A,r); f : ord_iso(A, r, pred(A,x,r), r); x:A |] ==> P"; by (metacut_tac not_well_ord_iso_pred_lemma 1); -by (REPEAT_SOME assume_tac); +by (REPEAT_FIRST assume_tac); (*Now we know f`x = x*) by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type), assume_tac]); (*Now we know f`x : pred(A,x,r) *) by (asm_full_simp_tac (ZF_ss addsimps [well_ord_def, pred_def]) 1); by (fast_tac (ZF_cs addSEs [wf_on_not_refl RS notE]) 1); -qed "not_well_ord_iso_pred"; +qed "well_ord_iso_predE"; + +(*Simple consequence of Lemma 6.1*) +goal Order.thy + "!!r. [| well_ord(A,r); f : ord_iso(pred(A,a,r), r, pred(A,c,r), r); \ +\ a:A; c:A |] ==> a=c"; +by (forward_tac [well_ord_is_trans_on] 1); +by (forward_tac [well_ord_is_linear] 1); +by (linear_case_tac 1); +by (dtac ord_iso_sym 1); +by (REPEAT (*because there are two symmetric cases*) + (EVERY [eresolve_tac [pred_subset RSN (2, well_ord_subset) RS + well_ord_iso_predE] 1, + fast_tac (ZF_cs addSIs [predI]) 2, + asm_simp_tac (ZF_ss addsimps [trans_pred_pred_eq]) 1])); +qed "well_ord_iso_pred_eq"; + +(*Does not assume r is a wellordering!*) +goalw Order.thy [ord_iso_def, pred_def] + "!!r. [| f : ord_iso(A,r,B,s); a:A |] ==> \ +\ f `` pred(A,a,r) = pred(B, f`a, s)"; +by (etac CollectE 1); +by (asm_simp_tac + (ZF_ss addsimps [[bij_is_fun, Collect_subset] MRS image_fun]) 1); +by (safe_tac (eq_cs addSEs [bij_is_fun RS apply_type])); +by (resolve_tac [RepFun_eqI] 1); +by (fast_tac (ZF_cs addSIs [right_inverse_bij RS sym]) 1); +by (asm_simp_tac + (ZF_ss addsimps [right_inverse_bij] + setsolver type_auto_tac + [bij_is_fun, apply_funtype, bij_converse_bij]) 1); +qed "ord_iso_image_pred"; +(*But in use, A and B may themselves be initial segments. Then use + trans_pred_pred_eq to simplify the pred(pred...) terms. See just below.*) +goal Order.thy + "!!r. [| f : ord_iso(A,r,B,s); a:A |] ==> \ +\ restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"; +by (asm_simp_tac (ZF_ss addsimps [ord_iso_image_pred RS sym]) 1); +by (rewrite_goals_tac [ord_iso_def]); +by (step_tac ZF_cs 1); +by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 2); +by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 2); +by (eresolve_tac [[bij_is_inj, pred_subset] MRS restrict_bij] 1); +qed "ord_iso_restrict_pred"; + +(*Tricky; a lot of forward proof!*) +goal Order.thy + "!!r. [| well_ord(A,r); well_ord(B,s); : r; \ +\ f : ord_iso(pred(A,a,r), r, pred(B,b,s), s); \ +\ g : ord_iso(pred(A,c,r), r, pred(B,d,s), s); \ +\ a:A; c:A; b:B; d:B |] ==> : s"; +by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1 THEN + REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1)); +by (subgoal_tac "b = g`a" 1); +by (asm_simp_tac ZF_ss 1); +by (resolve_tac [well_ord_iso_pred_eq] 1); +by (REPEAT_SOME assume_tac); +by (forward_tac [ord_iso_restrict_pred] 1 THEN + REPEAT1 (eresolve_tac [asm_rl, predI] 1)); +by (asm_full_simp_tac + (ZF_ss addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1); +by (eresolve_tac [ord_iso_sym RS ord_iso_trans] 1); +by (assume_tac 1); +qed "well_ord_iso_preserving"; (*Inductive argument for proving Kunen's Lemma 6.2*) goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def] @@ -170,62 +414,157 @@ by (asm_full_simp_tac bij_inverse_ss 1); qed "well_ord_iso_unique_lemma"; - (*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*) goal Order.thy - "!!r. [| well_ord(A,r); well_ord(B,s); \ + "!!r. [| well_ord(B,s); \ \ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s) |] ==> f = g"; by (rtac fun_extension 1); by (etac (ord_iso_is_bij RS bij_is_fun) 1); by (etac (ord_iso_is_bij RS bij_is_fun) 1); by (rtac well_ord_iso_unique_lemma 1); -by (REPEAT_SOME assume_tac); +by (REPEAT_SOME (eresolve_tac [asm_rl, well_ord_ord_iso])); qed "well_ord_iso_unique"; -goalw Order.thy [irrefl_def, part_ord_def, tot_ord_def, - trans_on_def, well_ord_def] - "!!r. [| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"; -by (asm_simp_tac (ZF_ss addsimps [wf_on_not_refl]) 1); +(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **) + +goalw Order.thy [ord_iso_map_def] + "ord_iso_map(A,r,B,s) <= A*B"; +by (fast_tac ZF_cs 1); +qed "ord_iso_map_subset"; + +goalw Order.thy [ord_iso_map_def] + "domain(ord_iso_map(A,r,B,s)) <= A"; +by (fast_tac ZF_cs 1); +qed "domain_ord_iso_map"; + +goalw Order.thy [ord_iso_map_def] + "range(ord_iso_map(A,r,B,s)) <= B"; +by (fast_tac ZF_cs 1); +qed "range_ord_iso_map"; + +goalw Order.thy [ord_iso_map_def] + "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)"; +by (fast_tac (eq_cs addIs [ord_iso_sym]) 1); +qed "converse_ord_iso_map"; + +goalw Order.thy [ord_iso_map_def, function_def] + "!!B. well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))"; by (safe_tac ZF_cs); -by (linear_case_tac 1); -(*case x=xb*) -by (fast_tac (ZF_cs addSEs [wf_on_asym]) 1); -(*case x ord_iso_map(A,r,B,s) \ +\ : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))"; +by (asm_simp_tac + (ZF_ss addsimps [Pi_iff, function_ord_iso_map, + ord_iso_map_subset RS domain_times_range]) 1); +qed "ord_iso_map_fun"; -goalw Order.thy [well_ord_def] - "!!r. well_ord(A,r) ==> wf[A](r)"; +goalw Order.thy [mono_map_def] + "!!B. [| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ +\ : mono_map(domain(ord_iso_map(A,r,B,s)), r, \ +\ range(ord_iso_map(A,r,B,s)), s)"; +by (asm_simp_tac (ZF_ss addsimps [ord_iso_map_fun]) 1); by (safe_tac ZF_cs); -qed "well_ord_is_wf"; +by (subgoals_tac ["x:A", "xa:A", "y:B", "ya:B"] 1); +by (REPEAT + (fast_tac (ZF_cs addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2)); +by (asm_simp_tac (ZF_ss addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1); +by (rewrite_goals_tac [ord_iso_map_def]); +by (safe_tac (ZF_cs addSEs [UN_E])); +by (resolve_tac [well_ord_iso_preserving] 1 THEN REPEAT_FIRST assume_tac); +qed "ord_iso_map_mono_map"; -goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def] - "!!r. well_ord(A,r) ==> trans[A](r)"; -by (safe_tac ZF_cs); -qed "well_ord_is_trans_on"; +goalw Order.thy [mono_map_def] + "!!B. [| well_ord(A,r); well_ord(B,s) |] ==> ord_iso_map(A,r,B,s) \ +\ : ord_iso(domain(ord_iso_map(A,r,B,s)), r, \ +\ range(ord_iso_map(A,r,B,s)), s)"; +by (resolve_tac [well_ord_mono_ord_isoI] 1); +by (resolve_tac [converse_ord_iso_map RS subst] 4); +by (asm_simp_tac + (ZF_ss addsimps [ord_iso_map_subset RS converse_converse, + domain_converse, range_converse]) 4); +by (REPEAT (ares_tac [ord_iso_map_mono_map] 3)); +by (ALLGOALS (etac well_ord_subset)); +by (ALLGOALS (resolve_tac [domain_ord_iso_map, range_ord_iso_map])); +qed "ord_iso_map_ord_iso"; -(*** Derived rules for pred(A,x,r) ***) - -val [major,minor] = goalw Order.thy [pred_def] - "[| y: pred(A,x,r); [| y:A; :r |] ==> P |] ==> P"; -by (rtac (major RS CollectE) 1); -by (REPEAT (ares_tac [minor] 1)); -qed "predE"; - -goalw Order.thy [pred_def] "pred(A,x,r) <= r -`` {x}"; +(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*) +goalw Order.thy [ord_iso_map_def] + "!!B. [| well_ord(A,r); well_ord(B,s); \ +\ x: A; x ~: domain(ord_iso_map(A,r,B,s)) \ +\ |] ==> domain(ord_iso_map(A,r,B,s)) <= pred(A, x, r)"; +by (step_tac (ZF_cs addSIs [predI]) 1); +(*Case analysis on xaa vs x in r *) +by (forw_inst_tac [("A","A")] well_ord_is_linear 1); +by (linear_case_tac 1); +(*Trivial case: xaa=x*) by (fast_tac ZF_cs 1); -qed "pred_subset_under"; +(*Harder case: : r*) +by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1 THEN + REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1)); +by (forward_tac [ord_iso_restrict_pred] 1 THEN + REPEAT1 (eresolve_tac [asm_rl, predI] 1)); +by (asm_full_simp_tac + (ZF_ss addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1); +by (fast_tac ZF_cs 1); +qed "domain_ord_iso_map_subset"; -goalw Order.thy [pred_def] "pred(A,x,r) <= A"; -by (fast_tac ZF_cs 1); -qed "pred_subset"; +(*For the 4-way case analysis in the main result*) +goal Order.thy + "!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ +\ domain(ord_iso_map(A,r,B,s)) = A | \ +\ (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))"; +by (forward_tac [well_ord_is_wf] 1); +by (rewrite_goals_tac [wf_on_def, wf_def]); +by (dres_inst_tac [("x", "A-domain(ord_iso_map(A,r,B,s))")] spec 1); +by (step_tac ZF_cs 1); +(*The first case: the domain equals A*) +by (rtac (domain_ord_iso_map RS equalityI) 1); +by (etac (Diff_eq_0_iff RS iffD1) 1); +(*The other case: the domain equals an initial segment*) +by (swap_res_tac [bexI] 1); +by (assume_tac 2); +by (rtac equalityI 1); +(*not ZF_cs below; that would use rules like domainE!*) +by (fast_tac (pair_cs addSEs [predE]) 2); +by (REPEAT (ares_tac [domain_ord_iso_map_subset] 1)); +qed "domain_ord_iso_map_cases"; -goalw Order.thy [pred_def] "y : pred(A,x,r) <-> :r & y:A"; +(*As above, by duality*) +goal Order.thy + "!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ +\ range(ord_iso_map(A,r,B,s)) = B | \ +\ (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))"; +by (resolve_tac [converse_ord_iso_map RS subst] 1); +by (asm_simp_tac + (ZF_ss addsimps [range_converse, domain_ord_iso_map_cases]) 1); +qed "range_ord_iso_map_cases"; + +(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*) +goal Order.thy + "!!B. [| well_ord(A,r); well_ord(B,s) |] ==> \ +\ ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) | \ +\ (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | \ +\ (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))"; +by (forw_inst_tac [("B","B")] domain_ord_iso_map_cases 1); +by (forw_inst_tac [("B","B")] range_ord_iso_map_cases 2); +by (REPEAT_FIRST (eresolve_tac [asm_rl, disjE, bexE])); +by (ALLGOALS (dresolve_tac [ord_iso_map_ord_iso] THEN' assume_tac THEN' + asm_full_simp_tac (ZF_ss addsimps [bexI]))); + +by (resolve_tac [wf_on_not_refl RS notE] 1); +by (eresolve_tac [well_ord_is_wf] 1); +by (assume_tac 1); +by (subgoal_tac ": ord_iso_map(A,r,B,s)" 1); +by (dresolve_tac [rangeI] 1); +by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1); +by (rewrite_goals_tac [ord_iso_map_def]); by (fast_tac ZF_cs 1); -qed "pred_iff"; +qed "well_ord_trichotomy"; -goalw Order.thy [pred_def] - "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)"; -by (fast_tac eq_cs 1); -qed "pred_pred_eq";