src/ZF/CardinalArith.thy
 changeset 13328 703de709a64b parent 13269 3ba9be497c33 child 13356 c9cfe1638bf2
equal inserted replaced
13327:be7105a066d3 13328:703de709a64b
`     1 (*  Title:      ZF/CardinalArith.thy`
`     1 (*  Title:      ZF/CardinalArith.thy`
`     2     ID:         \$Id\$`
`     2     ID:         \$Id\$`
`     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory`
`     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory`
`     4     Copyright   1994  University of Cambridge`
`     4     Copyright   1994  University of Cambridge`
`     5 `
`     5 `
`    12 *)`
`     6 *)`
`       `
`     7 `
`       `
`     8 header{*Cardinal Arithmetic Without the Axiom of Choice*}`
`    13 `
`     9 `
`    14 theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:`
`    10 theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:`
`    15 `
`    11 `
`    16 constdefs`
`    12 constdefs`
`    17 `
`    13 `
`    91             elim!: eqpollE lepoll_trans)`
`    87             elim!: eqpollE lepoll_trans)`
`    92 done`
`    88 done`
`    93 `
`    89 `
`    94 `
`    90 `
`    95 (*** Cardinal addition ***)`
`    91 (*** Cardinal addition ***)`
`       `
`    92 `
`       `
`    93 text{*Note: Could omit proving the algebraic laws for cardinal addition and`
`       `
`    94 multiplication.  On finite cardinals these operations coincide with`
`       `
`    95 addition and multiplication of natural numbers; on infinite cardinals they`
`       `
`    96 coincide with union (maximum).  Either way we get most laws for free.*}`
`    96 `
`    97 `
`    97 (** Cardinal addition is commutative **)`
`    98 (** Cardinal addition is commutative **)`
`    98 `
`    99 `
`    99 lemma sum_commute_eqpoll: "A+B \<approx> B+A"`
`   100 lemma sum_commute_eqpoll: "A+B \<approx> B+A"`
`   100 apply (unfold eqpoll_def)`
`   101 apply (unfold eqpoll_def)`