# HG changeset patch # User paulson # Date 1020959459 -7200 # Node ID be50e0b050b2e24f95dafab97d28e625604ffb2a # Parent 6e1decd8a7a96019fd07a90c2c6c39fa59a5b383 ordinal addition now coerces its arguments to ordinals diff -r 6e1decd8a7a9 -r be50e0b050b2 src/ZF/OrderType.ML --- a/src/ZF/OrderType.ML Wed May 08 13:01:40 2002 +0200 +++ b/src/ZF/OrderType.ML Thu May 09 17:50:59 2002 +0200 @@ -10,6 +10,13 @@ *) +(*??for Ordinal.ML*) +(*suitable for rewriting PROVIDED i has been fixed*) +Goal "[| j:i; Ord(i) |] ==> Ord(j)"; +by (blast_tac (claset() addIs [Ord_in_Ord]) 1); +qed "Ord_in_Ord'"; + + (**** Proofs needing the combination of Ordinal.thy and Order.thy ****) val [prem] = goal (the_context ()) "j le i ==> well_ord(j, Memrel(i))"; @@ -164,10 +171,10 @@ Goalw [well_ord_def, tot_ord_def, bij_def, inj_def] "well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"; -by (fast_tac (claset() addSIs [ordermap_type, ordermap_surj] - addEs [linearE] - addDs [ordermap_mono] - addss (simpset() addsimps [mem_not_refl])) 1); +by (force_tac (claset() addSIs [ordermap_type, ordermap_surj] + addEs [linearE] + addDs [ordermap_mono], + simpset() addsimps [mem_not_refl]) 1); qed "ordermap_bij"; (*** Isomorphisms involving ordertype ***) @@ -278,14 +285,12 @@ \ ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}"; by (rtac equalityI 1); by (safe_tac (claset() addSIs [ordertype_pred_lt RS ltD])); -by (fast_tac - (claset() addss - (simpset() addsimps [ordertype_def, +by (auto_tac (claset(), + simpset() addsimps [ordertype_def, well_ord_is_wf RS ordermap_eq_image, ordermap_type RS image_fun, ordermap_pred_eq_ordermap, - pred_subset])) - 1); + pred_subset])); qed "ordertype_pred_unfold"; @@ -370,49 +375,92 @@ \ ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \ \ ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"; by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); -by (fast_tac (claset() addss (simpset() addsimps [pred_def, id_def])) 2); +by (force_tac (claset(), simpset() addsimps [pred_def, id_def]) 2); by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset])); qed "ordertype_pred_Inr_eq"; + +(*** ordify: trivial coercion to an ordinal ***) + +Goal "Ord(ordify(x))"; +by (asm_full_simp_tac (simpset() addsimps [ordify_def]) 1); +qed "Ord_ordify"; +AddIffs [Ord_ordify]; +AddTCs [Ord_ordify]; + +(*Collapsing*) +Goal "ordify(ordify(x)) = ordify(x)"; +by (asm_full_simp_tac (simpset() addsimps [ordify_def]) 1); +qed "ordify_idem"; +Addsimps [ordify_idem]; + + (*** Basic laws for ordinal addition ***) -Goalw [oadd_def] - "[| Ord(i); Ord(j) |] ==> Ord(i++j)"; -by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 1)); +Goal "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))"; +by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Ord_ordertype, well_ord_radd, well_ord_Memrel]) 1); +qed "Ord_raw_oadd"; + +Goal "Ord(i++j)"; +by (asm_full_simp_tac (simpset() addsimps [oadd_def, Ord_raw_oadd]) 1); qed "Ord_oadd"; -Addsimps [Ord_oadd]; AddIs [Ord_oadd]; AddTCs [Ord_oadd]; +AddIffs [Ord_oadd]; AddTCs [Ord_oadd]; + (** Ordinal addition with zero **) -Goalw [oadd_def] "Ord(i) ==> i++0 = i"; -by (asm_simp_tac (simpset() addsimps [Memrel_0, ordertype_sum_0_eq, +Goal "Ord(i) ==> raw_oadd(i,0) = i"; +by (asm_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Memrel_0, ordertype_sum_0_eq, ordertype_Memrel, well_ord_Memrel]) 1); +qed "raw_oadd_0"; + +Goal "Ord(i) ==> i++0 = i"; +by (asm_simp_tac (simpset() addsimps [oadd_def, raw_oadd_0, ordify_def]) 1); qed "oadd_0"; +Addsimps [oadd_0]; + +Goal "Ord(i) ==> raw_oadd(0,i) = i"; +by (asm_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Memrel_0, ordertype_0_sum_eq, + ordertype_Memrel, well_ord_Memrel]) 1); +qed "raw_oadd_0_left"; -Goalw [oadd_def] "Ord(i) ==> 0++i = i"; -by (asm_simp_tac (simpset() addsimps [Memrel_0, ordertype_0_sum_eq, - ordertype_Memrel, well_ord_Memrel]) 1); +Goal "Ord(i) ==> 0++i = i"; +by (asm_simp_tac (simpset() addsimps [oadd_def, raw_oadd_0_left, ordify_def]) 1); qed "oadd_0_left"; +Addsimps [oadd_0_left]; -Addsimps [oadd_0, oadd_0_left]; + +Goal "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i) \ +\ else (if Ord(j) then j else 0))"; +by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, raw_oadd_0_left, raw_oadd_0]) 1); +qed "oadd_eq_if_raw_oadd"; + + +Goal "[|Ord(i); Ord(j)|] ==> raw_oadd(i,j) = i++j"; +by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def]) 1); +qed "raw_oadd_eq_oadd"; (*** Further properties of ordinal addition. Statements by Grabczewski, proofs by lcp. ***) -Goalw [oadd_def] "[| k k < i++j"; +(*Surely also provable by transfinite induction on j?*) +Goal "k k < i++j"; +by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, lt_Ord2, raw_oadd_0]) 1); +by (Clarify_tac 1); +by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1); by (rtac ltE 1 THEN assume_tac 1); by (rtac ltI 1); by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2)); -by (asm_simp_tac - (simpset() addsimps [ordertype_pred_unfold, +by (force_tac + (claset(), + simpset() addsimps [ordertype_pred_unfold, well_ord_radd, well_ord_Memrel, ordertype_pred_Inl_eq, - lt_pred_Memrel, leI RS le_ordertype_Memrel] - setloop rtac (InlI RSN (2,bexI))) 1); + lt_pred_Memrel, leI RS le_ordertype_Memrel]) 1); qed "lt_oadd1"; (*Thus also we obtain the rule i++j = k ==> i le k *) -Goal "[| Ord(i); Ord(j) |] ==> i le i++j"; +Goal "Ord(i) ==> i le i++j"; by (rtac all_lt_imp_le 1); by (REPEAT (ares_tac [Ord_oadd, lt_oadd1] 1)); qed "oadd_le_self"; @@ -434,7 +482,10 @@ by (REPEAT_FIRST (ares_tac [well_ord_radd, well_ord_Memrel])); qed "ordertype_sum_Memrel"; -Goalw [oadd_def] "[| k i++k < i++j"; +Goal "k i++k < i++j"; +by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, raw_oadd_0_left, lt_Ord, lt_Ord2]) 1); +by (Clarify_tac 1); +by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1); by (rtac ltE 1 THEN assume_tac 1); by (resolve_tac [ordertype_pred_unfold RS equalityD2 RS subsetD RS ltI] 1); by (REPEAT_FIRST (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel])); @@ -446,45 +497,52 @@ ordertype_sum_Memrel]) 1); qed "oadd_lt_mono2"; -Goal "[| i++j < i++k; Ord(i); Ord(j); Ord(k) |] ==> j j i++j < i++k <-> j i++j < i++k <-> j j=k"; +Goal "[| i++j = i++k; Ord(j); Ord(k) |] ==> j=k"; +by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd] addsplits [split_if_asm]) 1); +by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1); by (rtac Ord_linear_lt 1); by (REPEAT_SOME assume_tac); by (ALLGOALS - (fast_tac (claset() addDs [oadd_lt_mono2] - addss (simpset() addsimps [lt_not_refl])))); + (force_tac (claset() addDs [inst "i" "i" oadd_lt_mono2], + simpset() addsimps [lt_not_refl]))); qed "oadd_inject"; -Goalw [oadd_def] - "[| k < i++j; Ord(i); Ord(j) |] ==> k k (i++j)++k = i++(j++k)"; +Goal "(i++j)++k = i++(j++k)"; +by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd, Ord_raw_oadd, raw_oadd_0, raw_oadd_0_left]) 1); +by (Clarify_tac 1); +by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1); by (resolve_tac [ordertype_eq RS trans] 1); by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS sum_ord_iso_cong) 1); @@ -499,8 +557,8 @@ by (rtac (subsetI RS equalityI) 1); by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1); by (REPEAT (ares_tac [Ord_oadd] 1)); -by (fast_tac (claset() addIs [lt_oadd1, oadd_lt_mono2] - addss (simpset() addsimps [Ord_mem_iff_lt, Ord_oadd])) 3); +by (force_tac (claset() addIs [lt_oadd1, oadd_lt_mono2], + simpset() addsimps [Ord_mem_iff_lt]) 3); by (Blast_tac 2); by (blast_tac (claset() addSEs [ltE]) 1); qed "oadd_unfold"; @@ -510,10 +568,12 @@ by (Blast_tac 1); qed "oadd_1"; -Goal "[| Ord(i); Ord(j) |] ==> i++succ(j) = succ(i++j)"; - (*FOL_ss prevents looping*) -by (asm_simp_tac (FOL_ss delsimps [oadd_1] - addsimps [Ord_oadd, oadd_1 RS sym, oadd_assoc, Ord_1]) 1); +Goal "Ord(j) ==> i++succ(j) = succ(i++j)"; +by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1); +by (Clarify_tac 1); +by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1); +by (asm_simp_tac (simpset() + addsimps [inst "i" "j" oadd_1 RS sym, inst "i" "i++j" oadd_1 RS sym, oadd_assoc]) 1); qed "oadd_succ"; Addsimps [oadd_succ]; @@ -521,14 +581,14 @@ (** Ordinal addition with limit ordinals **) val prems = -Goal "[| Ord(i); !!x. x:A ==> Ord(j(x)); a:A |] ==> \ +Goal "[| !!x. x:A ==> Ord(j(x)); a:A |] ==> \ \ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"; by (blast_tac (claset() addIs prems @ [ltI, Ord_UN, Ord_oadd, lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD] addSEs [ltE] addSDs [ltI RS lt_oadd_disj]) 1); qed "oadd_UN"; -Goal "[| Ord(i); Limit(j) |] ==> i++j = (UN k:j. i++k)"; +Goal "Limit(j) ==> i++j = (UN k:j. i++k)"; by (forward_tac [Limit_has_0 RS ltD] 1); by (asm_simp_tac (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord, oadd_UN RS sym, Union_eq_UN RS sym, @@ -537,22 +597,26 @@ (** Order/monotonicity properties of ordinal addition **) -Goal "[| Ord(i); Ord(j) |] ==> i le j++i"; +Goal "Ord(i) ==> i le j++i"; by (eres_inst_tac [("i","i")] trans_induct3 1); by (asm_simp_tac (simpset() addsimps [Ord_0_le]) 1); by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_leI]) 1); by (asm_simp_tac (simpset() addsimps [oadd_Limit]) 1); by (rtac le_trans 1); by (rtac le_implies_UN_le_UN 2); -by (Blast_tac 2); +by (etac bspec 2); +by (assume_tac 2); by (asm_simp_tac (simpset() addsimps [Union_eq_UN RS sym, Limit_Union_eq, le_refl, Limit_is_Ord]) 1); qed "oadd_le_self2"; -Goal "[| k le j; Ord(i) |] ==> k++i le j++i"; +Goal "k le j ==> k++i le j++i"; by (ftac lt_Ord 1); by (ftac le_Ord2 1); -by (etac trans_induct3 1); +by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1); +by (Clarify_tac 1); +by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1); +by (eres_inst_tac [("i","i")] trans_induct3 1); by (Asm_simp_tac 1); by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_le_iff]) 1); by (asm_simp_tac (simpset() addsimps [oadd_Limit]) 1); @@ -571,10 +635,9 @@ addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1); qed "oadd_le_mono"; -Goal "[| Ord(i); Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"; +Goal "[| Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"; by (asm_simp_tac (simpset() delsimps [oadd_succ] - addsimps [oadd_lt_iff2, oadd_succ RS sym, - Ord_succ]) 1); + addsimps [oadd_lt_iff2, oadd_succ RS sym, Ord_succ]) 1); qed "oadd_le_iff2"; @@ -604,44 +667,46 @@ by (blast_tac (claset() addIs [lt_trans2, lt_trans]) 1); qed "ordertype_sum_Diff"; -Goalw [oadd_def, odiff_def] +Goalw [odiff_def] + "[| Ord(i); Ord(j) |] ==> Ord(i--j)"; +by (REPEAT (ares_tac [Ord_ordertype, well_ord_Memrel RS well_ord_subset, + Diff_subset] 1)); +qed "Ord_odiff"; +Addsimps [Ord_odiff]; AddTCs [Ord_odiff]; + + +Goal "i le j \ -\ ==> i ++ (j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"; +\ ==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"; +by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def, odiff_def]) 1); by (safe_tac (claset() addSDs [le_subset_iff RS iffD1])); by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1); by (etac id_ord_iso_Memrel 1); by (resolve_tac [ordertype_ord_iso RS ord_iso_sym] 1); by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel RS well_ord_subset, Diff_subset] 1)); -qed "oadd_ordertype_Diff"; +qed "raw_oadd_ordertype_Diff"; Goal "i le j ==> i ++ (j--i) = j"; -by (asm_simp_tac (simpset() addsimps [oadd_ordertype_Diff, ordertype_sum_Diff, +by (asm_simp_tac (simpset() addsimps [lt_Ord, le_Ord2, oadd_def, ordify_def, raw_oadd_ordertype_Diff, ordertype_sum_Diff, ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1); qed "oadd_odiff_inverse"; -Goalw [odiff_def] - "[| Ord(i); Ord(j) |] ==> Ord(i--j)"; -by (REPEAT (ares_tac [Ord_ordertype, well_ord_Memrel RS well_ord_subset, - Diff_subset] 1)); -qed "Ord_odiff"; - (*By oadd_inject, the difference between i and j is unique. Note that we get i++j = k ==> j = k--i. *) Goal "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j"; by (rtac oadd_inject 1); by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2)); -by (asm_simp_tac (simpset() addsimps [oadd_odiff_inverse, oadd_le_self]) 1); +by (blast_tac (claset() addIs [oadd_odiff_inverse, oadd_le_self]) 1); qed "odiff_oadd_inverse"; -val [i_lt_j, k_le_i] = goal (the_context ()) - "[| i i--k < j--k"; -by (rtac (k_le_i RS lt_Ord RSN (2,oadd_lt_cancel2)) 1); -by (simp_tac - (simpset() addsimps [i_lt_j, k_le_i, [k_le_i, leI] MRS le_trans, - oadd_odiff_inverse]) 1); -by (REPEAT (resolve_tac (Ord_odiff :: - ([i_lt_j, k_le_i] RL [lt_Ord, lt_Ord2])) 1)); +Goal "[| i i--k < j--k"; +by (res_inst_tac [("i","k")] oadd_lt_cancel2 1); +by (asm_full_simp_tac (simpset() addsimps [oadd_odiff_inverse]) 1); +by (stac oadd_odiff_inverse 1); +by (blast_tac (claset() addIs [le_trans, leI]) 1); +by (assume_tac 1); +by (asm_simp_tac (simpset() addsimps [lt_Ord, le_Ord2]) 1); qed "odiff_lt_mono2"; @@ -651,16 +716,14 @@ "[| Ord(i); Ord(j) |] ==> Ord(i**j)"; by (REPEAT (ares_tac [Ord_ordertype, well_ord_rmult, well_ord_Memrel] 1)); qed "Ord_omult"; +Addsimps [Ord_omult]; AddTCs [Ord_omult]; (*** A useful unfolding law ***) Goalw [pred_def] "[| a:A; b:B |] ==> pred(A*B, , rmult(A,r,B,s)) = \ \ pred(A,a,r)*B Un ({a} * pred(B,b,s))"; -by (rtac equalityI 1); -by Safe_tac; -by (ALLGOALS Asm_full_simp_tac); -by (ALLGOALS Blast_tac); +by (Blast_tac 1); qed "pred_Pair_eq"; Goal "[| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==> \ @@ -674,11 +737,11 @@ by (blast_tac (claset() addSEs [predE]) 1); qed "ordertype_pred_Pair_eq"; -Goalw [oadd_def, omult_def] +Goalw [raw_oadd_def, omult_def] "[| i' \ \ ordertype(pred(i*j, , rmult(i,Memrel(i),j,Memrel(j))), \ \ rmult(i,Memrel(i),j,Memrel(j))) = \ -\ j**i' ++ j'"; +\ raw_oadd (j**i', j')"; by (asm_simp_tac (simpset() addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, ltD, lt_Ord2, well_ord_Memrel]) 1); by (rtac trans 1); @@ -700,7 +763,8 @@ well_ord_rmult, well_ord_Memrel]) 1); by (safe_tac (claset() addSEs [ltE])); by (asm_simp_tac (simpset() addsimps [ordertype_pred_Pair_lemma, ltI, - symmetric omult_def]) 1); + symmetric omult_def, + inst "i" "i" Ord_in_Ord', inst "i" "j" Ord_in_Ord', raw_oadd_eq_oadd]) 1); by (blast_tac (claset() addIs [ltI]) 1); qed "lt_omult"; @@ -718,6 +782,8 @@ by (asm_simp_tac (simpset() addsimps [ordertype_pred_Pair_lemma, ltI, symmetric omult_def]) 1); +by (asm_simp_tac (simpset() addsimps [ + lt_Ord, lt_Ord2, raw_oadd_eq_oadd]) 1); qed "omult_oadd_lt"; Goal "[| Ord(i); Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})"; @@ -765,8 +831,9 @@ (** Distributive law for ordinal multiplication and addition **) -Goalw [omult_def, oadd_def] - "[| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"; +Goal "[| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"; +by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1); +by (asm_full_simp_tac (simpset() addsimps [omult_def, raw_oadd_def]) 1); by (resolve_tac [ordertype_eq RS trans] 1); by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS prod_ord_iso_cong) 1); @@ -780,9 +847,9 @@ qed "oadd_omult_distrib"; Goal "[| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i"; - (*FOL_ss prevents looping*) -by (asm_simp_tac (FOL_ss addsimps [oadd_1 RS sym, omult_1, oadd_omult_distrib, - Ord_1]) 1); +by (asm_simp_tac (simpset() + delsimps [oadd_succ] + addsimps [inst "i" "j" oadd_1 RS sym, oadd_omult_distrib]) 1); qed "omult_succ"; (** Associative law **) @@ -894,8 +961,7 @@ by (rtac Ord_linear_lt 1); by (REPEAT_SOME assume_tac); by (ALLGOALS - (best_tac (claset() addDs [omult_lt_mono2] - addss (simpset() addsimps [lt_not_refl])))); + (force_tac (claset() addDs [omult_lt_mono2], + simpset() addsimps [lt_not_refl]))); qed "omult_inject"; - diff -r 6e1decd8a7a9 -r be50e0b050b2 src/ZF/OrderType.thy --- a/src/ZF/OrderType.thy Wed May 08 13:01:40 2002 +0200 +++ b/src/ZF/OrderType.thy Thu May 09 17:50:59 2002 +0200 @@ -9,35 +9,38 @@ *) OrderType = OrderArith + OrdQuant + -consts +constdefs + ordermap :: [i,i]=>i - ordertype :: [i,i]=>i + "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))" - Ord_alt :: i => o - - "**" :: [i,i]=>i (infixl 70) - "++" :: [i,i]=>i (infixl 65) - "--" :: [i,i]=>i (infixl 65) - + ordertype :: [i,i]=>i + "ordertype(A,r) == ordermap(A,r)``A" -defs - ordermap_def - "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))" - - ordertype_def "ordertype(A,r) == ordermap(A,r)``A" + (*alternative definition of ordinal numbers*) + Ord_alt :: i => o + "Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))" - Ord_alt_def (*alternative definition of ordinal numbers*) - "Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))" - + (*coercion to ordinal: if not, just 0*) + ordify :: i=>i + "ordify(x) == if Ord(x) then x else 0" + (*ordinal multiplication*) - omult_def "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))" + omult :: [i,i]=>i (infixl "**" 70) + "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))" (*ordinal addition*) - oadd_def "i ++ j == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))" + raw_oadd :: [i,i]=>i + "raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))" + + oadd :: [i,i]=>i (infixl "++" 65) + "i ++ j == raw_oadd(ordify(i),ordify(j))" (*ordinal subtraction*) - odiff_def "i -- j == ordertype(i-j, Memrel(i))" + odiff :: [i,i]=>i (infixl "--" 65) + "i -- j == ordertype(i-j, Memrel(i))" + syntax (xsymbols) "op **" :: [i,i] => i (infixl "\\\\" 70)