src/ZF/CardinalArith.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09)
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
     1 (*  Title: 	ZF/CardinalArith.thy
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Cardinal Arithmetic
     7 *)
     8 
     9 CardinalArith = Cardinal + OrderArith + Arith + Finite + 
    10 consts
    11 
    12   InfCard       :: i=>o
    13   "|*|"         :: [i,i]=>i       (infixl 70)
    14   "|+|"         :: [i,i]=>i       (infixl 65)
    15   csquare_rel   :: i=>i
    16   jump_cardinal :: i=>i
    17   csucc         :: i=>i
    18 
    19 defs
    20 
    21   InfCard_def  "InfCard(i) == Card(i) & nat le i"
    22 
    23   cadd_def     "i |+| j == |i+j|"
    24 
    25   cmult_def    "i |*| j == |i*j|"
    26 
    27   csquare_rel_def
    28   "csquare_rel(K) ==   
    29         rvimage(K*K,   
    30                 lam <x,y>:K*K. <x Un y, x, y>, 
    31                 rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
    32 
    33   (*This def is more complex than Kunen's but it more easily proved to
    34     be a cardinal*)
    35   jump_cardinal_def
    36       "jump_cardinal(K) ==   
    37          UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
    38 
    39   (*needed because jump_cardinal(K) might not be the successor of K*)
    40   csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
    41 
    42 end