src/ZF/CardinalArith.thy
author wenzelm
Fri Sep 15 00:18:36 2000 +0200 (2000-09-15)
changeset 9964 7966a2902266
parent 9683 f87c8c449018
child 12114 a8e860c86252
permissions -rw-r--r--
tuned symbols;
clasohm@1478
     1
(*  Title:      ZF/CardinalArith.thy
lcp@437
     2
    ID:         $Id$
clasohm@1478
     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
paulson@9548
     9
CardinalArith = Cardinal + OrderArith + ArithSimp + Finite + 
lcp@437
    10
consts
lcp@467
    11
clasohm@1401
    12
  InfCard       :: i=>o
clasohm@1401
    13
  "|*|"         :: [i,i]=>i       (infixl 70)
clasohm@1401
    14
  "|+|"         :: [i,i]=>i       (infixl 65)
clasohm@1401
    15
  csquare_rel   :: i=>i
clasohm@1401
    16
  jump_cardinal :: i=>i
clasohm@1401
    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
clasohm@1155
    28
  "csquare_rel(K) ==   
clasohm@1155
    29
        rvimage(K*K,   
clasohm@1155
    30
                lam <x,y>:K*K. <x Un y, x, y>, 
clasohm@1155
    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
clasohm@1155
    36
      "jump_cardinal(K) ==   
clasohm@1155
    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
wenzelm@9964
    42
syntax (symbols)
paulson@9683
    43
  "op |+|"     :: [i,i] => i          (infixl "\\<oplus>" 65)
paulson@9683
    44
  "op |*|"     :: [i,i] => i          (infixl "\\<otimes>" 70)
paulson@9654
    45
lcp@437
    46
end