Ordinals-0.0.0.2: Main.hs

import Math.Ordinals.MultiSet
import Test.QuickCheck
import Control.Monad
import Data.List

sortwf (O os) = O $ sortBy (\ a b -> case compare a b of
                                       { GT -> LT; LT -> GT; EQ -> EQ }) os

instance Arbitrary Ordinal where
  arbitrary = liftM sortwf $ oneof [ return 0
                                   , liftM2 (.:) arbitrary arbitrary ]

prop_wf o = wf o -- sanity check for arbitrary definition for Ordinal

-- http://planetmath.org/encyclopedia/PropertiesOfOrdinalArithmetic.html
prop_add_identity_l o = 0 + o == o where types = o :: Ordinal
prop_add_identity_r o = o + 0 == o where types = o :: Ordinal
prop_add_assoc a b c = a + (b + c) ==  (a + b) + c where types = a :: Ordinal
prop_sub_def a b | a <= b     =  a + (b - a) == b
                 | otherwise =  prop_sub_def b a
                 where types = a :: Ordinal
prop_mult_identity_l o = 1 * o == o where types = o :: Ordinal
prop_mult_identity_r o = o * 1 == o where types = o :: Ordinal
prop_mult_zero_l o = 0 * o == 0 where types = o :: Ordinal
prop_mult_zero_r o = o * 0 == 0 where types = o :: Ordinal
prop_mult_assoc a b c = a * (b * c) == (a * b) * c where types = a :: Ordinal
prop_mult_dist_l a b c = a * (b + c) == a*b + a*c where types = a :: Ordinal
-- TODO division ??? div not yet defined
-- http://planetmath.org/encyclopedia/OrdinalExponentiation.html
-- TODO exponentiation
prop_power_zero o = o > 0 ==> 0 ^: o == 0 where types = o :: Ordinal
prop_power_one o = 1 ^: o == 1 where types = o :: Ordinal -- fails TODO
prop_power_of_one o = o ^: 1 == o where types = o :: Ordinal
prop_power_mult a b c = a^:b * a^:c == a^:(b+c) where types = a :: Ordinal -- fails TODO

a :: Ordinal
a = 2 -- O [O [],O []]
b :: Ordinal
b = 1 -- O [O []]
c :: Ordinal
c = w (w 1 + 1) + 1 -- [O [O [O []],O []],O []]

prop_power_power a b c = (a^:b)^:c == a^:(b*c) where types = a :: Ordinal -- fails TODO

main = print $ O []