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.
```
(*  Title:      ZF/OrderArith.thy
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Towards ordinal arithmetic
*)

OrderArith = Order + Sum +
consts
rvimage          :: [i,i,i]=>i

defs
(*disjoint sum of two relations; underlies ordinal addition*)
{z: (A+B) * (A+B).
(EX x y. z = <Inl(x), Inr(y)>)   |
(EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |
(EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"

(*lexicographic product of two relations; underlies ordinal multiplication*)
rmult_def "rmult(A,r,B,s) ==
{z: (A*B) * (A*B).
EX x' y' x y. z = <<x',y'>, <x,y>> &
(<x',x>: r | (x'=x & <y',y>: s))}"

(*inverse image of a relation*)
rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"

end
```