equal
deleted
inserted
replaced
810 apply (unfold omult_def) |
810 apply (unfold omult_def) |
811 apply (rule ltI) |
811 apply (rule ltI) |
812 prefer 2 |
812 prefer 2 |
813 apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2) |
813 apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2) |
814 apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2) |
814 apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2) |
815 apply (rule bexI) |
815 apply (rule bexI [of _ i']) |
816 prefer 2 apply (blast elim!: ltE) |
816 apply (rule bexI [of _ j']) |
817 apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric]) |
817 apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric]) |
818 apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd) |
818 apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd) |
|
819 apply (simp_all add: lt_def) |
819 done |
820 done |
820 |
821 |
821 lemma omult_unfold: |
822 lemma omult_unfold: |
822 "[| Ord(i); Ord(j) |] ==> j**i = (\<Union>j'\<in>j. \<Union>i'\<in>i. {j**i' ++ j'})" |
823 "[| Ord(i); Ord(j) |] ==> j**i = (\<Union>j'\<in>j. \<Union>i'\<in>i. {j**i' ++ j'})" |
823 apply (rule subsetI [THEN equalityI]) |
824 apply (rule subsetI [THEN equalityI]) |