src/ZF/OrderArith.thy
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1478 2b8c2a7547ab
child 9883 c1c8647af477
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/OrderArith.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
Towards ordinal arithmetic 
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     7
*)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     8
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
     9
OrderArith = Order + Sum + 
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    10
consts
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    11
  radd, rmult      :: [i,i,i,i]=>i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 1155
diff changeset
    12
  rvimage          :: [i,i,i]=>i
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    13
753
ec86863e87c8 replaced "rules" by "defs"
lcp
parents: 437
diff changeset
    14
defs
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    15
  (*disjoint sum of two relations; underlies ordinal addition*)
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 753
diff changeset
    16
  radd_def "radd(A,r,B,s) == 
928a16e02f9f removed \...\ inside strings
clasohm
parents: 753
diff changeset
    17
                {z: (A+B) * (A+B).  
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    18
                    (EX x y. z = <Inl(x), Inr(y)>)   |   
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    19
                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |      
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 753
diff changeset
    20
                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    21
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    22
  (*lexicographic product of two relations; underlies ordinal multiplication*)
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 753
diff changeset
    23
  rmult_def "rmult(A,r,B,s) == 
928a16e02f9f removed \...\ inside strings
clasohm
parents: 753
diff changeset
    24
                {z: (A*B) * (A*B).  
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    25
                    EX x' y' x y. z = <<x',y'>, <x,y>> &         
1155
928a16e02f9f removed \...\ inside strings
clasohm
parents: 753
diff changeset
    26
                       (<x',x>: r | (x'=x & <y',y>: s))}"
437
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    27
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    28
  (*inverse image of a relation*)
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    29
  rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    30
435875e4b21d modifications for cardinal arithmetic
lcp
parents:
diff changeset
    31
end