src/ZF/CardinalArith.thy
changeset 13328 703de709a64b
parent 13269 3ba9be497c33
child 13356 c9cfe1638bf2
equal deleted 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 
     6 Cardinal arithmetic -- WITHOUT the Axiom of Choice
       
     7 
       
     8 Note: Could omit proving the algebraic laws for cardinal addition and
       
     9 multiplication.  On finite cardinals these operations coincide with
       
    10 addition and multiplication of natural numbers; on infinite cardinals they
       
    11 coincide with union (maximum).  Either way we get most laws for free.
       
    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)