src/ZF/CardinalArith.thy
author lcp
Tue, 25 Apr 1995 11:14:03 +0200
changeset 1072 0140ff702b23
parent 827 aa332949ce1a
child 1091 f55f54a032ce
permissions -rw-r--r--
updated version
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/CardinalArith.thy
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     2
    ID:         $Id$
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     5
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     6
Cardinal Arithmetic
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     7
*)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     8
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 484
diff changeset
     9
CardinalArith = Cardinal + OrderArith + Arith + Finite + 
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    10
consts
467
92868dab2939 new cardinal arithmetic developments
lcp
parents: 437
diff changeset
    11
827
aa332949ce1a csquare_rel_def: renamed k to K
lcp
parents: 753
diff changeset
    12
  InfCard       :: "i=>o"
aa332949ce1a csquare_rel_def: renamed k to K
lcp
parents: 753
diff changeset
    13
  "|*|"         :: "[i,i]=>i"       (infixl 70)
aa332949ce1a csquare_rel_def: renamed k to K
lcp
parents: 753
diff changeset
    14
  "|+|"         :: "[i,i]=>i"       (infixl 65)
aa332949ce1a csquare_rel_def: renamed k to K
lcp
parents: 753
diff changeset
    15
  csquare_rel   :: "i=>i"
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
    16
  jump_cardinal :: "i=>i"
827
aa332949ce1a csquare_rel_def: renamed k to K
lcp
parents: 753
diff changeset
    17
  csucc         :: "i=>i"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    18
753
ec86863e87c8 replaced "rules" by "defs"
lcp
parents: 516
diff changeset
    19
defs
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    20
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    21
  InfCard_def  "InfCard(i) == Card(i) & nat le i"
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    22
827
aa332949ce1a csquare_rel_def: renamed k to K
lcp
parents: 753
diff changeset
    23
  cadd_def     "i |+| j == |i+j|"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    24
827
aa332949ce1a csquare_rel_def: renamed k to K
lcp
parents: 753
diff changeset
    25
  cmult_def    "i |*| j == |i*j|"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    26
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    27
  csquare_rel_def
827
aa332949ce1a csquare_rel_def: renamed k to K
lcp
parents: 753
diff changeset
    28
  "csquare_rel(K) ==   \
aa332949ce1a csquare_rel_def: renamed k to K
lcp
parents: 753
diff changeset
    29
\        rvimage(K*K,   \
aa332949ce1a csquare_rel_def: renamed k to K
lcp
parents: 753
diff changeset
    30
\                lam z:K*K. split(%x y. <x Un y, <x,y>>, z), \
aa332949ce1a csquare_rel_def: renamed k to K
lcp
parents: 753
diff changeset
    31
\                rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    32
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
    33
  (*This def is more complex than Kunen's but it more easily proved to
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
    34
    be a cardinal*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
    35
  jump_cardinal_def
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
    36
      "jump_cardinal(K) ==   \
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
    37
\         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
    38
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
    39
  (*needed because jump_cardinal(K) might not be the successor of K*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
    40
  csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents: 467
diff changeset
    41
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    42
end