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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/CardinalArith.thy
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     2
    ID:         $Id$
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
437
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
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    12
  InfCard       :: i=>o
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    13
  "|*|"         :: [i,i]=>i       (infixl 70)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    14
  "|+|"         :: [i,i]=>i       (infixl 65)
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    15
  csquare_rel   :: i=>i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    16
  jump_cardinal :: i=>i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
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
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 1091
diff changeset
    28
  "csquare_rel(K) ==   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 1091
diff changeset
    29
        rvimage(K*K,   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 1091
diff changeset
    30
                lam <x,y>:K*K. <x Un y, x, y>, 
928a16e02f9f removed \...\ inside strings
clasohm
parents: 1091
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
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 1091
diff changeset
    36
      "jump_cardinal(K) ==   
928a16e02f9f removed \...\ inside strings
clasohm
parents: 1091
diff changeset
    37
         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
484
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