--- a/src/ZF/OrderType.thy Sun Mar 04 23:20:43 2012 +0100
+++ b/src/ZF/OrderType.thy Tue Mar 06 15:15:49 2012 +0000
@@ -11,44 +11,44 @@
Ordinal arithmetic is traditionally defined in terms of order types, as it is
here. But a definition by transfinite recursion would be much simpler!*}
-definition
+definition
ordermap :: "[i,i]=>i" where
- "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
+ "ordermap(A,r) == \<lambda>x\<in>A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
-definition
+definition
ordertype :: "[i,i]=>i" where
"ordertype(A,r) == ordermap(A,r)``A"
-definition
+definition
(*alternative definition of ordinal numbers*)
Ord_alt :: "i => o" where
- "Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))"
+ "Ord_alt(X) == well_ord(X, Memrel(X)) & (\<forall>u\<in>X. u=pred(X, u, Memrel(X)))"
-definition
+definition
(*coercion to ordinal: if not, just 0*)
ordify :: "i=>i" where
"ordify(x) == if Ord(x) then x else 0"
-definition
+definition
(*ordinal multiplication*)
omult :: "[i,i]=>i" (infixl "**" 70) where
"i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
-definition
+definition
(*ordinal addition*)
raw_oadd :: "[i,i]=>i" where
"raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
-definition
+definition
oadd :: "[i,i]=>i" (infixl "++" 65) where
"i ++ j == raw_oadd(ordify(i),ordify(j))"
-definition
+definition
(*ordinal subtraction*)
odiff :: "[i,i]=>i" (infixl "--" 65) where
"i -- j == ordertype(i-j, Memrel(i))"
-
+
notation (xsymbols)
omult (infixl "\<times>\<times>" 70)
@@ -58,7 +58,7 @@
subsection{*Proofs needing the combination of Ordinal.thy and Order.thy*}
-lemma le_well_ord_Memrel: "j le i ==> well_ord(j, Memrel(i))"
+lemma le_well_ord_Memrel: "j \<le> i ==> well_ord(j, Memrel(i))"
apply (rule well_ordI)
apply (rule wf_Memrel [THEN wf_imp_wf_on])
apply (simp add: ltD lt_Ord linear_def
@@ -72,22 +72,22 @@
(*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:
+lemma lt_pred_Memrel:
"j<i ==> pred(i, j, Memrel(i)) = j"
apply (unfold pred_def lt_def)
apply (simp (no_asm_simp))
apply (blast intro: Ord_trans)
done
-lemma pred_Memrel:
- "x:A ==> pred(A, x, Memrel(A)) = A Int x"
+lemma pred_Memrel:
+ "x:A ==> pred(A, x, Memrel(A)) = A \<inter> x"
by (unfold pred_def Memrel_def, blast)
lemma Ord_iso_implies_eq_lemma:
"[| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R"
apply (frule lt_pred_Memrel)
apply (erule ltE)
-apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto)
+apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto)
apply (unfold ord_iso_def)
(*Combining the two simplifications causes looping*)
apply (simp (no_asm_simp))
@@ -96,7 +96,7 @@
(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*)
lemma Ord_iso_implies_eq:
- "[| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) |]
+ "[| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) |]
==> i=j"
apply (rule_tac i = i and j = j in Ord_linear_lt)
apply (blast intro: ord_iso_sym Ord_iso_implies_eq_lemma)+
@@ -105,8 +105,8 @@
subsection{*Ordermap and ordertype*}
-lemma ordermap_type:
- "ordermap(A,r) : A -> ordertype(A,r)"
+lemma ordermap_type:
+ "ordermap(A,r) \<in> A -> ordertype(A,r)"
apply (unfold ordermap_def ordertype_def)
apply (rule lam_type)
apply (rule lamI [THEN imageI], assumption+)
@@ -115,7 +115,7 @@
subsubsection{*Unfolding of ordermap *}
(*Useful for cardinality reasoning; see CardinalArith.ML*)
-lemma ordermap_eq_image:
+lemma ordermap_eq_image:
"[| wf[A](r); x:A |]
==> ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"
apply (unfold ordermap_def pred_def)
@@ -127,23 +127,23 @@
(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
lemma ordermap_pred_unfold:
"[| wf[A](r); x:A |]
- ==> ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"
+ ==> 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!*)
-lemmas ordermap_unfold = ordermap_pred_unfold [simplified pred_def]
+lemmas ordermap_unfold = ordermap_pred_unfold [simplified pred_def]
-(*The theorem above is
+(*The theorem above is
-[| wf[A](r); x : A |]
-==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}}
+[| wf[A](r); x \<in> A |]
+==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: 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
ordermap(nat,predr) ` n equals {n-1} and not n. A more complicated definition,
like
- ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> : r}},
+ ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> \<in> r}},
might eliminate the need for r to be transitive.
*)
@@ -151,7 +151,7 @@
subsubsection{*Showing that ordermap, ordertype yield ordinals *}
-lemma Ord_ordermap:
+lemma Ord_ordermap:
"[| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)"
apply (unfold well_ord_def tot_ord_def part_ord_def, safe)
apply (rule_tac a=x in wf_on_induct, assumption+)
@@ -159,10 +159,10 @@
apply (rule OrdI [OF _ Ord_is_Transset])
apply (unfold pred_def Transset_def)
apply (blast intro: trans_onD
- dest!: ordermap_unfold [THEN equalityD1])+
+ dest!: ordermap_unfold [THEN equalityD1])+
done
-lemma Ord_ordertype:
+lemma Ord_ordertype:
"well_ord(A,r) ==> Ord(ordertype(A,r))"
apply (unfold ordertype_def)
apply (subst image_fun [OF ordermap_type subset_refl])
@@ -178,38 +178,38 @@
lemma ordermap_mono:
"[| <w,x>: r; wf[A](r); w: A; x: A |]
- ==> ordermap(A,r)`w : ordermap(A,r)`x"
+ ==> 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 : ordermap(A,r)`x; well_ord(A,r); w: A; x: A |]
+lemma converse_ordermap_mono:
+ "[| ordermap(A,r)`w \<in> ordermap(A,r)`x; well_ord(A,r); w: A; x: A |]
==> <w,x>: r"
apply (unfold well_ord_def tot_ord_def, safe)
-apply (erule_tac x=w and y=x in linearE, assumption+)
+apply (erule_tac x=w and y=x in linearE, assumption+)
apply (blast elim!: mem_not_refl [THEN notE])
-apply (blast dest: ordermap_mono intro: mem_asym)
+apply (blast dest: ordermap_mono intro: mem_asym)
done
-lemmas ordermap_surj =
+lemmas ordermap_surj =
ordermap_type [THEN surj_image, unfolded ordertype_def [symmetric]]
-lemma ordermap_bij:
- "well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"
+lemma ordermap_bij:
+ "well_ord(A,r) ==> 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
+apply (force intro!: ordermap_type ordermap_surj
+ elim: linearE dest: ordermap_mono
simp add: mem_not_refl)
done
subsubsection{*Isomorphisms involving ordertype *}
-lemma ordertype_ord_iso:
+lemma ordertype_ord_iso:
"well_ord(A,r)
- ==> ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"
+ ==> 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
+apply (safe elim!: well_ord_is_wf
intro!: ordermap_type [THEN apply_type] ordermap_mono ordermap_bij)
apply (blast dest!: converse_ordermap_mono)
done
@@ -223,8 +223,8 @@
done
lemma ordertype_eq_imp_ord_iso:
- "[| ordertype(A,r) = ordertype(B,s); well_ord(A,r); well_ord(B,s) |]
- ==> EX f. f: ord_iso(A,r,B,s)"
+ "[| ordertype(A,r) = ordertype(B,s); well_ord(A,r); well_ord(B,s) |]
+ ==> \<exists>f. f: ord_iso(A,r,B,s)"
apply (rule exI)
apply (rule ordertype_ord_iso [THEN ord_iso_trans], assumption)
apply (erule ssubst)
@@ -234,7 +234,7 @@
subsubsection{*Basic equalities for ordertype *}
(*Ordertype of Memrel*)
-lemma le_ordertype_Memrel: "j le i ==> ordertype(j,Memrel(i)) = j"
+lemma le_ordertype_Memrel: "j \<le> i ==> ordertype(j,Memrel(i)) = j"
apply (rule Ord_iso_implies_eq [symmetric])
apply (erule ltE, assumption)
apply (blast intro: le_well_ord_Memrel Ord_ordertype)
@@ -277,16 +277,16 @@
apply (fast elim!: trans_onD)
done
-lemma ordertype_unfold:
- "ordertype(A,r) = {ordermap(A,r)`y . y : A}"
+lemma ordertype_unfold:
+ "ordertype(A,r) = {ordermap(A,r)`y . y \<in> A}"
apply (unfold ordertype_def)
apply (rule image_fun [OF ordermap_type subset_refl])
done
text{*Theorems by Krzysztof Grabczewski; proofs simplified by lcp *}
-lemma ordertype_pred_subset: "[| well_ord(A,r); x:A |] ==>
- ordertype(pred(A,x,r),r) <= ordertype(A,r)"
+lemma ordertype_pred_subset: "[| well_ord(A,r); x:A |] ==>
+ 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
@@ -321,13 +321,13 @@
apply (unfold Ord_alt_def)
apply (rule conjI)
apply (erule well_ord_Memrel)
-apply (unfold Ord_def Transset_def pred_def Memrel_def, blast)
+apply (unfold Ord_def Transset_def pred_def Memrel_def, blast)
done
(*proof by lcp*)
-lemma Ord_alt_is_Ord:
+lemma Ord_alt_is_Ord:
"Ord_alt(i) ==> Ord(i)"
-apply (unfold Ord_alt_def Ord_def Transset_def well_ord_def
+apply (unfold Ord_alt_def Ord_def Transset_def well_ord_def
tot_ord_def part_ord_def trans_on_def)
apply (simp add: pred_Memrel)
apply (blast elim!: equalityE)
@@ -340,7 +340,7 @@
text{*Addition with 0 *}
-lemma bij_sum_0: "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)"
+lemma bij_sum_0: "(\<lambda>z\<in>A+0. case(%x. x, %y. y, z)) \<in> bij(A+0, A)"
apply (rule_tac d = Inl in lam_bijective, safe)
apply (simp_all (no_asm_simp))
done
@@ -352,7 +352,7 @@
apply force
done
-lemma bij_0_sum: "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)"
+lemma bij_0_sum: "(\<lambda>z\<in>0+A. case(%x. x, %y. y, z)) \<in> bij(0+A, A)"
apply (rule_tac d = Inr in lam_bijective, safe)
apply (simp_all (no_asm_simp))
done
@@ -367,9 +367,9 @@
text{*Initial segments of radd. Statements by Grabczewski *}
(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
-lemma pred_Inl_bij:
- "a:A ==> (lam x:pred(A,a,r). Inl(x))
- : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"
+lemma pred_Inl_bij:
+ "a:A ==> (\<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)
apply auto
@@ -377,24 +377,24 @@
lemma ordertype_pred_Inl_eq:
"[| a:A; well_ord(A,r) |]
- ==> ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) =
+ ==> ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) =
ordertype(pred(A,a,r), r)"
apply (rule pred_Inl_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
apply (simp_all add: well_ord_subset [OF _ pred_subset])
apply (simp add: pred_def)
done
-lemma pred_Inr_bij:
- "b:B ==>
- id(A+pred(B,b,s))
- : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"
+lemma pred_Inr_bij:
+ "b:B ==>
+ 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)
-apply (rule_tac d = "%z. z" in lam_bijective, auto)
+apply (rule_tac d = "%z. z" in lam_bijective, auto)
done
lemma ordertype_pred_Inr_eq:
"[| b:B; well_ord(A,r); well_ord(B,s) |]
- ==> ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) =
+ ==> ordertype(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)
@@ -441,7 +441,7 @@
lemma oadd_eq_if_raw_oadd:
- "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i)
+ "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i)
else (if Ord(j) then j else 0))"
by (simp add: oadd_def ordify_def raw_oadd_0_left raw_oadd_0)
@@ -462,15 +462,15 @@
apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)
done
-(*Thus also we obtain the rule i++j = k ==> i le k *)
-lemma oadd_le_self: "Ord(i) ==> i le i++j"
+(*Thus also we obtain the rule @{term"i++j = k ==> i \<le> k"} *)
+lemma oadd_le_self: "Ord(i) ==> i \<le> i++j"
apply (rule all_lt_imp_le)
-apply (auto simp add: Ord_oadd lt_oadd1)
+apply (auto simp add: Ord_oadd lt_oadd1)
done
text{*Various other results *}
-lemma id_ord_iso_Memrel: "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"
+lemma id_ord_iso_Memrel: "A<=B ==> 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
@@ -478,32 +478,32 @@
lemma subset_ord_iso_Memrel:
"[| f: ord_iso(A,Memrel(B),C,r); A<=B |] ==> f: 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)
+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;
+ "[| 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)"
-apply (frule ltD)
-apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
-apply (frule ord_iso_restrict_pred, assumption)
+apply (frule ltD)
+apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
+apply (frule ord_iso_restrict_pred, assumption)
apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel)
-apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI])
+apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI])
done
lemma restrict_ord_iso2:
- "[| f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i)); a \<in> A;
+ "[| 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))
+ ==> 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))) =
+ ==> 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])
@@ -528,7 +528,7 @@
prefer 2
apply (frule_tac i = i and j = j in oadd_le_self)
apply (simp (asm_lr) add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])
-apply (rule Ord_linear_lt, auto)
+apply (rule Ord_linear_lt, auto)
apply (simp_all add: raw_oadd_eq_oadd)
apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+
done
@@ -539,18 +539,18 @@
lemma oadd_inject: "[| i++j = i++k; Ord(j); Ord(k) |] ==> j=k"
apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
apply (simp add: raw_oadd_eq_oadd)
-apply (rule Ord_linear_lt, auto)
+apply (rule Ord_linear_lt, auto)
apply (force dest: oadd_lt_mono2 [of concl: i] simp add: lt_not_refl)+
done
-lemma lt_oadd_disj: "k < i++j ==> k<i | (EX l:j. k = i++l )"
+lemma lt_oadd_disj: "k < i++j ==> k<i | (\<exists>l\<in>j. k = i++l )"
apply (simp add: Ord_in_Ord' [of _ j] oadd_eq_if_raw_oadd
split add: split_if_asm)
prefer 2
apply (simp add: Ord_in_Ord' [of _ j] lt_def)
apply (simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel raw_oadd_def)
apply (erule ltD [THEN RepFunE])
-apply (force simp add: ordertype_pred_Inl_eq well_ord_Memrel ltI
+apply (force simp add: ordertype_pred_Inl_eq well_ord_Memrel ltI
lt_pred_Memrel le_ordertype_Memrel leI
ordertype_pred_Inr_eq ordertype_sum_Memrel)
done
@@ -562,7 +562,7 @@
apply (simp add: oadd_eq_if_raw_oadd Ord_raw_oadd raw_oadd_0 raw_oadd_0_left, clarify)
apply (simp add: raw_oadd_def)
apply (rule ordertype_eq [THEN trans])
-apply (rule sum_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]
+apply (rule sum_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]
ord_iso_refl])
apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)
apply (rule sum_assoc_ord_iso [THEN ordertype_eq, THEN trans])
@@ -571,11 +571,11 @@
apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)+
done
-lemma oadd_unfold: "[| Ord(i); Ord(j) |] ==> i++j = i Un (\<Union>k\<in>j. {i++k})"
+lemma oadd_unfold: "[| Ord(i); Ord(j) |] ==> 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)
-apply (blast elim!: ltE, blast)
+apply (blast intro: Ord_oadd)
+apply (blast elim!: ltE, blast)
apply (force intro: lt_oadd1 oadd_lt_mono2 simp add: Ord_mem_iff_lt)
done
@@ -597,13 +597,13 @@
lemma oadd_UN:
"[| !!x. x:A ==> Ord(j(x)); a:A |]
==> 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]
+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)"
apply (frule Limit_has_0 [THEN ltD])
-apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric]
+apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric]
Union_eq_UN [symmetric] Limit_Union_eq)
done
@@ -626,12 +626,12 @@
Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
apply (rule_tac x="succ(y)" in bexI)
apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
-apply (simp add: Limit_def lt_def)
+apply (simp add: Limit_def lt_def)
done
text{*Order/monotonicity properties of ordinal addition *}
-lemma oadd_le_self2: "Ord(i) ==> i le j++i"
+lemma oadd_le_self2: "Ord(i) ==> i \<le> j++i"
apply (erule_tac i = i in trans_induct3)
apply (simp (no_asm_simp) add: Ord_0_le)
apply (simp (no_asm_simp) add: oadd_succ succ_leI)
@@ -643,7 +643,7 @@
apply (simp add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord)
done
-lemma oadd_le_mono1: "k le j ==> k++i le j++i"
+lemma oadd_le_mono1: "k \<le> j ==> k++i \<le> j++i"
apply (frule lt_Ord)
apply (frule le_Ord2)
apply (simp add: oadd_eq_if_raw_oadd, clarify)
@@ -655,31 +655,31 @@
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: "[| i' \<le> i; j'<j |] ==> i'++j' < i++j"
by (blast intro: lt_trans1 oadd_le_mono1 oadd_lt_mono2 Ord_succD elim: ltE)
-lemma oadd_le_mono: "[| i' le i; j' le j |] ==> i'++j' le i++j"
+lemma oadd_le_mono: "[| i' \<le> i; j' \<le> j |] ==> i'++j' \<le> i++j"
by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)
-lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"
+lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k <-> j \<le> k"
by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
lemma oadd_lt_self: "[| Ord(i); 0<j |] ==> i < i++j"
-apply (rule lt_trans2)
-apply (erule le_refl)
-apply (simp only: lt_Ord2 oadd_1 [of i, symmetric])
+apply (rule lt_trans2)
+apply (erule le_refl)
+apply (simp only: lt_Ord2 oadd_1 [of i, symmetric])
apply (blast intro: succ_leI oadd_le_mono)
done
text{*Every ordinal is exceeded by some limit ordinal.*}
lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
-apply (rule_tac x="i ++ nat" in exI)
+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)"
-apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit])
-apply (simp add: Un_least_lt_iff)
+apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit])
+apply (simp add: Un_least_lt_iff)
done
@@ -689,7 +689,7 @@
It's probably simpler to define the difference recursively!*}
lemma bij_sum_Diff:
- "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))"
+ "A<=B ==> (\<lambda>y\<in>B. if(y: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)
@@ -698,8 +698,8 @@
done
lemma ordertype_sum_Diff:
- "i le j ==>
- ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =
+ "i \<le> j ==>
+ ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =
ordertype(j, Memrel(j))"
apply (safe dest!: le_subset_iff [THEN iffD1])
apply (rule bij_sum_Diff [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
@@ -711,15 +711,15 @@
apply (blast intro: lt_trans2 lt_trans)
done
-lemma Ord_odiff [simp,TC]:
+lemma Ord_odiff [simp,TC]:
"[| Ord(i); Ord(j) |] ==> Ord(i--j)"
apply (unfold odiff_def)
apply (blast intro: Ord_ordertype Diff_subset well_ord_subset well_ord_Memrel)
done
-lemma raw_oadd_ordertype_Diff:
- "i le j
+lemma raw_oadd_ordertype_Diff:
+ "i \<le> j
==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"
apply (simp add: raw_oadd_def odiff_def)
apply (safe dest!: le_subset_iff [THEN iffD1])
@@ -729,7 +729,7 @@
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 ==> 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])
@@ -741,7 +741,7 @@
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: "[| i<j; k \<le> i |] ==> i--k < j--k"
apply (rule_tac i = k in oadd_lt_cancel2)
apply (simp add: oadd_odiff_inverse)
apply (subst oadd_odiff_inverse)
@@ -752,7 +752,7 @@
subsection{*Ordinal Multiplication*}
-lemma Ord_omult [simp,TC]:
+lemma Ord_omult [simp,TC]:
"[| Ord(i); Ord(j) |] ==> Ord(i**j)"
apply (unfold omult_def)
apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel)
@@ -760,67 +760,67 @@
subsubsection{*A useful unfolding law *}
-lemma pred_Pair_eq:
- "[| a:A; b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) =
- pred(A,a,r)*B Un ({a} * pred(B,b,s))"
+lemma pred_Pair_eq:
+ "[| a:A; b:B |] ==> 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:A; b:B; well_ord(A,r); well_ord(B,s) |] ==>
- ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) =
- ordertype(pred(A,a,r)*B + pred(B,b,s),
+ "[| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==>
+ ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) =
+ ordertype(pred(A,a,r)*B + pred(B,b,s),
radd(A*B, rmult(A,r,B,s), B, s))"
apply (simp (no_asm_simp) add: pred_Pair_eq)
apply (rule ordertype_eq [symmetric])
apply (rule prod_sum_singleton_ord_iso)
apply (simp_all add: pred_subset well_ord_rmult [THEN well_ord_subset])
-apply (blast intro: pred_subset well_ord_rmult [THEN well_ord_subset]
+apply (blast intro: pred_subset well_ord_rmult [THEN well_ord_subset]
elim!: predE)
done
-lemma ordertype_pred_Pair_lemma:
+lemma ordertype_pred_Pair_lemma:
"[| i'<i; j'<j |]
- ==> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),
- rmult(i,Memrel(i),j,Memrel(j))) =
+ ==> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),
+ rmult(i,Memrel(i),j,Memrel(j))) =
raw_oadd (j**i', j')"
apply (unfold raw_oadd_def omult_def)
-apply (simp add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2
+apply (simp add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2
well_ord_Memrel)
apply (rule trans)
- apply (rule_tac [2] ordertype_ord_iso
+ apply (rule_tac [2] ordertype_ord_iso
[THEN sum_ord_iso_cong, THEN ordertype_eq])
apply (rule_tac [3] ord_iso_refl)
apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq])
apply (elim SigmaE sumE ltE ssubst)
apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
- Ord_ordertype lt_Ord lt_Ord2)
+ Ord_ordertype lt_Ord lt_Ord2)
apply (blast intro: Ord_trans)+
done
-lemma lt_omult:
+lemma lt_omult:
"[| Ord(i); Ord(j); k<j**i |]
- ==> EX j' i'. k = j**i' ++ j' & j'<j & i'<i"
+ ==> \<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)
-apply (simp add: ordertype_pred_Pair_lemma ltI raw_oadd_eq_oadd
+apply (simp add: ordertype_pred_Pair_lemma ltI raw_oadd_eq_oadd
omult_def [symmetric] Ord_in_Ord' [of _ i] Ord_in_Ord' [of _ j])
apply (blast intro: ltI)
done
-lemma omult_oadd_lt:
+lemma omult_oadd_lt:
"[| j'<j; i'<i |] ==> j**i' ++ j' < j**i"
apply (unfold omult_def)
apply (rule ltI)
prefer 2
apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)
-apply (rule bexI [of _ i'])
-apply (rule bexI [of _ j'])
+apply (rule bexI [of _ i'])
+apply (rule bexI [of _ j'])
apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric])
apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd)
-apply (simp_all add: lt_def)
+apply (simp_all add: lt_def)
done
lemma omult_unfold:
@@ -828,7 +828,7 @@
apply (rule subsetI [THEN equalityI])
apply (rule lt_omult [THEN exE])
apply (erule_tac [3] ltI)
-apply (simp_all add: Ord_omult)
+apply (simp_all add: Ord_omult)
apply (blast elim!: ltE)
apply (blast intro: omult_oadd_lt [THEN ltD] ltI)
done
@@ -851,7 +851,7 @@
lemma omult_1 [simp]: "Ord(i) ==> i**1 = i"
apply (unfold omult_def)
-apply (rule_tac s1="Memrel(i)"
+apply (rule_tac s1="Memrel(i)"
in ord_isoI [THEN ordertype_eq, THEN trans])
apply (rule_tac c = snd and d = "%z.<0,z>" in lam_bijective)
apply (auto elim!: snd_type well_ord_Memrel ordertype_Memrel)
@@ -859,7 +859,7 @@
lemma omult_1_left [simp]: "Ord(i) ==> 1**i = i"
apply (unfold omult_def)
-apply (rule_tac s1="Memrel(i)"
+apply (rule_tac s1="Memrel(i)"
in ord_isoI [THEN ordertype_eq, THEN trans])
apply (rule_tac c = fst and d = "%z.<z,0>" in lam_bijective)
apply (auto elim!: fst_type well_ord_Memrel ordertype_Memrel)
@@ -872,14 +872,14 @@
apply (simp add: oadd_eq_if_raw_oadd)
apply (simp add: omult_def raw_oadd_def)
apply (rule ordertype_eq [THEN trans])
-apply (rule prod_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]
+apply (rule prod_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]
ord_iso_refl])
-apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
+apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
Ord_ordertype)
apply (rule sum_prod_distrib_ord_iso [THEN ordertype_eq, THEN trans])
apply (rule_tac [2] ordertype_eq)
apply (rule_tac [2] sum_ord_iso_cong [OF ordertype_ord_iso ordertype_ord_iso])
-apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
+apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
Ord_ordertype)
done
@@ -888,14 +888,14 @@
text{*Associative law *}
-lemma omult_assoc:
+lemma omult_assoc:
"[| Ord(i); Ord(j); Ord(k) |] ==> (i**j)**k = i**(j**k)"
apply (unfold omult_def)
apply (rule ordertype_eq [THEN trans])
-apply (rule prod_ord_iso_cong [OF ord_iso_refl
+apply (rule prod_ord_iso_cong [OF ord_iso_refl
ordertype_ord_iso [THEN ord_iso_sym]])
apply (blast intro: well_ord_rmult well_ord_Memrel)+
-apply (rule prod_assoc_ord_iso
+apply (rule prod_assoc_ord_iso
[THEN ord_iso_sym, THEN ordertype_eq, THEN trans])
apply (rule_tac [2] ordertype_eq)
apply (rule_tac [2] prod_ord_iso_cong [OF ordertype_ord_iso ord_iso_refl])
@@ -905,13 +905,13 @@
text{*Ordinal multiplication with limit ordinals *}
-lemma omult_UN:
+lemma omult_UN:
"[| Ord(i); !!x. x:A ==> Ord(j(x)) |]
==> 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)"
-by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric]
+by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric]
Union_eq_UN [symmetric] Limit_Union_eq)
@@ -923,10 +923,10 @@
apply (force simp add: omult_unfold)
done
-lemma omult_le_self: "[| Ord(i); 0<j |] ==> i le i**j"
+lemma omult_le_self: "[| Ord(i); 0<j |] ==> i \<le> i**j"
by (blast intro: all_lt_imp_le Ord_omult lt_omult1 lt_Ord2)
-lemma omult_le_mono1: "[| k le j; Ord(i) |] ==> k**i le j**i"
+lemma omult_le_mono1: "[| k \<le> j; Ord(i) |] ==> k**i \<le> j**i"
apply (frule lt_Ord)
apply (frule le_Ord2)
apply (erule trans_induct3)
@@ -943,20 +943,20 @@
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: "[| k \<le> j; Ord(i) |] ==> i**k \<le> i**j"
apply (rule subset_imp_le)
apply (safe elim!: ltE dest!: Ord_succD intro!: Ord_omult)
apply (simp add: omult_unfold)
-apply (blast intro: Ord_trans)
+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: "[| i' \<le> i; j' \<le> j |] ==> i'**j' \<le> i**j"
by (blast intro: le_trans omult_le_mono1 omult_le_mono2 Ord_succD elim: ltE)
-lemma omult_lt_mono: "[| i' le i; j'<j; 0<i |] ==> i'**j' < i**j"
+lemma omult_lt_mono: "[| i' \<le> i; j'<j; 0<i |] ==> i'**j' < i**j"
by (blast intro: lt_trans1 omult_le_mono1 omult_lt_mono2 Ord_succD elim: ltE)
-lemma omult_le_self2: "[| Ord(i); 0<j |] ==> i le j**i"
+lemma omult_le_self2: "[| Ord(i); 0<j |] ==> i \<le> j**i"
apply (frule lt_Ord2)
apply (erule_tac i = i in trans_induct3)
apply (simp (no_asm_simp))
@@ -977,32 +977,32 @@
lemma omult_inject: "[| i**j = i**k; 0<i; Ord(j); Ord(k) |] ==> j=k"
apply (rule Ord_linear_lt)
prefer 4 apply assumption
-apply auto
+apply auto
apply (force dest: omult_lt_mono2 simp add: lt_not_refl)+
done
subsection{*The Relation @{term Lt}*}
lemma wf_Lt: "wf(Lt)"
-apply (rule wf_subset)
-apply (rule wf_Memrel)
-apply (auto simp add: Lt_def Memrel_def lt_def)
+apply (rule wf_subset)
+apply (rule wf_Memrel)
+apply (auto simp add: Lt_def Memrel_def lt_def)
done
lemma irrefl_Lt: "irrefl(A,Lt)"
by (auto simp add: Lt_def irrefl_def)
lemma trans_Lt: "trans[A](Lt)"
-apply (simp add: Lt_def trans_on_def)
-apply (blast intro: lt_trans)
+apply (simp add: Lt_def trans_on_def)
+apply (blast intro: lt_trans)
done
lemma part_ord_Lt: "part_ord(A,Lt)"
by (simp add: part_ord_def irrefl_Lt trans_Lt)
lemma linear_Lt: "linear(nat,Lt)"
-apply (auto dest!: not_lt_imp_le simp add: Lt_def linear_def le_iff)
-apply (drule lt_asym, auto)
+apply (auto dest!: not_lt_imp_le simp add: Lt_def linear_def le_iff)
+apply (drule lt_asym, auto)
done
lemma tot_ord_Lt: "tot_ord(nat,Lt)"