src/ZF/CardinalArith.thy
author lcp
Thu Jun 23 17:38:12 1994 +0200 (1994-06-23)
changeset 437 435875e4b21d
child 467 92868dab2939
permissions -rw-r--r--
modifications for cardinal arithmetic
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@437
     9
CardinalArith = Cardinal + OrderArith + Arith + 
lcp@437
    10
consts
lcp@437
    11
  InfCard     :: "i=>o"
lcp@437
    12
  "|*|"       :: "[i,i]=>i"       (infixl 70)
lcp@437
    13
  "|+|"       :: "[i,i]=>i"       (infixl 65)
lcp@437
    14
  csquare_rel :: "i=>i"
lcp@437
    15
lcp@437
    16
rules
lcp@437
    17
lcp@437
    18
  InfCard_def  "InfCard(i) == Card(i) & nat le i"
lcp@437
    19
lcp@437
    20
  cadd_def     "i |+| j == | i+j |"
lcp@437
    21
lcp@437
    22
  cmult_def    "i |*| j == | i*j |"
lcp@437
    23
lcp@437
    24
  csquare_rel_def
lcp@437
    25
  "csquare_rel(k) == rvimage(k*k, lam z:k*k. split(%x y. <x Un y, <x,y>>, z), \
lcp@437
    26
\                            rmult(k,Memrel(k), k*k, 	\
lcp@437
    27
\                                  rmult(k,Memrel(k), k,Memrel(k))))"
lcp@437
    28
lcp@437
    29
end