Theory: sum

Parents

• combin

Types

• sum(Arity = 2)

Constants

• IS_SUM_REP  :(bool -> 'a -> 'b -> bool) -> bool
• OUTL  :'a + 'b -> 'a
• OUTR  :'a + 'b -> 'b
• sum_case  :('b -> 'a) -> ('c -> 'a) -> 'b + 'c -> 'a
• INL  :'a -> 'a + 'b
• INR  :'b -> 'a + 'b
• ISL  :'a + 'b -> bool
• ISR  :'a + 'b -> bool
• REP_sum  :'a + 'b -> bool -> 'a -> 'b -> bool
• ABS_sum  :(bool -> 'a -> 'b -> bool) -> 'a + 'b

Definitions

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)

IS_SUM_REP

|- !f.
     IS_SUM_REP f =
     ?v1 v2. (f = (\b x y. (x = v1) /\ b)) \/ (f = (\b x y. (y = v2) /\ ~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_ISO_DEF

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

sum_TY_DEF

|- ?rep. TYPE_DEFINITION IS_SUM_REP rep

Theorems

INL

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

INR

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

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)

ISL_OR_ISR

|- !x. ISL x \/ ISR x

sum_Axiom

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

sum_case_cong

|- !g' g f' f M' M.
     (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_CASES

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

sum_distinct

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

sum_INDUCT

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