29 ordify :: "i=>i" where |
29 ordify :: "i=>i" where |
30 "ordify(x) == if Ord(x) then x else 0" |
30 "ordify(x) == if Ord(x) then x else 0" |
31 |
31 |
32 definition |
32 definition |
33 (*ordinal multiplication*) |
33 (*ordinal multiplication*) |
34 omult :: "[i,i]=>i" (infixl "**" 70) where |
34 omult :: "[i,i]=>i" (infixl \<open>**\<close> 70) where |
35 "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))" |
35 "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))" |
36 |
36 |
37 definition |
37 definition |
38 (*ordinal addition*) |
38 (*ordinal addition*) |
39 raw_oadd :: "[i,i]=>i" where |
39 raw_oadd :: "[i,i]=>i" where |
40 "raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))" |
40 "raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))" |
41 |
41 |
42 definition |
42 definition |
43 oadd :: "[i,i]=>i" (infixl "++" 65) where |
43 oadd :: "[i,i]=>i" (infixl \<open>++\<close> 65) where |
44 "i ++ j == raw_oadd(ordify(i),ordify(j))" |
44 "i ++ j == raw_oadd(ordify(i),ordify(j))" |
45 |
45 |
46 definition |
46 definition |
47 (*ordinal subtraction*) |
47 (*ordinal subtraction*) |
48 odiff :: "[i,i]=>i" (infixl "--" 65) where |
48 odiff :: "[i,i]=>i" (infixl \<open>--\<close> 65) where |
49 "i -- j == ordertype(i-j, Memrel(i))" |
49 "i -- j == ordertype(i-j, Memrel(i))" |
50 |
50 |
51 |
51 |
52 subsection\<open>Proofs needing the combination of Ordinal.thy and Order.thy\<close> |
52 subsection\<open>Proofs needing the combination of Ordinal.thy and Order.thy\<close> |
53 |
53 |