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