src/ZF/OrderType.ML
 author lcp Thu, 12 Jan 1995 03:00:38 +0100 changeset 849 013a16d3addb parent 831 60d850cc5fe6 child 984 4fb1d099ba45 permissions -rw-r--r--
Proved equivalence of Ord and Ord_alt. Proved ordertype_eq_imp_ord_iso, le_well_ord_Memrel, le_ordertype_Memrel, lt_oadd1, oadd_le_self, bij_0_sum, oadd_0, oadd_assoc, id_ord_iso_Memrel, ordertype_0. Now well_ord_Memrel follows from le_well_ord_Memrel and ordertype_Memrel follows from le_ordertype_Memrel. Proved simpler versions of Krzysztof's theorems Ord_oadd, ordertype_pred_subset, ordertype_pred_lt, ordertype_pred_unfold, bij_sum_0, bij_sum_succ, ordertype_sum_Memrel, lt_oadd_disj, oadd_inject. Deleted ordertype_subset: subsumed by ordertype_pred_unfold. Proved ordinal multiplication theorems Ord_omult, lt_omult, omult_oadd_lt, omult_unfold, omult_0, omult_0_left, omult_1, omult_1_left, oadd_omult_distrib, omult_succ, omult_assoc, omult_UN, omult_Limit, lt_omult1, omult_le_self, omult_le_mono1, omult_lt_mono2, omult_le_mono2, omult_le_mono, omult_lt_mono, omult_le_self2, omult_inject.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 1` ```(* Title: ZF/OrderType.ML ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 2` ``` ID: \$Id\$ ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 4` ``` Copyright 1994 University of Cambridge ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 5` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 6` ```Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 7` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 8` ```Ordinal arithmetic is traditionally defined in terms of order types, as here. ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 9` ```But a definition by transfinite recursion would be much simpler! ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 10` ```*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 11` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 12` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 13` ```open OrderType; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 14` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 15` ```(**** Proofs needing the combination of Ordinal.thy and Order.thy ****) ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 16` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 17` ```val [prem] = goal OrderType.thy "j le i ==> well_ord(j, Memrel(i))"; ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 18` ```by (rtac well_ordI 1); ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 19` ```by (rtac (wf_Memrel RS wf_imp_wf_on) 1); ``` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 20` ```by (resolve_tac [prem RS ltE] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 21` ```by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 22` ``` [ltI, prem] MRS lt_trans2 RS ltD]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 23` ```by (REPEAT (resolve_tac [ballI, Ord_linear] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 24` ```by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 25` ```qed "le_well_ord_Memrel"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 26` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 27` ```(*"Ord(i) ==> well_ord(i, Memrel(i))"*) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 28` ```bind_thm ("well_ord_Memrel", le_refl RS le_well_ord_Memrel); ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 29` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 30` ```(*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 31` ``` The smaller ordinal is an initial segment of the larger *) ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 32` ```goalw OrderType.thy [pred_def, lt_def] ``` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 33` ``` "!!i j. j pred(i, j, Memrel(i)) = j"; ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 34` ```by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 35` ```by (fast_tac (eq_cs addEs [Ord_trans]) 1); ``` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 36` ```qed "lt_pred_Memrel"; ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 37` 831 60d850cc5fe6 Added Krzysztof's theorem pred_Memrel lcp parents: 814 diff changeset ` 38` ```goalw OrderType.thy [pred_def,Memrel_def] ``` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 39` ``` "!!A x. x:A ==> pred(A, x, Memrel(A)) = A Int x"; ``` 831 60d850cc5fe6 Added Krzysztof's theorem pred_Memrel lcp parents: 814 diff changeset ` 40` ```by (fast_tac eq_cs 1); ``` 60d850cc5fe6 Added Krzysztof's theorem pred_Memrel lcp parents: 814 diff changeset ` 41` ```qed "pred_Memrel"; ``` 60d850cc5fe6 Added Krzysztof's theorem pred_Memrel lcp parents: 814 diff changeset ` 42` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 43` ```goal OrderType.thy ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 44` ``` "!!i. [| j R"; ``` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 45` ```by (forward_tac [lt_pred_Memrel] 1); ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 46` ```by (etac ltE 1); ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 47` ```by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 48` ``` assume_tac 3 THEN assume_tac 1); ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 49` ```by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1); ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 50` ```(*Combining the two simplifications causes looping*) ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 51` ```by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1); ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 52` ```by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type] addEs [Ord_trans]) 1); ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 53` ```qed "Ord_iso_implies_eq_lemma"; ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 54` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 55` ```(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*) ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 56` ```goal OrderType.thy ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 57` ``` "!!i. [| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) \ ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 58` ```\ |] ==> i=j"; ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 59` ```by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 60` ```by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1)); ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 61` ```qed "Ord_iso_implies_eq"; ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 62` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 63` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 64` ```(**** Ordermap and ordertype ****) ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 65` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 66` ```goalw OrderType.thy [ordermap_def,ordertype_def] ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 67` ``` "ordermap(A,r) : A -> ordertype(A,r)"; ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 68` ```by (rtac lam_type 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 69` ```by (rtac (lamI RS imageI) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 70` ```by (REPEAT (assume_tac 1)); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 467 diff changeset ` 71` ```qed "ordermap_type"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 72` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 73` ```(*** Unfolding of ordermap ***) ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 74` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 75` ```(*Useful for cardinality reasoning; see CardinalArith.ML*) ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 76` ```goalw OrderType.thy [ordermap_def, pred_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 77` ``` "!!r. [| wf[A](r); x:A |] ==> \ ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 78` ```\ ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"; ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 79` ```by (asm_simp_tac ZF_ss 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 80` ```by (etac (wfrec_on RS trans) 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 81` ```by (assume_tac 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 82` ```by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam, ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 83` ``` vimage_singleton_iff]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 467 diff changeset ` 84` ```qed "ordermap_eq_image"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 85` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 86` ```(*Useful for rewriting PROVIDED pred is not unfolded until later!*) ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 87` ```goal OrderType.thy ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 88` ``` "!!r. [| wf[A](r); x:A |] ==> \ ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 89` ```\ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"; ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 90` ```by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset, ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 91` ``` ordermap_type RS image_fun]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 467 diff changeset ` 92` ```qed "ordermap_pred_unfold"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 93` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 94` ```(*pred-unfolded version. NOT suitable for rewriting -- loops!*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 95` ```val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 96` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 97` ```(*** Showing that ordermap, ordertype yield ordinals ***) ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 98` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 99` ```fun ordermap_elim_tac i = ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 100` ``` EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i, ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 101` ``` assume_tac (i+1), ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 102` ``` assume_tac i]; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 103` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 104` ```goalw OrderType.thy [well_ord_def, tot_ord_def, part_ord_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 105` ``` "!!r. [| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 106` ```by (safe_tac ZF_cs); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 107` ```by (wf_on_ind_tac "x" [] 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 108` ```by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 109` ```by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 110` ```by (rewrite_goals_tac [pred_def,Transset_def]); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 111` ```by (fast_tac ZF_cs 2); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 112` ```by (safe_tac ZF_cs); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 113` ```by (ordermap_elim_tac 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 114` ```by (fast_tac (ZF_cs addSEs [trans_onD]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 467 diff changeset ` 115` ```qed "Ord_ordermap"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 116` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 117` ```goalw OrderType.thy [ordertype_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 118` ``` "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 119` ```by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 120` ```by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 121` ```by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 122` ```by (rewrite_goals_tac [Transset_def,well_ord_def]); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 123` ```by (safe_tac ZF_cs); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 124` ```by (ordermap_elim_tac 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 125` ```by (fast_tac ZF_cs 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 467 diff changeset ` 126` ```qed "Ord_ordertype"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 127` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 128` ```(*** ordermap preserves the orderings in both directions ***) ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 129` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 130` ```goal OrderType.thy ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 131` ``` "!!r. [| : r; wf[A](r); w: A; x: A |] ==> \ ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 132` ```\ ordermap(A,r)`w : ordermap(A,r)`x"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 133` ```by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 134` ```by (assume_tac 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 135` ```by (fast_tac ZF_cs 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 467 diff changeset ` 136` ```qed "ordermap_mono"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 137` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 138` ```(*linearity of r is crucial here*) ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 139` ```goalw OrderType.thy [well_ord_def, tot_ord_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 140` ``` "!!r. [| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \ ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 141` ```\ w: A; x: A |] ==> : r"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 142` ```by (safe_tac ZF_cs); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 143` ```by (linear_case_tac 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 144` ```by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1); ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 145` ```by (dtac ordermap_mono 1); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 146` ```by (REPEAT_SOME assume_tac); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 147` ```by (etac mem_asym 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 148` ```by (assume_tac 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 467 diff changeset ` 149` ```qed "converse_ordermap_mono"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 150` 803 4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result", lcp parents: 788 diff changeset ` 151` ```bind_thm ("ordermap_surj", ``` 4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result", lcp parents: 788 diff changeset ` 152` ``` rewrite_rule [symmetric ordertype_def] ``` 4c8333ab3eae changed useless "qed" calls for lemmas back to uses of "result", lcp parents: 788 diff changeset ` 153` ``` (ordermap_type RS surj_image)); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 154` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 155` ```goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 156` ``` "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 157` ```by (safe_tac ZF_cs); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 158` ```by (rtac ordermap_type 1); ``` 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 159` ```by (rtac ordermap_surj 2); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 160` ```by (linear_case_tac 1); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 161` ```(*The two cases yield similar contradictions*) ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 162` ```by (ALLGOALS (dtac ordermap_mono)); ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 163` ```by (REPEAT_SOME assume_tac); ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 164` ```by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl]))); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 467 diff changeset ` 165` ```qed "ordermap_bij"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 166` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 167` ```(*** Isomorphisms involving ordertype ***) ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 168` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 169` ```goalw OrderType.thy [ord_iso_def] ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 170` ``` "!!r. well_ord(A,r) ==> \ ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 171` ```\ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"; ``` ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 172` ```by (safe_tac ZF_cs); ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 173` ```by (rtac ordermap_bij 1); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 174` ```by (assume_tac 1); ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 175` ```by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2); ``` 437 435875e4b21d modifications for cardinal arithmetic lcp parents: 435 diff changeset ` 176` ```by (rewtac well_ord_def); ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 177` ```by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono, ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 178` ``` ordermap_type RS apply_type]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 467 diff changeset ` 179` ```qed "ordertype_ord_iso"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 180` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 181` ```goal OrderType.thy ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 182` ``` "!!f. [| f: ord_iso(A,r,B,s); well_ord(B,s) |] ==> \ ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 183` ```\ ordertype(A,r) = ordertype(B,s)"; ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 184` ```by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1); ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 185` ```by (resolve_tac [Ord_iso_implies_eq] 1 ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 186` ``` THEN REPEAT (eresolve_tac [Ord_ordertype] 1)); ``` 831 60d850cc5fe6 Added Krzysztof's theorem pred_Memrel lcp parents: 814 diff changeset ` 187` ```by (deepen_tac (ZF_cs addIs [ord_iso_trans, ord_iso_sym] ``` 60d850cc5fe6 Added Krzysztof's theorem pred_Memrel lcp parents: 814 diff changeset ` 188` ``` addSEs [ordertype_ord_iso]) 0 1); ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 189` ```qed "ordertype_eq"; ``` a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 190` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 191` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 192` ``` "!!A B. [| ordertype(A,r) = ordertype(B,s); \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 193` ```\ well_ord(A,r); well_ord(B,s) \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 194` ```\ |] ==> EX f. f: ord_iso(A,r,B,s)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 195` ```by (resolve_tac [exI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 196` ```by (resolve_tac [ordertype_ord_iso RS ord_iso_trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 197` ```by (assume_tac 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 198` ```by (eresolve_tac [ssubst] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 199` ```by (eresolve_tac [ordertype_ord_iso RS ord_iso_sym] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 200` ```qed "ordertype_eq_imp_ord_iso"; ``` 435 ca5356bd315a Addition of cardinals and order types, various tidying lcp parents: diff changeset ` 201` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 202` ```(*** Basic equalities for ordertype ***) ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 203` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 204` ```(*Ordertype of Memrel*) ``` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 205` ```goal OrderType.thy "!!i. j le i ==> ordertype(j,Memrel(i)) = j"; ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 206` ```by (resolve_tac [Ord_iso_implies_eq RS sym] 1); ``` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 207` ```by (eresolve_tac [ltE] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 208` ```by (REPEAT (ares_tac [le_well_ord_Memrel, Ord_ordertype] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 209` ```by (resolve_tac [ord_iso_trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 210` ```by (eresolve_tac [le_well_ord_Memrel RS ordertype_ord_iso] 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 211` ```by (resolve_tac [id_bij RS ord_isoI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 212` ```by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 213` ```by (fast_tac (ZF_cs addEs [ltE, Ord_in_Ord, Ord_trans]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 214` ```qed "le_ordertype_Memrel"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 215` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 216` ```(*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 217` ```bind_thm ("ordertype_Memrel", le_refl RS le_ordertype_Memrel); ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 218` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 219` ```goal OrderType.thy "ordertype(0,r) = 0"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 220` ```by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq RS trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 221` ```by (etac emptyE 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 222` ```by (resolve_tac [well_ord_0] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 223` ```by (resolve_tac [Ord_0 RS ordertype_Memrel] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 224` ```qed "ordertype_0"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 225` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 226` ```(*Ordertype of rvimage: [| f: bij(A,B); well_ord(B,s) |] ==> ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 227` ``` ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *) ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 228` ```bind_thm ("bij_ordertype_vimage", ord_iso_rvimage RS ordertype_eq); ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 229` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 230` ```(*** A fundamental unfolding law for ordertype. ***) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 231` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 232` ```(*Ordermap returns the same result if applied to an initial segment*) ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 233` ```goal OrderType.thy ``` 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 234` ``` "!!r. [| well_ord(A,r); y:A; z: pred(A,y,r) |] ==> \ ``` 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 235` ```\ ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"; ``` 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 236` ```by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1); ``` 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 237` ```by (wf_on_ind_tac "z" [] 1); ``` 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 238` ```by (safe_tac (ZF_cs addSEs [predE])); ``` 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 239` ```by (asm_simp_tac ``` 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 240` ``` (ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1); ``` 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 241` ```(*combining these two simplifications LOOPS! *) ``` 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 242` ```by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1); ``` 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 243` ```by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1); ``` 807 3abd026e68a4 ran expandshort script lcp parents: 803 diff changeset ` 244` ```by (rtac (refl RSN (2,RepFun_cong)) 1); ``` 3abd026e68a4 ran expandshort script lcp parents: 803 diff changeset ` 245` ```by (dtac well_ord_is_trans_on 1); ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 246` ```by (fast_tac (eq_cs addSEs [trans_onD]) 1); ``` 760 f0200e91b272 added qed and qed_goal[w] clasohm parents: 467 diff changeset ` 247` ```qed "ordermap_pred_eq_ordermap"; ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 248` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 249` ```goalw OrderType.thy [ordertype_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 250` ``` "ordertype(A,r) = {ordermap(A,r)`y . y : A}"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 251` ```by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 252` ```qed "ordertype_unfold"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 253` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 254` ```(** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 255` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 256` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 257` ``` "!!r. [| well_ord(A,r); x:A |] ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 258` ```\ ordertype(pred(A,x,r),r) <= ordertype(A,r)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 259` ```by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 260` ``` pred_subset RSN (2, well_ord_subset)]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 261` ```by (fast_tac (ZF_cs addIs [ordermap_pred_eq_ordermap, RepFun_eqI] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 262` ``` addEs [predE]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 263` ```qed "ordertype_pred_subset"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 264` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 265` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 266` ``` "!!r. [| well_ord(A,r); x:A |] ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 267` ```\ ordertype(pred(A,x,r),r) < ordertype(A,r)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 268` ```by (resolve_tac [ordertype_pred_subset RS subset_imp_le RS leE] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 269` ```by (REPEAT (ares_tac [Ord_ordertype, well_ord_subset, pred_subset] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 270` ```by (eresolve_tac [sym RS ordertype_eq_imp_ord_iso RS exE] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 271` ```by (eresolve_tac [well_ord_iso_predE] 3); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 272` ```by (REPEAT (ares_tac [pred_subset, well_ord_subset] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 273` ```qed "ordertype_pred_lt"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 274` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 275` ```(*May rewrite with this -- provided no rules are supplied for proving that ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 276` ``` well_ord(pred(A,x,r), r) *) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 277` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 278` ``` "!!A r. well_ord(A,r) ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 279` ```\ ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 280` ```by (safe_tac (eq_cs addSIs [ordertype_pred_lt RS ltD])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 281` ```by (asm_full_simp_tac ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 282` ``` (ZF_ss addsimps [ordertype_def, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 283` ``` ordermap_bij RS bij_is_fun RS image_fun]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 284` ```by (eresolve_tac [RepFunE] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 285` ```by (asm_full_simp_tac ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 286` ``` (ZF_ss addsimps [well_ord_is_wf, ordermap_eq_image, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 287` ``` ordermap_type RS image_fun, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 288` ``` ordermap_pred_eq_ordermap, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 289` ``` pred_subset, subset_refl]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 290` ```by (eresolve_tac [RepFunI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 291` ```qed "ordertype_pred_unfold"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 292` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 293` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 294` ```(**** Alternative definition of ordinal ****) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 295` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 296` ```(*proof by Krzysztof Grabczewski*) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 297` ```goalw OrderType.thy [Ord_alt_def] "!!i. Ord(i) ==> Ord_alt(i)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 298` ```by (resolve_tac [conjI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 299` ```by (eresolve_tac [well_ord_Memrel] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 300` ```by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 301` ```by (fast_tac eq_cs 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 302` ```qed "Ord_is_Ord_alt"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 303` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 304` ```(*proof by lcp*) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 305` ```goalw OrderType.thy [Ord_alt_def, Ord_def, Transset_def, well_ord_def, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 306` ``` tot_ord_def, part_ord_def, trans_on_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 307` ``` "!!i. Ord_alt(i) ==> Ord(i)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 308` ```by (asm_full_simp_tac (ZF_ss addsimps [Memrel_iff, pred_Memrel]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 309` ```by (safe_tac ZF_cs); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 310` ```by (fast_tac (ZF_cs addSDs [equalityD1]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 311` ```by (subgoal_tac "xa: i" 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 312` ```by (fast_tac (ZF_cs addSDs [equalityD1]) 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 313` ```by (fast_tac (ZF_cs addSDs [equalityD1] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 314` ``` addSEs [bspec RS bspec RS bspec RS mp RS mp]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 315` ```qed "Ord_alt_is_Ord"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 316` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 317` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 318` ```(**** Ordinal Addition ****) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 319` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 320` ```(*** Order Type calculations for radd ***) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 321` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 322` ```(** Addition with 0 **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 323` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 324` ```goal OrderType.thy "(lam z:A+0. case(%x.x, %y.y, z)) : bij(A+0, A)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 325` ```by (res_inst_tac [("d", "Inl")] lam_bijective 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 326` ```by (safe_tac sum_cs); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 327` ```by (ALLGOALS (asm_simp_tac sum_ss)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 328` ```qed "bij_sum_0"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 329` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 330` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 331` ``` "!!A r. well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 332` ```by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 333` ```by (assume_tac 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 334` ```by (asm_simp_tac ZF_ss 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 335` ```by (REPEAT_FIRST (eresolve_tac [sumE, emptyE])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 336` ```by (asm_simp_tac (sum_ss addsimps [radd_Inl_iff, Memrel_iff]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 337` ```qed "ordertype_sum_0_eq"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 338` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 339` ```goal OrderType.thy "(lam z:0+A. case(%x.x, %y.y, z)) : bij(0+A, A)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 340` ```by (res_inst_tac [("d", "Inr")] lam_bijective 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 341` ```by (safe_tac sum_cs); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 342` ```by (ALLGOALS (asm_simp_tac sum_ss)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 343` ```qed "bij_0_sum"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 344` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 345` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 346` ``` "!!A r. well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 347` ```by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 348` ```by (assume_tac 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 349` ```by (asm_simp_tac ZF_ss 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 350` ```by (REPEAT_FIRST (eresolve_tac [sumE, emptyE])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 351` ```by (asm_simp_tac (sum_ss addsimps [radd_Inr_iff, Memrel_iff]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 352` ```qed "ordertype_0_sum_eq"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 353` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 354` ```(** Initial segments of radd. Statements by Grabczewski **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 355` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 356` ```(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 357` ```goalw OrderType.thy [pred_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 358` ``` "!!A B. a:A ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 359` ```\ (lam x:pred(A,a,r). Inl(x)) \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 360` ```\ : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 361` ```by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 362` ```by (safe_tac sum_cs); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 363` ```by (ALLGOALS ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 364` ``` (asm_full_simp_tac ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 365` ``` (sum_ss addsimps [radd_Inl_iff, radd_Inr_Inl_iff]))); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 366` ```qed "pred_Inl_bij"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 367` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 368` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 369` ``` "!!A B. [| a:A; well_ord(A,r) |] ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 370` ```\ ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) = \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 371` ```\ ordertype(pred(A,a,r), r)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 372` ```by (resolve_tac [pred_Inl_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 373` ```by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_subset])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 374` ```by (asm_full_simp_tac (ZF_ss addsimps [radd_Inl_iff, pred_def]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 375` ```qed "ordertype_pred_Inl_eq"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 376` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 377` ```goalw OrderType.thy [pred_def, id_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 378` ``` "!!A B. b:B ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 379` ```\ id(A+pred(B,b,s)) \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 380` ```\ : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 381` ```by (res_inst_tac [("d", "%z.z")] lam_bijective 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 382` ```by (safe_tac sum_cs); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 383` ```by (ALLGOALS (asm_full_simp_tac radd_ss)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 384` ```qed "pred_Inr_bij"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 385` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 386` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 387` ``` "!!A B. [| b:B; well_ord(A,r); well_ord(B,s) |] ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 388` ```\ ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 389` ```\ ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 390` ```by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 391` ```by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 392` ```by (asm_full_simp_tac (ZF_ss addsimps [pred_def, id_def]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 393` ```by (REPEAT_FIRST (eresolve_tac [sumE])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 394` ```by (ALLGOALS (asm_simp_tac radd_ss)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 395` ```qed "ordertype_pred_Inr_eq"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 396` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 397` ```(*** Basic laws for ordinal addition ***) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 398` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 399` ```goalw OrderType.thy [oadd_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 400` ``` "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i++j)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 401` ```by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 402` ```qed "Ord_oadd"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 403` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 404` ```(** Ordinal addition with zero **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 405` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 406` ```goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> i++0 = i"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 407` ```by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_sum_0_eq, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 408` ``` ordertype_Memrel, well_ord_Memrel]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 409` ```qed "oadd_0"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 410` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 411` ```goalw OrderType.thy [oadd_def] "!!i. Ord(i) ==> 0++i = i"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 412` ```by (asm_simp_tac (ZF_ss addsimps [Memrel_0, ordertype_0_sum_eq, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 413` ``` ordertype_Memrel, well_ord_Memrel]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 414` ```qed "oadd_0_left"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 415` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 416` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 417` ```(*** Further properties of ordinal addition. Statements by Grabczewski, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 418` ``` proofs by lcp. ***) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 419` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 420` ```goalw OrderType.thy [oadd_def] "!!i j k. [| k k < i++j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 421` ```by (resolve_tac [ltE] 1 THEN assume_tac 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 422` ```by (resolve_tac [ltI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 423` ```by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 424` ```by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_unfold, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 425` ``` well_ord_radd, well_ord_Memrel]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 426` ```by (resolve_tac [RepFun_eqI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 427` ```by (eresolve_tac [InlI] 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 428` ```by (asm_simp_tac ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 429` ``` (ZF_ss addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 430` ``` lt_pred_Memrel, leI RS le_ordertype_Memrel]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 431` ```qed "lt_oadd1"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 432` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 433` ```goal OrderType.thy "!!i j. [| Ord(i); Ord(j) |] ==> i le i++j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 434` ```by (resolve_tac [all_lt_imp_le] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 435` ```by (REPEAT (ares_tac [Ord_oadd, lt_oadd1] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 436` ```qed "oadd_le_self"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 437` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 438` ```(** A couple of strange but necessary results! **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 439` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 440` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 441` ``` "!!A B. A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 442` ```by (resolve_tac [id_bij RS ord_isoI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 443` ```by (asm_simp_tac (ZF_ss addsimps [id_conv, Memrel_iff]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 444` ```by (fast_tac ZF_cs 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 445` ```qed "id_ord_iso_Memrel"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 446` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 447` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 448` ``` "!!k. [| well_ord(A,r); k \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 449` ```\ ordertype(A+k, radd(A, r, k, Memrel(j))) = \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 450` ```\ ordertype(A+k, radd(A, r, k, Memrel(k)))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 451` ```by (eresolve_tac [ltE] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 452` ```by (resolve_tac [ord_iso_refl RS sum_ord_iso_cong RS ordertype_eq] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 453` ```by (eresolve_tac [OrdmemD RS id_ord_iso_Memrel RS ord_iso_sym] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 454` ```by (REPEAT_FIRST (ares_tac [well_ord_radd, well_ord_Memrel])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 455` ```qed "ordertype_sum_Memrel"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 456` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 457` ```goalw OrderType.thy [oadd_def] "!!i j k. [| k i++k < i++j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 458` ```by (resolve_tac [ltE] 1 THEN assume_tac 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 459` ```by (resolve_tac [ordertype_pred_unfold RS equalityD2 RS subsetD RS ltI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 460` ```by (REPEAT_FIRST (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 461` ```by (resolve_tac [RepFun_eqI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 462` ```by (eresolve_tac [InrI] 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 463` ```by (asm_simp_tac ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 464` ``` (ZF_ss addsimps [ordertype_pred_Inr_eq, well_ord_Memrel, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 465` ``` lt_pred_Memrel, leI RS le_ordertype_Memrel, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 466` ``` ordertype_sum_Memrel]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 467` ```qed "oadd_lt_mono2"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 468` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 469` ```goal OrderType.thy "!!i j. [| i++j = i++k; Ord(i); Ord(j); Ord(k) |] ==> j=k"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 470` ```by (rtac Ord_linear_lt 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 471` ```by (REPEAT_SOME assume_tac); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 472` ```by (ALLGOALS ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 473` ``` (dresolve_tac [oadd_lt_mono2] THEN' assume_tac THEN' ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 474` ``` asm_full_simp_tac (ZF_ss addsimps [lt_not_refl]))); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 475` ```qed "oadd_inject"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 476` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 477` ```goalw OrderType.thy [oadd_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 478` ``` "!!i j k. [| k < i++j; Ord(i); Ord(j) |] ==> k (i++j)++k = i++(j++k)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 500` ```by (resolve_tac [ordertype_eq RS trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 501` ```by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 502` ``` sum_ord_iso_cong) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 503` ```by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 504` ```by (resolve_tac [sum_assoc_ord_iso RS ordertype_eq RS trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 505` ```by (rtac ([ord_iso_refl, ordertype_ord_iso] MRS sum_ord_iso_cong RS ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 506` ``` ordertype_eq) 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 507` ```by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 508` ```qed "oadd_assoc"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 509` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 510` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 511` ``` "!!i j. [| Ord(i); Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 512` ```by (rtac (subsetI RS equalityI) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 513` ```by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 514` ```by (REPEAT (ares_tac [Ord_oadd] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 515` ```by (fast_tac (ZF_cs addSEs [ltE]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 516` ```by (fast_tac ZF_cs 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 517` ```by (safe_tac ZF_cs); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 518` ```by (ALLGOALS ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 519` ``` (asm_full_simp_tac (ZF_ss addsimps [Ord_mem_iff_lt, Ord_oadd]))); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 520` ```by (fast_tac (ZF_cs addIs [lt_oadd1]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 521` ```by (fast_tac (ZF_cs addIs [oadd_lt_mono2]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 522` ```qed "oadd_unfold"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 523` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 524` ```goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 525` ```by (asm_simp_tac (ZF_ss addsimps [oadd_unfold, Ord_1, oadd_0]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 526` ```by (fast_tac eq_cs 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 527` ```qed "oadd_1"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 528` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 529` ```goal OrderType.thy ``` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 530` ``` "!!i. [| Ord(i); Ord(j) |] ==> i++succ(j) = succ(i++j)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 531` ```by (asm_simp_tac ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 532` ``` (ZF_ss addsimps [oadd_1 RS sym, Ord_oadd, oadd_assoc, Ord_1]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 533` ```qed "oadd_succ"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 534` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 535` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 536` ```(** Ordinal addition with limit ordinals **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 537` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 538` ```val prems = goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 539` ``` "[| Ord(i); !!x. x:A ==> Ord(j(x)); a:A |] ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 540` ```\ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 541` ```by (fast_tac (eq_cs addIs (prems @ [ltI, Ord_UN, Ord_oadd, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 542` ``` lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD]) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 543` ``` addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 544` ```qed "oadd_UN"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 545` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 546` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 547` ``` "!!i j. [| Ord(i); Limit(j) |] ==> i++j = (UN k:j. i++k)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 548` ```by (forward_tac [Limit_has_0 RS ltD] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 549` ```by (asm_simp_tac (ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 550` ``` oadd_UN RS sym, Union_eq_UN RS sym, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 551` ``` Limit_Union_eq]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 552` ```qed "oadd_Limit"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 553` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 554` ```(** Order/monotonicity properties of ordinal addition **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 555` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 556` ```goal OrderType.thy "!!i j. [| Ord(i); Ord(j) |] ==> i le j++i"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 557` ```by (eres_inst_tac [("i","i")] trans_induct3 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 558` ```by (asm_simp_tac (ZF_ss addsimps [oadd_0, Ord_0_le]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 559` ```by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_leI]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 560` ```by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 561` ```by (resolve_tac [le_trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 562` ```by (resolve_tac [le_implies_UN_le_UN] 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 563` ```by (fast_tac ZF_cs 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 564` ```by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 565` ``` le_refl, Limit_is_Ord]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 566` ```qed "oadd_le_self2"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 567` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 568` ```goal OrderType.thy "!!i j k. [| k le j; Ord(i) |] ==> k++i le j++i"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 569` ```by (forward_tac [lt_Ord] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 570` ```by (forward_tac [le_Ord2] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 571` ```by (eresolve_tac [trans_induct3] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 572` ```by (asm_simp_tac (ZF_ss addsimps [oadd_0]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 573` ```by (asm_simp_tac (ZF_ss addsimps [oadd_succ, succ_le_iff]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 574` ```by (asm_simp_tac (ZF_ss addsimps [oadd_Limit]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 575` ```by (resolve_tac [le_implies_UN_le_UN] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 576` ```by (fast_tac ZF_cs 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 577` ```qed "oadd_le_mono1"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 578` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 579` ```goal OrderType.thy "!!i j. [| i' le i; j' i'++j' < i++j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 580` ```by (resolve_tac [lt_trans1] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 581` ```by (REPEAT (eresolve_tac [asm_rl, oadd_le_mono1, oadd_lt_mono2, ltE, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 582` ``` Ord_succD] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 583` ```qed "oadd_lt_mono"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 584` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 585` ```goal OrderType.thy "!!i j. [| i' le i; j' le j |] ==> i'++j' le i++j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 586` ```by (asm_simp_tac (ZF_ss addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 587` ```qed "oadd_le_mono"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 588` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 589` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 590` ```(** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)). ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 591` ``` Probably simpler to define the difference recursively! ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 592` ```**) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 593` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 594` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 595` ``` "!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 596` ```by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 597` ```by (fast_tac (sum_cs addSIs [if_type]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 598` ```by (fast_tac (ZF_cs addSIs [case_type]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 599` ```by (eresolve_tac [sumE] 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 600` ```by (ALLGOALS (asm_simp_tac (sum_ss setloop split_tac [expand_if]))); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 601` ```qed "bij_sum_Diff"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 602` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 603` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 604` ``` "!!i j. i le j ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 605` ```\ ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) = \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 606` ```\ ordertype(j, Memrel(j))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 607` ```by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 608` ```by (resolve_tac [bij_sum_Diff RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 609` ```by (eresolve_tac [well_ord_Memrel] 3); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 610` ```by (assume_tac 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 611` ```by (asm_simp_tac ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 612` ``` (radd_ss setloop split_tac [expand_if] addsimps [Memrel_iff]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 613` ```by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 614` ```by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 615` ```by (asm_simp_tac (ZF_ss addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 616` ```by (fast_tac (ZF_cs addEs [lt_trans2, lt_trans]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 617` ```qed "ordertype_sum_Diff"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 618` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 619` ```goalw OrderType.thy [oadd_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 620` ``` "!!i j. i le j ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 621` ```\ i ++ ordertype(j-i, Memrel(j)) = \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 622` ```\ ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 623` ```by (safe_tac (ZF_cs addSDs [le_subset_iff RS iffD1])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 624` ```by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 625` ```by (eresolve_tac [id_ord_iso_Memrel] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 626` ```by (resolve_tac [ordertype_ord_iso RS ord_iso_sym] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 627` ```by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel RS well_ord_subset, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 628` ``` Diff_subset] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 629` ```qed "oadd_ordertype_Diff"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 630` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 631` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 632` ``` "!!i j. i le j ==> i ++ ordertype(j-i, Memrel(j)) = j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 633` ```by (asm_simp_tac (ZF_ss addsimps [oadd_ordertype_Diff, ordertype_sum_Diff, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 634` ``` ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 635` ```qed "oadd_inverse"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 636` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 637` ```(*By oadd_inject, the difference between i and j is unique.*) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 638` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 639` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 640` ```(**** Ordinal Multiplication ****) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 641` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 642` ```goalw OrderType.thy [omult_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 643` ``` "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i**j)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 644` ```by (REPEAT (ares_tac [Ord_ordertype, well_ord_rmult, well_ord_Memrel] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 645` ```qed "Ord_omult"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 646` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 647` ```(*** A useful unfolding law ***) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 648` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 649` ```goalw OrderType.thy [pred_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 650` ``` "!!A B. [| a:A; b:B |] ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 651` ```\ pred(A*B, , rmult(A,r,B,s)) = \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 652` ```\ pred(A,a,r)*B Un ({a} * pred(B,b,s))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 653` ```by (safe_tac eq_cs); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 654` ```by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [rmult_iff]))); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 655` ```by (ALLGOALS (fast_tac ZF_cs)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 656` ```qed "pred_Pair_eq"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 657` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 658` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 659` ``` "!!A B. [| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 660` ```\ ordertype(pred(A*B, , rmult(A,r,B,s)), rmult(A,r,B,s)) = \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 661` ```\ ordertype(pred(A,a,r)*B + pred(B,b,s), \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 662` ```\ radd(A*B, rmult(A,r,B,s), B, s))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 663` ```by (asm_simp_tac (ZF_ss addsimps [pred_Pair_eq]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 664` ```by (resolve_tac [ordertype_eq RS sym] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 665` ```by (resolve_tac [prod_sum_singleton_ord_iso] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 666` ```by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 667` ```by (fast_tac (ZF_cs addSEs [predE]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 668` ```qed "ordertype_pred_Pair_eq"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 669` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 670` ```goalw OrderType.thy [oadd_def, omult_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 671` ``` "!!i j. [| i' \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 672` ```\ ordertype(pred(i*j, , rmult(i,Memrel(i),j,Memrel(j))), \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 673` ```\ rmult(i,Memrel(i),j,Memrel(j))) = \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 674` ```\ j**i' ++ j'"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 675` ```by (asm_simp_tac (ZF_ss addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, ltD, lt_Ord2, well_ord_Memrel]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 676` ```by (resolve_tac [trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 677` ```by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 678` ```by (resolve_tac [ord_iso_refl] 3); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 679` ```by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 680` ```by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 681` ```by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 682` ``` Ord_ordertype])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 683` ```by (ALLGOALS ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 684` ``` (asm_simp_tac (radd_ss addsimps [rmult_iff, id_conv, Memrel_iff]))); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 685` ```by (safe_tac ZF_cs); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 686` ```by (ALLGOALS (fast_tac (ZF_cs addEs [Ord_trans]))); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 687` ```qed "ordertype_pred_Pair_lemma"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 688` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 689` ```goalw OrderType.thy [omult_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 690` ``` "!!i j. [| Ord(i); Ord(j); k \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 691` ```\ EX j' i'. k = j**i' ++ j' & j' j**i' ++ j' < j**i"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 702` ```by (resolve_tac [ltI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 703` ```by (asm_full_simp_tac ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 704` ``` (ZF_ss addsimps [ordertype_pred_unfold, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 705` ``` well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 706` ```by (resolve_tac [RepFun_eqI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 707` ```by (fast_tac (ZF_cs addSEs [ltE]) 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 708` ```by (asm_simp_tac ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 709` ``` (ZF_ss addsimps [ordertype_pred_Pair_lemma, ltI, symmetric omult_def]) 1); ``` 814 a32b420c33d4 Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma, lcp parents: 807 diff changeset ` 710` ```by (asm_simp_tac ``` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 711` ``` (ZF_ss addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 712` ``` lt_Ord2]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 713` ```qed "omult_oadd_lt"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 714` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 715` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 716` ``` "!!i j. [| Ord(i); Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 717` ```by (rtac (subsetI RS equalityI) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 718` ```by (resolve_tac [lt_omult RS exE] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 719` ```by (eresolve_tac [ltI] 3); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 720` ```by (REPEAT (ares_tac [Ord_omult] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 721` ```by (fast_tac (ZF_cs addSEs [ltE]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 722` ```by (fast_tac (ZF_cs addIs [omult_oadd_lt RS ltD, ltI]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 723` ```qed "omult_unfold"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 724` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 725` ```(*** Basic laws for ordinal multiplication ***) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 726` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 727` ```(** Ordinal multiplication by zero **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 728` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 729` ```goalw OrderType.thy [omult_def] "i**0 = 0"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 730` ```by (asm_simp_tac (ZF_ss addsimps [ordertype_0]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 731` ```qed "omult_0"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 732` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 733` ```goalw OrderType.thy [omult_def] "0**i = 0"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 734` ```by (asm_simp_tac (ZF_ss addsimps [ordertype_0]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 735` ```qed "omult_0_left"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 736` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 737` ```(** Ordinal multiplication by 1 **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 738` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 739` ```goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> i**1 = i"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 740` ```by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 741` ```by (res_inst_tac [("c", "snd"), ("d", "%z.<0,z>")] lam_bijective 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 742` ```by (REPEAT_FIRST (eresolve_tac [snd_type, SigmaE, succE, emptyE, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 743` ``` well_ord_Memrel, ordertype_Memrel])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 744` ```by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff]))); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 745` ```qed "omult_1"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 746` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 747` ```goalw OrderType.thy [omult_def] "!!i. Ord(i) ==> 1**i = i"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 748` ```by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 749` ```by (res_inst_tac [("c", "fst"), ("d", "%z.")] lam_bijective 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 750` ```by (REPEAT_FIRST (eresolve_tac [fst_type, SigmaE, succE, emptyE, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 751` ``` well_ord_Memrel, ordertype_Memrel])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 752` ```by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [rmult_iff, Memrel_iff]))); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 753` ```qed "omult_1_left"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 754` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 755` ```(** Distributive law for ordinal multiplication and addition **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 756` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 757` ```goalw OrderType.thy [omult_def, oadd_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 758` ``` "!!i. [| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 759` ```by (resolve_tac [ordertype_eq RS trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 760` ```by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 761` ``` prod_ord_iso_cong) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 762` ```by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 763` ``` Ord_ordertype] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 764` ```by (rtac (sum_prod_distrib_ord_iso RS ordertype_eq RS trans) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 765` ```by (rtac ordertype_eq 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 766` ```by (rtac ([ordertype_ord_iso, ordertype_ord_iso] MRS sum_ord_iso_cong) 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 767` ```by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 768` ``` Ord_ordertype] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 769` ```qed "oadd_omult_distrib"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 770` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 771` ```goal OrderType.thy "!!i. [| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 772` ```by (asm_simp_tac ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 773` ``` (ZF_ss addsimps [oadd_1 RS sym, omult_1, oadd_omult_distrib, Ord_1]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 774` ```qed "omult_succ"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 775` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 776` ```(** Associative law **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 777` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 778` ```goalw OrderType.thy [omult_def] ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 779` ``` "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> (i**j)**k = i**(j**k)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 780` ```by (resolve_tac [ordertype_eq RS trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 781` ```by (rtac ([ord_iso_refl, ordertype_ord_iso RS ord_iso_sym] MRS ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 782` ``` prod_ord_iso_cong) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 783` ```by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 784` ```by (resolve_tac [prod_assoc_ord_iso RS ord_iso_sym RS ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 785` ``` ordertype_eq RS trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 786` ```by (rtac ([ordertype_ord_iso, ord_iso_refl] MRS prod_ord_iso_cong RS ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 787` ``` ordertype_eq) 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 788` ```by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Ord_ordertype] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 789` ```qed "omult_assoc"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 790` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 791` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 792` ```(** Ordinal multiplication with limit ordinals **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 793` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 794` ```val prems = goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 795` ``` "[| Ord(i); !!x. x:A ==> Ord(j(x)) |] ==> \ ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 796` ```\ i ** (UN x:A. j(x)) = (UN x:A. i**j(x))"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 797` ```by (asm_simp_tac (ZF_ss addsimps (prems@[Ord_UN, omult_unfold])) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 798` ```by (fast_tac eq_cs 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 799` ```qed "omult_UN"; ``` 467 92868dab2939 new cardinal arithmetic developments lcp parents: 437 diff changeset ` 800` 849 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 801` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 802` ``` "!!i j. [| Ord(i); Limit(j) |] ==> i**j = (UN k:j. i**k)"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 803` ```by (asm_simp_tac ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 804` ``` (ZF_ss addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 805` ``` Union_eq_UN RS sym, Limit_Union_eq]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 806` ```qed "omult_Limit"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 807` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 808` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 809` ```(*** Ordering/monotonicity properties of ordinal multiplication ***) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 810` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 811` ```(*As a special case we have "[| 0 0 < i**j" *) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 812` ```goal OrderType.thy "!!i j. [| k k < i**j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 813` ```by (safe_tac (ZF_cs addSEs [ltE] addSIs [ltI, Ord_omult])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 814` ```by (asm_simp_tac (ZF_ss addsimps [omult_unfold]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 815` ```by (REPEAT (eresolve_tac [UN_I] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 816` ```by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0_left]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 817` ```qed "lt_omult1"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 818` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 819` ```goal OrderType.thy "!!i j. [| Ord(i); 0 i le i**j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 820` ```by (resolve_tac [all_lt_imp_le] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 821` ```by (REPEAT (ares_tac [Ord_omult, lt_omult1, lt_Ord2] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 822` ```qed "omult_le_self"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 823` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 824` ```goal OrderType.thy "!!i j k. [| k le j; Ord(i) |] ==> k**i le j**i"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 825` ```by (forward_tac [lt_Ord] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 826` ```by (forward_tac [le_Ord2] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 827` ```by (eresolve_tac [trans_induct3] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 828` ```by (asm_simp_tac (ZF_ss addsimps [omult_0, le_refl, Ord_0]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 829` ```by (asm_simp_tac (ZF_ss addsimps [omult_succ, oadd_le_mono]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 830` ```by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 831` ```by (resolve_tac [le_implies_UN_le_UN] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 832` ```by (fast_tac ZF_cs 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 833` ```qed "omult_le_mono1"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 834` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 835` ```goal OrderType.thy "!!i j k. [| k i**k < i**j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 836` ```by (resolve_tac [ltI] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 837` ```by (asm_simp_tac (ZF_ss addsimps [omult_unfold, lt_Ord2]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 838` ```by (safe_tac (ZF_cs addSEs [ltE] addSIs [Ord_omult])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 839` ```by (REPEAT (eresolve_tac [UN_I] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 840` ```by (asm_simp_tac (ZF_ss addsimps [omult_0, oadd_0, Ord_omult]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 841` ```qed "omult_lt_mono2"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 842` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 843` ```goal OrderType.thy "!!i j k. [| k le j; Ord(i) |] ==> i**k le i**j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 844` ```by (resolve_tac [subset_imp_le] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 845` ```by (safe_tac (ZF_cs addSEs [ltE, make_elim Ord_succD] addSIs [Ord_omult])); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 846` ```by (asm_full_simp_tac (ZF_ss addsimps [omult_unfold]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 847` ```by (safe_tac ZF_cs); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 848` ```by (eresolve_tac [UN_I] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 849` ```by (deepen_tac (ZF_cs addEs [Ord_trans]) 0 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 850` ```qed "omult_le_mono2"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 851` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 852` ```goal OrderType.thy "!!i j. [| i' le i; j' le j |] ==> i'**j' le i**j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 853` ```by (resolve_tac [le_trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 854` ```by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_le_mono2, ltE, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 855` ``` Ord_succD] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 856` ```qed "omult_le_mono"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 857` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 858` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 859` ``` "!!i j. [| i' le i; j' i'**j' < i**j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 860` ```by (resolve_tac [lt_trans1] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 861` ```by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_lt_mono2, ltE, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 862` ``` Ord_succD] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 863` ```qed "omult_lt_mono"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 864` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 865` ```goal OrderType.thy ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 866` ``` "!!i j. [| i' le i; j' le j |] ==> i'++j' le i++j"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 867` ```by (asm_simp_tac (ZF_ss addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 868` ```qed "oadd_le_mono"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 869` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 870` ```goal OrderType.thy "!!i j. [| Ord(i); 0 i le j**i"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 871` ```by (forward_tac [lt_Ord2] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 872` ```by (eres_inst_tac [("i","i")] trans_induct3 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 873` ```by (asm_simp_tac (ZF_ss addsimps [omult_0, Ord_0 RS le_refl]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 874` ```by (asm_simp_tac (ZF_ss addsimps [omult_succ, succ_le_iff]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 875` ```by (eresolve_tac [lt_trans1] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 876` ```by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 877` ``` rtac oadd_lt_mono2 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 878` ```by (REPEAT (ares_tac [Ord_omult] 1)); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 879` ```by (asm_simp_tac (ZF_ss addsimps [omult_Limit]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 880` ```by (resolve_tac [le_trans] 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 881` ```by (resolve_tac [le_implies_UN_le_UN] 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 882` ```by (fast_tac ZF_cs 2); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 883` ```by (asm_simp_tac (ZF_ss addsimps [Union_eq_UN RS sym, Limit_Union_eq, ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 884` ``` Limit_is_Ord RS le_refl]) 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 885` ```qed "omult_le_self2"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 886` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 887` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 888` ```(** Further properties of ordinal multiplication **) ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 889` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 890` ```goal OrderType.thy "!!i j. [| i**j = i**k; 0 j=k"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 891` ```by (rtac Ord_linear_lt 1); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 892` ```by (REPEAT_SOME assume_tac); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 893` ```by (ALLGOALS ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 894` ``` (dresolve_tac [omult_lt_mono2] THEN' assume_tac THEN' ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 895` ``` asm_full_simp_tac (ZF_ss addsimps [lt_not_refl]))); ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 896` ```qed "omult_inject"; ``` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 897` 013a16d3addb Proved equivalence of Ord and Ord_alt. Proved lcp parents: 831 diff changeset ` 898`