src/ZF/CardinalArith.thy
author lcp
Tue Jul 12 18:05:03 1994 +0200 (1994-07-12)
changeset 467 92868dab2939
parent 437 435875e4b21d
child 484 70b789956bd3
permissions -rw-r--r--
new cardinal arithmetic developments
     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 + 
    10 consts
    11   jump_cardinal :: "i=>i"
    12 
    13   InfCard     :: "i=>o"
    14   "|*|"       :: "[i,i]=>i"       (infixl 70)
    15   "|+|"       :: "[i,i]=>i"       (infixl 65)
    16   csquare_rel :: "i=>i"
    17 
    18 rules
    19 
    20   jump_cardinal_def
    21       "jump_cardinal(K) ==   \
    22 \         UN X:Pow(K). {z. r: Pow(X*X), well_ord(X,r) & z = ordertype(X,r)}"
    23 
    24 
    25   InfCard_def  "InfCard(i) == Card(i) & nat le i"
    26 
    27   cadd_def     "i |+| j == | i+j |"
    28 
    29   cmult_def    "i |*| j == | i*j |"
    30 
    31   csquare_rel_def
    32   "csquare_rel(k) == rvimage(k*k, lam z:k*k. split(%x y. <x Un y, <x,y>>, z), \
    33 \                            rmult(k,Memrel(k), k*k, 	\
    34 \                                  rmult(k,Memrel(k), k,Memrel(k))))"
    35 
    36 end