equal
deleted
inserted
replaced
531 apply (rule Ord_linear_lt, auto) |
531 apply (rule Ord_linear_lt, auto) |
532 apply (simp_all add: raw_oadd_eq_oadd) |
532 apply (simp_all add: raw_oadd_eq_oadd) |
533 apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+ |
533 apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+ |
534 done |
534 done |
535 |
535 |
536 lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k <-> j<k" |
536 lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k \<longleftrightarrow> j<k" |
537 by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2) |
537 by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2) |
538 |
538 |
539 lemma oadd_inject: "[| i++j = i++k; Ord(j); Ord(k) |] ==> j=k" |
539 lemma oadd_inject: "[| i++j = i++k; Ord(j); Ord(k) |] ==> j=k" |
540 apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm) |
540 apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm) |
541 apply (simp add: raw_oadd_eq_oadd) |
541 apply (simp add: raw_oadd_eq_oadd) |
605 apply (frule Limit_has_0 [THEN ltD]) |
605 apply (frule Limit_has_0 [THEN ltD]) |
606 apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] |
606 apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] |
607 Union_eq_UN [symmetric] Limit_Union_eq) |
607 Union_eq_UN [symmetric] Limit_Union_eq) |
608 done |
608 done |
609 |
609 |
610 lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0" |
610 lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 \<longleftrightarrow> i=0 & j=0" |
611 apply (erule trans_induct3 [of j]) |
611 apply (erule trans_induct3 [of j]) |
612 apply (simp_all add: oadd_Limit) |
612 apply (simp_all add: oadd_Limit) |
613 apply (simp add: Union_empty_iff Limit_def lt_def, blast) |
613 apply (simp add: Union_empty_iff Limit_def lt_def, blast) |
614 done |
614 done |
615 |
615 |
616 lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j" |
616 lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) \<longleftrightarrow> 0<i | 0<j" |
617 by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff) |
617 by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff) |
618 |
618 |
619 lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)" |
619 lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)" |
620 apply (simp add: oadd_Limit) |
620 apply (simp add: oadd_Limit) |
621 apply (frule Limit_has_1 [THEN ltD]) |
621 apply (frule Limit_has_1 [THEN ltD]) |
659 by (blast intro: lt_trans1 oadd_le_mono1 oadd_lt_mono2 Ord_succD elim: ltE) |
659 by (blast intro: lt_trans1 oadd_le_mono1 oadd_lt_mono2 Ord_succD elim: ltE) |
660 |
660 |
661 lemma oadd_le_mono: "[| i' \<le> i; j' \<le> j |] ==> i'++j' \<le> i++j" |
661 lemma oadd_le_mono: "[| i' \<le> i; j' \<le> j |] ==> i'++j' \<le> i++j" |
662 by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono) |
662 by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono) |
663 |
663 |
664 lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k <-> j \<le> k" |
664 lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k \<longleftrightarrow> j \<le> k" |
665 by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ) |
665 by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ) |
666 |
666 |
667 lemma oadd_lt_self: "[| Ord(i); 0<j |] ==> i < i++j" |
667 lemma oadd_lt_self: "[| Ord(i); 0<j |] ==> i < i++j" |
668 apply (rule lt_trans2) |
668 apply (rule lt_trans2) |
669 apply (erule le_refl) |
669 apply (erule le_refl) |