src/ZF/OrderArith.thy
 author clasohm Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago) changeset 1401 0c439768f45c parent 1155 928a16e02f9f child 1478 2b8c2a7547ab permissions -rw-r--r--
removed quotes from consts and syntax sections
 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 ``` clasohm@1401 ` 11` ``` radd, rmult :: [i,i,i,i]=>i ``` clasohm@1401 ` 12` ``` rvimage :: [i,i,i]=>i ``` lcp@437 ` 13` lcp@753 ` 14` ```defs ``` lcp@437 ` 15` ``` (*disjoint sum of two relations; underlies ordinal addition*) ``` clasohm@1155 ` 16` ``` radd_def "radd(A,r,B,s) == ``` clasohm@1155 ` 17` ``` {z: (A+B) * (A+B). ``` clasohm@1155 ` 18` ``` (EX x y. z = ) | ``` clasohm@1155 ` 19` ``` (EX x' x. z = & :r) | ``` clasohm@1155 ` 20` ``` (EX y' y. z = & :s)}" ``` lcp@437 ` 21` lcp@437 ` 22` ``` (*lexicographic product of two relations; underlies ordinal multiplication*) ``` clasohm@1155 ` 23` ``` rmult_def "rmult(A,r,B,s) == ``` clasohm@1155 ` 24` ``` {z: (A*B) * (A*B). ``` clasohm@1155 ` 25` ``` EX x' y' x y. z = <, > & ``` clasohm@1155 ` 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 ```