src/ZF/OrderArith.thy
 author clasohm Tue Feb 06 12:27:17 1996 +0100 (1996-02-06) changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 9883 c1c8647af477 permissions -rw-r--r--
expanded tabs
 clasohm@1478 ` 1` ```(* Title: ZF/OrderArith.thy ``` lcp@437 ` 2` ``` ID: \$Id\$ ``` clasohm@1478 ` 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@1478 ` 18` ``` (EX x y. z = ) | ``` clasohm@1478 ` 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@1478 ` 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 ```