src/ZF/CardinalArith.thy
author lcp
Tue Nov 29 00:31:31 1994 +0100 (1994-11-29)
changeset 753 ec86863e87c8
parent 516 1957113f0d7d
child 827 aa332949ce1a
permissions -rw-r--r--
replaced "rules" by "defs"
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@437
    12
  InfCard     :: "i=>o"
lcp@437
    13
  "|*|"       :: "[i,i]=>i"       (infixl 70)
lcp@437
    14
  "|+|"       :: "[i,i]=>i"       (infixl 65)
lcp@437
    15
  csquare_rel :: "i=>i"
lcp@484
    16
  jump_cardinal :: "i=>i"
lcp@484
    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@437
    23
  cadd_def     "i |+| j == | i+j |"
lcp@437
    24
lcp@437
    25
  cmult_def    "i |*| j == | i*j |"
lcp@437
    26
lcp@437
    27
  csquare_rel_def
lcp@437
    28
  "csquare_rel(k) == rvimage(k*k, lam z:k*k. split(%x y. <x Un y, <x,y>>, z), \
lcp@437
    29
\                            rmult(k,Memrel(k), k*k, 	\
lcp@437
    30
\                                  rmult(k,Memrel(k), k,Memrel(k))))"
lcp@437
    31
lcp@484
    32
  (*This def is more complex than Kunen's but it more easily proved to
lcp@484
    33
    be a cardinal*)
lcp@484
    34
  jump_cardinal_def
lcp@484
    35
      "jump_cardinal(K) ==   \
lcp@484
    36
\         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
lcp@484
    37
lcp@484
    38
  (*needed because jump_cardinal(K) might not be the successor of K*)
lcp@484
    39
  csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
lcp@484
    40
lcp@437
    41
end