src/ZF/OrderArith.thy
author lcp
Tue Nov 29 00:31:31 1994 +0100 (1994-11-29)
changeset 753 ec86863e87c8
parent 437 435875e4b21d
child 1155 928a16e02f9f
permissions -rw-r--r--
replaced "rules" by "defs"
lcp@437
     1
(*  Title: 	ZF/OrderArith.thy
lcp@437
     2
    ID:         $Id$
lcp@437
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@437
     4
    Copyright   1994  University of Cambridge
lcp@437
     5
lcp@437
     6
Towards ordinal arithmetic 
lcp@437
     7
*)
lcp@437
     8
lcp@437
     9
OrderArith = Order + Sum + 
lcp@437
    10
consts
lcp@437
    11
  radd, rmult      :: "[i,i,i,i]=>i"
lcp@437
    12
  rvimage          :: "[i,i,i]=>i"
lcp@437
    13
lcp@753
    14
defs
lcp@437
    15
  (*disjoint sum of two relations; underlies ordinal addition*)
lcp@437
    16
  radd_def "radd(A,r,B,s) == \
lcp@437
    17
\                {z: (A+B) * (A+B).  \
lcp@437
    18
\                    (EX x y. z = <Inl(x), Inr(y)>)   | 	 \
lcp@437
    19
\                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 \
lcp@437
    20
\                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
lcp@437
    21
lcp@437
    22
  (*lexicographic product of two relations; underlies ordinal multiplication*)
lcp@437
    23
  rmult_def "rmult(A,r,B,s) == \
lcp@437
    24
\                {z: (A*B) * (A*B).  \
lcp@437
    25
\                    EX x' y' x y. z = <<x',y'>, <x,y>> &	 \
lcp@437
    26
\                       (<x',x>: r | (x'=x & <y',y>: s))}"
lcp@437
    27
lcp@437
    28
  (*inverse image of a relation*)
lcp@437
    29
  rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
lcp@437
    30
lcp@437
    31
end