src/ZF/OrderArith.thy
 author lcp Tue Nov 29 00:31:31 1994 +0100 (1994-11-29 ago) 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 = ) | \ ``` lcp@437 ` 19` ```\ (EX x' x. z = & :r) | \ ``` lcp@437 ` 20` ```\ (EX y' y. z = & :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 = <, > & \ ``` lcp@437 ` 26` ```\ (: r | (x'=x & : 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 = & : r}" ``` lcp@437 ` 30` lcp@437 ` 31` ```end ```