--- a/src/ZF/CardinalArith.ML Sat May 11 20:40:31 2002 +0200
+++ b/src/ZF/CardinalArith.ML Mon May 13 09:02:13 2002 +0200
@@ -412,7 +412,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2])));
qed "csquareD";
-Goalw [Order.pred_def]
+Goalw [thm "Order.pred_def"]
"z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)";
by (safe_tac (claset() delrules [SigmaI, succCI]));
by (etac (csquareD RS conjE) 1);
--- a/src/ZF/IsaMakefile Sat May 11 20:40:31 2002 +0200
+++ b/src/ZF/IsaMakefile Mon May 13 09:02:13 2002 +0200
@@ -38,8 +38,8 @@
Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML \
Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy \
Main_ZFC.ML Main_ZFC.thy \
- Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML OrderArith.thy \
- OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy OrdQuant.ML OrdQuant.thy \
+ Nat.ML Nat.thy Order.thy OrderArith.thy \
+ OrderType.thy Ordinal.ML Ordinal.thy OrdQuant.ML OrdQuant.thy \
Perm.ML Perm.thy \
QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML \
Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \
--- a/src/ZF/Order.ML Sat May 11 20:40:31 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,638 +0,0 @@
-(* Title: ZF/Order.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Orders in Zermelo-Fraenkel Set Theory
-
-Results from the book "Set Theory: an Introduction to Independence Proofs"
- by Ken Kunen. Chapter 1, section 6.
-*)
-
-(** Basic properties of the definitions **)
-
-(*needed?*)
-Goalw [part_ord_def, irrefl_def, trans_on_def, asym_def]
- "part_ord(A,r) ==> asym(r Int A*A)";
-by (Blast_tac 1);
-qed "part_ord_Imp_asym";
-
-val major::premx::premy::prems = Goalw [linear_def]
- "[| linear(A,r); x:A; y:A; \
-\ <x,y>:r ==> P; x=y ==> P; <y,x>: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 [irrefl_def, part_ord_def, tot_ord_def,
- trans_on_def, well_ord_def]
- "[| wf[A](r); linear(A,r) |] ==> well_ord(A,r)";
-by (asm_simp_tac (simpset() addsimps [wf_on_not_refl]) 1);
-by (fast_tac (claset() addEs [linearE, wf_on_asym, wf_on_chain3]) 1);
-qed "well_ordI";
-
-Goalw [well_ord_def]
- "well_ord(A,r) ==> wf[A](r)";
-by Safe_tac;
-qed "well_ord_is_wf";
-
-Goalw [well_ord_def, tot_ord_def, part_ord_def]
- "well_ord(A,r) ==> trans[A](r)";
-by Safe_tac;
-qed "well_ord_is_trans_on";
-
-Goalw [well_ord_def, tot_ord_def]
- "well_ord(A,r) ==> linear(A,r)";
-by (Blast_tac 1);
-qed "well_ord_is_linear";
-
-
-(** Derived rules for pred(A,x,r) **)
-
-Goalw [pred_def] "y : pred(A,x,r) <-> <y,x>:r & y:A";
-by (Blast_tac 1);
-qed "pred_iff";
-
-bind_thm ("predI", conjI RS (pred_iff RS iffD2));
-
-val [major,minor] = Goalw [pred_def]
- "[| y: pred(A,x,r); [| y:A; <y,x>:r |] ==> P |] ==> P";
-by (rtac (major RS CollectE) 1);
-by (REPEAT (ares_tac [minor] 1));
-qed "predE";
-
-Goalw [pred_def] "pred(A,x,r) <= r -`` {x}";
-by (Blast_tac 1);
-qed "pred_subset_under";
-
-Goalw [pred_def] "pred(A,x,r) <= A";
-by (Blast_tac 1);
-qed "pred_subset";
-
-Goalw [pred_def]
- "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)";
-by (Blast_tac 1);
-qed "pred_pred_eq";
-
-Goalw [trans_on_def, pred_def]
- "[| trans[A](r); <y,x>:r; x:A; y:A \
-\ |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)";
-by (Blast_tac 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 [part_ord_def, irrefl_def, trans_on_def]
- "[| part_ord(A,r); B<=A |] ==> part_ord(B,r)";
-by (Blast_tac 1);
-qed "part_ord_subset";
-
-Goalw [linear_def]
- "[| linear(A,r); B<=A |] ==> linear(B,r)";
-by (Blast_tac 1);
-qed "linear_subset";
-
-Goalw [tot_ord_def]
- "[| tot_ord(A,r); B<=A |] ==> tot_ord(B,r)";
-by (fast_tac (claset() addSEs [part_ord_subset, linear_subset]) 1);
-qed "tot_ord_subset";
-
-Goalw [well_ord_def]
- "[| well_ord(A,r); B<=A |] ==> well_ord(B,r)";
-by (fast_tac (claset() addSEs [tot_ord_subset, wf_on_subset_A]) 1);
-qed "well_ord_subset";
-
-
-(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
-
-Goalw [irrefl_def] "irrefl(A,r Int A*A) <-> irrefl(A,r)";
-by (Blast_tac 1);
-qed "irrefl_Int_iff";
-
-Goalw [trans_on_def] "trans[A](r Int A*A) <-> trans[A](r)";
-by (Blast_tac 1);
-qed "trans_on_Int_iff";
-
-Goalw [part_ord_def] "part_ord(A,r Int A*A) <-> part_ord(A,r)";
-by (simp_tac (simpset() addsimps [irrefl_Int_iff, trans_on_Int_iff]) 1);
-qed "part_ord_Int_iff";
-
-Goalw [linear_def] "linear(A,r Int A*A) <-> linear(A,r)";
-by (Blast_tac 1);
-qed "linear_Int_iff";
-
-Goalw [tot_ord_def] "tot_ord(A,r Int A*A) <-> tot_ord(A,r)";
-by (simp_tac (simpset() addsimps [part_ord_Int_iff, linear_Int_iff]) 1);
-qed "tot_ord_Int_iff";
-
-Goalw [wf_on_def, wf_def] "wf[A](r Int A*A) <-> wf[A](r)";
-by (Fast_tac 1); (*10 times faster than Blast_tac!*)
-qed "wf_on_Int_iff";
-
-Goalw [well_ord_def] "well_ord(A,r Int A*A) <-> well_ord(A,r)";
-by (simp_tac (simpset() addsimps [tot_ord_Int_iff, wf_on_Int_iff]) 1);
-qed "well_ord_Int_iff";
-
-
-(** Relations over the Empty Set **)
-
-Goalw [irrefl_def] "irrefl(0,r)";
-by (Blast_tac 1);
-qed "irrefl_0";
-
-Goalw [trans_on_def] "trans[0](r)";
-by (Blast_tac 1);
-qed "trans_on_0";
-
-Goalw [part_ord_def] "part_ord(0,r)";
-by (simp_tac (simpset() addsimps [irrefl_0, trans_on_0]) 1);
-qed "part_ord_0";
-
-Goalw [linear_def] "linear(0,r)";
-by (Blast_tac 1);
-qed "linear_0";
-
-Goalw [tot_ord_def] "tot_ord(0,r)";
-by (simp_tac (simpset() addsimps [part_ord_0, linear_0]) 1);
-qed "tot_ord_0";
-
-Goalw [wf_on_def, wf_def] "wf[0](r)";
-by (Blast_tac 1);
-qed "wf_on_0";
-
-Goalw [well_ord_def] "well_ord(0,r)";
-by (simp_tac (simpset() addsimps [tot_ord_0, wf_on_0]) 1);
-qed "well_ord_0";
-
-
-(** The unit set is well-ordered by the empty relation (Grabczewski) **)
-
-Goalw [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def]
- "tot_ord({a},0)";
-by (Simp_tac 1);
-qed "tot_ord_unit";
-
-Goalw [wf_on_def, wf_def] "wf[{a}](0)";
-by (Fast_tac 1);
-qed "wf_on_unit";
-
-Goalw [well_ord_def] "well_ord({a},0)";
-by (simp_tac (simpset() addsimps [tot_ord_unit, wf_on_unit]) 1);
-qed "well_ord_unit";
-
-
-(** Order-preserving (monotone) maps **)
-
-Goalw [mono_map_def]
- "f: mono_map(A,r,B,s) ==> f: A->B";
-by (etac CollectD1 1);
-qed "mono_map_is_fun";
-
-Goalw [mono_map_def, inj_def]
- "[| linear(A,r); wf[B](s); f: mono_map(A,r,B,s) |] ==> f: inj(A,B)";
-by (Clarify_tac 1);
-by (linear_case_tac 1);
-by (REPEAT
- (EVERY [eresolve_tac [wf_on_not_refl RS notE] 1,
- etac ssubst 2,
- Fast_tac 2,
- REPEAT (ares_tac [apply_type] 1)]));
-qed "mono_map_is_inj";
-
-
-(** Order-isomorphisms -- or similarities, as Suppes calls them **)
-
-val prems = Goalw [ord_iso_def]
- "[| f: bij(A, B); \
-\ !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s \
-\ |] ==> f: ord_iso(A,r,B,s)";
-by (blast_tac (claset() addSIs prems) 1);
-qed "ord_isoI";
-
-Goalw [ord_iso_def, mono_map_def]
- "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)";
-by (blast_tac (claset() addSDs [bij_is_fun]) 1);
-qed "ord_iso_is_mono_map";
-
-Goalw [ord_iso_def]
- "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 [ord_iso_def]
- "[| f: ord_iso(A,r,B,s); <x,y>: r; x:A; y:A |] ==> <f`x, f`y> : s";
-by (Blast_tac 1);
-qed "ord_iso_apply";
-
-(*Rewriting with bijections and converse (function inverse)*)
-val bij_inverse_ss =
- simpset() setSolver (mk_solver ""
- (type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj,
- inj_is_fun, comp_fun, comp_bij])))
- addsimps [right_inverse_bij];
-
-Goalw [ord_iso_def]
- "[| f: ord_iso(A,r,B,s); <x,y>: s; x:B; y:B |] \
-\ ==> <converse(f) ` x, converse(f) ` y> : r";
-by (etac CollectE 1);
-by (etac (bspec RS bspec RS iffD2) 1);
-by (REPEAT (eresolve_tac [asm_rl,
- bij_converse_bij RS bij_is_fun RS apply_type] 1));
-by (asm_simp_tac bij_inverse_ss 1);
-qed "ord_iso_converse";
-
-
-(** Symmetry and Transitivity Rules **)
-
-(*Reflexivity of similarity*)
-Goal "id(A): ord_iso(A,r,A,r)";
-by (resolve_tac [id_bij RS ord_isoI] 1);
-by (Asm_simp_tac 1);
-qed "ord_iso_refl";
-
-(*Symmetry of similarity*)
-Goalw [ord_iso_def] "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)";
-by (force_tac (claset(), bij_inverse_ss) 1);
-qed "ord_iso_sym";
-
-(*Transitivity of similarity*)
-Goalw [mono_map_def]
- "[| g: mono_map(A,r,B,s); f: mono_map(B,s,C,t) |] ==> \
-\ (f O g): mono_map(A,r,C,t)";
-by (force_tac (claset(), bij_inverse_ss) 1);
-qed "mono_map_trans";
-
-(*Transitivity of similarity: the order-isomorphism relation*)
-Goalw [ord_iso_def]
- "[| g: ord_iso(A,r,B,s); f: ord_iso(B,s,C,t) |] ==> \
-\ (f O g): ord_iso(A,r,C,t)";
-by (force_tac (claset(), bij_inverse_ss) 1);
-qed "ord_iso_trans";
-
-(** Two monotone maps can make an order-isomorphism **)
-
-Goalw [ord_iso_def, mono_map_def]
- "[| 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;
-by (REPEAT_FIRST (ares_tac [fg_imp_bijective]));
-by (Blast_tac 1);
-by (subgoal_tac "<g`(f`x), g`(f`y)> : r" 1);
-by (blast_tac (claset() addIs [apply_funtype]) 2);
-by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff RS iffD1]) 1);
-qed "mono_ord_isoI";
-
-Goal "[| 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 [part_ord_def, irrefl_def, trans_on_def, ord_iso_def]
- "[| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)";
-by (Asm_simp_tac 1);
-by (fast_tac (claset() addIs [bij_is_fun RS apply_type]) 1);
-qed "part_ord_ord_iso";
-
-Goalw [linear_def, ord_iso_def]
- "[| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)";
-by (Asm_simp_tac 1);
-by Safe_tac;
-by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1);
-by (safe_tac (claset() addSEs [bij_is_fun RS apply_type]));
-by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1);
-by (asm_full_simp_tac bij_inverse_ss 1);
-qed "linear_ord_iso";
-
-Goalw [wf_on_def, wf_def, ord_iso_def]
- "[| 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 (simpset() addcongs [conj_cong2]) 1);
-by Safe_tac;
-by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1);
-by (safe_tac (claset() addSIs [equalityI]));
-by (ALLGOALS (blast_tac
- (claset() addSDs [equalityD1] addIs [bij_is_fun RS apply_type])));
-qed "wf_on_ord_iso";
-
-Goalw [well_ord_def, tot_ord_def]
- "[| well_ord(B,s); f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)";
-by (fast_tac
- (claset() 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 Kunen's Lemma 6.1, etc.
- Simple proof from Halmos, page 72*)
-Goalw [well_ord_def, ord_iso_def]
- "[| well_ord(A,r); f: ord_iso(A,r, A',r); A'<= A; y: A |] \
-\ ==> ~ <f`y, y>: r";
-by (REPEAT (eresolve_tac [conjE, CollectE] 1));
-by (wf_on_ind_tac "y" [] 1);
-by (dres_inst_tac [("a","y1")] (bij_is_fun RS apply_type) 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-qed "well_ord_iso_subset_lemma";
-
-(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
- of a well-ordering*)
-Goal "[| well_ord(A,r); f : ord_iso(A, r, pred(A,x,r), r); x:A |] ==> P";
-by (metacut_tac well_ord_iso_subset_lemma 1);
-by (REPEAT_FIRST (ares_tac [pred_subset]));
-(*Now we know f`x < x *)
-by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type),
- assume_tac]);
-(*Now we also know f`x : pred(A,x,r); contradiction! *)
-by (asm_full_simp_tac (simpset() addsimps [well_ord_def, pred_def]) 1);
-qed "well_ord_iso_predE";
-
-(*Simple consequence of Lemma 6.1*)
-Goal "[| well_ord(A,r); f : ord_iso(pred(A,a,r), r, pred(A,c,r), r); \
-\ a:A; c:A |] ==> a=c";
-by (ftac well_ord_is_trans_on 1);
-by (ftac well_ord_is_linear 1);
-by (linear_case_tac 1);
-by (dtac ord_iso_sym 1);
-(*two symmetric cases*)
-by (auto_tac (claset() addSEs [pred_subset RSN (2, well_ord_subset) RS
- well_ord_iso_predE]
- addSIs [predI],
- simpset() addsimps [trans_pred_pred_eq]));
-qed "well_ord_iso_pred_eq";
-
-(*Does not assume r is a wellordering!*)
-Goalw [ord_iso_def, pred_def]
- "[|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
- (simpset() addsimps [[bij_is_fun, Collect_subset] MRS image_fun]) 1);
-by (rtac equalityI 1);
-by (safe_tac (claset() addSEs [bij_is_fun RS apply_type]));
-by (rtac RepFun_eqI 1);
-by (blast_tac (claset() addSIs [right_inverse_bij RS sym]) 1);
-by (asm_simp_tac bij_inverse_ss 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 "[| 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 (simpset() addsimps [ord_iso_image_pred RS sym]) 1);
-by (rewtac ord_iso_def);
-by (etac CollectE 1);
-by (rtac CollectI 1);
-by (eresolve_tac [[bij_is_inj, pred_subset] MRS restrict_bij] 1);
-by (ftac bij_is_fun 1);
-by (auto_tac (claset(), simpset() addsimps [pred_def]));
-qed "ord_iso_restrict_pred";
-
-(*Tricky; a lot of forward proof!*)
-Goal "[| well_ord(A,r); well_ord(B,s); <a,c>: 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 |] ==> <b,d>: 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 1);
-by (rtac well_ord_iso_pred_eq 1);
-by (REPEAT_SOME assume_tac);
-by (ftac ord_iso_restrict_pred 1 THEN
- REPEAT1 (eresolve_tac [asm_rl, predI] 1));
-by (asm_full_simp_tac
- (simpset() 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";
-
-val bij_apply_cs = claset() addSIs [bij_converse_bij]
- addIs [ord_iso_is_bij, bij_is_fun, apply_funtype];
-
-(*See Halmos, page 72*)
-Goal "[| well_ord(A,r); \
-\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s); y: A |] \
-\ ==> ~ <g`y, f`y> : s";
-by (ftac well_ord_iso_subset_lemma 1);
-by (res_inst_tac [("f","converse(f)"), ("g","g")] ord_iso_trans 1);
-by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym]));
-by Safe_tac;
-by (ftac ord_iso_converse 1);
-by (EVERY (map (blast_tac bij_apply_cs) [1,1,1]));
-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 "[| well_ord(A,r); \
-\ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s) |] ==> f = g";
-by (rtac fun_extension 1);
-by (REPEAT (etac (ord_iso_is_bij RS bij_is_fun) 1));
-by (subgoals_tac ["f`x : B", "g`x : B", "linear(B,s)"] 1);
-by (REPEAT (blast_tac bij_apply_cs 3));
-by (dtac well_ord_ord_iso 2 THEN etac ord_iso_sym 2);
-by (asm_full_simp_tac (simpset() addsimps [tot_ord_def, well_ord_def]) 2);
-by (linear_case_tac 1);
-by (DEPTH_SOLVE (eresolve_tac [asm_rl, well_ord_iso_unique_lemma RS notE] 1));
-qed "well_ord_iso_unique";
-
-
-(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
-
-Goalw [ord_iso_map_def] "ord_iso_map(A,r,B,s) <= A*B";
-by (Blast_tac 1);
-qed "ord_iso_map_subset";
-
-Goalw [ord_iso_map_def] "domain(ord_iso_map(A,r,B,s)) <= A";
-by (Blast_tac 1);
-qed "domain_ord_iso_map";
-
-Goalw [ord_iso_map_def] "range(ord_iso_map(A,r,B,s)) <= B";
-by (Blast_tac 1);
-qed "range_ord_iso_map";
-
-Goalw [ord_iso_map_def]
- "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)";
-by (blast_tac (claset() addIs [ord_iso_sym]) 1);
-qed "converse_ord_iso_map";
-
-Goalw [ord_iso_map_def, function_def]
- "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))";
-by (blast_tac (claset() addIs [well_ord_iso_pred_eq,
- ord_iso_sym, ord_iso_trans]) 1);
-qed "function_ord_iso_map";
-
-Goal "well_ord(B,s) ==> 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
- (simpset() addsimps [Pi_iff, function_ord_iso_map,
- ord_iso_map_subset RS domain_times_range]) 1);
-qed "ord_iso_map_fun";
-
-Goalw [mono_map_def]
- "[| 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 (simpset() addsimps [ord_iso_map_fun]) 1);
-by Safe_tac;
-by (subgoals_tac ["x:A", "ya:A", "y:B", "yb:B"] 1);
-by (REPEAT
- (blast_tac (claset() addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
-by (asm_simp_tac
- (simpset() addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1);
-by (rewtac ord_iso_map_def);
-by Safe_tac;
-by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac);
-qed "ord_iso_map_mono_map";
-
-Goalw [mono_map_def]
- "[| 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 (rtac well_ord_mono_ord_isoI 1);
-by (resolve_tac [converse_ord_iso_map RS subst] 4);
-by (asm_simp_tac
- (simpset() addsimps [ord_iso_map_subset RS converse_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";
-
-(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*)
-Goalw [ord_iso_map_def]
- "[| well_ord(A,r); well_ord(B,s); \
-\ a: A; a ~: domain(ord_iso_map(A,r,B,s)) \
-\ |] ==> domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)";
-by (safe_tac (claset() addSIs [predI]));
-(*Case analysis on xaa vs a in r *)
-by (forw_inst_tac [("A","A")] well_ord_is_linear 1);
-by (linear_case_tac 1);
-(*Trivial case: a=xa*)
-by (Blast_tac 2);
-(*Harder case: <a, xa>: 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 (ftac ord_iso_restrict_pred 1 THEN
- REPEAT1 (eresolve_tac [asm_rl, predI] 1));
-by (asm_full_simp_tac
- (simpset() addsplits [split_if_asm]
- addsimps [well_ord_is_trans_on, trans_pred_pred_eq,
- domain_UN, domain_Union]) 1);
-by (Blast_tac 1);
-qed "domain_ord_iso_map_subset";
-
-(*For the 4-way case analysis in the main result*)
-Goal "[| 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 (ftac 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 Safe_tac;
-(*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 (claset()) below; that would use rules like domainE!*)
-by (blast_tac (claset() addSEs [predE]) 2);
-by (REPEAT (ares_tac [domain_ord_iso_map_subset] 1));
-qed "domain_ord_iso_map_cases";
-
-(*As above, by duality*)
-Goal "[| 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 (simpset() addsimps [domain_ord_iso_map_cases]) 1);
-qed "range_ord_iso_map_cases";
-
-(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
-Goal "[| 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 (dtac ord_iso_map_ord_iso THEN' assume_tac THEN'
- asm_full_simp_tac (simpset() addsimps [bexI])));
-by (resolve_tac [wf_on_not_refl RS notE] 1);
-by (etac well_ord_is_wf 1);
-by (assume_tac 1);
-by (subgoal_tac "<x,y>: ord_iso_map(A,r,B,s)" 1);
-by (dtac rangeI 1);
-by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1);
-by (rewtac ord_iso_map_def);
-by (Blast_tac 1);
-qed "well_ord_trichotomy";
-
-
-(*** Properties of converse(r), by Krzysztof Grabczewski ***)
-
-Goalw [irrefl_def] "irrefl(A,r) ==> irrefl(A,converse(r))";
-by (Blast_tac 1);
-qed "irrefl_converse";
-
-Goalw [trans_on_def] "trans[A](r) ==> trans[A](converse(r))";
-by (Blast_tac 1);
-qed "trans_on_converse";
-
-Goalw [part_ord_def] "part_ord(A,r) ==> part_ord(A,converse(r))";
-by (blast_tac (claset() addSIs [irrefl_converse, trans_on_converse]) 1);
-qed "part_ord_converse";
-
-Goalw [linear_def] "linear(A,r) ==> linear(A,converse(r))";
-by (Blast_tac 1);
-qed "linear_converse";
-
-Goalw [tot_ord_def] "tot_ord(A,r) ==> tot_ord(A,converse(r))";
-by (blast_tac (claset() addSIs [part_ord_converse, linear_converse]) 1);
-qed "tot_ord_converse";
-
-
-(** By Krzysztof Grabczewski.
- Lemmas involving the first element of a well ordered set **)
-
-Goalw [first_def] "first(b,B,r) ==> b:B";
-by (Blast_tac 1);
-qed "first_is_elem";
-
-Goalw [well_ord_def, wf_on_def, wf_def, first_def]
- "[| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))";
-by (REPEAT (eresolve_tac [conjE,allE,disjE] 1));
-by (contr_tac 1);
-by (etac bexE 1);
-by (res_inst_tac [("a","x")] ex1I 1);
-by (Blast_tac 2);
-by (rewrite_goals_tac [tot_ord_def, linear_def]);
-by (Blast.depth_tac (claset()) 7 1);
-qed "well_ord_imp_ex1_first";
-
-Goal "[| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B";
-by (dtac well_ord_imp_ex1_first 1 THEN REPEAT (assume_tac 1));
-by (rtac first_is_elem 1);
-by (etac theI 1);
-qed "the_first_in";
--- a/src/ZF/Order.thy Sat May 11 20:40:31 2002 +0200
+++ b/src/ZF/Order.thy Mon May 13 09:02:13 2002 +0200
@@ -3,47 +3,717 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Orders in Zermelo-Fraenkel Set Theory
+Orders in Zermelo-Fraenkel Set Theory
+
+Results from the book "Set Theory: an Introduction to Independence Proofs"
+ by Kenneth Kunen. Chapter 1, section 6.
*)
-Order = WF + Perm +
-consts
- part_ord :: [i,i]=>o (*Strict partial ordering*)
- linear, tot_ord :: [i,i]=>o (*Strict total ordering*)
- well_ord :: [i,i]=>o (*Well-ordering*)
- mono_map :: [i,i,i,i]=>i (*Order-preserving maps*)
- ord_iso :: [i,i,i,i]=>i (*Order isomorphisms*)
- pred :: [i,i,i]=>i (*Set of predecessors*)
- ord_iso_map :: [i,i,i,i]=>i (*Construction for linearity theorem*)
-
-defs
- part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
-
- linear_def "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
-
- tot_ord_def "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
-
- well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
-
- mono_map_def "mono_map(A,r,B,s) ==
- {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
-
- ord_iso_def "ord_iso(A,r,B,s) ==
- {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
-
- pred_def "pred(A,x,r) == {y:A. <y,x>:r}"
-
- ord_iso_map_def
- "ord_iso_map(A,r,B,s) ==
- UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
+theory Order = WF + Perm:
constdefs
- first :: [i, i, i] => o
+ part_ord :: "[i,i]=>o" (*Strict partial ordering*)
+ "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
+
+ linear :: "[i,i]=>o" (*Strict total ordering*)
+ "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
+
+ tot_ord :: "[i,i]=>o" (*Strict total ordering*)
+ "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
+
+ well_ord :: "[i,i]=>o" (*Well-ordering*)
+ "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
+
+ mono_map :: "[i,i,i,i]=>i" (*Order-preserving maps*)
+ "mono_map(A,r,B,s) ==
+ {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
+
+ ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*)
+ "ord_iso(A,r,B,s) ==
+ {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
+
+ pred :: "[i,i,i]=>i" (*Set of predecessors*)
+ "pred(A,x,r) == {y:A. <y,x>:r}"
+
+ ord_iso_map :: "[i,i,i,i]=>i" (*Construction for linearity theorem*)
+ "ord_iso_map(A,r,B,s) ==
+ UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
+
+ first :: "[i, i, i] => o"
"first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
+
syntax (xsymbols)
- ord_iso :: [i,i,i,i]=>i ("(\\<langle>_, _\\<rangle> \\<cong>/ \\<langle>_, _\\<rangle>)" 51)
+ ord_iso :: "[i,i,i,i]=>i" ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)
+
+
+(** Basic properties of the definitions **)
+
+(*needed?*)
+lemma part_ord_Imp_asym:
+ "part_ord(A,r) ==> asym(r Int A*A)"
+by (unfold part_ord_def irrefl_def trans_on_def asym_def, blast)
+
+lemma linearE:
+ "[| linear(A,r); x:A; y:A;
+ <x,y>:r ==> P; x=y ==> P; <y,x>:r ==> P |]
+ ==> P"
+by (simp add: linear_def, blast)
+
+
+(** General properties of well_ord **)
+
+lemma well_ordI:
+ "[| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"
+apply (simp add: irrefl_def part_ord_def tot_ord_def
+ trans_on_def well_ord_def wf_on_not_refl)
+apply (fast elim: linearE wf_on_asym wf_on_chain3)
+done
+
+lemma well_ord_is_wf:
+ "well_ord(A,r) ==> wf[A](r)"
+by (unfold well_ord_def, safe)
+
+lemma well_ord_is_trans_on:
+ "well_ord(A,r) ==> trans[A](r)"
+by (unfold well_ord_def tot_ord_def part_ord_def, safe)
+
+lemma well_ord_is_linear: "well_ord(A,r) ==> linear(A,r)"
+by (unfold well_ord_def tot_ord_def, blast)
+
+
+(** Derived rules for pred(A,x,r) **)
+
+lemma pred_iff: "y : pred(A,x,r) <-> <y,x>:r & y:A"
+by (unfold pred_def, blast)
+
+lemmas predI = conjI [THEN pred_iff [THEN iffD2]]
+
+lemma predE: "[| y: pred(A,x,r); [| y:A; <y,x>:r |] ==> P |] ==> P"
+by (simp add: pred_def)
+
+lemma pred_subset_under: "pred(A,x,r) <= r -`` {x}"
+by (simp add: pred_def, blast)
+
+lemma pred_subset: "pred(A,x,r) <= A"
+by (simp add: pred_def, blast)
+
+lemma pred_pred_eq:
+ "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)"
+by (simp add: pred_def, blast)
+
+lemma trans_pred_pred_eq:
+ "[| trans[A](r); <y,x>:r; x:A; y:A |]
+ ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"
+by (unfold trans_on_def pred_def, blast)
+
+
+(** 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*)
+lemma part_ord_subset:
+ "[| part_ord(A,r); B<=A |] ==> part_ord(B,r)"
+by (unfold part_ord_def irrefl_def trans_on_def, blast)
+
+lemma linear_subset:
+ "[| linear(A,r); B<=A |] ==> linear(B,r)"
+by (unfold linear_def, blast)
+
+lemma tot_ord_subset:
+ "[| tot_ord(A,r); B<=A |] ==> tot_ord(B,r)"
+apply (unfold tot_ord_def)
+apply (fast elim!: part_ord_subset linear_subset)
+done
+
+lemma well_ord_subset:
+ "[| well_ord(A,r); B<=A |] ==> well_ord(B,r)"
+apply (unfold well_ord_def)
+apply (fast elim!: tot_ord_subset wf_on_subset_A)
+done
+
+
+(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
+
+lemma irrefl_Int_iff: "irrefl(A,r Int A*A) <-> irrefl(A,r)"
+by (unfold irrefl_def, blast)
+
+lemma trans_on_Int_iff: "trans[A](r Int A*A) <-> trans[A](r)"
+by (unfold trans_on_def, blast)
+
+lemma part_ord_Int_iff: "part_ord(A,r Int A*A) <-> part_ord(A,r)"
+apply (unfold part_ord_def)
+apply (simp add: irrefl_Int_iff trans_on_Int_iff)
+done
+
+lemma linear_Int_iff: "linear(A,r Int A*A) <-> linear(A,r)"
+by (unfold linear_def, blast)
+
+lemma tot_ord_Int_iff: "tot_ord(A,r Int A*A) <-> tot_ord(A,r)"
+apply (unfold tot_ord_def)
+apply (simp add: part_ord_Int_iff linear_Int_iff)
+done
+
+lemma wf_on_Int_iff: "wf[A](r Int A*A) <-> wf[A](r)"
+apply (unfold wf_on_def wf_def, fast) (*10 times faster than Blast_tac!*)
+done
+
+lemma well_ord_Int_iff: "well_ord(A,r Int A*A) <-> well_ord(A,r)"
+apply (unfold well_ord_def)
+apply (simp add: tot_ord_Int_iff wf_on_Int_iff)
+done
+
+
+(** Relations over the Empty Set **)
+
+lemma irrefl_0: "irrefl(0,r)"
+by (unfold irrefl_def, blast)
+
+lemma trans_on_0: "trans[0](r)"
+by (unfold trans_on_def, blast)
+
+lemma part_ord_0: "part_ord(0,r)"
+apply (unfold part_ord_def)
+apply (simp add: irrefl_0 trans_on_0)
+done
+
+lemma linear_0: "linear(0,r)"
+by (unfold linear_def, blast)
+
+lemma tot_ord_0: "tot_ord(0,r)"
+apply (unfold tot_ord_def)
+apply (simp add: part_ord_0 linear_0)
+done
+
+lemma wf_on_0: "wf[0](r)"
+by (unfold wf_on_def wf_def, blast)
+
+lemma well_ord_0: "well_ord(0,r)"
+apply (unfold well_ord_def)
+apply (simp add: tot_ord_0 wf_on_0)
+done
+
+
+(** The unit set is well-ordered by the empty relation (Grabczewski) **)
+
+lemma tot_ord_unit: "tot_ord({a},0)"
+by (simp add: irrefl_def trans_on_def part_ord_def linear_def tot_ord_def)
+
+lemma wf_on_unit: "wf[{a}](0)"
+by (simp add: wf_on_def wf_def, fast)
+
+lemma well_ord_unit: "well_ord({a},0)"
+apply (unfold well_ord_def)
+apply (simp add: tot_ord_unit wf_on_unit)
+done
+
+
+(** Order-preserving (monotone) maps **)
+
+lemma mono_map_is_fun: "f: mono_map(A,r,B,s) ==> f: A->B"
+by (simp add: mono_map_def)
+
+lemma mono_map_is_inj:
+ "[| linear(A,r); wf[B](s); f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"
+apply (unfold mono_map_def inj_def, clarify)
+apply (erule_tac x=w and y=x in linearE, assumption+)
+apply (force intro: apply_type dest: wf_on_not_refl)+
+done
+
+
+(** Order-isomorphisms -- or similarities, as Suppes calls them **)
+
+lemma ord_isoI:
+ "[| f: bij(A, B);
+ !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s |]
+ ==> f: ord_iso(A,r,B,s)"
+by (simp add: ord_iso_def)
+
+lemma ord_iso_is_mono_map:
+ "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)"
+apply (simp add: ord_iso_def mono_map_def)
+apply (blast dest!: bij_is_fun)
+done
+
+lemma ord_iso_is_bij:
+ "f: ord_iso(A,r,B,s) ==> f: bij(A,B)"
+by (simp add: ord_iso_def)
+
+(*Needed? But ord_iso_converse is!*)
+lemma ord_iso_apply:
+ "[| f: ord_iso(A,r,B,s); <x,y>: r; x:A; y:A |] ==> <f`x, f`y> : s"
+by (simp add: ord_iso_def, blast)
+
+lemma ord_iso_converse:
+ "[| f: ord_iso(A,r,B,s); <x,y>: s; x:B; y:B |]
+ ==> <converse(f) ` x, converse(f) ` y> : r"
+apply (simp add: ord_iso_def, clarify)
+apply (erule bspec [THEN bspec, THEN iffD2])
+apply (erule asm_rl bij_converse_bij [THEN bij_is_fun, THEN apply_type])+
+apply (auto simp add: right_inverse_bij)
+done
+
+
+(** Symmetry and Transitivity Rules **)
+
+(*Reflexivity of similarity*)
+lemma ord_iso_refl: "id(A): ord_iso(A,r,A,r)"
+by (rule id_bij [THEN ord_isoI], simp)
+
+(*Symmetry of similarity*)
+lemma ord_iso_sym: "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"
+apply (simp add: ord_iso_def)
+apply (auto simp add: right_inverse_bij bij_converse_bij
+ bij_is_fun [THEN apply_funtype])
+done
+
+(*Transitivity of similarity*)
+lemma mono_map_trans:
+ "[| g: mono_map(A,r,B,s); f: mono_map(B,s,C,t) |]
+ ==> (f O g): mono_map(A,r,C,t)"
+apply (unfold mono_map_def)
+apply (auto simp add: comp_fun)
+done
+
+(*Transitivity of similarity: the order-isomorphism relation*)
+lemma ord_iso_trans:
+ "[| g: ord_iso(A,r,B,s); f: ord_iso(B,s,C,t) |]
+ ==> (f O g): ord_iso(A,r,C,t)"
+apply (unfold ord_iso_def, clarify)
+apply (frule bij_is_fun [of f])
+apply (frule bij_is_fun [of g])
+apply (auto simp add: comp_bij)
+done
+
+(** Two monotone maps can make an order-isomorphism **)
+
+lemma mono_ord_isoI:
+ "[| 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)"
+apply (simp add: ord_iso_def mono_map_def, safe)
+apply (intro fg_imp_bijective, auto)
+apply (subgoal_tac "<g` (f`x), g` (f`y) > : r")
+apply (simp add: comp_eq_id_iff [THEN iffD1])
+apply (blast intro: apply_funtype)
+done
+
+lemma well_ord_mono_ord_isoI:
+ "[| 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)"
+apply (intro mono_ord_isoI, auto)
+apply (frule mono_map_is_fun [THEN fun_is_rel])
+apply (erule converse_converse [THEN subst], rule left_comp_inverse)
+apply (blast intro: left_comp_inverse mono_map_is_inj well_ord_is_linear
+ well_ord_is_wf)+
+done
+
+
+(** Order-isomorphisms preserve the ordering's properties **)
+
+lemma part_ord_ord_iso:
+ "[| part_ord(B,s); f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)"
+apply (simp add: part_ord_def irrefl_def trans_on_def ord_iso_def)
+apply (fast intro: bij_is_fun [THEN apply_type])
+done
+
+lemma linear_ord_iso:
+ "[| linear(B,s); f: ord_iso(A,r,B,s) |] ==> linear(A,r)"
+apply (simp add: linear_def ord_iso_def, safe)
+apply (drule_tac x1 = "f`x" and x = "f`xa" in bspec [THEN bspec])
+apply (safe elim!: bij_is_fun [THEN apply_type])
+apply (drule_tac t = "op ` (converse (f))" in subst_context)
+apply (simp add: left_inverse_bij)
+done
+
+lemma wf_on_ord_iso:
+ "[| wf[B](s); f: ord_iso(A,r,B,s) |] ==> wf[A](r)"
+apply (simp add: wf_on_def wf_def ord_iso_def, safe)
+apply (drule_tac x = "{f`z. z:Z Int A}" in spec)
+apply (safe intro!: equalityI)
+apply (blast dest!: equalityD1 intro: bij_is_fun [THEN apply_type])+
+done
+
+lemma well_ord_ord_iso:
+ "[| well_ord(B,s); f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)"
+apply (unfold well_ord_def tot_ord_def)
+apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso)
+done
+(*** Main results of Kunen, Chapter 1 section 6 ***)
+
+(*Inductive argument for Kunen's Lemma 6.1, etc.
+ Simple proof from Halmos, page 72*)
+lemma well_ord_iso_subset_lemma:
+ "[| well_ord(A,r); f: ord_iso(A,r, A',r); A'<= A; y: A |]
+ ==> ~ <f`y, y>: r"
+apply (simp add: well_ord_def ord_iso_def)
+apply (elim conjE CollectE)
+apply (rule_tac a=y in wf_on_induct, assumption+)
+apply (blast dest: bij_is_fun [THEN apply_type])
+done
+
+(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
+ of a well-ordering*)
+lemma well_ord_iso_predE:
+ "[| well_ord(A,r); f : ord_iso(A, r, pred(A,x,r), r); x:A |] ==> P"
+apply (insert well_ord_iso_subset_lemma [of A r f "pred(A,x,r)" x])
+apply (simp add: pred_subset)
+(*Now we know f`x < x *)
+apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
+(*Now we also know f`x : pred(A,x,r); contradiction! *)
+apply (simp add: well_ord_def pred_def)
+done
+
+(*Simple consequence of Lemma 6.1*)
+lemma well_ord_iso_pred_eq:
+ "[| well_ord(A,r); f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);
+ a:A; c:A |] ==> a=c"
+apply (frule well_ord_is_trans_on)
+apply (frule well_ord_is_linear)
+apply (erule_tac x=a and y=c in linearE, assumption+)
+apply (drule ord_iso_sym)
+(*two symmetric cases*)
+apply (auto elim!: well_ord_subset [OF _ pred_subset, THEN well_ord_iso_predE]
+ intro!: predI
+ simp add: trans_pred_pred_eq)
+done
+
+(*Does not assume r is a wellordering!*)
+lemma ord_iso_image_pred:
+ "[|f : ord_iso(A,r,B,s); a:A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)"
+apply (unfold ord_iso_def pred_def)
+apply (erule CollectE)
+apply (simp (no_asm_simp) add: image_fun [OF bij_is_fun Collect_subset])
+apply (rule equalityI)
+apply (safe elim!: bij_is_fun [THEN apply_type])
+apply (rule RepFun_eqI)
+apply (blast intro!: right_inverse_bij [symmetric])
+apply (auto simp add: right_inverse_bij bij_is_fun [THEN apply_funtype])
+done
+
+(*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.*)
+lemma ord_iso_restrict_pred: "[| 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)"
+apply (simp add: ord_iso_image_pred [symmetric])
+apply (simp add: ord_iso_def, clarify)
+apply (rule conjI)
+apply (erule restrict_bij [OF bij_is_inj pred_subset])
+apply (frule bij_is_fun)
+apply (auto simp add: pred_def)
+done
+
+(*Tricky; a lot of forward proof!*)
+lemma well_ord_iso_preserving:
+ "[| well_ord(A,r); well_ord(B,s); <a,c>: 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 |] ==> <b,d>: s"
+apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], (erule asm_rl predI predE)+)
+apply (subgoal_tac "b = g`a")
+apply (simp (no_asm_simp))
+apply (rule well_ord_iso_pred_eq, auto)
+apply (frule ord_iso_restrict_pred, (erule asm_rl predI)+)
+apply (simp add: well_ord_is_trans_on trans_pred_pred_eq)
+apply (erule ord_iso_sym [THEN ord_iso_trans], assumption)
+done
+
+(*See Halmos, page 72*)
+lemma well_ord_iso_unique_lemma:
+ "[| well_ord(A,r);
+ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s); y: A |]
+ ==> ~ <g`y, f`y> : s"
+apply (frule well_ord_iso_subset_lemma)
+apply (rule_tac f = "converse (f) " and g = g in ord_iso_trans)
+apply auto
+apply (blast intro: ord_iso_sym)
+apply (frule ord_iso_is_bij [of f])
+apply (frule ord_iso_is_bij [of g])
+apply (frule ord_iso_converse)
+apply (blast intro!: bij_converse_bij
+ intro: bij_is_fun apply_funtype)+
+apply (erule notE)
+apply (simp add: left_inverse_bij bij_converse_bij bij_is_fun
+ comp_fun_apply [of _ A B _ A])
+done
+
+
+(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
+lemma well_ord_iso_unique: "[| well_ord(A,r);
+ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s) |] ==> f = g"
+apply (rule fun_extension)
+apply (erule ord_iso_is_bij [THEN bij_is_fun])+
+apply (subgoal_tac "f`x : B & g`x : B & linear(B,s)")
+ apply (simp add: linear_def)
+ apply (blast dest: well_ord_iso_unique_lemma)
+apply (blast intro: ord_iso_is_bij bij_is_fun apply_funtype
+ well_ord_is_linear well_ord_ord_iso ord_iso_sym)
+done
+
+(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
+
+lemma ord_iso_map_subset: "ord_iso_map(A,r,B,s) <= A*B"
+by (unfold ord_iso_map_def, blast)
+
+lemma domain_ord_iso_map: "domain(ord_iso_map(A,r,B,s)) <= A"
+by (unfold ord_iso_map_def, blast)
+
+lemma range_ord_iso_map: "range(ord_iso_map(A,r,B,s)) <= B"
+by (unfold ord_iso_map_def, blast)
+
+lemma converse_ord_iso_map:
+ "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)"
+apply (unfold ord_iso_map_def)
+apply (blast intro: ord_iso_sym)
+done
+
+lemma function_ord_iso_map:
+ "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))"
+apply (unfold ord_iso_map_def function_def)
+apply (blast intro: well_ord_iso_pred_eq ord_iso_sym ord_iso_trans)
+done
+
+lemma ord_iso_map_fun: "well_ord(B,s) ==> ord_iso_map(A,r,B,s)
+ : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))"
+by (simp add: Pi_iff function_ord_iso_map
+ ord_iso_map_subset [THEN domain_times_range])
+
+lemma ord_iso_map_mono_map:
+ "[| 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)"
+apply (unfold mono_map_def)
+apply (simp (no_asm_simp) add: ord_iso_map_fun)
+apply safe
+apply (subgoal_tac "x:A & ya:A & y:B & yb:B")
+ apply (simp add: apply_equality [OF _ ord_iso_map_fun])
+ apply (unfold ord_iso_map_def)
+ apply (blast intro: well_ord_iso_preserving, blast)
+done
+
+lemma ord_iso_map_ord_iso:
+ "[| 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)"
+apply (rule well_ord_mono_ord_isoI)
+ prefer 4
+ apply (rule converse_ord_iso_map [THEN subst])
+ apply (simp add: ord_iso_map_mono_map
+ ord_iso_map_subset [THEN converse_converse])
+apply (blast intro!: domain_ord_iso_map range_ord_iso_map
+ intro: well_ord_subset ord_iso_map_mono_map)+
+done
+
+
+(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*)
+lemma domain_ord_iso_map_subset:
+ "[| well_ord(A,r); well_ord(B,s);
+ a: A; a ~: domain(ord_iso_map(A,r,B,s)) |]
+ ==> domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)"
+apply (unfold ord_iso_map_def)
+apply (safe intro!: predI)
+(*Case analysis on xa vs a in r *)
+apply (simp (no_asm_simp))
+apply (frule_tac A = A in well_ord_is_linear)
+apply (rename_tac b y f)
+apply (erule_tac x=b and y=a in linearE, assumption+)
+(*Trivial case: b=a*)
+apply clarify
+apply blast
+(*Harder case: <a, xa>: r*)
+apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type],
+ (erule asm_rl predI predE)+)
+apply (frule ord_iso_restrict_pred)
+ apply (simp add: pred_iff)
+apply (simp split: split_if_asm
+ add: well_ord_is_trans_on trans_pred_pred_eq domain_UN domain_Union, blast)
+done
+
+(*For the 4-way case analysis in the main result*)
+lemma domain_ord_iso_map_cases:
+ "[| 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))"
+apply (frule well_ord_is_wf)
+apply (unfold wf_on_def wf_def)
+apply (drule_tac x = "A-domain (ord_iso_map (A,r,B,s))" in spec)
+apply safe
+(*The first case: the domain equals A*)
+apply (rule domain_ord_iso_map [THEN equalityI])
+apply (erule Diff_eq_0_iff [THEN iffD1])
+(*The other case: the domain equals an initial segment*)
+apply (blast del: domainI subsetI
+ elim!: predE
+ intro!: domain_ord_iso_map_subset
+ intro: subsetI)+
+done
+
+(*As above, by duality*)
+lemma range_ord_iso_map_cases:
+ "[| 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))"
+apply (rule converse_ord_iso_map [THEN subst])
+apply (simp add: domain_ord_iso_map_cases)
+done
+
+(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
+lemma well_ord_trichotomy:
+ "[| 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))"
+apply (frule_tac B = B in domain_ord_iso_map_cases, assumption)
+apply (frule_tac B = B in range_ord_iso_map_cases, assumption)
+apply (drule ord_iso_map_ord_iso, assumption)
+apply (elim disjE bexE)
+ apply (simp_all add: bexI)
+apply (rule wf_on_not_refl [THEN notE])
+ apply (erule well_ord_is_wf)
+ apply assumption
+apply (subgoal_tac "<x,y>: ord_iso_map (A,r,B,s) ")
+ apply (drule rangeI)
+ apply (simp add: pred_def)
+apply (unfold ord_iso_map_def, blast)
+done
+
+
+(*** Properties of converse(r), by Krzysztof Grabczewski ***)
+
+lemma irrefl_converse: "irrefl(A,r) ==> irrefl(A,converse(r))"
+by (unfold irrefl_def, blast)
+
+lemma trans_on_converse: "trans[A](r) ==> trans[A](converse(r))"
+by (unfold trans_on_def, blast)
+
+lemma part_ord_converse: "part_ord(A,r) ==> part_ord(A,converse(r))"
+apply (unfold part_ord_def)
+apply (blast intro!: irrefl_converse trans_on_converse)
+done
+
+lemma linear_converse: "linear(A,r) ==> linear(A,converse(r))"
+by (unfold linear_def, blast)
+
+lemma tot_ord_converse: "tot_ord(A,r) ==> tot_ord(A,converse(r))"
+apply (unfold tot_ord_def)
+apply (blast intro!: part_ord_converse linear_converse)
+done
+
+
+(** By Krzysztof Grabczewski.
+ Lemmas involving the first element of a well ordered set **)
+
+lemma first_is_elem: "first(b,B,r) ==> b:B"
+by (unfold first_def, blast)
+
+lemma well_ord_imp_ex1_first:
+ "[| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"
+apply (unfold well_ord_def wf_on_def wf_def first_def)
+apply (elim conjE allE disjE, blast)
+apply (erule bexE)
+apply (rule_tac a = x in ex1I, auto)
+apply (unfold tot_ord_def linear_def, blast)
+done
+
+lemma the_first_in:
+ "[| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B"
+apply (drule well_ord_imp_ex1_first, assumption+)
+apply (rule first_is_elem)
+apply (erule theI)
+done
+
+ML {*
+val pred_def = thm "pred_def"
+val linear_def = thm "linear_def"
+val part_ord_def = thm "part_ord_def"
+val tot_ord_def = thm "tot_ord_def"
+val well_ord_def = thm "well_ord_def"
+val ord_iso_def = thm "ord_iso_def"
+val mono_map_def = thm "mono_map_def";
+
+val part_ord_Imp_asym = thm "part_ord_Imp_asym";
+val linearE = thm "linearE";
+val well_ordI = thm "well_ordI";
+val well_ord_is_wf = thm "well_ord_is_wf";
+val well_ord_is_trans_on = thm "well_ord_is_trans_on";
+val well_ord_is_linear = thm "well_ord_is_linear";
+val pred_iff = thm "pred_iff";
+val predI = thm "predI";
+val predE = thm "predE";
+val pred_subset_under = thm "pred_subset_under";
+val pred_subset = thm "pred_subset";
+val pred_pred_eq = thm "pred_pred_eq";
+val trans_pred_pred_eq = thm "trans_pred_pred_eq";
+val part_ord_subset = thm "part_ord_subset";
+val linear_subset = thm "linear_subset";
+val tot_ord_subset = thm "tot_ord_subset";
+val well_ord_subset = thm "well_ord_subset";
+val irrefl_Int_iff = thm "irrefl_Int_iff";
+val trans_on_Int_iff = thm "trans_on_Int_iff";
+val part_ord_Int_iff = thm "part_ord_Int_iff";
+val linear_Int_iff = thm "linear_Int_iff";
+val tot_ord_Int_iff = thm "tot_ord_Int_iff";
+val wf_on_Int_iff = thm "wf_on_Int_iff";
+val well_ord_Int_iff = thm "well_ord_Int_iff";
+val irrefl_0 = thm "irrefl_0";
+val trans_on_0 = thm "trans_on_0";
+val part_ord_0 = thm "part_ord_0";
+val linear_0 = thm "linear_0";
+val tot_ord_0 = thm "tot_ord_0";
+val wf_on_0 = thm "wf_on_0";
+val well_ord_0 = thm "well_ord_0";
+val tot_ord_unit = thm "tot_ord_unit";
+val wf_on_unit = thm "wf_on_unit";
+val well_ord_unit = thm "well_ord_unit";
+val mono_map_is_fun = thm "mono_map_is_fun";
+val mono_map_is_inj = thm "mono_map_is_inj";
+val ord_isoI = thm "ord_isoI";
+val ord_iso_is_mono_map = thm "ord_iso_is_mono_map";
+val ord_iso_is_bij = thm "ord_iso_is_bij";
+val ord_iso_apply = thm "ord_iso_apply";
+val ord_iso_converse = thm "ord_iso_converse";
+val ord_iso_refl = thm "ord_iso_refl";
+val ord_iso_sym = thm "ord_iso_sym";
+val mono_map_trans = thm "mono_map_trans";
+val ord_iso_trans = thm "ord_iso_trans";
+val mono_ord_isoI = thm "mono_ord_isoI";
+val well_ord_mono_ord_isoI = thm "well_ord_mono_ord_isoI";
+val part_ord_ord_iso = thm "part_ord_ord_iso";
+val linear_ord_iso = thm "linear_ord_iso";
+val wf_on_ord_iso = thm "wf_on_ord_iso";
+val well_ord_ord_iso = thm "well_ord_ord_iso";
+val well_ord_iso_subset_lemma = thm "well_ord_iso_subset_lemma";
+val well_ord_iso_predE = thm "well_ord_iso_predE";
+val well_ord_iso_pred_eq = thm "well_ord_iso_pred_eq";
+val ord_iso_image_pred = thm "ord_iso_image_pred";
+val ord_iso_restrict_pred = thm "ord_iso_restrict_pred";
+val well_ord_iso_preserving = thm "well_ord_iso_preserving";
+val well_ord_iso_unique_lemma = thm "well_ord_iso_unique_lemma";
+val well_ord_iso_unique = thm "well_ord_iso_unique";
+val ord_iso_map_subset = thm "ord_iso_map_subset";
+val domain_ord_iso_map = thm "domain_ord_iso_map";
+val range_ord_iso_map = thm "range_ord_iso_map";
+val converse_ord_iso_map = thm "converse_ord_iso_map";
+val function_ord_iso_map = thm "function_ord_iso_map";
+val ord_iso_map_fun = thm "ord_iso_map_fun";
+val ord_iso_map_mono_map = thm "ord_iso_map_mono_map";
+val ord_iso_map_ord_iso = thm "ord_iso_map_ord_iso";
+val domain_ord_iso_map_subset = thm "domain_ord_iso_map_subset";
+val domain_ord_iso_map_cases = thm "domain_ord_iso_map_cases";
+val range_ord_iso_map_cases = thm "range_ord_iso_map_cases";
+val well_ord_trichotomy = thm "well_ord_trichotomy";
+val irrefl_converse = thm "irrefl_converse";
+val trans_on_converse = thm "trans_on_converse";
+val part_ord_converse = thm "part_ord_converse";
+val linear_converse = thm "linear_converse";
+val tot_ord_converse = thm "tot_ord_converse";
+val first_is_elem = thm "first_is_elem";
+val well_ord_imp_ex1_first = thm "well_ord_imp_ex1_first";
+val the_first_in = thm "the_first_in";
+*}
+
end
--- a/src/ZF/OrderArith.ML Sat May 11 20:40:31 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,434 +0,0 @@
-(* Title: ZF/OrderArith.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Towards ordinal arithmetic
-*)
-
-(**** Addition of relations -- disjoint sum ****)
-
-(** Rewrite rules. Can be used to obtain introduction rules **)
-
-Goalw [radd_def]
- "<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B";
-by (Blast_tac 1);
-qed "radd_Inl_Inr_iff";
-
-Goalw [radd_def]
- "<Inl(a'), Inl(a)> : radd(A,r,B,s) <-> a':A & a:A & <a',a>:r";
-by (Blast_tac 1);
-qed "radd_Inl_iff";
-
-Goalw [radd_def]
- "<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s";
-by (Blast_tac 1);
-qed "radd_Inr_iff";
-
-Goalw [radd_def]
- "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False";
-by (Blast_tac 1);
-qed "radd_Inr_Inl_iff";
-
-(** Elimination Rule **)
-
-val major::prems = Goalw [radd_def]
- "[| <p',p> : radd(A,r,B,s); \
-\ !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q; \
-\ !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q; \
-\ !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q \
-\ |] ==> Q";
-by (cut_facts_tac [major] 1);
-(*Split into the three cases*)
-by (REPEAT_FIRST (*can't use safe_tac: don't want hyp_subst_tac*)
- (eresolve_tac [CollectE, Pair_inject, conjE, exE, SigmaE, disjE]));
-(*Apply each premise to correct subgoal; can't just use fast_tac
- because hyp_subst_tac would delete equalities too quickly*)
-by (EVERY (map (fn prem =>
- EVERY1 [rtac prem, assume_tac, REPEAT o Fast_tac])
- prems));
-qed "raddE";
-
-(** Type checking **)
-
-Goalw [radd_def] "radd(A,r,B,s) <= (A+B) * (A+B)";
-by (rtac Collect_subset 1);
-qed "radd_type";
-
-bind_thm ("field_radd", radd_type RS field_rel_subset);
-
-(** Linearity **)
-
-AddIffs [radd_Inl_iff, radd_Inr_iff,
- radd_Inl_Inr_iff, radd_Inr_Inl_iff];
-
-Goalw [linear_def]
- "[| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))";
-by (Force_tac 1);
-qed "linear_radd";
-
-
-(** Well-foundedness **)
-
-Goal "[| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))";
-by (rtac wf_onI2 1);
-by (subgoal_tac "ALL x:A. Inl(x): Ba" 1);
-(*Proving the lemma, which is needed twice!*)
-by (thin_tac "y : A + B" 2);
-by (rtac ballI 2);
-by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
-by (best_tac (claset() addSEs [raddE, bspec RS mp]) 2);
-(*Returning to main part of proof*)
-by Safe_tac;
-by (Blast_tac 1);
-by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
-by (best_tac (claset() addSEs [raddE, bspec RS mp]) 1);
-qed "wf_on_radd";
-
-Goal "[| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))";
-by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
-by (rtac (field_radd RSN (2, wf_on_subset_A)) 1);
-by (REPEAT (ares_tac [wf_on_radd] 1));
-qed "wf_radd";
-
-Goal "[| well_ord(A,r); well_ord(B,s) |] ==> \
-\ well_ord(A+B, radd(A,r,B,s))";
-by (rtac well_ordI 1);
-by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_radd]) 1);
-by (asm_full_simp_tac
- (simpset() addsimps [well_ord_def, tot_ord_def, linear_radd]) 1);
-qed "well_ord_radd";
-
-(** An ord_iso congruence law **)
-
-Goal "[| f: bij(A,C); g: bij(B,D) |] ==> \
-\ (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)";
-by (res_inst_tac
- [("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(g)`y))")]
- lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS (asm_simp_tac bij_inverse_ss));
-qed "sum_bij";
-
-Goalw [ord_iso_def]
- "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ==> \
-\ (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) \
-\ : ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))";
-by (safe_tac (claset() addSIs [sum_bij]));
-(*Do the beta-reductions now*)
-by (ALLGOALS (Asm_full_simp_tac));
-by Safe_tac;
-(*8 subgoals!*)
-by (ALLGOALS
- (asm_full_simp_tac
- (simpset() addcongs [conj_cong] addsimps [bij_is_fun RS apply_type])));
-qed "sum_ord_iso_cong";
-
-(*Could we prove an ord_iso result? Perhaps
- ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
-Goal "A Int B = 0 ==> \
-\ (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)";
-by (res_inst_tac [("d", "%z. if z:A then Inl(z) else Inr(z)")]
- lam_bijective 1);
-by Auto_tac;
-qed "sum_disjoint_bij";
-
-(** Associativity **)
-
-Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
-\ : bij((A+B)+C, A+(B+C))";
-by (res_inst_tac [("d", "case(%x. Inl(Inl(x)), case(%x. Inl(Inr(x)), Inr))")]
- lam_bijective 1);
-by Auto_tac;
-qed "sum_assoc_bij";
-
-Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
-\ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), \
-\ A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))";
-by (resolve_tac [sum_assoc_bij RS ord_isoI] 1);
-by Auto_tac;
-qed "sum_assoc_ord_iso";
-
-
-(**** Multiplication of relations -- lexicographic product ****)
-
-(** Rewrite rule. Can be used to obtain introduction rules **)
-
-Goalw [rmult_def]
- "<<a',b'>, <a,b>> : rmult(A,r,B,s) <-> \
-\ (<a',a>: r & a':A & a:A & b': B & b: B) | \
-\ (<b',b>: s & a'=a & a:A & b': B & b: B)";
-by (Blast_tac 1);
-qed "rmult_iff";
-
-AddIffs [rmult_iff];
-
-val major::prems = Goal
- "[| <<a',b'>, <a,b>> : rmult(A,r,B,s); \
-\ [| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q; \
-\ [| <b',b>: s; a:A; a'=a; b':B; b:B |] ==> Q \
-\ |] ==> Q";
-by (rtac (major RS (rmult_iff RS iffD1) RS disjE) 1);
-by (DEPTH_SOLVE (eresolve_tac ([asm_rl, conjE] @ prems) 1));
-qed "rmultE";
-
-(** Type checking **)
-
-Goalw [rmult_def] "rmult(A,r,B,s) <= (A*B) * (A*B)";
-by (rtac Collect_subset 1);
-qed "rmult_type";
-
-bind_thm ("field_rmult", (rmult_type RS field_rel_subset));
-
-(** Linearity **)
-
-val [lina,linb] = goal (the_context ())
- "[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))";
-by (rewtac linear_def); (*Note! the premises are NOT rewritten*)
-by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac SigmaE));
-by (Asm_simp_tac 1);
-by (res_inst_tac [("x","xa"), ("y","xb")] (lina RS linearE) 1);
-by (res_inst_tac [("x","ya"), ("y","yb")] (linb RS linearE) 4);
-by (REPEAT_SOME (Blast_tac));
-qed "linear_rmult";
-
-
-(** Well-foundedness **)
-
-Goal "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))";
-by (rtac wf_onI2 1);
-by (etac SigmaE 1);
-by (etac ssubst 1);
-by (subgoal_tac "ALL b:B. <x,b>: Ba" 1);
-by (Blast_tac 1);
-by (eres_inst_tac [("a","x")] wf_on_induct 1 THEN assume_tac 1);
-by (rtac ballI 1);
-by (eres_inst_tac [("a","b")] wf_on_induct 1 THEN assume_tac 1);
-by (best_tac (claset() addSEs [rmultE, bspec RS mp]) 1);
-qed "wf_on_rmult";
-
-
-Goal "[| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))";
-by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
-by (rtac (field_rmult RSN (2, wf_on_subset_A)) 1);
-by (REPEAT (ares_tac [wf_on_rmult] 1));
-qed "wf_rmult";
-
-Goal "[| well_ord(A,r); well_ord(B,s) |] ==> \
-\ well_ord(A*B, rmult(A,r,B,s))";
-by (rtac well_ordI 1);
-by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_rmult]) 1);
-by (asm_full_simp_tac
- (simpset() addsimps [well_ord_def, tot_ord_def, linear_rmult]) 1);
-qed "well_ord_rmult";
-
-
-(** An ord_iso congruence law **)
-
-Goal "[| f: bij(A,C); g: bij(B,D) |] \
-\ ==> (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)";
-by (res_inst_tac [("d", "%<x,y>. <converse(f)`x, converse(g)`y>")]
- lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS (asm_simp_tac bij_inverse_ss));
-qed "prod_bij";
-
-Goalw [ord_iso_def]
- "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] \
-\ ==> (lam <x,y>:A*B. <f`x, g`y>) \
-\ : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))";
-by (safe_tac (claset() addSIs [prod_bij]));
-by (ALLGOALS
- (asm_full_simp_tac (simpset() addsimps [bij_is_fun RS apply_type])));
-by (blast_tac (claset() addIs [bij_is_inj RS inj_apply_equality]) 1);
-qed "prod_ord_iso_cong";
-
-Goal "(lam z:A. <x,z>) : bij(A, {x}*A)";
-by (res_inst_tac [("d", "snd")] lam_bijective 1);
-by Auto_tac;
-qed "singleton_prod_bij";
-
-(*Used??*)
-Goal "well_ord({x},xr) ==> \
-\ (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))";
-by (resolve_tac [singleton_prod_bij RS ord_isoI] 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addDs [well_ord_is_wf RS wf_on_not_refl]) 1);
-qed "singleton_prod_ord_iso";
-
-(*Here we build a complicated function term, then simplify it using
- case_cong, id_conv, comp_lam, case_case.*)
-Goal "a~:C ==> \
-\ (lam x:C*B + D. case(%x. x, %y.<a,y>, x)) \
-\ : bij(C*B + D, C*B Un {a}*D)";
-by (rtac subst_elem 1);
-by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1);
-by (rtac singleton_prod_bij 1);
-by (rtac sum_disjoint_bij 1);
-by (Blast_tac 1);
-by (asm_simp_tac (simpset() addcongs [case_cong]) 1);
-by (resolve_tac [comp_lam RS trans RS sym] 1);
-by (fast_tac (claset() addSEs [case_type]) 1);
-by (asm_simp_tac (simpset() addsimps [case_case]) 1);
-qed "prod_sum_singleton_bij";
-
-Goal "[| a:A; well_ord(A,r) |] ==> \
-\ (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x)) \
-\ : ord_iso(pred(A,a,r)*B + pred(B,b,s), \
-\ radd(A*B, rmult(A,r,B,s), B, s), \
-\ pred(A,a,r)*B Un {a}*pred(B,b,s), rmult(A,r,B,s))";
-by (resolve_tac [prod_sum_singleton_bij RS ord_isoI] 1);
-by (asm_simp_tac
- (simpset() addsimps [pred_iff, well_ord_is_wf RS wf_on_not_refl]) 1);
-by (auto_tac (claset() addSEs [well_ord_is_wf RS wf_on_asym, predE],
- simpset()));
-qed "prod_sum_singleton_ord_iso";
-
-(** Distributive law **)
-
-Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
-\ : bij((A+B)*C, (A*C)+(B*C))";
-by (res_inst_tac
- [("d", "case(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1);
-by Auto_tac;
-qed "sum_prod_distrib_bij";
-
-Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
-\ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \
-\ (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))";
-by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1);
-by Auto_tac;
-qed "sum_prod_distrib_ord_iso";
-
-(** Associativity **)
-
-Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))";
-by (res_inst_tac [("d", "%<x, <y,z>>. <<x,y>, z>")] lam_bijective 1);
-by Auto_tac;
-qed "prod_assoc_bij";
-
-Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) \
-\ : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), \
-\ A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))";
-by (resolve_tac [prod_assoc_bij RS ord_isoI] 1);
-by Auto_tac;
-qed "prod_assoc_ord_iso";
-
-(**** Inverse image of a relation ****)
-
-(** Rewrite rule **)
-
-Goalw [rvimage_def] "<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A";
-by (Blast_tac 1);
-qed "rvimage_iff";
-
-(** Type checking **)
-
-Goalw [rvimage_def] "rvimage(A,f,r) <= A*A";
-by (rtac Collect_subset 1);
-qed "rvimage_type";
-
-bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset));
-
-Goalw [rvimage_def] "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
-by (Blast_tac 1);
-qed "rvimage_converse";
-
-
-(** Partial Ordering Properties **)
-
-Goalw [irrefl_def, rvimage_def]
- "[| f: inj(A,B); irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))";
-by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
-qed "irrefl_rvimage";
-
-Goalw [trans_on_def, rvimage_def]
- "[| f: inj(A,B); trans[B](r) |] ==> trans[A](rvimage(A,f,r))";
-by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
-qed "trans_on_rvimage";
-
-Goalw [part_ord_def]
- "[| f: inj(A,B); part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))";
-by (blast_tac (claset() addSIs [irrefl_rvimage, trans_on_rvimage]) 1);
-qed "part_ord_rvimage";
-
-(** Linearity **)
-
-val [finj,lin] = goalw (the_context ()) [inj_def]
- "[| f: inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))";
-by (rewtac linear_def); (*Note! the premises are NOT rewritten*)
-by (REPEAT_FIRST (ares_tac [ballI]));
-by (asm_simp_tac (simpset() addsimps [rvimage_iff]) 1);
-by (cut_facts_tac [finj] 1);
-by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1);
-by (REPEAT_SOME (blast_tac (claset() addIs [apply_funtype])));
-qed "linear_rvimage";
-
-Goalw [tot_ord_def]
- "[| f: inj(A,B); tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))";
-by (blast_tac (claset() addSIs [part_ord_rvimage, linear_rvimage]) 1);
-qed "tot_ord_rvimage";
-
-
-(** Well-foundedness **)
-
-(*Not sure if wf_on_rvimage could be proved from this!*)
-Goal "wf(r) ==> wf(rvimage(A,f,r))";
-by (full_simp_tac (simpset() addsimps [rvimage_def, wf_eq_minimal]) 1);
-by (Clarify_tac 1);
-by (subgoal_tac "EX w. w : {w: {f`x. x:Q}. EX x. x: Q & (f`x = w)}" 1);
-by (blast_tac (claset() delrules [allE]) 2);
-by (etac allE 1);
-by (mp_tac 1);
-by (Blast_tac 1);
-qed "wf_rvimage";
-AddSIs [wf_rvimage];
-
-Goal "[| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
-by (rtac wf_onI2 1);
-by (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba" 1);
-by (Blast_tac 1);
-by (eres_inst_tac [("a","f`y")] wf_on_induct 1);
-by (blast_tac (claset() addSIs [apply_funtype]) 1);
-by (blast_tac (claset() addSIs [apply_funtype]
- addSDs [rvimage_iff RS iffD1]) 1);
-qed "wf_on_rvimage";
-
-(*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
-Goal "[| f: inj(A,B); well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
-by (rtac well_ordI 1);
-by (rewrite_goals_tac [well_ord_def, tot_ord_def]);
-by (blast_tac (claset() addSIs [wf_on_rvimage, inj_is_fun]) 1);
-by (blast_tac (claset() addSIs [linear_rvimage]) 1);
-qed "well_ord_rvimage";
-
-Goalw [ord_iso_def]
- "f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)";
-by (asm_full_simp_tac (simpset() addsimps [rvimage_iff]) 1);
-qed "ord_iso_rvimage";
-
-Goalw [ord_iso_def, rvimage_def]
- "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A";
-by (Blast_tac 1);
-qed "ord_iso_rvimage_eq";
-
-
-(** The "measure" relation is useful with wfrec **)
-
-Goal "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))";
-by (simp_tac (simpset() addsimps [measure_def, rvimage_def, Memrel_iff]) 1);
-by (rtac equalityI 1);
-by Auto_tac;
-by (auto_tac (claset() addIs [Ord_in_Ord], simpset() addsimps [lt_def]));
-qed "measure_eq_rvimage_Memrel";
-
-Goal "wf(measure(A,f))";
-by (simp_tac (simpset() addsimps [measure_eq_rvimage_Memrel, wf_Memrel,
- wf_rvimage]) 1);
-qed "wf_measure";
-AddIffs [wf_measure];
-
-Goal "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)";
-by (simp_tac (simpset() addsimps [measure_def]) 1);
-qed "measure_iff";
-AddIffs [measure_iff];
--- a/src/ZF/OrderArith.thy Sat May 11 20:40:31 2002 +0200
+++ b/src/ZF/OrderArith.thy Mon May 13 09:02:13 2002 +0200
@@ -6,31 +6,507 @@
Towards ordinal arithmetic. Also useful with wfrec.
*)
-OrderArith = Order + Sum + Ordinal +
-consts
- radd, rmult :: [i,i,i,i]=>i
- rvimage :: [i,i,i]=>i
+theory OrderArith = Order + Sum + Ordinal:
+constdefs
-defs
(*disjoint sum of two relations; underlies ordinal addition*)
- radd_def "radd(A,r,B,s) ==
+ radd :: "[i,i,i,i]=>i"
+ "radd(A,r,B,s) ==
{z: (A+B) * (A+B).
(EX x y. z = <Inl(x), Inr(y)>) |
(EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r) |
(EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
(*lexicographic product of two relations; underlies ordinal multiplication*)
- rmult_def "rmult(A,r,B,s) ==
+ rmult :: "[i,i,i,i]=>i"
+ "rmult(A,r,B,s) ==
{z: (A*B) * (A*B).
EX x' y' x y. z = <<x',y'>, <x,y>> &
(<x',x>: r | (x'=x & <y',y>: s))}"
(*inverse image of a relation*)
- rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
+ rvimage :: "[i,i,i]=>i"
+ "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
+
+ measure :: "[i, i\<Rightarrow>i] \<Rightarrow> i"
+ "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}"
+
+
+(**** Addition of relations -- disjoint sum ****)
+
+(** Rewrite rules. Can be used to obtain introduction rules **)
+
+lemma radd_Inl_Inr_iff [iff]:
+ "<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B"
+apply (unfold radd_def)
+apply blast
+done
+
+lemma radd_Inl_iff [iff]:
+ "<Inl(a'), Inl(a)> : radd(A,r,B,s) <-> a':A & a:A & <a',a>:r"
+apply (unfold radd_def)
+apply blast
+done
+
+lemma radd_Inr_iff [iff]:
+ "<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s"
+apply (unfold radd_def)
+apply blast
+done
+
+lemma radd_Inr_Inl_iff [iff]:
+ "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False"
+apply (unfold radd_def)
+apply blast
+done
+
+(** Elimination Rule **)
+
+lemma raddE:
+ "[| <p',p> : radd(A,r,B,s);
+ !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q;
+ !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q;
+ !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q
+ |] ==> Q"
+apply (unfold radd_def)
+apply (blast intro: elim:);
+done
+
+(** Type checking **)
+
+lemma radd_type: "radd(A,r,B,s) <= (A+B) * (A+B)"
+apply (unfold radd_def)
+apply (rule Collect_subset)
+done
+
+lemmas field_radd = radd_type [THEN field_rel_subset]
+
+(** Linearity **)
+
+lemma linear_radd:
+ "[| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"
+apply (unfold linear_def)
+apply (blast intro: elim:);
+done
+
+
+(** Well-foundedness **)
+
+lemma wf_on_radd: "[| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"
+apply (rule wf_onI2)
+apply (subgoal_tac "ALL x:A. Inl (x) : Ba")
+(*Proving the lemma, which is needed twice!*)
+ prefer 2
+ apply (erule_tac V = "y : A + B" in thin_rl)
+ apply (rule_tac ballI)
+ apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption)
+ apply (blast intro: elim:);
+(*Returning to main part of proof*)
+apply safe
+apply blast
+apply (erule_tac r = "s" and a = "ya" in wf_on_induct , assumption)
+apply (blast intro: elim:);
+done
+
+lemma wf_radd: "[| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))"
+apply (simp add: wf_iff_wf_on_field)
+apply (rule wf_on_subset_A [OF _ field_radd])
+apply (blast intro: wf_on_radd)
+done
+
+lemma well_ord_radd:
+ "[| well_ord(A,r); well_ord(B,s) |] ==> well_ord(A+B, radd(A,r,B,s))"
+apply (rule well_ordI)
+apply (simp add: well_ord_def wf_on_radd)
+apply (simp add: well_ord_def tot_ord_def linear_radd)
+done
+
+(** An ord_iso congruence law **)
-constdefs
- measure :: "[i, i\\<Rightarrow>i] \\<Rightarrow> i"
- "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}"
+lemma sum_bij:
+ "[| f: bij(A,C); g: bij(B,D) |]
+ ==> (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)"
+apply (rule_tac d = "case (%x. Inl (converse (f) `x) , %y. Inr (converse (g) `y))" in lam_bijective)
+apply (typecheck add: bij_is_inj inj_is_fun)
+apply (auto simp add: left_inverse_bij right_inverse_bij)
+done
+
+lemma sum_ord_iso_cong:
+ "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ==>
+ (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z))
+ : ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))"
+apply (unfold ord_iso_def)
+apply (safe intro!: sum_bij)
+(*Do the beta-reductions now*)
+apply (auto cong add: conj_cong simp add: bij_is_fun [THEN apply_type])
+done
+
+(*Could we prove an ord_iso result? Perhaps
+ ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
+lemma sum_disjoint_bij: "A Int B = 0 ==>
+ (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)"
+apply (rule_tac d = "%z. if z:A then Inl (z) else Inr (z) " in lam_bijective)
+apply auto
+done
+
+(** Associativity **)
+
+lemma sum_assoc_bij:
+ "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))
+ : bij((A+B)+C, A+(B+C))"
+apply (rule_tac d = "case (%x. Inl (Inl (x)), case (%x. Inl (Inr (x)), Inr))"
+ in lam_bijective)
+apply auto
+done
+
+lemma sum_assoc_ord_iso:
+ "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))
+ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),
+ A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))"
+apply (rule sum_assoc_bij [THEN ord_isoI])
+apply auto
+done
+
+
+(**** Multiplication of relations -- lexicographic product ****)
+
+(** Rewrite rule. Can be used to obtain introduction rules **)
+
+lemma rmult_iff [iff]:
+ "<<a',b'>, <a,b>> : rmult(A,r,B,s) <->
+ (<a',a>: r & a':A & a:A & b': B & b: B) |
+ (<b',b>: s & a'=a & a:A & b': B & b: B)"
+
+apply (unfold rmult_def)
+apply blast
+done
+
+lemma rmultE:
+ "[| <<a',b'>, <a,b>> : rmult(A,r,B,s);
+ [| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q;
+ [| <b',b>: s; a:A; a'=a; b':B; b:B |] ==> Q
+ |] ==> Q"
+apply (blast intro: elim:);
+done
+
+(** Type checking **)
+
+lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)"
+apply (unfold rmult_def)
+apply (rule Collect_subset)
+done
+
+lemmas field_rmult = rmult_type [THEN field_rel_subset]
+
+(** Linearity **)
+
+lemma linear_rmult:
+ "[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"
+apply (simp add: linear_def);
+apply (blast intro: elim:);
+done
+
+(** Well-foundedness **)
+
+lemma wf_on_rmult: "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))"
+apply (rule wf_onI2)
+apply (erule SigmaE)
+apply (erule ssubst)
+apply (subgoal_tac "ALL b:B. <x,b>: Ba")
+apply blast
+apply (erule_tac a = "x" in wf_on_induct , assumption)
+apply (rule ballI)
+apply (erule_tac a = "b" in wf_on_induct , assumption)
+apply (best elim!: rmultE bspec [THEN mp])
+done
+
+
+lemma wf_rmult: "[| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))"
+apply (simp add: wf_iff_wf_on_field)
+apply (rule wf_on_subset_A [OF _ field_rmult])
+apply (blast intro: wf_on_rmult)
+done
+
+lemma well_ord_rmult:
+ "[| well_ord(A,r); well_ord(B,s) |] ==> well_ord(A*B, rmult(A,r,B,s))"
+apply (rule well_ordI)
+apply (simp add: well_ord_def wf_on_rmult)
+apply (simp add: well_ord_def tot_ord_def linear_rmult)
+done
+(** An ord_iso congruence law **)
+
+lemma prod_bij:
+ "[| f: bij(A,C); g: bij(B,D) |]
+ ==> (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)"
+apply (rule_tac d = "%<x,y>. <converse (f) `x, converse (g) `y>"
+ in lam_bijective)
+apply (typecheck add: bij_is_inj inj_is_fun)
+apply (auto simp add: left_inverse_bij right_inverse_bij)
+done
+
+lemma prod_ord_iso_cong:
+ "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |]
+ ==> (lam <x,y>:A*B. <f`x, g`y>)
+ : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))"
+apply (unfold ord_iso_def)
+apply (safe intro!: prod_bij)
+apply (simp_all add: bij_is_fun [THEN apply_type])
+apply (blast intro: bij_is_inj [THEN inj_apply_equality])
+done
+
+lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)"
+apply (rule_tac d = "snd" in lam_bijective)
+apply auto
+done
+
+(*Used??*)
+lemma singleton_prod_ord_iso:
+ "well_ord({x},xr) ==>
+ (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))"
+apply (rule singleton_prod_bij [THEN ord_isoI])
+apply (simp (no_asm_simp))
+apply (blast dest: well_ord_is_wf [THEN wf_on_not_refl])
+done
+
+(*Here we build a complicated function term, then simplify it using
+ case_cong, id_conv, comp_lam, case_case.*)
+lemma prod_sum_singleton_bij:
+ "a~:C ==>
+ (lam x:C*B + D. case(%x. x, %y.<a,y>, x))
+ : bij(C*B + D, C*B Un {a}*D)"
+apply (rule subst_elem)
+apply (rule id_bij [THEN sum_bij, THEN comp_bij])
+apply (rule singleton_prod_bij)
+apply (rule sum_disjoint_bij)
+apply blast
+apply (simp (no_asm_simp) cong add: case_cong)
+apply (rule comp_lam [THEN trans, symmetric])
+apply (fast elim!: case_type)
+apply (simp (no_asm_simp) add: case_case)
+done
+
+lemma prod_sum_singleton_ord_iso:
+ "[| a:A; well_ord(A,r) |] ==>
+ (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x))
+ : ord_iso(pred(A,a,r)*B + pred(B,b,s),
+ radd(A*B, rmult(A,r,B,s), B, s),
+ pred(A,a,r)*B Un {a}*pred(B,b,s), rmult(A,r,B,s))"
+apply (rule prod_sum_singleton_bij [THEN ord_isoI])
+apply (simp (no_asm_simp) add: pred_iff well_ord_is_wf [THEN wf_on_not_refl])
+apply (auto elim!: well_ord_is_wf [THEN wf_on_asym] predE)
+done
+
+(** Distributive law **)
+
+lemma sum_prod_distrib_bij:
+ "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))
+ : bij((A+B)*C, (A*C)+(B*C))"
+apply (rule_tac d = "case (%<x,y>.<Inl (x) ,y>, %<x,y>.<Inr (x) ,y>) "
+ in lam_bijective)
+apply auto
+done
+
+lemma sum_prod_distrib_ord_iso:
+ "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))
+ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t),
+ (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"
+apply (rule sum_prod_distrib_bij [THEN ord_isoI])
+apply auto
+done
+
+(** Associativity **)
+
+lemma prod_assoc_bij:
+ "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))"
+apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective)
+apply auto
+done
+
+lemma prod_assoc_ord_iso:
+ "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)
+ : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),
+ A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"
+apply (rule prod_assoc_bij [THEN ord_isoI])
+apply auto
+done
+
+(**** Inverse image of a relation ****)
+
+(** Rewrite rule **)
+
+lemma rvimage_iff: "<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A"
+apply (unfold rvimage_def)
+apply blast
+done
+
+(** Type checking **)
+
+lemma rvimage_type: "rvimage(A,f,r) <= A*A"
+apply (unfold rvimage_def)
+apply (rule Collect_subset)
+done
+
+lemmas field_rvimage = rvimage_type [THEN field_rel_subset]
+
+lemma rvimage_converse: "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))"
+apply (unfold rvimage_def)
+apply blast
+done
+
+
+(** Partial Ordering Properties **)
+
+lemma irrefl_rvimage:
+ "[| f: inj(A,B); irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))"
+apply (unfold irrefl_def rvimage_def)
+apply (blast intro: inj_is_fun [THEN apply_type])
+done
+
+lemma trans_on_rvimage:
+ "[| f: inj(A,B); trans[B](r) |] ==> trans[A](rvimage(A,f,r))"
+apply (unfold trans_on_def rvimage_def)
+apply (blast intro: inj_is_fun [THEN apply_type])
+done
+
+lemma part_ord_rvimage:
+ "[| f: inj(A,B); part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))"
+apply (unfold part_ord_def)
+apply (blast intro!: irrefl_rvimage trans_on_rvimage)
+done
+
+(** Linearity **)
+
+lemma linear_rvimage:
+ "[| f: inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))"
+apply (simp add: inj_def linear_def rvimage_iff)
+apply (blast intro: apply_funtype);
+done
+
+lemma tot_ord_rvimage:
+ "[| f: inj(A,B); tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))"
+apply (unfold tot_ord_def)
+apply (blast intro!: part_ord_rvimage linear_rvimage)
+done
+
+
+(** Well-foundedness **)
+
+(*Not sure if wf_on_rvimage could be proved from this!*)
+lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))"
+apply (simp (no_asm_use) add: rvimage_def wf_eq_minimal)
+apply clarify
+apply (subgoal_tac "EX w. w : {w: {f`x. x:Q}. EX x. x: Q & (f`x = w) }")
+ apply (erule allE)
+ apply (erule impE)
+ apply assumption;
+ apply blast
+apply (blast intro: elim:);
+done
+
+lemma wf_on_rvimage: "[| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
+apply (rule wf_onI2)
+apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba")
+ apply blast
+apply (erule_tac a = "f`y" in wf_on_induct)
+ apply (blast intro!: apply_funtype)
+apply (blast intro!: apply_funtype dest!: rvimage_iff [THEN iffD1])
+done
+
+(*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
+lemma well_ord_rvimage:
+ "[| f: inj(A,B); well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))"
+apply (rule well_ordI)
+apply (unfold well_ord_def tot_ord_def)
+apply (blast intro!: wf_on_rvimage inj_is_fun)
+apply (blast intro!: linear_rvimage)
+done
+
+lemma ord_iso_rvimage:
+ "f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)"
+apply (unfold ord_iso_def)
+apply (simp add: rvimage_iff)
+done
+
+lemma ord_iso_rvimage_eq:
+ "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A"
+apply (unfold ord_iso_def rvimage_def)
+apply blast
+done
+
+
+(** The "measure" relation is useful with wfrec **)
+
+lemma measure_eq_rvimage_Memrel:
+ "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))"
+apply (simp (no_asm) add: measure_def rvimage_def Memrel_iff)
+apply (rule equalityI)
+apply auto
+apply (auto intro: Ord_in_Ord simp add: lt_def)
+done
+
+lemma wf_measure [iff]: "wf(measure(A,f))"
+apply (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage)
+done
+
+lemma measure_iff [iff]: "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)"
+apply (simp (no_asm) add: measure_def)
+done
+
+ML {*
+val measure_def = thm "measure_def";
+val radd_Inl_Inr_iff = thm "radd_Inl_Inr_iff";
+val radd_Inl_iff = thm "radd_Inl_iff";
+val radd_Inr_iff = thm "radd_Inr_iff";
+val radd_Inr_Inl_iff = thm "radd_Inr_Inl_iff";
+val raddE = thm "raddE";
+val radd_type = thm "radd_type";
+val field_radd = thm "field_radd";
+val linear_radd = thm "linear_radd";
+val wf_on_radd = thm "wf_on_radd";
+val wf_radd = thm "wf_radd";
+val well_ord_radd = thm "well_ord_radd";
+val sum_bij = thm "sum_bij";
+val sum_ord_iso_cong = thm "sum_ord_iso_cong";
+val sum_disjoint_bij = thm "sum_disjoint_bij";
+val sum_assoc_bij = thm "sum_assoc_bij";
+val sum_assoc_ord_iso = thm "sum_assoc_ord_iso";
+val rmult_iff = thm "rmult_iff";
+val rmultE = thm "rmultE";
+val rmult_type = thm "rmult_type";
+val field_rmult = thm "field_rmult";
+val linear_rmult = thm "linear_rmult";
+val wf_on_rmult = thm "wf_on_rmult";
+val wf_rmult = thm "wf_rmult";
+val well_ord_rmult = thm "well_ord_rmult";
+val prod_bij = thm "prod_bij";
+val prod_ord_iso_cong = thm "prod_ord_iso_cong";
+val singleton_prod_bij = thm "singleton_prod_bij";
+val singleton_prod_ord_iso = thm "singleton_prod_ord_iso";
+val prod_sum_singleton_bij = thm "prod_sum_singleton_bij";
+val prod_sum_singleton_ord_iso = thm "prod_sum_singleton_ord_iso";
+val sum_prod_distrib_bij = thm "sum_prod_distrib_bij";
+val sum_prod_distrib_ord_iso = thm "sum_prod_distrib_ord_iso";
+val prod_assoc_bij = thm "prod_assoc_bij";
+val prod_assoc_ord_iso = thm "prod_assoc_ord_iso";
+val rvimage_iff = thm "rvimage_iff";
+val rvimage_type = thm "rvimage_type";
+val field_rvimage = thm "field_rvimage";
+val rvimage_converse = thm "rvimage_converse";
+val irrefl_rvimage = thm "irrefl_rvimage";
+val trans_on_rvimage = thm "trans_on_rvimage";
+val part_ord_rvimage = thm "part_ord_rvimage";
+val linear_rvimage = thm "linear_rvimage";
+val tot_ord_rvimage = thm "tot_ord_rvimage";
+val wf_rvimage = thm "wf_rvimage";
+val wf_on_rvimage = thm "wf_on_rvimage";
+val well_ord_rvimage = thm "well_ord_rvimage";
+val ord_iso_rvimage = thm "ord_iso_rvimage";
+val ord_iso_rvimage_eq = thm "ord_iso_rvimage_eq";
+val measure_eq_rvimage_Memrel = thm "measure_eq_rvimage_Memrel";
+val wf_measure = thm "wf_measure";
+val measure_iff = thm "measure_iff";
+*}
+
end
--- a/src/ZF/OrderType.ML Sat May 11 20:40:31 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,967 +0,0 @@
-(* Title: ZF/OrderType.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory
-
-Ordinal arithmetic is traditionally defined in terms of order types, as here.
-But a definition by transfinite recursion would be much simpler!
-*)
-
-
-(*??for Ordinal.ML*)
-(*suitable for rewriting PROVIDED i has been fixed*)
-Goal "[| j:i; Ord(i) |] ==> Ord(j)";
-by (blast_tac (claset() addIs [Ord_in_Ord]) 1);
-qed "Ord_in_Ord'";
-
-
-(**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
-
-val [prem] = goal (the_context ()) "j le i ==> well_ord(j, Memrel(i))";
-by (rtac well_ordI 1);
-by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
-by (resolve_tac [prem RS ltE] 1);
-by (asm_simp_tac (simpset() addsimps [linear_def,
- [ltI, prem] MRS lt_trans2 RS ltD]) 1);
-by (REPEAT (resolve_tac [ballI, Ord_linear] 1));
-by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
-qed "le_well_ord_Memrel";
-
-(*"Ord(i) ==> well_ord(i, Memrel(i))"*)
-bind_thm ("well_ord_Memrel", le_refl RS le_well_ord_Memrel);
-
-(*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord
- The smaller ordinal is an initial segment of the larger *)
-Goalw [pred_def, lt_def]
- "j<i ==> pred(i, j, Memrel(i)) = j";
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [Ord_trans]) 1);
-qed "lt_pred_Memrel";
-
-Goalw [pred_def,Memrel_def]
- "x:A ==> pred(A, x, Memrel(A)) = A Int x";
-by (Blast_tac 1);
-qed "pred_Memrel";
-
-Goal "[| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
-by (ftac lt_pred_Memrel 1);
-by (etac ltE 1);
-by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
- assume_tac 3 THEN assume_tac 1);
-by (rewtac ord_iso_def);
-(*Combining the two simplifications causes looping*)
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [bij_is_fun RS apply_type, Ord_trans]) 1);
-qed "Ord_iso_implies_eq_lemma";
-
-(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*)
-Goal "[| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) |] \
-\ ==> i=j";
-by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
-by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1));
-qed "Ord_iso_implies_eq";
-
-
-(**** Ordermap and ordertype ****)
-
-Goalw [ordermap_def,ordertype_def]
- "ordermap(A,r) : A -> ordertype(A,r)";
-by (rtac lam_type 1);
-by (rtac (lamI RS imageI) 1);
-by (REPEAT (assume_tac 1));
-qed "ordermap_type";
-
-(*** Unfolding of ordermap ***)
-
-(*Useful for cardinality reasoning; see CardinalArith.ML*)
-Goalw [ordermap_def, pred_def]
- "[| wf[A](r); x:A |] ==> \
-\ ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)";
-by (Asm_simp_tac 1);
-by (etac (wfrec_on RS trans) 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [subset_iff, image_lam,
- vimage_singleton_iff]) 1);
-qed "ordermap_eq_image";
-
-(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
-Goal "[| wf[A](r); x:A |] ==> \
-\ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
-by (asm_simp_tac (simpset() addsimps [ordermap_eq_image, pred_subset,
- ordermap_type RS image_fun]) 1);
-qed "ordermap_pred_unfold";
-
-(*pred-unfolded version. NOT suitable for rewriting -- loops!*)
-bind_thm ("ordermap_unfold", rewrite_rule [pred_def] ordermap_pred_unfold);
-
-(*The theorem above is
-
-[| wf[A](r); x : A |]
-==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}}
-
-NOTE: the definition of ordermap used here delivers ordinals only if r is
-transitive. If r is the predecessor relation on the naturals then
-ordermap(nat,predr) ` n equals {n-1} and not n. A more complicated definition,
-like
-
- ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> : r}},
-
-might eliminate the need for r to be transitive.
-*)
-
-
-(*** Showing that ordermap, ordertype yield ordinals ***)
-
-fun ordermap_elim_tac i =
- EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i,
- assume_tac (i+1),
- assume_tac i];
-
-Goalw [well_ord_def, tot_ord_def, part_ord_def]
- "[| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)";
-by Safe_tac;
-by (wf_on_ind_tac "x" [] 1);
-by (asm_simp_tac (simpset() addsimps [ordermap_pred_unfold]) 1);
-by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-by (rewrite_goals_tac [pred_def,Transset_def]);
-by (Blast_tac 2);
-by Safe_tac;
-by (ordermap_elim_tac 1);
-by (fast_tac (claset() addSEs [trans_onD]) 1);
-qed "Ord_ordermap";
-
-Goalw [ordertype_def]
- "well_ord(A,r) ==> Ord(ordertype(A,r))";
-by (stac ([ordermap_type, subset_refl] MRS image_fun) 1);
-by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-by (blast_tac (claset() addIs [Ord_ordermap]) 2);
-by (rewrite_goals_tac [Transset_def,well_ord_def]);
-by Safe_tac;
-by (ordermap_elim_tac 1);
-by (Blast_tac 1);
-qed "Ord_ordertype";
-
-(*** ordermap preserves the orderings in both directions ***)
-
-Goal "[| <w,x>: r; wf[A](r); w: A; x: A |] ==> \
-\ ordermap(A,r)`w : ordermap(A,r)`x";
-by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-qed "ordermap_mono";
-
-(*linearity of r is crucial here*)
-Goalw [well_ord_def, tot_ord_def]
- "[| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \
-\ w: A; x: A |] ==> <w,x>: r";
-by Safe_tac;
-by (linear_case_tac 1);
-by (blast_tac (claset() addSEs [mem_not_refl RS notE]) 1);
-by (dtac ordermap_mono 1);
-by (REPEAT_SOME assume_tac);
-by (etac mem_asym 1);
-by (assume_tac 1);
-qed "converse_ordermap_mono";
-
-bind_thm ("ordermap_surj",
- rewrite_rule [symmetric ordertype_def]
- (ordermap_type RS surj_image));
-
-Goalw [well_ord_def, tot_ord_def, bij_def, inj_def]
- "well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
-by (force_tac (claset() addSIs [ordermap_type, ordermap_surj]
- addEs [linearE]
- addDs [ordermap_mono],
- simpset() addsimps [mem_not_refl]) 1);
-qed "ordermap_bij";
-
-(*** Isomorphisms involving ordertype ***)
-
-Goalw [ord_iso_def]
- "well_ord(A,r) ==> \
-\ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
-by (safe_tac (claset() addSEs [well_ord_is_wf]
- addSIs [ordermap_type RS apply_type,
- ordermap_mono, ordermap_bij]));
-by (blast_tac (claset() addSDs [converse_ordermap_mono]) 1);
-qed "ordertype_ord_iso";
-
-Goal "[| f: ord_iso(A,r,B,s); well_ord(B,s) |] ==> \
-\ ordertype(A,r) = ordertype(B,s)";
-by (ftac well_ord_ord_iso 1 THEN assume_tac 1);
-by (rtac Ord_iso_implies_eq 1
- THEN REPEAT (etac Ord_ordertype 1));
-by (deepen_tac (claset() addIs [ord_iso_trans, ord_iso_sym]
- addSEs [ordertype_ord_iso]) 0 1);
-qed "ordertype_eq";
-
-Goal "[| ordertype(A,r) = ordertype(B,s); \
-\ well_ord(A,r); well_ord(B,s) \
-\ |] ==> EX f. f: ord_iso(A,r,B,s)";
-by (rtac exI 1);
-by (resolve_tac [ordertype_ord_iso RS ord_iso_trans] 1);
-by (assume_tac 1);
-by (etac ssubst 1);
-by (eresolve_tac [ordertype_ord_iso RS ord_iso_sym] 1);
-qed "ordertype_eq_imp_ord_iso";
-
-(*** Basic equalities for ordertype ***)
-
-(*Ordertype of Memrel*)
-Goal "j le i ==> ordertype(j,Memrel(i)) = j";
-by (resolve_tac [Ord_iso_implies_eq RS sym] 1);
-by (etac ltE 1);
-by (REPEAT (ares_tac [le_well_ord_Memrel, Ord_ordertype] 1));
-by (rtac ord_iso_trans 1);
-by (eresolve_tac [le_well_ord_Memrel RS ordertype_ord_iso] 2);
-by (resolve_tac [id_bij RS ord_isoI] 1);
-by (Asm_simp_tac 1);
-by (fast_tac (claset() addEs [ltE, Ord_in_Ord, Ord_trans]) 1);
-qed "le_ordertype_Memrel";
-
-(*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*)
-bind_thm ("ordertype_Memrel", le_refl RS le_ordertype_Memrel);
-
-Goal "ordertype(0,r) = 0";
-by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq RS trans] 1);
-by (etac emptyE 1);
-by (rtac well_ord_0 1);
-by (resolve_tac [Ord_0 RS ordertype_Memrel] 1);
-qed "ordertype_0";
-
-Addsimps [ordertype_0];
-
-(*Ordertype of rvimage: [| f: bij(A,B); well_ord(B,s) |] ==>
- ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)
-bind_thm ("bij_ordertype_vimage", ord_iso_rvimage RS ordertype_eq);
-
-(*** A fundamental unfolding law for ordertype. ***)
-
-(*Ordermap returns the same result if applied to an initial segment*)
-Goal "[| well_ord(A,r); y:A; z: pred(A,y,r) |] ==> \
-\ ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
-by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1);
-by (wf_on_ind_tac "z" [] 1);
-by (safe_tac (claset() addSEs [predE]));
-by (asm_simp_tac
- (simpset() addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
-(*combining these two simplifications LOOPS! *)
-by (asm_simp_tac (simpset() addsimps [pred_pred_eq]) 1);
-by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1);
-by (rtac (refl RSN (2,RepFun_cong)) 1);
-by (dtac well_ord_is_trans_on 1);
-by (fast_tac (claset() addSEs [trans_onD]) 1);
-qed "ordermap_pred_eq_ordermap";
-
-Goalw [ordertype_def]
- "ordertype(A,r) = {ordermap(A,r)`y . y : A}";
-by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
-qed "ordertype_unfold";
-
-(** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **)
-
-Goal "[| well_ord(A,r); x:A |] ==> \
-\ ordertype(pred(A,x,r),r) <= ordertype(A,r)";
-by (asm_simp_tac (simpset() addsimps [ordertype_unfold,
- pred_subset RSN (2, well_ord_subset)]) 1);
-by (fast_tac (claset() addIs [ordermap_pred_eq_ordermap]
- addEs [predE]) 1);
-qed "ordertype_pred_subset";
-
-Goal "[| well_ord(A,r); x:A |] ==> \
-\ ordertype(pred(A,x,r),r) < ordertype(A,r)";
-by (resolve_tac [ordertype_pred_subset RS subset_imp_le RS leE] 1);
-by (REPEAT (ares_tac [Ord_ordertype, well_ord_subset, pred_subset] 1));
-by (eresolve_tac [sym RS ordertype_eq_imp_ord_iso RS exE] 1);
-by (etac well_ord_iso_predE 3);
-by (REPEAT (ares_tac [pred_subset, well_ord_subset] 1));
-qed "ordertype_pred_lt";
-
-(*May rewrite with this -- provided no rules are supplied for proving that
- well_ord(pred(A,x,r), r) *)
-Goal "well_ord(A,r) ==> \
-\ ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}";
-by (rtac equalityI 1);
-by (safe_tac (claset() addSIs [ordertype_pred_lt RS ltD]));
-by (auto_tac (claset(),
- simpset() addsimps [ordertype_def,
- well_ord_is_wf RS ordermap_eq_image,
- ordermap_type RS image_fun,
- ordermap_pred_eq_ordermap,
- pred_subset]));
-qed "ordertype_pred_unfold";
-
-
-(**** Alternative definition of ordinal ****)
-
-(*proof by Krzysztof Grabczewski*)
-Goalw [Ord_alt_def] "Ord(i) ==> Ord_alt(i)";
-by (rtac conjI 1);
-by (etac well_ord_Memrel 1);
-by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]);
-by (Blast.depth_tac (claset()) 8 1);
-qed "Ord_is_Ord_alt";
-
-(*proof by lcp*)
-Goalw [Ord_alt_def, Ord_def, Transset_def, well_ord_def,
- tot_ord_def, part_ord_def, trans_on_def]
- "Ord_alt(i) ==> Ord(i)";
-by (asm_full_simp_tac (simpset() addsimps [pred_Memrel]) 1);
-by (blast_tac (claset() addSEs [equalityE]) 1);
-qed "Ord_alt_is_Ord";
-
-
-(**** Ordinal Addition ****)
-
-(*** Order Type calculations for radd ***)
-
-(** Addition with 0 **)
-
-Goal "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)";
-by (res_inst_tac [("d", "Inl")] lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS Asm_simp_tac);
-qed "bij_sum_0";
-
-Goal "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
-by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1);
-by (assume_tac 2);
-by (Force_tac 1);
-qed "ordertype_sum_0_eq";
-
-Goal "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)";
-by (res_inst_tac [("d", "Inr")] lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS Asm_simp_tac);
-qed "bij_0_sum";
-
-Goal "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
-by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1);
-by (assume_tac 2);
-by (Force_tac 1);
-qed "ordertype_0_sum_eq";
-
-(** Initial segments of radd. Statements by Grabczewski **)
-
-(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
-Goalw [pred_def]
- "a:A ==> \
-\ (lam x:pred(A,a,r). Inl(x)) \
-\ : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
-by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
-by Auto_tac;
-qed "pred_Inl_bij";
-
-Goal "[| a:A; well_ord(A,r) |] ==> \
-\ ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) = \
-\ ordertype(pred(A,a,r), r)";
-by (resolve_tac [pred_Inl_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
-by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_subset]));
-by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1);
-qed "ordertype_pred_Inl_eq";
-
-Goalw [pred_def, id_def]
- "b:B ==> \
-\ id(A+pred(B,b,s)) \
-\ : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
-by (res_inst_tac [("d", "%z. z")] lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS (Asm_full_simp_tac));
-qed "pred_Inr_bij";
-
-Goal "[| b:B; well_ord(A,r); well_ord(B,s) |] ==> \
-\ ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \
-\ ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))";
-by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
-by (force_tac (claset(), simpset() addsimps [pred_def, id_def]) 2);
-by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset]));
-qed "ordertype_pred_Inr_eq";
-
-
-(*** ordify: trivial coercion to an ordinal ***)
-
-Goal "Ord(ordify(x))";
-by (asm_full_simp_tac (simpset() addsimps [ordify_def]) 1);
-qed "Ord_ordify";
-AddIffs [Ord_ordify];
-AddTCs [Ord_ordify];
-
-(*Collapsing*)
-Goal "ordify(ordify(x)) = ordify(x)";
-by (asm_full_simp_tac (simpset() addsimps [ordify_def]) 1);
-qed "ordify_idem";
-Addsimps [ordify_idem];
-
-
-(*** Basic laws for ordinal addition ***)
-
-Goal "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))";
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Ord_ordertype, well_ord_radd, well_ord_Memrel]) 1);
-qed "Ord_raw_oadd";
-
-Goal "Ord(i++j)";
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, Ord_raw_oadd]) 1);
-qed "Ord_oadd";
-AddIffs [Ord_oadd]; AddTCs [Ord_oadd];
-
-
-(** Ordinal addition with zero **)
-
-Goal "Ord(i) ==> raw_oadd(i,0) = i";
-by (asm_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Memrel_0, ordertype_sum_0_eq,
- ordertype_Memrel, well_ord_Memrel]) 1);
-qed "raw_oadd_0";
-
-Goal "Ord(i) ==> i++0 = i";
-by (asm_simp_tac (simpset() addsimps [oadd_def, raw_oadd_0, ordify_def]) 1);
-qed "oadd_0";
-Addsimps [oadd_0];
-
-Goal "Ord(i) ==> raw_oadd(0,i) = i";
-by (asm_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Memrel_0, ordertype_0_sum_eq,
- ordertype_Memrel, well_ord_Memrel]) 1);
-qed "raw_oadd_0_left";
-
-Goal "Ord(i) ==> 0++i = i";
-by (asm_simp_tac (simpset() addsimps [oadd_def, raw_oadd_0_left, ordify_def]) 1);
-qed "oadd_0_left";
-Addsimps [oadd_0_left];
-
-
-Goal "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i) \
-\ else (if Ord(j) then j else 0))";
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, raw_oadd_0_left, raw_oadd_0]) 1);
-qed "oadd_eq_if_raw_oadd";
-
-
-Goal "[|Ord(i); Ord(j)|] ==> raw_oadd(i,j) = i++j";
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def]) 1);
-qed "raw_oadd_eq_oadd";
-
-(*** Further properties of ordinal addition. Statements by Grabczewski,
- proofs by lcp. ***)
-
-(*Surely also provable by transfinite induction on j?*)
-Goal "k<i ==> k < i++j";
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, lt_Ord2, raw_oadd_0]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1);
-by (rtac ltE 1 THEN assume_tac 1);
-by (rtac ltI 1);
-by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2));
-by (force_tac
- (claset(),
- simpset() addsimps [ordertype_pred_unfold,
- well_ord_radd, well_ord_Memrel,
- ordertype_pred_Inl_eq,
- lt_pred_Memrel, leI RS le_ordertype_Memrel]) 1);
-qed "lt_oadd1";
-
-(*Thus also we obtain the rule i++j = k ==> i le k *)
-Goal "Ord(i) ==> i le i++j";
-by (rtac all_lt_imp_le 1);
-by (REPEAT (ares_tac [Ord_oadd, lt_oadd1] 1));
-qed "oadd_le_self";
-
-(** A couple of strange but necessary results! **)
-
-Goal "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))";
-by (resolve_tac [id_bij RS ord_isoI] 1);
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
-qed "id_ord_iso_Memrel";
-
-Goal "[| well_ord(A,r); k<j |] ==> \
-\ ordertype(A+k, radd(A, r, k, Memrel(j))) = \
-\ ordertype(A+k, radd(A, r, k, Memrel(k)))";
-by (etac ltE 1);
-by (resolve_tac [ord_iso_refl RS sum_ord_iso_cong RS ordertype_eq] 1);
-by (eresolve_tac [OrdmemD RS id_ord_iso_Memrel RS ord_iso_sym] 1);
-by (REPEAT_FIRST (ares_tac [well_ord_radd, well_ord_Memrel]));
-qed "ordertype_sum_Memrel";
-
-Goal "k<j ==> i++k < i++j";
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, raw_oadd_0_left, lt_Ord, lt_Ord2]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1);
-by (rtac ltE 1 THEN assume_tac 1);
-by (resolve_tac [ordertype_pred_unfold RS equalityD2 RS subsetD RS ltI] 1);
-by (REPEAT_FIRST (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel]));
-by (rtac RepFun_eqI 1);
-by (etac InrI 2);
-by (asm_simp_tac
- (simpset() addsimps [ordertype_pred_Inr_eq, well_ord_Memrel,
- lt_pred_Memrel, leI RS le_ordertype_Memrel,
- ordertype_sum_Memrel]) 1);
-qed "oadd_lt_mono2";
-
-Goal "[| i++j < i++k; Ord(j) |] ==> j<k";
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd] addsplits [split_if_asm]) 1);
-by (forw_inst_tac [("i","i"),("j","j")] oadd_le_self 2);
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, lt_Ord, not_lt_iff_le RS iff_sym]) 2);
-by (rtac Ord_linear_lt 1);
-by (REPEAT_SOME assume_tac);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd])));
-by (ALLGOALS
- (blast_tac (claset() addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
-qed "oadd_lt_cancel2";
-
-Goal "Ord(j) ==> i++j < i++k <-> j<k";
-by (blast_tac (claset() addSIs [oadd_lt_mono2] addSDs [oadd_lt_cancel2]) 1);
-qed "oadd_lt_iff2";
-
-Goal "[| i++j = i++k; Ord(j); Ord(k) |] ==> j=k";
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd] addsplits [split_if_asm]) 1);
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1);
-by (rtac Ord_linear_lt 1);
-by (REPEAT_SOME assume_tac);
-by (ALLGOALS
- (force_tac (claset() addDs [inst "i" "i" oadd_lt_mono2],
- simpset() addsimps [lt_not_refl])));
-qed "oadd_inject";
-
-Goal "k < i++j ==> k<i | (EX l:j. k = i++l )";
-by (asm_full_simp_tac (simpset() addsimps [inst "i" "j" Ord_in_Ord', oadd_eq_if_raw_oadd] addsplits [split_if_asm]) 1);
-by (asm_full_simp_tac
- (simpset() addsimps [inst "i" "j" Ord_in_Ord', lt_def]) 2);
-by (asm_full_simp_tac (simpset() addsimps [ordertype_pred_unfold, well_ord_radd,
- well_ord_Memrel, raw_oadd_def]) 1);
-by (eresolve_tac [ltD RS RepFunE] 1);
-by (force_tac (claset(),
- simpset() addsimps [ordertype_pred_Inl_eq, well_ord_Memrel,
- ltI, lt_pred_Memrel, le_ordertype_Memrel, leI,
- ordertype_pred_Inr_eq,
- ordertype_sum_Memrel]) 1);
-qed "lt_oadd_disj";
-
-
-(*** Ordinal addition with successor -- via associativity! ***)
-
-Goal "(i++j)++k = i++(j++k)";
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd, Ord_raw_oadd, raw_oadd_0, raw_oadd_0_left]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1);
-by (resolve_tac [ordertype_eq RS trans] 1);
-by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS
- sum_ord_iso_cong) 1);
-by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
-by (resolve_tac [sum_assoc_ord_iso RS ordertype_eq RS trans] 1);
-by (rtac ([ord_iso_refl, ordertype_ord_iso] MRS sum_ord_iso_cong RS
- ordertype_eq) 2);
-by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
-qed "oadd_assoc";
-
-Goal "[| Ord(i); Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})";
-by (rtac (subsetI RS equalityI) 1);
-by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1);
-by (REPEAT (ares_tac [Ord_oadd] 1));
-by (force_tac (claset() addIs [lt_oadd1, oadd_lt_mono2],
- simpset() addsimps [Ord_mem_iff_lt]) 3);
-by (Blast_tac 2);
-by (blast_tac (claset() addSEs [ltE]) 1);
-qed "oadd_unfold";
-
-Goal "Ord(i) ==> i++1 = succ(i)";
-by (asm_simp_tac (simpset() addsimps [oadd_unfold, Ord_1, oadd_0]) 1);
-by (Blast_tac 1);
-qed "oadd_1";
-
-Goal "Ord(j) ==> i++succ(j) = succ(i++j)";
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1);
-by (asm_simp_tac (simpset()
- addsimps [inst "i" "j" oadd_1 RS sym, inst "i" "i++j" oadd_1 RS sym, oadd_assoc]) 1);
-qed "oadd_succ";
-Addsimps [oadd_succ];
-
-
-(** Ordinal addition with limit ordinals **)
-
-val prems =
-Goal "[| !!x. x:A ==> Ord(j(x)); a:A |] ==> \
-\ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
-by (blast_tac (claset() addIs prems @ [ltI, Ord_UN, Ord_oadd,
- lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD]
- addSEs [ltE] addSDs [ltI RS lt_oadd_disj]) 1);
-qed "oadd_UN";
-
-Goal "Limit(j) ==> i++j = (UN k:j. i++k)";
-by (forward_tac [Limit_has_0 RS ltD] 1);
-by (asm_simp_tac (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord,
- oadd_UN RS sym, Union_eq_UN RS sym,
- Limit_Union_eq]) 1);
-qed "oadd_Limit";
-
-(** Order/monotonicity properties of ordinal addition **)
-
-Goal "Ord(i) ==> i le j++i";
-by (eres_inst_tac [("i","i")] trans_induct3 1);
-by (asm_simp_tac (simpset() addsimps [Ord_0_le]) 1);
-by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_leI]) 1);
-by (asm_simp_tac (simpset() addsimps [oadd_Limit]) 1);
-by (rtac le_trans 1);
-by (rtac le_implies_UN_le_UN 2);
-by (etac bspec 2);
-by (assume_tac 2);
-by (asm_simp_tac (simpset() addsimps [Union_eq_UN RS sym, Limit_Union_eq,
- le_refl, Limit_is_Ord]) 1);
-qed "oadd_le_self2";
-
-Goal "k le j ==> k++i le j++i";
-by (ftac lt_Ord 1);
-by (ftac le_Ord2 1);
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1);
-by (eres_inst_tac [("i","i")] trans_induct3 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_le_iff]) 1);
-by (asm_simp_tac (simpset() addsimps [oadd_Limit]) 1);
-by (rtac le_implies_UN_le_UN 1);
-by (Blast_tac 1);
-qed "oadd_le_mono1";
-
-Goal "[| i' le i; j'<j |] ==> i'++j' < i++j";
-by (rtac lt_trans1 1);
-by (REPEAT (eresolve_tac [asm_rl, oadd_le_mono1, oadd_lt_mono2, ltE,
- Ord_succD] 1));
-qed "oadd_lt_mono";
-
-Goal "[| i' le i; j' le j |] ==> i'++j' le i++j";
-by (asm_simp_tac (simpset() delsimps [oadd_succ]
- addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
-qed "oadd_le_mono";
-
-Goal "[| Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
-by (asm_simp_tac (simpset() delsimps [oadd_succ]
- addsimps [oadd_lt_iff2, oadd_succ RS sym, Ord_succ]) 1);
-qed "oadd_le_iff2";
-
-
-(** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)).
- Probably simpler to define the difference recursively!
-**)
-
-Goal "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
-by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
-by (blast_tac (claset() addSIs [if_type]) 1);
-by (fast_tac (claset() addSIs [case_type]) 1);
-by (etac sumE 2);
-by (ALLGOALS Asm_simp_tac);
-qed "bij_sum_Diff";
-
-Goal "i le j ==> \
-\ ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) = \
-\ ordertype(j, Memrel(j))";
-by (safe_tac (claset() addSDs [le_subset_iff RS iffD1]));
-by (resolve_tac [bij_sum_Diff RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
-by (etac well_ord_Memrel 3);
-by (assume_tac 1);
-by (Asm_simp_tac 1);
-by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1);
-by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1);
-by (blast_tac (claset() addIs [lt_trans2, lt_trans]) 1);
-qed "ordertype_sum_Diff";
-
-Goalw [odiff_def]
- "[| Ord(i); Ord(j) |] ==> Ord(i--j)";
-by (REPEAT (ares_tac [Ord_ordertype, well_ord_Memrel RS well_ord_subset,
- Diff_subset] 1));
-qed "Ord_odiff";
-Addsimps [Ord_odiff]; AddTCs [Ord_odiff];
-
-
-Goal
- "i le j \
-\ ==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def, odiff_def]) 1);
-by (safe_tac (claset() addSDs [le_subset_iff RS iffD1]));
-by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1);
-by (etac id_ord_iso_Memrel 1);
-by (resolve_tac [ordertype_ord_iso RS ord_iso_sym] 1);
-by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel RS well_ord_subset,
- Diff_subset] 1));
-qed "raw_oadd_ordertype_Diff";
-
-Goal "i le j ==> i ++ (j--i) = j";
-by (asm_simp_tac (simpset() addsimps [lt_Ord, le_Ord2, oadd_def, ordify_def, raw_oadd_ordertype_Diff, ordertype_sum_Diff,
- ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1);
-qed "oadd_odiff_inverse";
-
-(*By oadd_inject, the difference between i and j is unique. Note that we get
- i++j = k ==> j = k--i. *)
-Goal "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j";
-by (rtac oadd_inject 1);
-by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2));
-by (blast_tac (claset() addIs [oadd_odiff_inverse, oadd_le_self]) 1);
-qed "odiff_oadd_inverse";
-
-Goal "[| i<j; k le i |] ==> i--k < j--k";
-by (res_inst_tac [("i","k")] oadd_lt_cancel2 1);
-by (asm_full_simp_tac (simpset() addsimps [oadd_odiff_inverse]) 1);
-by (stac oadd_odiff_inverse 1);
-by (blast_tac (claset() addIs [le_trans, leI]) 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [lt_Ord, le_Ord2]) 1);
-qed "odiff_lt_mono2";
-
-
-(**** Ordinal Multiplication ****)
-
-Goalw [omult_def]
- "[| Ord(i); Ord(j) |] ==> Ord(i**j)";
-by (REPEAT (ares_tac [Ord_ordertype, well_ord_rmult, well_ord_Memrel] 1));
-qed "Ord_omult";
-Addsimps [Ord_omult]; AddTCs [Ord_omult];
-
-(*** A useful unfolding law ***)
-
-Goalw [pred_def]
- "[| a:A; b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) = \
-\ pred(A,a,r)*B Un ({a} * pred(B,b,s))";
-by (Blast_tac 1);
-qed "pred_Pair_eq";
-
-Goal "[| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==> \
-\ ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \
-\ ordertype(pred(A,a,r)*B + pred(B,b,s), \
-\ radd(A*B, rmult(A,r,B,s), B, s))";
-by (asm_simp_tac (simpset() addsimps [pred_Pair_eq]) 1);
-by (resolve_tac [ordertype_eq RS sym] 1);
-by (rtac prod_sum_singleton_ord_iso 1);
-by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset]));
-by (blast_tac (claset() addSEs [predE]) 1);
-qed "ordertype_pred_Pair_eq";
-
-Goalw [raw_oadd_def, omult_def]
- "[| i'<i; j'<j |] ==> \
-\ ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))), \
-\ rmult(i,Memrel(i),j,Memrel(j))) = \
-\ raw_oadd (j**i', j')";
-by (asm_simp_tac (simpset() addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel,
- ltD, lt_Ord2, well_ord_Memrel]) 1);
-by (rtac trans 1);
-by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2);
-by (rtac ord_iso_refl 3);
-by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq] 1);
-by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst]));
-by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel,
- Ord_ordertype]));
-by (ALLGOALS Asm_simp_tac);
-by Safe_tac;
-by (ALLGOALS (blast_tac (claset() addIs [Ord_trans])));
-qed "ordertype_pred_Pair_lemma";
-
-Goalw [omult_def]
- "[| Ord(i); Ord(j); k<j**i |] ==> \
-\ EX j' i'. k = j**i' ++ j' & j'<j & i'<i";
-by (asm_full_simp_tac (simpset() addsimps [ordertype_pred_unfold,
- well_ord_rmult, well_ord_Memrel]) 1);
-by (safe_tac (claset() addSEs [ltE]));
-by (asm_simp_tac (simpset() addsimps [ordertype_pred_Pair_lemma, ltI,
- symmetric omult_def,
- inst "i" "i" Ord_in_Ord', inst "i" "j" Ord_in_Ord', raw_oadd_eq_oadd]) 1);
-by (blast_tac (claset() addIs [ltI]) 1);
-qed "lt_omult";
-
-Goalw [omult_def]
- "[| j'<j; i'<i |] ==> j**i' ++ j' < j**i";
-by (rtac ltI 1);
-by (asm_simp_tac
- (simpset() addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel,
- lt_Ord2]) 2);
-by (asm_simp_tac
- (simpset() addsimps [ordertype_pred_unfold,
- well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1);
-by (rtac bexI 1);
-by (blast_tac (claset() addSEs [ltE]) 2);
-by (asm_simp_tac
- (simpset() addsimps [ordertype_pred_Pair_lemma, ltI,
- symmetric omult_def]) 1);
-by (asm_simp_tac (simpset() addsimps [
- lt_Ord, lt_Ord2, raw_oadd_eq_oadd]) 1);
-qed "omult_oadd_lt";
-
-Goal "[| Ord(i); Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})";
-by (rtac (subsetI RS equalityI) 1);
-by (resolve_tac [lt_omult RS exE] 1);
-by (etac ltI 3);
-by (REPEAT (ares_tac [Ord_omult] 1));
-by (blast_tac (claset() addSEs [ltE]) 1);
-by (blast_tac (claset() addIs [omult_oadd_lt RS ltD, ltI]) 1);
-qed "omult_unfold";
-
-(*** Basic laws for ordinal multiplication ***)
-
-(** Ordinal multiplication by zero **)
-
-Goalw [omult_def] "i**0 = 0";
-by (Asm_simp_tac 1);
-qed "omult_0";
-
-Goalw [omult_def] "0**i = 0";
-by (Asm_simp_tac 1);
-qed "omult_0_left";
-
-Addsimps [omult_0, omult_0_left];
-
-(** Ordinal multiplication by 1 **)
-
-Goalw [omult_def] "Ord(i) ==> i**1 = i";
-by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1);
-by (res_inst_tac [("c", "snd"), ("d", "%z.<0,z>")] lam_bijective 1);
-by (REPEAT_FIRST (eresolve_tac [snd_type, SigmaE, succE, emptyE,
- well_ord_Memrel, ordertype_Memrel]));
-by (ALLGOALS Asm_simp_tac);
-qed "omult_1";
-
-Goalw [omult_def] "Ord(i) ==> 1**i = i";
-by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1);
-by (res_inst_tac [("c", "fst"), ("d", "%z.<z,0>")] lam_bijective 1);
-by (REPEAT_FIRST (eresolve_tac [fst_type, SigmaE, succE, emptyE,
- well_ord_Memrel, ordertype_Memrel]));
-by (ALLGOALS Asm_simp_tac);
-qed "omult_1_left";
-
-Addsimps [omult_1, omult_1_left];
-
-(** Distributive law for ordinal multiplication and addition **)
-
-Goal "[| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)";
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1);
-by (asm_full_simp_tac (simpset() addsimps [omult_def, raw_oadd_def]) 1);
-by (resolve_tac [ordertype_eq RS trans] 1);
-by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS
- prod_ord_iso_cong) 1);
-by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel,
- Ord_ordertype] 1));
-by (rtac (sum_prod_distrib_ord_iso RS ordertype_eq RS trans) 1);
-by (rtac ordertype_eq 2);
-by (rtac ([ordertype_ord_iso, ordertype_ord_iso] MRS sum_ord_iso_cong) 2);
-by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel,
- Ord_ordertype] 1));
-qed "oadd_omult_distrib";
-
-Goal "[| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i";
-by (asm_simp_tac (simpset()
- delsimps [oadd_succ]
- addsimps [inst "i" "j" oadd_1 RS sym, oadd_omult_distrib]) 1);
-qed "omult_succ";
-
-(** Associative law **)
-
-Goalw [omult_def]
- "[| Ord(i); Ord(j); Ord(k) |] ==> (i**j)**k = i**(j**k)";
-by (resolve_tac [ordertype_eq RS trans] 1);
-by (rtac ([ord_iso_refl, ordertype_ord_iso RS ord_iso_sym] MRS
- prod_ord_iso_cong) 1);
-by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
-by (resolve_tac [prod_assoc_ord_iso RS ord_iso_sym RS
- ordertype_eq RS trans] 1);
-by (rtac ([ordertype_ord_iso, ord_iso_refl] MRS prod_ord_iso_cong RS
- ordertype_eq) 2);
-by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Ord_ordertype] 1));
-qed "omult_assoc";
-
-
-(** Ordinal multiplication with limit ordinals **)
-
-val prems =
-Goal "[| Ord(i); !!x. x:A ==> Ord(j(x)) |] ==> \
-\ i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
-by (asm_simp_tac (simpset() addsimps prems @ [Ord_UN, omult_unfold]) 1);
-by (Blast_tac 1);
-qed "omult_UN";
-
-Goal "[| Ord(i); Limit(j) |] ==> i**j = (UN k:j. i**k)";
-by (asm_simp_tac
- (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym,
- Union_eq_UN RS sym, Limit_Union_eq]) 1);
-qed "omult_Limit";
-
-
-(*** Ordering/monotonicity properties of ordinal multiplication ***)
-
-(*As a special case we have "[| 0<i; 0<j |] ==> 0 < i**j" *)
-Goal "[| k<i; 0<j |] ==> k < i**j";
-by (safe_tac (claset() addSEs [ltE] addSIs [ltI, Ord_omult]));
-by (asm_simp_tac (simpset() addsimps [omult_unfold]) 1);
-by (REPEAT_FIRST (ares_tac [bexI]));
-by (Asm_simp_tac 1);
-qed "lt_omult1";
-
-Goal "[| Ord(i); 0<j |] ==> i le i**j";
-by (rtac all_lt_imp_le 1);
-by (REPEAT (ares_tac [Ord_omult, lt_omult1, lt_Ord2] 1));
-qed "omult_le_self";
-
-Goal "[| k le j; Ord(i) |] ==> k**i le j**i";
-by (ftac lt_Ord 1);
-by (ftac le_Ord2 1);
-by (etac trans_induct3 1);
-by (asm_simp_tac (simpset() addsimps [le_refl, Ord_0]) 1);
-by (asm_simp_tac (simpset() addsimps [omult_succ, oadd_le_mono]) 1);
-by (asm_simp_tac (simpset() addsimps [omult_Limit]) 1);
-by (rtac le_implies_UN_le_UN 1);
-by (Blast_tac 1);
-qed "omult_le_mono1";
-
-Goal "[| k<j; 0<i |] ==> i**k < i**j";
-by (rtac ltI 1);
-by (asm_simp_tac (simpset() addsimps [omult_unfold, lt_Ord2]) 1);
-by (safe_tac (claset() addSEs [ltE] addSIs [Ord_omult]));
-by (REPEAT_FIRST (ares_tac [bexI]));
-by (asm_simp_tac (simpset() addsimps [Ord_omult]) 1);
-qed "omult_lt_mono2";
-
-Goal "[| k le j; Ord(i) |] ==> i**k le i**j";
-by (rtac subset_imp_le 1);
-by (safe_tac (claset() addSEs [ltE, make_elim Ord_succD] addSIs [Ord_omult]));
-by (asm_full_simp_tac (simpset() addsimps [omult_unfold]) 1);
-by (deepen_tac (claset() addEs [Ord_trans]) 0 1);
-qed "omult_le_mono2";
-
-Goal "[| i' le i; j' le j |] ==> i'**j' le i**j";
-by (rtac le_trans 1);
-by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_le_mono2, ltE,
- Ord_succD] 1));
-qed "omult_le_mono";
-
-Goal "[| i' le i; j'<j; 0<i |] ==> i'**j' < i**j";
-by (rtac lt_trans1 1);
-by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_lt_mono2, ltE,
- Ord_succD] 1));
-qed "omult_lt_mono";
-
-Goal "[| Ord(i); 0<j |] ==> i le j**i";
-by (ftac lt_Ord2 1);
-by (eres_inst_tac [("i","i")] trans_induct3 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [omult_succ]) 1);
-by (etac lt_trans1 1);
-by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN
- rtac oadd_lt_mono2 2);
-by (REPEAT (ares_tac [Ord_omult] 1));
-by (asm_simp_tac (simpset() addsimps [omult_Limit]) 1);
-by (rtac le_trans 1);
-by (rtac le_implies_UN_le_UN 2);
-by (Blast_tac 2);
-by (asm_simp_tac (simpset() addsimps [Union_eq_UN RS sym, Limit_Union_eq,
- Limit_is_Ord]) 1);
-qed "omult_le_self2";
-
-
-(** Further properties of ordinal multiplication **)
-
-Goal "[| i**j = i**k; 0<i; Ord(j); Ord(k) |] ==> j=k";
-by (rtac Ord_linear_lt 1);
-by (REPEAT_SOME assume_tac);
-by (ALLGOALS
- (force_tac (claset() addDs [omult_lt_mono2],
- simpset() addsimps [lt_not_refl])));
-qed "omult_inject";
-
--- a/src/ZF/OrderType.thy Sat May 11 20:40:31 2002 +0200
+++ b/src/ZF/OrderType.thy Mon May 13 09:02:13 2002 +0200
@@ -3,48 +3,1022 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Order types and ordinal arithmetic.
+Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory
The order type of a well-ordering is the least ordinal isomorphic to it.
+
+Ordinal arithmetic is traditionally defined in terms of order types, as here.
+But a definition by transfinite recursion would be much simpler!
*)
-OrderType = OrderArith + OrdQuant +
+theory OrderType = OrderArith + OrdQuant:
constdefs
- ordermap :: [i,i]=>i
+ ordermap :: "[i,i]=>i"
"ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
- ordertype :: [i,i]=>i
+ ordertype :: "[i,i]=>i"
"ordertype(A,r) == ordermap(A,r)``A"
(*alternative definition of ordinal numbers*)
- Ord_alt :: i => o
+ Ord_alt :: "i => o"
"Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))"
(*coercion to ordinal: if not, just 0*)
- ordify :: i=>i
+ ordify :: "i=>i"
"ordify(x) == if Ord(x) then x else 0"
(*ordinal multiplication*)
- omult :: [i,i]=>i (infixl "**" 70)
+ omult :: "[i,i]=>i" (infixl "**" 70)
"i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
(*ordinal addition*)
- raw_oadd :: [i,i]=>i
+ raw_oadd :: "[i,i]=>i"
"raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
- oadd :: [i,i]=>i (infixl "++" 65)
+ oadd :: "[i,i]=>i" (infixl "++" 65)
"i ++ j == raw_oadd(ordify(i),ordify(j))"
(*ordinal subtraction*)
- odiff :: [i,i]=>i (infixl "--" 65)
+ odiff :: "[i,i]=>i" (infixl "--" 65)
"i -- j == ordertype(i-j, Memrel(i))"
syntax (xsymbols)
- "op **" :: [i,i] => i (infixl "\\<times>\\<times>" 70)
+ "op **" :: "[i,i] => i" (infixl "\<times>\<times>" 70)
syntax (HTML output)
- "op **" :: [i,i] => i (infixl "\\<times>\\<times>" 70)
+ "op **" :: "[i,i] => i" (infixl "\<times>\<times>" 70)
+
+
+(*??for Ordinal.ML*)
+(*suitable for rewriting PROVIDED i has been fixed*)
+lemma Ord_in_Ord': "[| j:i; Ord(i) |] ==> Ord(j)"
+by (blast intro: Ord_in_Ord)
+
+
+(**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
+
+lemma le_well_ord_Memrel: "j le i ==> well_ord(j, Memrel(i))"
+apply (rule well_ordI)
+apply (rule wf_Memrel [THEN wf_imp_wf_on])
+apply (simp add: ltD lt_Ord linear_def
+ ltI [THEN lt_trans2 [of _ j i]])
+apply (intro ballI Ord_linear)
+apply (blast intro: Ord_in_Ord lt_Ord)+
+done
+
+(*"Ord(i) ==> well_ord(i, Memrel(i))"*)
+lemmas well_ord_Memrel = le_refl [THEN le_well_ord_Memrel]
+
+(*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord
+ The smaller ordinal is an initial segment of the larger *)
+lemma lt_pred_Memrel:
+ "j<i ==> pred(i, j, Memrel(i)) = j"
+apply (unfold pred_def lt_def)
+apply (simp (no_asm_simp))
+apply (blast intro: Ord_trans)
+done
+
+lemma pred_Memrel:
+ "x:A ==> pred(A, x, Memrel(A)) = A Int x"
+by (unfold pred_def Memrel_def, blast)
+
+lemma Ord_iso_implies_eq_lemma:
+ "[| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R"
+apply (frule lt_pred_Memrel)
+apply (erule ltE)
+apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto)
+apply (unfold ord_iso_def)
+(*Combining the two simplifications causes looping*)
+apply (simp (no_asm_simp))
+apply (blast intro: bij_is_fun [THEN apply_type] Ord_trans)
+done
+
+(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*)
+lemma Ord_iso_implies_eq:
+ "[| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) |]
+ ==> i=j"
+apply (rule_tac i = i and j = j in Ord_linear_lt)
+apply (blast intro: ord_iso_sym Ord_iso_implies_eq_lemma)+
+done
+
+
+(**** Ordermap and ordertype ****)
+
+lemma ordermap_type:
+ "ordermap(A,r) : A -> ordertype(A,r)"
+apply (unfold ordermap_def ordertype_def)
+apply (rule lam_type)
+apply (rule lamI [THEN imageI], assumption+)
+done
+
+(*** Unfolding of ordermap ***)
+
+(*Useful for cardinality reasoning; see CardinalArith.ML*)
+lemma ordermap_eq_image:
+ "[| wf[A](r); x:A |]
+ ==> ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"
+apply (unfold ordermap_def pred_def)
+apply (simp (no_asm_simp))
+apply (erule wfrec_on [THEN trans], assumption)
+apply (simp (no_asm_simp) add: subset_iff image_lam vimage_singleton_iff)
+done
+
+(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
+lemma ordermap_pred_unfold:
+ "[| wf[A](r); x:A |]
+ ==> ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"
+by (simp add: ordermap_eq_image pred_subset ordermap_type [THEN image_fun])
+
+(*pred-unfolded version. NOT suitable for rewriting -- loops!*)
+lemmas ordermap_unfold = ordermap_pred_unfold [simplified pred_def]
+
+(*The theorem above is
+
+[| wf[A](r); x : A |]
+==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}}
+
+NOTE: the definition of ordermap used here delivers ordinals only if r is
+transitive. If r is the predecessor relation on the naturals then
+ordermap(nat,predr) ` n equals {n-1} and not n. A more complicated definition,
+like
+
+ ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> : r}},
+
+might eliminate the need for r to be transitive.
+*)
+
+
+(*** Showing that ordermap, ordertype yield ordinals ***)
+
+lemma Ord_ordermap:
+ "[| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)"
+apply (unfold well_ord_def tot_ord_def part_ord_def, safe)
+apply (rule_tac a=x in wf_on_induct, assumption+)
+apply (simp (no_asm_simp) add: ordermap_pred_unfold)
+apply (rule OrdI [OF _ Ord_is_Transset])
+apply (unfold pred_def Transset_def)
+apply (blast intro: trans_onD
+ dest!: ordermap_unfold [THEN equalityD1])+
+done
+
+lemma Ord_ordertype:
+ "well_ord(A,r) ==> Ord(ordertype(A,r))"
+apply (unfold ordertype_def)
+apply (subst image_fun [OF ordermap_type subset_refl])
+apply (rule OrdI [OF _ Ord_is_Transset])
+prefer 2 apply (blast intro: Ord_ordermap)
+apply (unfold Transset_def well_ord_def)
+apply (blast intro: trans_onD
+ dest!: ordermap_unfold [THEN equalityD1])
+done
+
+
+(*** ordermap preserves the orderings in both directions ***)
+
+lemma ordermap_mono:
+ "[| <w,x>: r; wf[A](r); w: A; x: A |]
+ ==> ordermap(A,r)`w : ordermap(A,r)`x"
+apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption)
+apply blast
+done
+
+(*linearity of r is crucial here*)
+lemma converse_ordermap_mono:
+ "[| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); w: A; x: A |]
+ ==> <w,x>: r"
+apply (unfold well_ord_def tot_ord_def, safe)
+apply (erule_tac x=w and y=x in linearE, assumption+)
+apply (blast elim!: mem_not_refl [THEN notE])
+apply (blast dest: ordermap_mono intro: mem_asym)
+done
+
+lemmas ordermap_surj =
+ ordermap_type [THEN surj_image, unfolded ordertype_def [symmetric]]
+
+lemma ordermap_bij:
+ "well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"
+apply (unfold well_ord_def tot_ord_def bij_def inj_def)
+apply (force intro!: ordermap_type ordermap_surj
+ elim: linearE dest: ordermap_mono
+ simp add: mem_not_refl)
+done
+
+(*** Isomorphisms involving ordertype ***)
+
+lemma ordertype_ord_iso:
+ "well_ord(A,r)
+ ==> ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"
+apply (unfold ord_iso_def)
+apply (safe elim!: well_ord_is_wf
+ intro!: ordermap_type [THEN apply_type] ordermap_mono ordermap_bij)
+apply (blast dest!: converse_ordermap_mono)
+done
+
+lemma ordertype_eq:
+ "[| f: ord_iso(A,r,B,s); well_ord(B,s) |]
+ ==> ordertype(A,r) = ordertype(B,s)"
+apply (frule well_ord_ord_iso, assumption)
+apply (rule Ord_iso_implies_eq, (erule Ord_ordertype)+)
+apply (blast intro: ord_iso_trans ord_iso_sym ordertype_ord_iso)
+done
+
+lemma ordertype_eq_imp_ord_iso:
+ "[| ordertype(A,r) = ordertype(B,s); well_ord(A,r); well_ord(B,s) |]
+ ==> EX f. f: ord_iso(A,r,B,s)"
+apply (rule exI)
+apply (rule ordertype_ord_iso [THEN ord_iso_trans], assumption)
+apply (erule ssubst)
+apply (erule ordertype_ord_iso [THEN ord_iso_sym])
+done
+
+(*** Basic equalities for ordertype ***)
+
+(*Ordertype of Memrel*)
+lemma le_ordertype_Memrel: "j le i ==> ordertype(j,Memrel(i)) = j"
+apply (rule Ord_iso_implies_eq [symmetric])
+apply (erule ltE, assumption)
+apply (blast intro: le_well_ord_Memrel Ord_ordertype)
+apply (rule ord_iso_trans)
+apply (erule_tac [2] le_well_ord_Memrel [THEN ordertype_ord_iso])
+apply (rule id_bij [THEN ord_isoI])
+apply (simp (no_asm_simp))
+apply (fast elim: ltE Ord_in_Ord Ord_trans)
+done
+
+(*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*)
+lemmas ordertype_Memrel = le_refl [THEN le_ordertype_Memrel]
+
+lemma ordertype_0 [simp]: "ordertype(0,r) = 0"
+apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq, THEN trans])
+apply (erule emptyE)
+apply (rule well_ord_0)
+apply (rule Ord_0 [THEN ordertype_Memrel])
+done
+
+(*Ordertype of rvimage: [| f: bij(A,B); well_ord(B,s) |] ==>
+ ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)
+lemmas bij_ordertype_vimage = ord_iso_rvimage [THEN ordertype_eq]
+
+(*** A fundamental unfolding law for ordertype. ***)
+
+(*Ordermap returns the same result if applied to an initial segment*)
+lemma ordermap_pred_eq_ordermap:
+ "[| well_ord(A,r); y:A; z: pred(A,y,r) |]
+ ==> ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"
+apply (frule wf_on_subset_A [OF well_ord_is_wf pred_subset])
+apply (rule_tac a=z in wf_on_induct, assumption+)
+apply (safe elim!: predE)
+apply (simp (no_asm_simp) add: ordermap_pred_unfold well_ord_is_wf pred_iff)
+(*combining these two simplifications LOOPS! *)
+apply (simp (no_asm_simp) add: pred_pred_eq)
+apply (simp add: pred_def)
+apply (rule RepFun_cong [OF _ refl])
+apply (drule well_ord_is_trans_on)
+apply (fast elim!: trans_onD)
+done
+
+lemma ordertype_unfold:
+ "ordertype(A,r) = {ordermap(A,r)`y . y : A}"
+apply (unfold ordertype_def)
+apply (rule image_fun [OF ordermap_type subset_refl])
+done
+
+(** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **)
+
+lemma ordertype_pred_subset: "[| well_ord(A,r); x:A |] ==>
+ ordertype(pred(A,x,r),r) <= ordertype(A,r)"
+apply (simp add: ordertype_unfold well_ord_subset [OF _ pred_subset])
+apply (fast intro: ordermap_pred_eq_ordermap elim: predE)
+done
+
+lemma ordertype_pred_lt:
+ "[| well_ord(A,r); x:A |]
+ ==> ordertype(pred(A,x,r),r) < ordertype(A,r)"
+apply (rule ordertype_pred_subset [THEN subset_imp_le, THEN leE])
+apply (simp_all add: Ord_ordertype well_ord_subset [OF _ pred_subset])
+apply (erule sym [THEN ordertype_eq_imp_ord_iso, THEN exE])
+apply (erule_tac [3] well_ord_iso_predE)
+apply (simp_all add: well_ord_subset [OF _ pred_subset])
+done
+
+(*May rewrite with this -- provided no rules are supplied for proving that
+ well_ord(pred(A,x,r), r) *)
+lemma ordertype_pred_unfold:
+ "well_ord(A,r)
+ ==> ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}"
+apply (rule equalityI)
+apply (safe intro!: ordertype_pred_lt [THEN ltD])
+apply (auto simp add: ordertype_def well_ord_is_wf [THEN ordermap_eq_image]
+ ordermap_type [THEN image_fun]
+ ordermap_pred_eq_ordermap pred_subset)
+done
+
+
+(**** Alternative definition of ordinal ****)
+
+(*proof by Krzysztof Grabczewski*)
+lemma Ord_is_Ord_alt: "Ord(i) ==> Ord_alt(i)"
+apply (unfold Ord_alt_def)
+apply (rule conjI)
+apply (erule well_ord_Memrel)
+apply (unfold Ord_def Transset_def pred_def Memrel_def, blast)
+done
+
+(*proof by lcp*)
+lemma Ord_alt_is_Ord:
+ "Ord_alt(i) ==> Ord(i)"
+apply (unfold Ord_alt_def Ord_def Transset_def well_ord_def
+ tot_ord_def part_ord_def trans_on_def)
+apply (simp add: pred_Memrel)
+apply (blast elim!: equalityE)
+done
+
+
+(**** Ordinal Addition ****)
+
+(*** Order Type calculations for radd ***)
+
+(** Addition with 0 **)
+
+lemma bij_sum_0: "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)"
+apply (rule_tac d = Inl in lam_bijective, safe)
+apply (simp_all (no_asm_simp))
+done
+
+lemma ordertype_sum_0_eq:
+ "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"
+apply (rule bij_sum_0 [THEN ord_isoI, THEN ordertype_eq])
+prefer 2 apply assumption
+apply force
+done
+
+lemma bij_0_sum: "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)"
+apply (rule_tac d = Inr in lam_bijective, safe)
+apply (simp_all (no_asm_simp))
+done
+
+lemma ordertype_0_sum_eq:
+ "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"
+apply (rule bij_0_sum [THEN ord_isoI, THEN ordertype_eq])
+prefer 2 apply assumption
+apply force
+done
+
+(** Initial segments of radd. Statements by Grabczewski **)
+
+(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
+lemma pred_Inl_bij:
+ "a:A ==> (lam x:pred(A,a,r). Inl(x))
+ : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"
+apply (unfold pred_def)
+apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
+apply auto
+done
+
+lemma ordertype_pred_Inl_eq:
+ "[| a:A; well_ord(A,r) |]
+ ==> ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) =
+ ordertype(pred(A,a,r), r)"
+apply (rule pred_Inl_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
+apply (simp_all add: well_ord_subset [OF _ pred_subset])
+apply (simp add: pred_def)
+done
+
+lemma pred_Inr_bij:
+ "b:B ==>
+ id(A+pred(B,b,s))
+ : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"
+apply (unfold pred_def id_def)
+apply (rule_tac d = "%z. z" in lam_bijective, auto)
+done
+
+lemma ordertype_pred_Inr_eq:
+ "[| b:B; well_ord(A,r); well_ord(B,s) |]
+ ==> ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) =
+ ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"
+apply (rule pred_Inr_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
+prefer 2 apply (force simp add: pred_def id_def, assumption)
+apply (blast intro: well_ord_radd well_ord_subset [OF _ pred_subset])
+done
+
+
+(*** ordify: trivial coercion to an ordinal ***)
+
+lemma Ord_ordify [iff, TC]: "Ord(ordify(x))"
+by (simp add: ordify_def)
+
+(*Collapsing*)
+lemma ordify_idem [simp]: "ordify(ordify(x)) = ordify(x)"
+by (simp add: ordify_def)
+
+
+(*** Basic laws for ordinal addition ***)
+
+lemma Ord_raw_oadd: "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))"
+by (simp add: raw_oadd_def ordify_def Ord_ordertype well_ord_radd
+ well_ord_Memrel)
+
+lemma Ord_oadd [iff,TC]: "Ord(i++j)"
+by (simp add: oadd_def Ord_raw_oadd)
+
+
+(** Ordinal addition with zero **)
+
+lemma raw_oadd_0: "Ord(i) ==> raw_oadd(i,0) = i"
+by (simp add: raw_oadd_def ordify_def ordertype_sum_0_eq
+ ordertype_Memrel well_ord_Memrel)
+
+lemma oadd_0 [simp]: "Ord(i) ==> i++0 = i"
+apply (simp (no_asm_simp) add: oadd_def raw_oadd_0 ordify_def)
+done
+
+lemma raw_oadd_0_left: "Ord(i) ==> raw_oadd(0,i) = i"
+by (simp add: raw_oadd_def ordify_def ordertype_0_sum_eq ordertype_Memrel
+ well_ord_Memrel)
+
+lemma oadd_0_left [simp]: "Ord(i) ==> 0++i = i"
+by (simp add: oadd_def raw_oadd_0_left ordify_def)
+
+
+lemma oadd_eq_if_raw_oadd:
+ "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i)
+ else (if Ord(j) then j else 0))"
+by (simp add: oadd_def ordify_def raw_oadd_0_left raw_oadd_0)
+
+lemma raw_oadd_eq_oadd: "[|Ord(i); Ord(j)|] ==> raw_oadd(i,j) = i++j"
+by (simp add: oadd_def ordify_def)
+
+(*** Further properties of ordinal addition. Statements by Grabczewski,
+ proofs by lcp. ***)
+
+(*Surely also provable by transfinite induction on j?*)
+lemma lt_oadd1: "k<i ==> k < i++j"
+apply (simp add: oadd_def ordify_def lt_Ord2 raw_oadd_0, clarify)
+apply (simp add: raw_oadd_def)
+apply (rule ltE, assumption)
+apply (rule ltI)
+apply (force simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel
+ ordertype_pred_Inl_eq lt_pred_Memrel leI [THEN le_ordertype_Memrel])
+apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)
+done
+
+(*Thus also we obtain the rule i++j = k ==> i le k *)
+lemma oadd_le_self: "Ord(i) ==> i le i++j"
+apply (rule all_lt_imp_le)
+apply (auto simp add: Ord_oadd lt_oadd1)
+done
+
+(** A couple of strange but necessary results! **)
+
+lemma id_ord_iso_Memrel: "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"
+apply (rule id_bij [THEN ord_isoI])
+apply (simp (no_asm_simp))
+apply blast
+done
+
+lemma ordertype_sum_Memrel:
+ "[| well_ord(A,r); k<j |]
+ ==> ordertype(A+k, radd(A, r, k, Memrel(j))) =
+ ordertype(A+k, radd(A, r, k, Memrel(k)))"
+apply (erule ltE)
+apply (rule ord_iso_refl [THEN sum_ord_iso_cong, THEN ordertype_eq])
+apply (erule OrdmemD [THEN id_ord_iso_Memrel, THEN ord_iso_sym])
+apply (simp_all add: well_ord_radd well_ord_Memrel)
+done
+
+lemma oadd_lt_mono2: "k<j ==> i++k < i++j"
+apply (simp add: oadd_def ordify_def raw_oadd_0_left lt_Ord lt_Ord2, clarify)
+apply (simp add: raw_oadd_def)
+apply (rule ltE, assumption)
+apply (rule ordertype_pred_unfold [THEN equalityD2, THEN subsetD, THEN ltI])
+apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)
+apply (rule bexI)
+apply (erule_tac [2] InrI)
+apply (simp add: ordertype_pred_Inr_eq well_ord_Memrel lt_pred_Memrel
+ leI [THEN le_ordertype_Memrel] ordertype_sum_Memrel)
+done
+
+lemma oadd_lt_cancel2: "[| i++j < i++k; Ord(j) |] ==> j<k"
+apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
+ prefer 2
+ apply (frule_tac i = i and j = j in oadd_le_self)
+ apply (simp add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])
+apply (rule Ord_linear_lt, auto)
+apply (simp_all add: raw_oadd_eq_oadd)
+apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+
+done
+
+lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k <-> j<k"
+by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
+
+lemma oadd_inject: "[| i++j = i++k; Ord(j); Ord(k) |] ==> j=k"
+apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
+apply (simp add: raw_oadd_eq_oadd)
+apply (rule Ord_linear_lt, auto)
+apply (force dest: oadd_lt_mono2 [of concl: i] simp add: lt_not_refl)+
+done
+
+lemma lt_oadd_disj: "k < i++j ==> k<i | (EX l:j. k = i++l )"
+apply (simp add: Ord_in_Ord' [of _ j] oadd_eq_if_raw_oadd
+ split add: split_if_asm)
+ prefer 2
+ apply (simp add: Ord_in_Ord' [of _ j] lt_def)
+apply (simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel raw_oadd_def)
+apply (erule ltD [THEN RepFunE])
+apply (force simp add: ordertype_pred_Inl_eq well_ord_Memrel ltI
+ lt_pred_Memrel le_ordertype_Memrel leI
+ ordertype_pred_Inr_eq ordertype_sum_Memrel)
+done
+
+
+(*** Ordinal addition with successor -- via associativity! ***)
+
+lemma oadd_assoc: "(i++j)++k = i++(j++k)"
+apply (simp add: oadd_eq_if_raw_oadd Ord_raw_oadd raw_oadd_0 raw_oadd_0_left, clarify)
+apply (simp add: raw_oadd_def)
+apply (rule ordertype_eq [THEN trans])
+apply (rule sum_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]
+ ord_iso_refl])
+apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)
+apply (rule sum_assoc_ord_iso [THEN ordertype_eq, THEN trans])
+apply (rule_tac [2] ordertype_eq)
+apply (rule_tac [2] sum_ord_iso_cong [OF ord_iso_refl ordertype_ord_iso])
+apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)+
+done
+
+lemma oadd_unfold: "[| Ord(i); Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})"
+apply (rule subsetI [THEN equalityI])
+apply (erule ltI [THEN lt_oadd_disj, THEN disjE])
+apply (blast intro: Ord_oadd)
+apply (blast elim!: ltE, blast)
+apply (force intro: lt_oadd1 oadd_lt_mono2 simp add: Ord_mem_iff_lt)
+done
+
+lemma oadd_1: "Ord(i) ==> i++1 = succ(i)"
+apply (simp (no_asm_simp) add: oadd_unfold Ord_1 oadd_0)
+apply blast
+done
+
+lemma oadd_succ [simp]: "Ord(j) ==> i++succ(j) = succ(i++j)"
+apply (simp add: oadd_eq_if_raw_oadd, clarify)
+apply (simp add: raw_oadd_eq_oadd)
+apply (simp add: oadd_1 [of j, symmetric] oadd_1 [of "i++j", symmetric]
+ oadd_assoc)
+done
+
+
+(** Ordinal addition with limit ordinals **)
+
+lemma oadd_UN:
+ "[| !!x. x:A ==> Ord(j(x)); a:A |]
+ ==> i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"
+by (blast intro: ltI Ord_UN Ord_oadd lt_oadd1 [THEN ltD]
+ oadd_lt_mono2 [THEN ltD]
+ elim!: ltE dest!: ltI [THEN lt_oadd_disj])
+
+lemma oadd_Limit: "Limit(j) ==> i++j = (UN k:j. i++k)"
+apply (frule Limit_has_0 [THEN ltD])
+apply (simp (no_asm_simp) add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] Union_eq_UN [symmetric] Limit_Union_eq)
+done
+
+(** Order/monotonicity properties of ordinal addition **)
+
+lemma oadd_le_self2: "Ord(i) ==> i le j++i"
+apply (erule_tac i = i in trans_induct3)
+apply (simp (no_asm_simp) add: Ord_0_le)
+apply (simp (no_asm_simp) add: oadd_succ succ_leI)
+apply (simp (no_asm_simp) add: oadd_Limit)
+apply (rule le_trans)
+apply (rule_tac [2] le_implies_UN_le_UN)
+apply (erule_tac [2] bspec)
+prefer 2 apply assumption
+apply (simp (no_asm_simp) add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord)
+done
+
+lemma oadd_le_mono1: "k le j ==> k++i le j++i"
+apply (frule lt_Ord)
+apply (frule le_Ord2)
+apply (simp add: oadd_eq_if_raw_oadd, clarify)
+apply (simp add: raw_oadd_eq_oadd)
+apply (erule_tac i = i in trans_induct3)
+apply (simp (no_asm_simp))
+apply (simp (no_asm_simp) add: oadd_succ succ_le_iff)
+apply (simp (no_asm_simp) add: oadd_Limit)
+apply (rule le_implies_UN_le_UN, blast)
+done
+
+lemma oadd_lt_mono: "[| i' le i; j'<j |] ==> i'++j' < i++j"
+by (blast intro: lt_trans1 oadd_le_mono1 oadd_lt_mono2 Ord_succD elim: ltE)
+
+lemma oadd_le_mono: "[| i' le i; j' le j |] ==> i'++j' le i++j"
+by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)
+
+lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"
+by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
+
+
+(** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)).
+ Probably simpler to define the difference recursively!
+**)
+
+lemma bij_sum_Diff:
+ "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))"
+apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
+apply (blast intro!: if_type)
+apply (fast intro!: case_type)
+apply (erule_tac [2] sumE)
+apply (simp_all (no_asm_simp))
+done
+
+lemma ordertype_sum_Diff:
+ "i le j ==>
+ ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =
+ ordertype(j, Memrel(j))"
+apply (safe dest!: le_subset_iff [THEN iffD1])
+apply (rule bij_sum_Diff [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
+apply (erule_tac [3] well_ord_Memrel, assumption)
+apply (simp (no_asm_simp))
+apply (frule_tac j = y in Ord_in_Ord, assumption)
+apply (frule_tac j = x in Ord_in_Ord, assumption)
+apply (simp (no_asm_simp) add: Ord_mem_iff_lt lt_Ord not_lt_iff_le)
+apply (blast intro: lt_trans2 lt_trans)
+done
+
+lemma Ord_odiff [simp,TC]:
+ "[| Ord(i); Ord(j) |] ==> Ord(i--j)"
+apply (unfold odiff_def)
+apply (blast intro: Ord_ordertype Diff_subset well_ord_subset well_ord_Memrel)
+done
+
+
+lemma raw_oadd_ordertype_Diff:
+ "i le j
+ ==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"
+apply (simp add: raw_oadd_def odiff_def)
+apply (safe dest!: le_subset_iff [THEN iffD1])
+apply (rule sum_ord_iso_cong [THEN ordertype_eq])
+apply (erule id_ord_iso_Memrel)
+apply (rule ordertype_ord_iso [THEN ord_iso_sym])
+apply (blast intro: well_ord_radd Diff_subset well_ord_subset well_ord_Memrel)+
+done
+
+lemma oadd_odiff_inverse: "i le j ==> i ++ (j--i) = j"
+by (simp add: lt_Ord le_Ord2 oadd_def ordify_def raw_oadd_ordertype_Diff
+ ordertype_sum_Diff ordertype_Memrel lt_Ord2 [THEN Ord_succD])
+
+(*By oadd_inject, the difference between i and j is unique. Note that we get
+ i++j = k ==> j = k--i. *)
+lemma odiff_oadd_inverse: "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j"
+apply (rule oadd_inject)
+apply (blast intro: oadd_odiff_inverse oadd_le_self)
+apply (blast intro: Ord_ordertype Ord_oadd Ord_odiff)+
+done
+
+lemma odiff_lt_mono2: "[| i<j; k le i |] ==> i--k < j--k"
+apply (rule_tac i = k in oadd_lt_cancel2)
+apply (simp add: oadd_odiff_inverse)
+apply (subst oadd_odiff_inverse)
+apply (blast intro: le_trans leI, assumption)
+apply (simp (no_asm_simp) add: lt_Ord le_Ord2)
+done
+
+
+(**** Ordinal Multiplication ****)
+
+lemma Ord_omult [simp,TC]:
+ "[| Ord(i); Ord(j) |] ==> Ord(i**j)"
+apply (unfold omult_def)
+apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel)
+done
+
+(*** A useful unfolding law ***)
+
+lemma pred_Pair_eq:
+ "[| a:A; b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) =
+ pred(A,a,r)*B Un ({a} * pred(B,b,s))"
+apply (unfold pred_def, blast)
+done
+
+lemma ordertype_pred_Pair_eq:
+ "[| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==>
+ ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) =
+ ordertype(pred(A,a,r)*B + pred(B,b,s),
+ radd(A*B, rmult(A,r,B,s), B, s))"
+apply (simp (no_asm_simp) add: pred_Pair_eq)
+apply (rule ordertype_eq [symmetric])
+apply (rule prod_sum_singleton_ord_iso)
+apply (simp_all add: pred_subset well_ord_rmult [THEN well_ord_subset])
+apply (blast intro: pred_subset well_ord_rmult [THEN well_ord_subset]
+ elim!: predE)
+done
+
+lemma ordertype_pred_Pair_lemma:
+ "[| i'<i; j'<j |]
+ ==> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),
+ rmult(i,Memrel(i),j,Memrel(j))) =
+ raw_oadd (j**i', j')"
+apply (unfold raw_oadd_def omult_def)
+apply (simp (no_asm_simp) add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2 well_ord_Memrel)
+apply (rule trans)
+apply (rule_tac [2] ordertype_ord_iso [THEN sum_ord_iso_cong, THEN ordertype_eq])
+apply (rule_tac [3] ord_iso_refl)
+apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq])
+apply (elim SigmaE sumE ltE ssubst)
+apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
+ Ord_ordertype lt_Ord lt_Ord2)
+apply (blast intro: Ord_trans)+
+done
+
+lemma lt_omult:
+ "[| Ord(i); Ord(j); k<j**i |]
+ ==> EX j' i'. k = j**i' ++ j' & j'<j & i'<i"
+apply (unfold omult_def)
+apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel)
+apply (safe elim!: ltE)
+apply (simp add: ordertype_pred_Pair_lemma ltI raw_oadd_eq_oadd
+ omult_def [symmetric] Ord_in_Ord' [of _ i] Ord_in_Ord' [of _ j])
+apply (blast intro: ltI)
+done
+
+lemma omult_oadd_lt:
+ "[| j'<j; i'<i |] ==> j**i' ++ j' < j**i"
+apply (unfold omult_def)
+apply (rule ltI)
+ prefer 2
+ apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
+apply (simp (no_asm_simp) add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)
+apply (rule bexI)
+prefer 2 apply (blast elim!: ltE)
+apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric])
+apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd)
+done
+
+lemma omult_unfold:
+ "[| Ord(i); Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})"
+apply (rule subsetI [THEN equalityI])
+apply (rule lt_omult [THEN exE])
+apply (erule_tac [3] ltI)
+apply (simp_all add: Ord_omult)
+apply (blast elim!: ltE)
+apply (blast intro: omult_oadd_lt [THEN ltD] ltI)
+done
+
+(*** Basic laws for ordinal multiplication ***)
+
+(** Ordinal multiplication by zero **)
+
+lemma omult_0 [simp]: "i**0 = 0"
+apply (unfold omult_def)
+apply (simp (no_asm_simp))
+done
+
+lemma omult_0_left [simp]: "0**i = 0"
+apply (unfold omult_def)
+apply (simp (no_asm_simp))
+done
+
+(** Ordinal multiplication by 1 **)
+
+lemma omult_1 [simp]: "Ord(i) ==> i**1 = i"
+apply (unfold omult_def)
+apply (rule_tac s1="Memrel(i)"
+ in ord_isoI [THEN ordertype_eq, THEN trans])
+apply (rule_tac c = snd and d = "%z.<0,z>" in lam_bijective)
+apply (auto elim!: snd_type well_ord_Memrel ordertype_Memrel)
+done
+
+lemma omult_1_left [simp]: "Ord(i) ==> 1**i = i"
+apply (unfold omult_def)
+apply (rule_tac s1="Memrel(i)"
+ in ord_isoI [THEN ordertype_eq, THEN trans])
+apply (rule_tac c = fst and d = "%z.<z,0>" in lam_bijective)
+apply (auto elim!: fst_type well_ord_Memrel ordertype_Memrel)
+done
+
+(** Distributive law for ordinal multiplication and addition **)
+
+lemma oadd_omult_distrib:
+ "[| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"
+apply (simp add: oadd_eq_if_raw_oadd)
+apply (simp add: omult_def raw_oadd_def)
+apply (rule ordertype_eq [THEN trans])
+apply (rule prod_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]
+ ord_iso_refl])
+apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
+ Ord_ordertype)
+apply (rule sum_prod_distrib_ord_iso [THEN ordertype_eq, THEN trans])
+apply (rule_tac [2] ordertype_eq)
+apply (rule_tac [2] sum_ord_iso_cong [OF ordertype_ord_iso ordertype_ord_iso])
+apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
+ Ord_ordertype)
+done
+
+lemma omult_succ: "[| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i"
+by (simp del: oadd_succ add: oadd_1 [of j, symmetric] oadd_omult_distrib)
+
+(** Associative law **)
+
+lemma omult_assoc:
+ "[| Ord(i); Ord(j); Ord(k) |] ==> (i**j)**k = i**(j**k)"
+apply (unfold omult_def)
+apply (rule ordertype_eq [THEN trans])
+apply (rule prod_ord_iso_cong [OF ord_iso_refl
+ ordertype_ord_iso [THEN ord_iso_sym]])
+apply (blast intro: well_ord_rmult well_ord_Memrel)+
+apply (rule prod_assoc_ord_iso [THEN ord_iso_sym, THEN ordertype_eq, THEN trans])
+apply (rule_tac [2] ordertype_eq)
+apply (rule_tac [2] prod_ord_iso_cong [OF ordertype_ord_iso ord_iso_refl])
+apply (blast intro: well_ord_rmult well_ord_Memrel Ord_ordertype)+
+done
+
+
+(** Ordinal multiplication with limit ordinals **)
+
+lemma omult_UN:
+ "[| Ord(i); !!x. x:A ==> Ord(j(x)) |]
+ ==> i ** (UN x:A. j(x)) = (UN x:A. i**j(x))"
+by (simp (no_asm_simp) add: Ord_UN omult_unfold, blast)
+
+lemma omult_Limit: "[| Ord(i); Limit(j) |] ==> i**j = (UN k:j. i**k)"
+by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric]
+ Union_eq_UN [symmetric] Limit_Union_eq)
+
+
+(*** Ordering/monotonicity properties of ordinal multiplication ***)
+
+(*As a special case we have "[| 0<i; 0<j |] ==> 0 < i**j" *)
+lemma lt_omult1: "[| k<i; 0<j |] ==> k < i**j"
+apply (safe elim!: ltE intro!: ltI Ord_omult)
+apply (force simp add: omult_unfold)
+done
+
+lemma omult_le_self: "[| Ord(i); 0<j |] ==> i le i**j"
+by (blast intro: all_lt_imp_le Ord_omult lt_omult1 lt_Ord2)
+
+lemma omult_le_mono1: "[| k le j; Ord(i) |] ==> k**i le j**i"
+apply (frule lt_Ord)
+apply (frule le_Ord2)
+apply (erule trans_induct3)
+apply (simp (no_asm_simp) add: le_refl Ord_0)
+apply (simp (no_asm_simp) add: omult_succ oadd_le_mono)
+apply (simp (no_asm_simp) add: omult_Limit)
+apply (rule le_implies_UN_le_UN, blast)
+done
+
+lemma omult_lt_mono2: "[| k<j; 0<i |] ==> i**k < i**j"
+apply (rule ltI)
+apply (simp (no_asm_simp) add: omult_unfold lt_Ord2)
+apply (safe elim!: ltE intro!: Ord_omult)
+apply (force simp add: Ord_omult)
+done
+
+lemma omult_le_mono2: "[| k le j; Ord(i) |] ==> i**k le i**j"
+apply (rule subset_imp_le)
+apply (safe elim!: ltE dest!: Ord_succD intro!: Ord_omult)
+apply (simp add: omult_unfold)
+apply (blast intro: Ord_trans)
+done
+
+lemma omult_le_mono: "[| i' le i; j' le j |] ==> i'**j' le i**j"
+by (blast intro: le_trans omult_le_mono1 omult_le_mono2 Ord_succD elim: ltE)
+
+lemma omult_lt_mono: "[| i' le i; j'<j; 0<i |] ==> i'**j' < i**j"
+by (blast intro: lt_trans1 omult_le_mono1 omult_lt_mono2 Ord_succD elim: ltE)
+
+lemma omult_le_self2: "[| Ord(i); 0<j |] ==> i le j**i"
+apply (frule lt_Ord2)
+apply (erule_tac i = i in trans_induct3)
+apply (simp (no_asm_simp))
+apply (simp (no_asm_simp) add: omult_succ)
+apply (erule lt_trans1)
+apply (rule_tac b = "j**x" in oadd_0 [THEN subst], rule_tac [2] oadd_lt_mono2)
+apply (blast intro: Ord_omult, assumption)
+apply (simp (no_asm_simp) add: omult_Limit)
+apply (rule le_trans)
+apply (rule_tac [2] le_implies_UN_le_UN)
+prefer 2 apply blast
+apply (simp (no_asm_simp) add: Union_eq_UN [symmetric] Limit_Union_eq Limit_is_Ord)
+done
+
+
+(** Further properties of ordinal multiplication **)
+
+lemma omult_inject: "[| i**j = i**k; 0<i; Ord(j); Ord(k) |] ==> j=k"
+apply (rule Ord_linear_lt)
+prefer 4 apply assumption
+apply auto
+apply (force dest: omult_lt_mono2 simp add: lt_not_refl)+
+done
+
+ML {*
+val ordermap_def = thm "ordermap_def";
+val ordertype_def = thm "ordertype_def";
+val Ord_alt_def = thm "Ord_alt_def";
+val ordify_def = thm "ordify_def";
+
+val Ord_in_Ord' = thm "Ord_in_Ord'";
+val le_well_ord_Memrel = thm "le_well_ord_Memrel";
+val well_ord_Memrel = thm "well_ord_Memrel";
+val lt_pred_Memrel = thm "lt_pred_Memrel";
+val pred_Memrel = thm "pred_Memrel";
+val Ord_iso_implies_eq_lemma = thm "Ord_iso_implies_eq_lemma";
+val Ord_iso_implies_eq = thm "Ord_iso_implies_eq";
+val ordermap_type = thm "ordermap_type";
+val ordermap_eq_image = thm "ordermap_eq_image";
+val ordermap_pred_unfold = thm "ordermap_pred_unfold";
+val ordermap_unfold = thm "ordermap_unfold";
+val Ord_ordermap = thm "Ord_ordermap";
+val Ord_ordertype = thm "Ord_ordertype";
+val ordermap_mono = thm "ordermap_mono";
+val converse_ordermap_mono = thm "converse_ordermap_mono";
+val ordermap_surj = thm "ordermap_surj";
+val ordermap_bij = thm "ordermap_bij";
+val ordertype_ord_iso = thm "ordertype_ord_iso";
+val ordertype_eq = thm "ordertype_eq";
+val ordertype_eq_imp_ord_iso = thm "ordertype_eq_imp_ord_iso";
+val le_ordertype_Memrel = thm "le_ordertype_Memrel";
+val ordertype_Memrel = thm "ordertype_Memrel";
+val ordertype_0 = thm "ordertype_0";
+val bij_ordertype_vimage = thm "bij_ordertype_vimage";
+val ordermap_pred_eq_ordermap = thm "ordermap_pred_eq_ordermap";
+val ordertype_unfold = thm "ordertype_unfold";
+val ordertype_pred_subset = thm "ordertype_pred_subset";
+val ordertype_pred_lt = thm "ordertype_pred_lt";
+val ordertype_pred_unfold = thm "ordertype_pred_unfold";
+val Ord_is_Ord_alt = thm "Ord_is_Ord_alt";
+val Ord_alt_is_Ord = thm "Ord_alt_is_Ord";
+val bij_sum_0 = thm "bij_sum_0";
+val ordertype_sum_0_eq = thm "ordertype_sum_0_eq";
+val bij_0_sum = thm "bij_0_sum";
+val ordertype_0_sum_eq = thm "ordertype_0_sum_eq";
+val pred_Inl_bij = thm "pred_Inl_bij";
+val ordertype_pred_Inl_eq = thm "ordertype_pred_Inl_eq";
+val pred_Inr_bij = thm "pred_Inr_bij";
+val ordertype_pred_Inr_eq = thm "ordertype_pred_Inr_eq";
+val Ord_ordify = thm "Ord_ordify";
+val ordify_idem = thm "ordify_idem";
+val Ord_raw_oadd = thm "Ord_raw_oadd";
+val Ord_oadd = thm "Ord_oadd";
+val raw_oadd_0 = thm "raw_oadd_0";
+val oadd_0 = thm "oadd_0";
+val raw_oadd_0_left = thm "raw_oadd_0_left";
+val oadd_0_left = thm "oadd_0_left";
+val oadd_eq_if_raw_oadd = thm "oadd_eq_if_raw_oadd";
+val raw_oadd_eq_oadd = thm "raw_oadd_eq_oadd";
+val lt_oadd1 = thm "lt_oadd1";
+val oadd_le_self = thm "oadd_le_self";
+val id_ord_iso_Memrel = thm "id_ord_iso_Memrel";
+val ordertype_sum_Memrel = thm "ordertype_sum_Memrel";
+val oadd_lt_mono2 = thm "oadd_lt_mono2";
+val oadd_lt_cancel2 = thm "oadd_lt_cancel2";
+val oadd_lt_iff2 = thm "oadd_lt_iff2";
+val oadd_inject = thm "oadd_inject";
+val lt_oadd_disj = thm "lt_oadd_disj";
+val oadd_assoc = thm "oadd_assoc";
+val oadd_unfold = thm "oadd_unfold";
+val oadd_1 = thm "oadd_1";
+val oadd_succ = thm "oadd_succ";
+val oadd_UN = thm "oadd_UN";
+val oadd_Limit = thm "oadd_Limit";
+val oadd_le_self2 = thm "oadd_le_self2";
+val oadd_le_mono1 = thm "oadd_le_mono1";
+val oadd_lt_mono = thm "oadd_lt_mono";
+val oadd_le_mono = thm "oadd_le_mono";
+val oadd_le_iff2 = thm "oadd_le_iff2";
+val bij_sum_Diff = thm "bij_sum_Diff";
+val ordertype_sum_Diff = thm "ordertype_sum_Diff";
+val Ord_odiff = thm "Ord_odiff";
+val raw_oadd_ordertype_Diff = thm "raw_oadd_ordertype_Diff";
+val oadd_odiff_inverse = thm "oadd_odiff_inverse";
+val odiff_oadd_inverse = thm "odiff_oadd_inverse";
+val odiff_lt_mono2 = thm "odiff_lt_mono2";
+val Ord_omult = thm "Ord_omult";
+val pred_Pair_eq = thm "pred_Pair_eq";
+val ordertype_pred_Pair_eq = thm "ordertype_pred_Pair_eq";
+val ordertype_pred_Pair_lemma = thm "ordertype_pred_Pair_lemma";
+val lt_omult = thm "lt_omult";
+val omult_oadd_lt = thm "omult_oadd_lt";
+val omult_unfold = thm "omult_unfold";
+val omult_0 = thm "omult_0";
+val omult_0_left = thm "omult_0_left";
+val omult_1 = thm "omult_1";
+val omult_1_left = thm "omult_1_left";
+val oadd_omult_distrib = thm "oadd_omult_distrib";
+val omult_succ = thm "omult_succ";
+val omult_assoc = thm "omult_assoc";
+val omult_UN = thm "omult_UN";
+val omult_Limit = thm "omult_Limit";
+val lt_omult1 = thm "lt_omult1";
+val omult_le_self = thm "omult_le_self";
+val omult_le_mono1 = thm "omult_le_mono1";
+val omult_lt_mono2 = thm "omult_lt_mono2";
+val omult_le_mono2 = thm "omult_le_mono2";
+val omult_le_mono = thm "omult_le_mono";
+val omult_lt_mono = thm "omult_lt_mono";
+val omult_le_self2 = thm "omult_le_self2";
+val omult_inject = thm "omult_inject";
+*}
end