equal
deleted
inserted
replaced
508 (** Ordinal addition with limit ordinals **) |
508 (** Ordinal addition with limit ordinals **) |
509 |
509 |
510 val prems = |
510 val prems = |
511 Goal "[| Ord(i); !!x. x:A ==> Ord(j(x)); a:A |] ==> \ |
511 Goal "[| Ord(i); !!x. x:A ==> Ord(j(x)); a:A |] ==> \ |
512 \ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"; |
512 \ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"; |
513 by (blast_tac (claset() addIs (prems @ [ltI, Ord_UN, Ord_oadd, |
513 by (blast_tac (claset() addIs prems @ [ltI, Ord_UN, Ord_oadd, |
514 lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD]) |
514 lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD] |
515 addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1); |
515 addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1); |
516 qed "oadd_UN"; |
516 qed "oadd_UN"; |
517 |
517 |
518 Goal "[| Ord(i); Limit(j) |] ==> i++j = (UN k:j. i++k)"; |
518 Goal "[| Ord(i); Limit(j) |] ==> i++j = (UN k:j. i++k)"; |
519 by (forward_tac [Limit_has_0 RS ltD] 1); |
519 by (forward_tac [Limit_has_0 RS ltD] 1); |
520 by (asm_simp_tac (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord, |
520 by (asm_simp_tac (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord, |