src/ZF/OrderArith.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09)
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
     1 (*  Title: 	ZF/OrderArith.thy
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Towards ordinal arithmetic 
     7 *)
     8 
     9 OrderArith = Order + Sum + 
    10 consts
    11   radd, rmult      :: [i,i,i,i]=>i
    12   rvimage          :: [i,i,i]=>i
    13 
    14 defs
    15   (*disjoint sum of two relations; underlies ordinal addition*)
    16   radd_def "radd(A,r,B,s) == 
    17                 {z: (A+B) * (A+B).  
    18                     (EX x y. z = <Inl(x), Inr(y)>)   | 	 
    19                     (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 
    20                     (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
    21 
    22   (*lexicographic product of two relations; underlies ordinal multiplication*)
    23   rmult_def "rmult(A,r,B,s) == 
    24                 {z: (A*B) * (A*B).  
    25                     EX x' y' x y. z = <<x',y'>, <x,y>> &	 
    26                        (<x',x>: r | (x'=x & <y',y>: s))}"
    27 
    28   (*inverse image of a relation*)
    29   rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
    30 
    31 end