--- a/src/ZF/OrderType.thy Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/OrderType.thy Tue Sep 27 16:51:35 2022 +0100
@@ -13,45 +13,45 @@
definition
ordermap :: "[i,i]=>i" where
- "ordermap(A,r) == \<lambda>x\<in>A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
+ "ordermap(A,r) \<equiv> \<lambda>x\<in>A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
definition
ordertype :: "[i,i]=>i" where
- "ordertype(A,r) == ordermap(A,r)``A"
+ "ordertype(A,r) \<equiv> ordermap(A,r)``A"
definition
(*alternative definition of ordinal numbers*)
Ord_alt :: "i => o" where
- "Ord_alt(X) == well_ord(X, Memrel(X)) & (\<forall>u\<in>X. u=pred(X, u, Memrel(X)))"
+ "Ord_alt(X) \<equiv> well_ord(X, Memrel(X)) & (\<forall>u\<in>X. u=pred(X, u, Memrel(X)))"
definition
(*coercion to ordinal: if not, just 0*)
ordify :: "i=>i" where
- "ordify(x) == if Ord(x) then x else 0"
+ "ordify(x) \<equiv> if Ord(x) then x else 0"
definition
(*ordinal multiplication*)
omult :: "[i,i]=>i" (infixl \<open>**\<close> 70) where
- "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
+ "i ** j \<equiv> ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
definition
(*ordinal addition*)
raw_oadd :: "[i,i]=>i" where
- "raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
+ "raw_oadd(i,j) \<equiv> ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
definition
oadd :: "[i,i]=>i" (infixl \<open>++\<close> 65) where
- "i ++ j == raw_oadd(ordify(i),ordify(j))"
+ "i ++ j \<equiv> raw_oadd(ordify(i),ordify(j))"
definition
(*ordinal subtraction*)
odiff :: "[i,i]=>i" (infixl \<open>--\<close> 65) where
- "i -- j == ordertype(i-j, Memrel(i))"
+ "i -- j \<equiv> ordertype(i-j, Memrel(i))"
subsection\<open>Proofs needing the combination of Ordinal.thy and Order.thy\<close>
-lemma le_well_ord_Memrel: "j \<le> i ==> well_ord(j, Memrel(i))"
+lemma le_well_ord_Memrel: "j \<le> i \<Longrightarrow> well_ord(j, Memrel(i))"
apply (rule well_ordI)
apply (rule wf_Memrel [THEN wf_imp_wf_on])
apply (simp add: ltD lt_Ord linear_def
@@ -60,23 +60,23 @@
apply (blast intro: Ord_in_Ord lt_Ord)+
done
-(*"Ord(i) ==> well_ord(i, Memrel(i))"*)
+(*"Ord(i) \<Longrightarrow> well_ord(i, Memrel(i))"*)
lemmas well_ord_Memrel = le_refl [THEN le_well_ord_Memrel]
(*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord
The smaller ordinal is an initial segment of the larger *)
lemma lt_pred_Memrel:
- "j<i ==> pred(i, j, Memrel(i)) = j"
+ "j<i \<Longrightarrow> pred(i, j, Memrel(i)) = j"
apply (simp add: pred_def lt_def)
apply (blast intro: Ord_trans)
done
lemma pred_Memrel:
- "x \<in> A ==> pred(A, x, Memrel(A)) = A \<inter> x"
+ "x \<in> A \<Longrightarrow> pred(A, x, Memrel(A)) = A \<inter> x"
by (unfold pred_def Memrel_def, blast)
lemma Ord_iso_implies_eq_lemma:
- "[| j<i; f \<in> ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R"
+ "\<lbrakk>j<i; f \<in> ord_iso(i,Memrel(i),j,Memrel(j))\<rbrakk> \<Longrightarrow> R"
apply (frule lt_pred_Memrel)
apply (erule ltE)
apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto)
@@ -88,8 +88,8 @@
(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*)
lemma Ord_iso_implies_eq:
- "[| Ord(i); Ord(j); f \<in> ord_iso(i,Memrel(i),j,Memrel(j)) |]
- ==> i=j"
+ "\<lbrakk>Ord(i); Ord(j); f \<in> ord_iso(i,Memrel(i),j,Memrel(j))\<rbrakk>
+ \<Longrightarrow> i=j"
apply (rule_tac i = i and j = j in Ord_linear_lt)
apply (blast intro: ord_iso_sym Ord_iso_implies_eq_lemma)+
done
@@ -108,8 +108,8 @@
(*Useful for cardinality reasoning; see CardinalArith.ML*)
lemma ordermap_eq_image:
- "[| wf[A](r); x \<in> A |]
- ==> ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"
+ "\<lbrakk>wf[A](r); x \<in> A\<rbrakk>
+ \<Longrightarrow> ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"
apply (unfold ordermap_def pred_def)
apply (simp (no_asm_simp))
apply (erule wfrec_on [THEN trans], assumption)
@@ -118,8 +118,8 @@
(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
lemma ordermap_pred_unfold:
- "[| wf[A](r); x \<in> A |]
- ==> ordermap(A,r) ` x = {ordermap(A,r)`y . y \<in> pred(A,x,r)}"
+ "\<lbrakk>wf[A](r); x \<in> A\<rbrakk>
+ \<Longrightarrow> ordermap(A,r) ` x = {ordermap(A,r)`y . y \<in> pred(A,x,r)}"
by (simp add: ordermap_eq_image pred_subset ordermap_type [THEN image_fun])
(*pred-unfolded version. NOT suitable for rewriting -- loops!*)
@@ -127,8 +127,8 @@
(*The theorem above is
-[| wf[A](r); x \<in> A |]
-==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y \<in> A . <y,x> \<in> r}}
+\<lbrakk>wf[A](r); x \<in> A\<rbrakk>
+\<Longrightarrow> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y \<in> A . <y,x> \<in> r}}
NOTE: the definition of ordermap used here delivers ordinals only if r is
transitive. If r is the predecessor relation on the naturals then
@@ -144,7 +144,7 @@
subsubsection\<open>Showing that ordermap, ordertype yield ordinals\<close>
lemma Ord_ordermap:
- "[| well_ord(A,r); x \<in> A |] ==> Ord(ordermap(A,r) ` x)"
+ "\<lbrakk>well_ord(A,r); x \<in> A\<rbrakk> \<Longrightarrow> Ord(ordermap(A,r) ` x)"
apply (unfold well_ord_def tot_ord_def part_ord_def, safe)
apply (rule_tac a=x in wf_on_induct, assumption+)
apply (simp (no_asm_simp) add: ordermap_pred_unfold)
@@ -155,7 +155,7 @@
done
lemma Ord_ordertype:
- "well_ord(A,r) ==> Ord(ordertype(A,r))"
+ "well_ord(A,r) \<Longrightarrow> Ord(ordertype(A,r))"
apply (unfold ordertype_def)
apply (subst image_fun [OF ordermap_type subset_refl])
apply (rule OrdI [OF _ Ord_is_Transset])
@@ -169,15 +169,15 @@
subsubsection\<open>ordermap preserves the orderings in both directions\<close>
lemma ordermap_mono:
- "[| <w,x>: r; wf[A](r); w \<in> A; x \<in> A |]
- ==> ordermap(A,r)`w \<in> ordermap(A,r)`x"
+ "\<lbrakk><w,x>: r; wf[A](r); w \<in> A; x \<in> A\<rbrakk>
+ \<Longrightarrow> ordermap(A,r)`w \<in> ordermap(A,r)`x"
apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption, blast)
done
(*linearity of r is crucial here*)
lemma converse_ordermap_mono:
- "[| ordermap(A,r)`w \<in> ordermap(A,r)`x; well_ord(A,r); w \<in> A; x \<in> A |]
- ==> <w,x>: r"
+ "\<lbrakk>ordermap(A,r)`w \<in> ordermap(A,r)`x; well_ord(A,r); w \<in> A; x \<in> A\<rbrakk>
+ \<Longrightarrow> <w,x>: r"
apply (unfold well_ord_def tot_ord_def, safe)
apply (erule_tac x=w and y=x in linearE, assumption+)
apply (blast elim!: mem_not_refl [THEN notE])
@@ -189,7 +189,7 @@
by (rule surj_image) (rule ordermap_type)
lemma ordermap_bij:
- "well_ord(A,r) ==> ordermap(A,r) \<in> bij(A, ordertype(A,r))"
+ "well_ord(A,r) \<Longrightarrow> ordermap(A,r) \<in> bij(A, ordertype(A,r))"
apply (unfold well_ord_def tot_ord_def bij_def inj_def)
apply (force intro!: ordermap_type ordermap_surj
elim: linearE dest: ordermap_mono
@@ -200,7 +200,7 @@
lemma ordertype_ord_iso:
"well_ord(A,r)
- ==> ordermap(A,r) \<in> ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"
+ \<Longrightarrow> ordermap(A,r) \<in> ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"
apply (unfold ord_iso_def)
apply (safe elim!: well_ord_is_wf
intro!: ordermap_type [THEN apply_type] ordermap_mono ordermap_bij)
@@ -208,16 +208,16 @@
done
lemma ordertype_eq:
- "[| f \<in> ord_iso(A,r,B,s); well_ord(B,s) |]
- ==> ordertype(A,r) = ordertype(B,s)"
+ "\<lbrakk>f \<in> ord_iso(A,r,B,s); well_ord(B,s)\<rbrakk>
+ \<Longrightarrow> ordertype(A,r) = ordertype(B,s)"
apply (frule well_ord_ord_iso, assumption)
apply (rule Ord_iso_implies_eq, (erule Ord_ordertype)+)
apply (blast intro: ord_iso_trans ord_iso_sym ordertype_ord_iso)
done
lemma ordertype_eq_imp_ord_iso:
- "[| ordertype(A,r) = ordertype(B,s); well_ord(A,r); well_ord(B,s) |]
- ==> \<exists>f. f \<in> ord_iso(A,r,B,s)"
+ "\<lbrakk>ordertype(A,r) = ordertype(B,s); well_ord(A,r); well_ord(B,s)\<rbrakk>
+ \<Longrightarrow> \<exists>f. f \<in> ord_iso(A,r,B,s)"
apply (rule exI)
apply (rule ordertype_ord_iso [THEN ord_iso_trans], assumption)
apply (erule ssubst)
@@ -227,7 +227,7 @@
subsubsection\<open>Basic equalities for ordertype\<close>
(*Ordertype of Memrel*)
-lemma le_ordertype_Memrel: "j \<le> i ==> ordertype(j,Memrel(i)) = j"
+lemma le_ordertype_Memrel: "j \<le> i \<Longrightarrow> ordertype(j,Memrel(i)) = j"
apply (rule Ord_iso_implies_eq [symmetric])
apply (erule ltE, assumption)
apply (blast intro: le_well_ord_Memrel Ord_ordertype)
@@ -238,7 +238,7 @@
apply (fast elim: ltE Ord_in_Ord Ord_trans)
done
-(*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*)
+(*"Ord(i) \<Longrightarrow> ordertype(i, Memrel(i)) = i"*)
lemmas ordertype_Memrel = le_refl [THEN le_ordertype_Memrel]
lemma ordertype_0 [simp]: "ordertype(0,r) = 0"
@@ -248,7 +248,7 @@
apply (rule Ord_0 [THEN ordertype_Memrel])
done
-(*Ordertype of rvimage: [| f \<in> bij(A,B); well_ord(B,s) |] ==>
+(*Ordertype of rvimage: \<lbrakk>f \<in> bij(A,B); well_ord(B,s)\<rbrakk> \<Longrightarrow>
ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)
lemmas bij_ordertype_vimage = ord_iso_rvimage [THEN ordertype_eq]
@@ -256,8 +256,8 @@
(*Ordermap returns the same result if applied to an initial segment*)
lemma ordermap_pred_eq_ordermap:
- "[| well_ord(A,r); y \<in> A; z \<in> pred(A,y,r) |]
- ==> ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"
+ "\<lbrakk>well_ord(A,r); y \<in> A; z \<in> pred(A,y,r)\<rbrakk>
+ \<Longrightarrow> ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"
apply (frule wf_on_subset_A [OF well_ord_is_wf pred_subset])
apply (rule_tac a=z in wf_on_induct, assumption+)
apply (safe elim!: predE)
@@ -278,15 +278,15 @@
text\<open>Theorems by Krzysztof Grabczewski; proofs simplified by lcp\<close>
-lemma ordertype_pred_subset: "[| well_ord(A,r); x \<in> A |] ==>
+lemma ordertype_pred_subset: "\<lbrakk>well_ord(A,r); x \<in> A\<rbrakk> \<Longrightarrow>
ordertype(pred(A,x,r),r) \<subseteq> ordertype(A,r)"
apply (simp add: ordertype_unfold well_ord_subset [OF _ pred_subset])
apply (fast intro: ordermap_pred_eq_ordermap elim: predE)
done
lemma ordertype_pred_lt:
- "[| well_ord(A,r); x \<in> A |]
- ==> ordertype(pred(A,x,r),r) < ordertype(A,r)"
+ "\<lbrakk>well_ord(A,r); x \<in> A\<rbrakk>
+ \<Longrightarrow> ordertype(pred(A,x,r),r) < ordertype(A,r)"
apply (rule ordertype_pred_subset [THEN subset_imp_le, THEN leE])
apply (simp_all add: Ord_ordertype well_ord_subset [OF _ pred_subset])
apply (erule sym [THEN ordertype_eq_imp_ord_iso, THEN exE])
@@ -298,7 +298,7 @@
well_ord(pred(A,x,r), r) *)
lemma ordertype_pred_unfold:
"well_ord(A,r)
- ==> ordertype(A,r) = {ordertype(pred(A,x,r),r). x \<in> A}"
+ \<Longrightarrow> ordertype(A,r) = {ordertype(pred(A,x,r),r). x \<in> A}"
apply (rule equalityI)
apply (safe intro!: ordertype_pred_lt [THEN ltD])
apply (auto simp add: ordertype_def well_ord_is_wf [THEN ordermap_eq_image]
@@ -310,7 +310,7 @@
subsection\<open>Alternative definition of ordinal\<close>
(*proof by Krzysztof Grabczewski*)
-lemma Ord_is_Ord_alt: "Ord(i) ==> Ord_alt(i)"
+lemma Ord_is_Ord_alt: "Ord(i) \<Longrightarrow> Ord_alt(i)"
apply (unfold Ord_alt_def)
apply (rule conjI)
apply (erule well_ord_Memrel)
@@ -319,7 +319,7 @@
(*proof by lcp*)
lemma Ord_alt_is_Ord:
- "Ord_alt(i) ==> Ord(i)"
+ "Ord_alt(i) \<Longrightarrow> Ord(i)"
apply (unfold Ord_alt_def Ord_def Transset_def well_ord_def
tot_ord_def part_ord_def trans_on_def)
apply (simp add: pred_Memrel)
@@ -339,7 +339,7 @@
done
lemma ordertype_sum_0_eq:
- "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"
+ "well_ord(A,r) \<Longrightarrow> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"
apply (rule bij_sum_0 [THEN ord_isoI, THEN ordertype_eq])
prefer 2 apply assumption
apply force
@@ -351,7 +351,7 @@
done
lemma ordertype_0_sum_eq:
- "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"
+ "well_ord(A,r) \<Longrightarrow> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"
apply (rule bij_0_sum [THEN ord_isoI, THEN ordertype_eq])
prefer 2 apply assumption
apply force
@@ -361,7 +361,7 @@
(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
lemma pred_Inl_bij:
- "a \<in> A ==> (\<lambda>x\<in>pred(A,a,r). Inl(x))
+ "a \<in> A \<Longrightarrow> (\<lambda>x\<in>pred(A,a,r). Inl(x))
\<in> bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"
apply (unfold pred_def)
apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
@@ -369,8 +369,8 @@
done
lemma ordertype_pred_Inl_eq:
- "[| a \<in> A; well_ord(A,r) |]
- ==> ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) =
+ "\<lbrakk>a \<in> A; well_ord(A,r)\<rbrakk>
+ \<Longrightarrow> ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) =
ordertype(pred(A,a,r), r)"
apply (rule pred_Inl_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
apply (simp_all add: well_ord_subset [OF _ pred_subset])
@@ -378,7 +378,7 @@
done
lemma pred_Inr_bij:
- "b \<in> B ==>
+ "b \<in> B \<Longrightarrow>
id(A+pred(B,b,s))
\<in> bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"
apply (unfold pred_def id_def)
@@ -386,8 +386,8 @@
done
lemma ordertype_pred_Inr_eq:
- "[| b \<in> B; well_ord(A,r); well_ord(B,s) |]
- ==> ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) =
+ "\<lbrakk>b \<in> B; well_ord(A,r); well_ord(B,s)\<rbrakk>
+ \<Longrightarrow> ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) =
ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"
apply (rule pred_Inr_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
prefer 2 apply (force simp add: pred_def id_def, assumption)
@@ -407,7 +407,7 @@
subsubsection\<open>Basic laws for ordinal addition\<close>
-lemma Ord_raw_oadd: "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))"
+lemma Ord_raw_oadd: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> Ord(raw_oadd(i,j))"
by (simp add: raw_oadd_def ordify_def Ord_ordertype well_ord_radd
well_ord_Memrel)
@@ -417,19 +417,19 @@
text\<open>Ordinal addition with zero\<close>
-lemma raw_oadd_0: "Ord(i) ==> raw_oadd(i,0) = i"
+lemma raw_oadd_0: "Ord(i) \<Longrightarrow> raw_oadd(i,0) = i"
by (simp add: raw_oadd_def ordify_def ordertype_sum_0_eq
ordertype_Memrel well_ord_Memrel)
-lemma oadd_0 [simp]: "Ord(i) ==> i++0 = i"
+lemma oadd_0 [simp]: "Ord(i) \<Longrightarrow> i++0 = i"
apply (simp (no_asm_simp) add: oadd_def raw_oadd_0 ordify_def)
done
-lemma raw_oadd_0_left: "Ord(i) ==> raw_oadd(0,i) = i"
+lemma raw_oadd_0_left: "Ord(i) \<Longrightarrow> raw_oadd(0,i) = i"
by (simp add: raw_oadd_def ordify_def ordertype_0_sum_eq ordertype_Memrel
well_ord_Memrel)
-lemma oadd_0_left [simp]: "Ord(i) ==> 0++i = i"
+lemma oadd_0_left [simp]: "Ord(i) \<Longrightarrow> 0++i = i"
by (simp add: oadd_def raw_oadd_0_left ordify_def)
@@ -438,14 +438,14 @@
else (if Ord(j) then j else 0))"
by (simp add: oadd_def ordify_def raw_oadd_0_left raw_oadd_0)
-lemma raw_oadd_eq_oadd: "[|Ord(i); Ord(j)|] ==> raw_oadd(i,j) = i++j"
+lemma raw_oadd_eq_oadd: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> raw_oadd(i,j) = i++j"
by (simp add: oadd_def ordify_def)
(*** Further properties of ordinal addition. Statements by Grabczewski,
proofs by lcp. ***)
(*Surely also provable by transfinite induction on j?*)
-lemma lt_oadd1: "k<i ==> k < i++j"
+lemma lt_oadd1: "k<i \<Longrightarrow> k < i++j"
apply (simp add: oadd_def ordify_def lt_Ord2 raw_oadd_0, clarify)
apply (simp add: raw_oadd_def)
apply (rule ltE, assumption)
@@ -455,31 +455,31 @@
apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)
done
-(*Thus also we obtain the rule @{term"i++j = k ==> i \<le> k"} *)
-lemma oadd_le_self: "Ord(i) ==> i \<le> i++j"
+(*Thus also we obtain the rule @{term"i++j = k \<Longrightarrow> i \<le> k"} *)
+lemma oadd_le_self: "Ord(i) \<Longrightarrow> i \<le> i++j"
apply (rule all_lt_imp_le)
apply (auto simp add: Ord_oadd lt_oadd1)
done
text\<open>Various other results\<close>
-lemma id_ord_iso_Memrel: "A<=B ==> id(A) \<in> ord_iso(A, Memrel(A), A, Memrel(B))"
+lemma id_ord_iso_Memrel: "A<=B \<Longrightarrow> id(A) \<in> ord_iso(A, Memrel(A), A, Memrel(B))"
apply (rule id_bij [THEN ord_isoI])
apply (simp (no_asm_simp))
apply blast
done
lemma subset_ord_iso_Memrel:
- "[| f \<in> ord_iso(A,Memrel(B),C,r); A<=B |] ==> f \<in> ord_iso(A,Memrel(A),C,r)"
+ "\<lbrakk>f \<in> ord_iso(A,Memrel(B),C,r); A<=B\<rbrakk> \<Longrightarrow> f \<in> ord_iso(A,Memrel(A),C,r)"
apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel])
apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption)
apply (simp add: right_comp_id)
done
lemma restrict_ord_iso:
- "[| f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r); a \<in> A; j < i;
- trans[A](r) |]
- ==> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
+ "\<lbrakk>f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r); a \<in> A; j < i;
+ trans[A](r)\<rbrakk>
+ \<Longrightarrow> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
apply (frule ltD)
apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
apply (frule ord_iso_restrict_pred, assumption)
@@ -488,15 +488,15 @@
done
lemma restrict_ord_iso2:
- "[| f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i)); a \<in> A;
- j < i; trans[A](r) |]
- ==> converse(restrict(converse(f), j))
+ "\<lbrakk>f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i)); a \<in> A;
+ j < i; trans[A](r)\<rbrakk>
+ \<Longrightarrow> converse(restrict(converse(f), j))
\<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"
by (blast intro: restrict_ord_iso ord_iso_sym ltI)
lemma ordertype_sum_Memrel:
- "[| well_ord(A,r); k<j |]
- ==> ordertype(A+k, radd(A, r, k, Memrel(j))) =
+ "\<lbrakk>well_ord(A,r); k<j\<rbrakk>
+ \<Longrightarrow> ordertype(A+k, radd(A, r, k, Memrel(j))) =
ordertype(A+k, radd(A, r, k, Memrel(k)))"
apply (erule ltE)
apply (rule ord_iso_refl [THEN sum_ord_iso_cong, THEN ordertype_eq])
@@ -504,7 +504,7 @@
apply (simp_all add: well_ord_radd well_ord_Memrel)
done
-lemma oadd_lt_mono2: "k<j ==> i++k < i++j"
+lemma oadd_lt_mono2: "k<j \<Longrightarrow> i++k < i++j"
apply (simp add: oadd_def ordify_def raw_oadd_0_left lt_Ord lt_Ord2, clarify)
apply (simp add: raw_oadd_def)
apply (rule ltE, assumption)
@@ -516,7 +516,7 @@
leI [THEN le_ordertype_Memrel] ordertype_sum_Memrel)
done
-lemma oadd_lt_cancel2: "[| i++j < i++k; Ord(j) |] ==> j<k"
+lemma oadd_lt_cancel2: "\<lbrakk>i++j < i++k; Ord(j)\<rbrakk> \<Longrightarrow> j<k"
apply (simp (asm_lr) add: oadd_eq_if_raw_oadd split: split_if_asm)
prefer 2
apply (frule_tac i = i and j = j in oadd_le_self)
@@ -526,17 +526,17 @@
apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+
done
-lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k \<longleftrightarrow> j<k"
+lemma oadd_lt_iff2: "Ord(j) \<Longrightarrow> i++j < i++k \<longleftrightarrow> j<k"
by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
-lemma oadd_inject: "[| i++j = i++k; Ord(j); Ord(k) |] ==> j=k"
+lemma oadd_inject: "\<lbrakk>i++j = i++k; Ord(j); Ord(k)\<rbrakk> \<Longrightarrow> j=k"
apply (simp add: oadd_eq_if_raw_oadd split: split_if_asm)
apply (simp add: raw_oadd_eq_oadd)
apply (rule Ord_linear_lt, auto)
apply (force dest: oadd_lt_mono2 [of concl: i] simp add: lt_not_refl)+
done
-lemma lt_oadd_disj: "k < i++j ==> k<i | (\<exists>l\<in>j. k = i++l )"
+lemma lt_oadd_disj: "k < i++j \<Longrightarrow> k<i | (\<exists>l\<in>j. k = i++l )"
apply (simp add: Ord_in_Ord' [of _ j] oadd_eq_if_raw_oadd
split: split_if_asm)
prefer 2
@@ -564,7 +564,7 @@
apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)+
done
-lemma oadd_unfold: "[| Ord(i); Ord(j) |] ==> i++j = i \<union> (\<Union>k\<in>j. {i++k})"
+lemma oadd_unfold: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> i++j = i \<union> (\<Union>k\<in>j. {i++k})"
apply (rule subsetI [THEN equalityI])
apply (erule ltI [THEN lt_oadd_disj, THEN disjE])
apply (blast intro: Ord_oadd)
@@ -572,12 +572,12 @@
apply (force intro: lt_oadd1 oadd_lt_mono2 simp add: Ord_mem_iff_lt)
done
-lemma oadd_1: "Ord(i) ==> i++1 = succ(i)"
+lemma oadd_1: "Ord(i) \<Longrightarrow> i++1 = succ(i)"
apply (simp (no_asm_simp) add: oadd_unfold Ord_1 oadd_0)
apply blast
done
-lemma oadd_succ [simp]: "Ord(j) ==> i++succ(j) = succ(i++j)"
+lemma oadd_succ [simp]: "Ord(j) \<Longrightarrow> i++succ(j) = succ(i++j)"
apply (simp add: oadd_eq_if_raw_oadd, clarify)
apply (simp add: raw_oadd_eq_oadd)
apply (simp add: oadd_1 [of j, symmetric] oadd_1 [of "i++j", symmetric]
@@ -588,28 +588,28 @@
text\<open>Ordinal addition with limit ordinals\<close>
lemma oadd_UN:
- "[| !!x. x \<in> A ==> Ord(j(x)); a \<in> A |]
- ==> i ++ (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i++j(x))"
+ "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> Ord(j(x)); a \<in> A\<rbrakk>
+ \<Longrightarrow> i ++ (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i++j(x))"
by (blast intro: ltI Ord_UN Ord_oadd lt_oadd1 [THEN ltD]
oadd_lt_mono2 [THEN ltD]
elim!: ltE dest!: ltI [THEN lt_oadd_disj])
-lemma oadd_Limit: "Limit(j) ==> i++j = (\<Union>k\<in>j. i++k)"
+lemma oadd_Limit: "Limit(j) \<Longrightarrow> i++j = (\<Union>k\<in>j. i++k)"
apply (frule Limit_has_0 [THEN ltD])
apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric]
Union_eq_UN [symmetric] Limit_Union_eq)
done
-lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 \<longleftrightarrow> i=0 & j=0"
+lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 \<longleftrightarrow> i=0 & j=0"
apply (erule trans_induct3 [of j])
apply (simp_all add: oadd_Limit)
apply (simp add: Union_empty_iff Limit_def lt_def, blast)
done
-lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) \<longleftrightarrow> 0<i | 0<j"
+lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) \<longleftrightarrow> 0<i | 0<j"
by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
-lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"
+lemma oadd_LimitI: "\<lbrakk>Ord(i); Limit(j)\<rbrakk> \<Longrightarrow> Limit(i ++ j)"
apply (simp add: oadd_Limit)
apply (frule Limit_has_1 [THEN ltD])
apply (rule increasing_LimitI)
@@ -624,7 +624,7 @@
text\<open>Order/monotonicity properties of ordinal addition\<close>
-lemma oadd_le_self2: "Ord(i) ==> i \<le> j++i"
+lemma oadd_le_self2: "Ord(i) \<Longrightarrow> i \<le> j++i"
proof (induct i rule: trans_induct3)
case 0 thus ?case by (simp add: Ord_0_le)
next
@@ -639,7 +639,7 @@
thus ?case using limit.hyps by (simp add: oadd_Limit)
qed
-lemma oadd_le_mono1: "k \<le> j ==> k++i \<le> j++i"
+lemma oadd_le_mono1: "k \<le> j \<Longrightarrow> k++i \<le> j++i"
apply (frule lt_Ord)
apply (frule le_Ord2)
apply (simp add: oadd_eq_if_raw_oadd, clarify)
@@ -651,16 +651,16 @@
apply (rule le_implies_UN_le_UN, blast)
done
-lemma oadd_lt_mono: "[| i' \<le> i; j'<j |] ==> i'++j' < i++j"
+lemma oadd_lt_mono: "\<lbrakk>i' \<le> i; j'<j\<rbrakk> \<Longrightarrow> i'++j' < i++j"
by (blast intro: lt_trans1 oadd_le_mono1 oadd_lt_mono2 Ord_succD elim: ltE)
-lemma oadd_le_mono: "[| i' \<le> i; j' \<le> j |] ==> i'++j' \<le> i++j"
+lemma oadd_le_mono: "\<lbrakk>i' \<le> i; j' \<le> j\<rbrakk> \<Longrightarrow> i'++j' \<le> i++j"
by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)
-lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k \<longleftrightarrow> j \<le> k"
+lemma oadd_le_iff2: "\<lbrakk>Ord(j); Ord(k)\<rbrakk> \<Longrightarrow> i++j \<le> i++k \<longleftrightarrow> j \<le> k"
by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
-lemma oadd_lt_self: "[| Ord(i); 0<j |] ==> i < i++j"
+lemma oadd_lt_self: "\<lbrakk>Ord(i); 0<j\<rbrakk> \<Longrightarrow> i < i++j"
apply (rule lt_trans2)
apply (erule le_refl)
apply (simp only: lt_Ord2 oadd_1 [of i, symmetric])
@@ -668,12 +668,12 @@
done
text\<open>Every ordinal is exceeded by some limit ordinal.\<close>
-lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
+lemma Ord_imp_greater_Limit: "Ord(i) \<Longrightarrow> \<exists>k. i<k & Limit(k)"
apply (rule_tac x="i ++ nat" in exI)
apply (blast intro: oadd_LimitI oadd_lt_self Limit_nat [THEN Limit_has_0])
done
-lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
+lemma Ord2_imp_greater_Limit: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> \<exists>k. i<k & j<k & Limit(k)"
apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit])
apply (simp add: Un_least_lt_iff)
done
@@ -685,7 +685,7 @@
It's probably simpler to define the difference recursively!\<close>
lemma bij_sum_Diff:
- "A<=B ==> (\<lambda>y\<in>B. if(y \<in> A, Inl(y), Inr(y))) \<in> bij(B, A+(B-A))"
+ "A<=B \<Longrightarrow> (\<lambda>y\<in>B. if(y \<in> A, Inl(y), Inr(y))) \<in> bij(B, A+(B-A))"
apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
apply (blast intro!: if_type)
apply (fast intro!: case_type)
@@ -694,7 +694,7 @@
done
lemma ordertype_sum_Diff:
- "i \<le> j ==>
+ "i \<le> j \<Longrightarrow>
ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =
ordertype(j, Memrel(j))"
apply (safe dest!: le_subset_iff [THEN iffD1])
@@ -708,7 +708,7 @@
done
lemma Ord_odiff [simp,TC]:
- "[| Ord(i); Ord(j) |] ==> Ord(i--j)"
+ "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> Ord(i--j)"
apply (unfold odiff_def)
apply (blast intro: Ord_ordertype Diff_subset well_ord_subset well_ord_Memrel)
done
@@ -716,7 +716,7 @@
lemma raw_oadd_ordertype_Diff:
"i \<le> j
- ==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"
+ \<Longrightarrow> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"
apply (simp add: raw_oadd_def odiff_def)
apply (safe dest!: le_subset_iff [THEN iffD1])
apply (rule sum_ord_iso_cong [THEN ordertype_eq])
@@ -725,19 +725,19 @@
apply (blast intro: well_ord_radd Diff_subset well_ord_subset well_ord_Memrel)+
done
-lemma oadd_odiff_inverse: "i \<le> j ==> i ++ (j--i) = j"
+lemma oadd_odiff_inverse: "i \<le> j \<Longrightarrow> i ++ (j--i) = j"
by (simp add: lt_Ord le_Ord2 oadd_def ordify_def raw_oadd_ordertype_Diff
ordertype_sum_Diff ordertype_Memrel lt_Ord2 [THEN Ord_succD])
(*By oadd_inject, the difference between i and j is unique. Note that we get
- i++j = k ==> j = k--i. *)
-lemma odiff_oadd_inverse: "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j"
+ i++j = k \<Longrightarrow> j = k--i. *)
+lemma odiff_oadd_inverse: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i++j) -- i = j"
apply (rule oadd_inject)
apply (blast intro: oadd_odiff_inverse oadd_le_self)
apply (blast intro: Ord_ordertype Ord_oadd Ord_odiff)+
done
-lemma odiff_lt_mono2: "[| i<j; k \<le> i |] ==> i--k < j--k"
+lemma odiff_lt_mono2: "\<lbrakk>i<j; k \<le> i\<rbrakk> \<Longrightarrow> i--k < j--k"
apply (rule_tac i = k in oadd_lt_cancel2)
apply (simp add: oadd_odiff_inverse)
apply (subst oadd_odiff_inverse)
@@ -749,7 +749,7 @@
subsection\<open>Ordinal Multiplication\<close>
lemma Ord_omult [simp,TC]:
- "[| Ord(i); Ord(j) |] ==> Ord(i**j)"
+ "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> Ord(i**j)"
apply (unfold omult_def)
apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel)
done
@@ -757,13 +757,13 @@
subsubsection\<open>A useful unfolding law\<close>
lemma pred_Pair_eq:
- "[| a \<in> A; b \<in> B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) =
+ "\<lbrakk>a \<in> A; b \<in> B\<rbrakk> \<Longrightarrow> pred(A*B, <a,b>, rmult(A,r,B,s)) =
pred(A,a,r)*B \<union> ({a} * pred(B,b,s))"
apply (unfold pred_def, blast)
done
lemma ordertype_pred_Pair_eq:
- "[| a \<in> A; b \<in> B; well_ord(A,r); well_ord(B,s) |] ==>
+ "\<lbrakk>a \<in> A; b \<in> B; well_ord(A,r); well_ord(B,s)\<rbrakk> \<Longrightarrow>
ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) =
ordertype(pred(A,a,r)*B + pred(B,b,s),
radd(A*B, rmult(A,r,B,s), B, s))"
@@ -776,8 +776,8 @@
done
lemma ordertype_pred_Pair_lemma:
- "[| i'<i; j'<j |]
- ==> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),
+ "\<lbrakk>i'<i; j'<j\<rbrakk>
+ \<Longrightarrow> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),
rmult(i,Memrel(i),j,Memrel(j))) =
raw_oadd (j**i', j')"
apply (unfold raw_oadd_def omult_def)
@@ -795,8 +795,8 @@
done
lemma lt_omult:
- "[| Ord(i); Ord(j); k<j**i |]
- ==> \<exists>j' i'. k = j**i' ++ j' & j'<j & i'<i"
+ "\<lbrakk>Ord(i); Ord(j); k<j**i\<rbrakk>
+ \<Longrightarrow> \<exists>j' i'. k = j**i' ++ j' & j'<j & i'<i"
apply (unfold omult_def)
apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel)
apply (safe elim!: ltE)
@@ -806,7 +806,7 @@
done
lemma omult_oadd_lt:
- "[| j'<j; i'<i |] ==> j**i' ++ j' < j**i"
+ "\<lbrakk>j'<j; i'<i\<rbrakk> \<Longrightarrow> j**i' ++ j' < j**i"
apply (unfold omult_def)
apply (rule ltI)
prefer 2
@@ -820,7 +820,7 @@
done
lemma omult_unfold:
- "[| Ord(i); Ord(j) |] ==> j**i = (\<Union>j'\<in>j. \<Union>i'\<in>i. {j**i' ++ j'})"
+ "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> j**i = (\<Union>j'\<in>j. \<Union>i'\<in>i. {j**i' ++ j'})"
apply (rule subsetI [THEN equalityI])
apply (rule lt_omult [THEN exE])
apply (erule_tac [3] ltI)
@@ -845,7 +845,7 @@
text\<open>Ordinal multiplication by 1\<close>
-lemma omult_1 [simp]: "Ord(i) ==> i**1 = i"
+lemma omult_1 [simp]: "Ord(i) \<Longrightarrow> i**1 = i"
apply (unfold omult_def)
apply (rule_tac s1="Memrel(i)"
in ord_isoI [THEN ordertype_eq, THEN trans])
@@ -853,7 +853,7 @@
apply (auto elim!: snd_type well_ord_Memrel ordertype_Memrel)
done
-lemma omult_1_left [simp]: "Ord(i) ==> 1**i = i"
+lemma omult_1_left [simp]: "Ord(i) \<Longrightarrow> 1**i = i"
apply (unfold omult_def)
apply (rule_tac s1="Memrel(i)"
in ord_isoI [THEN ordertype_eq, THEN trans])
@@ -864,7 +864,7 @@
text\<open>Distributive law for ordinal multiplication and addition\<close>
lemma oadd_omult_distrib:
- "[| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"
+ "\<lbrakk>Ord(i); Ord(j); Ord(k)\<rbrakk> \<Longrightarrow> i**(j++k) = (i**j)++(i**k)"
apply (simp add: oadd_eq_if_raw_oadd)
apply (simp add: omult_def raw_oadd_def)
apply (rule ordertype_eq [THEN trans])
@@ -879,13 +879,13 @@
Ord_ordertype)
done
-lemma omult_succ: "[| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i"
+lemma omult_succ: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> i**succ(j) = (i**j)++i"
by (simp del: oadd_succ add: oadd_1 [of j, symmetric] oadd_omult_distrib)
text\<open>Associative law\<close>
lemma omult_assoc:
- "[| Ord(i); Ord(j); Ord(k) |] ==> (i**j)**k = i**(j**k)"
+ "\<lbrakk>Ord(i); Ord(j); Ord(k)\<rbrakk> \<Longrightarrow> (i**j)**k = i**(j**k)"
apply (unfold omult_def)
apply (rule ordertype_eq [THEN trans])
apply (rule prod_ord_iso_cong [OF ord_iso_refl
@@ -902,24 +902,24 @@
text\<open>Ordinal multiplication with limit ordinals\<close>
lemma omult_UN:
- "[| Ord(i); !!x. x \<in> A ==> Ord(j(x)) |]
- ==> i ** (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i**j(x))"
+ "\<lbrakk>Ord(i); \<And>x. x \<in> A \<Longrightarrow> Ord(j(x))\<rbrakk>
+ \<Longrightarrow> i ** (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i**j(x))"
by (simp (no_asm_simp) add: Ord_UN omult_unfold, blast)
-lemma omult_Limit: "[| Ord(i); Limit(j) |] ==> i**j = (\<Union>k\<in>j. i**k)"
+lemma omult_Limit: "\<lbrakk>Ord(i); Limit(j)\<rbrakk> \<Longrightarrow> i**j = (\<Union>k\<in>j. i**k)"
by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric]
Union_eq_UN [symmetric] Limit_Union_eq)
subsubsection\<open>Ordering/monotonicity properties of ordinal multiplication\<close>
-(*As a special case we have "[| 0<i; 0<j |] ==> 0 < i**j" *)
-lemma lt_omult1: "[| k<i; 0<j |] ==> k < i**j"
+(*As a special case we have "\<lbrakk>0<i; 0<j\<rbrakk> \<Longrightarrow> 0 < i**j" *)
+lemma lt_omult1: "\<lbrakk>k<i; 0<j\<rbrakk> \<Longrightarrow> k < i**j"
apply (safe elim!: ltE intro!: ltI Ord_omult)
apply (force simp add: omult_unfold)
done
-lemma omult_le_self: "[| Ord(i); 0<j |] ==> i \<le> i**j"
+lemma omult_le_self: "\<lbrakk>Ord(i); 0<j\<rbrakk> \<Longrightarrow> i \<le> i**j"
by (blast intro: all_lt_imp_le Ord_omult lt_omult1 lt_Ord2)
lemma omult_le_mono1:
@@ -940,24 +940,24 @@
qed
qed
-lemma omult_lt_mono2: "[| k<j; 0<i |] ==> i**k < i**j"
+lemma omult_lt_mono2: "\<lbrakk>k<j; 0<i\<rbrakk> \<Longrightarrow> i**k < i**j"
apply (rule ltI)
apply (simp (no_asm_simp) add: omult_unfold lt_Ord2)
apply (safe elim!: ltE intro!: Ord_omult)
apply (force simp add: Ord_omult)
done
-lemma omult_le_mono2: "[| k \<le> j; Ord(i) |] ==> i**k \<le> i**j"
+lemma omult_le_mono2: "\<lbrakk>k \<le> j; Ord(i)\<rbrakk> \<Longrightarrow> i**k \<le> i**j"
apply (rule subset_imp_le)
apply (safe elim!: ltE dest!: Ord_succD intro!: Ord_omult)
apply (simp add: omult_unfold)
apply (blast intro: Ord_trans)
done
-lemma omult_le_mono: "[| i' \<le> i; j' \<le> j |] ==> i'**j' \<le> i**j"
+lemma omult_le_mono: "\<lbrakk>i' \<le> i; j' \<le> j\<rbrakk> \<Longrightarrow> i'**j' \<le> i**j"
by (blast intro: le_trans omult_le_mono1 omult_le_mono2 Ord_succD elim: ltE)
-lemma omult_lt_mono: "[| i' \<le> i; j'<j; 0<i |] ==> i'**j' < i**j"
+lemma omult_lt_mono: "\<lbrakk>i' \<le> i; j'<j; 0<i\<rbrakk> \<Longrightarrow> i'**j' < i**j"
by (blast intro: lt_trans1 omult_le_mono1 omult_lt_mono2 Ord_succD elim: ltE)
lemma omult_le_self2:
@@ -988,7 +988,7 @@
text\<open>Further properties of ordinal multiplication\<close>
-lemma omult_inject: "[| i**j = i**k; 0<i; Ord(j); Ord(k) |] ==> j=k"
+lemma omult_inject: "\<lbrakk>i**j = i**k; 0<i; Ord(j); Ord(k)\<rbrakk> \<Longrightarrow> j=k"
apply (rule Ord_linear_lt)
prefer 4 apply assumption
apply auto