Theory "sum"

Signature

Definitions

IS_SUM_REP

|- !f.
     IS_SUM_REP f =
     ?v1 v2. (f = (\b x y. (x = v1) /\ b)) \/ (f = (\b x y. (y = v2) /\ ~b))

sum_TY_DEF

|- ?rep. TYPE_DEFINITION IS_SUM_REP rep

sum_ISO_DEF

|- (!a. ABS_sum (REP_sum a) = a) /\
   !r. IS_SUM_REP r = (REP_sum (ABS_sum r) = r)

INL_DEF

|- !e. INL e = ABS_sum (\b x y. (x = e) /\ b)

INR_DEF

|- !e. INR e = ABS_sum (\b x y. (y = e) /\ ~b)

ISL

|- (!x. ISL (INL x)) /\ !y. ~ISL (INR y)

ISR

|- (!x. ISR (INR x)) /\ !y. ~ISR (INL y)

OUTL

|- !x. OUTL (INL x) = x

OUTR

|- !x. OUTR (INR x) = x

sum_case_def

|- (!f g x. sum_case f g (INL x) = f x) /\ !f g y. sum_case f g (INR y) = g y

SUM_MAP_def

|- (!f g a. (f ++ g) (INL a) = INL (f a)) /\
   !f g b. (f ++ g) (INR b) = INR (g b)

Theorems

INR_INL_11

|- (!y x. (INL x = INL y) = (x = y)) /\ !y x. (INR x = INR y) = (x = y)

INR_neq_INL

|- !v1 v2. ~(INR v2 = INL v1)

sum_axiom

|- !f g. ?!h. (h o INL = f) /\ (h o INR = g)

sum_INDUCT

|- !P. (!x. P (INL x)) /\ (!y. P (INR y)) ==> !s. P s

FORALL_SUM

|- (!s. P s) = (!x. P (INL x)) /\ !y. P (INR y)

sum_Axiom

|- !f g. ?h. (!x. h (INL x) = f x) /\ !y. h (INR y) = g y

sum_CASES

|- !s. (?x. s = INL x) \/ ?y. s = INR y

sum_distinct

|- !x y. ~(INL x = INR y)

sum_distinct1

|- !x y. ~(INR y = INL x)

ISL_OR_ISR

|- !x. ISL x \/ ISR x

INL

|- !x. ISL x ==> (INL (OUTL x) = x)

INR

|- !x. ISR x ==> (INR (OUTR x) = x)

sum_case_cong

|- !M M' f g.
     (M = M') /\ (!x. (M' = INL x) ==> (f x = f' x)) /\
     (!y. (M' = INR y) ==> (g y = g' y)) ==>
     (sum_case f g M = sum_case f' g' M')

SUM_MAP

|- !f g z. (f ++ g) z = (if ISL z then INL (f (OUTL z)) else INR (g (OUTR z)))

SUM_MAP_CASE

|- !f g z. (f ++ g) z = sum_case (INL o f) (INR o g) z

SUM_MAP_I

|- I ++ I = I