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 = <Inl(x), Inr(y)>)   |   
clasohm@1478
    19
                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |      
clasohm@1155
    20
                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>: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 = <<x',y'>, <x,y>> &         
clasohm@1155
    26
                       (<x',x>: r | (x'=x & <y',y>: 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 = <x,y> & <f`x,f`y>: r}"
lcp@437
    30
paulson@9883
    31
constdefs
paulson@9883
    32
   measure :: "[i, i\\<Rightarrow>i] \\<Rightarrow> i"
paulson@9883
    33
   "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}"
paulson@9883
    34
paulson@9883
    35
lcp@437
    36
end