src/ZF/OrderArith.thy
 author paulson Thu Sep 07 17:36:37 2000 +0200 (2000-09-07) changeset 9883 c1c8647af477 parent 1478 2b8c2a7547ab child 13140 6d97dbb189a9 permissions -rw-r--r--
a number of new theorems
 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 paulson@9883 6 Towards ordinal arithmetic. Also useful with wfrec. lcp@437 7 *) lcp@437 8 paulson@9883 9 OrderArith = Order + Sum + Ordinal + 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 paulson@9883 31 constdefs paulson@9883 32 measure :: "[i, i\\i] \\ i" paulson@9883 33 "measure(A,f) == {: A*A. f(x) < f(y)}" paulson@9883 34 paulson@9883 35 lcp@437 36 end