src/ZF/CardinalArith.thy
 author paulson Fri, 16 Feb 1996 18:00:47 +0100 changeset 1512 ce37c64244c0 parent 1478 2b8c2a7547ab child 9548 15bee2731e43 permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
```
(*  Title:      ZF/CardinalArith.thy
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Cardinal Arithmetic
*)

CardinalArith = Cardinal + OrderArith + Arith + Finite +
consts

InfCard       :: i=>o
"|*|"         :: [i,i]=>i       (infixl 70)
"|+|"         :: [i,i]=>i       (infixl 65)
csquare_rel   :: i=>i
jump_cardinal :: i=>i
csucc         :: i=>i

defs

InfCard_def  "InfCard(i) == Card(i) & nat le i"

cadd_def     "i |+| j == |i+j|"

cmult_def    "i |*| j == |i*j|"

csquare_rel_def
"csquare_rel(K) ==
rvimage(K*K,
lam <x,y>:K*K. <x Un y, x, y>,
rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"

(*This def is more complex than Kunen's but it more easily proved to
be a cardinal*)
jump_cardinal_def
"jump_cardinal(K) ==
UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"

(*needed because jump_cardinal(K) might not be the successor of K*)
csucc_def "csucc(K) == LEAST L. Card(L) & K<L"

end
```