UP

The Theory sum

Parents

combin

Children

hol

Constants

IsSumRep'a cross 'b cross BOOL func1 BOOL
IsR'a + 'b func1 BOOL
IsL'a + 'b func1 BOOL
OutR'a + 'b func1 'b
OutL'a + 'b func1 'a
InR'b func1 'a + 'b
InL'a func1 'a + 'b

Types

'1 + '2

Fixity

Infix 300:+

Definitions

IsSumRep
is_sum_rep_def turnstil exists inl inr outl outr isl isr
spot forall x1 x2 y1 y2 z
spot IsSumRep (inl x1)
and IsSumRep (inr y1)
and (IsSumRep z
implies inl (outl z) = z or inr (outr z) = z)
and (inl x1 = inl x2 equiv x1 = x2)
and (inr y1 = inr y2 equiv y1 = y2)
and not inl x1 = inr y1
and not inr y1 = inl x1
and outl (inl x1) = x1
and outr (inr y1) = y1
and (IsSumRep z implies (isl z equiv inl (outl z) = z))
and (IsSumRep z implies (isr z equiv inr (outr z) = z))
+
sum_defturnstil exists fspot TypeDefn IsSumRep f
InL
InR
OutL
OutR
IsL
IsR
sum_clauses turnstil forall x1 x2 y1 y2 z
spot (InL (OutL z) = z or InR (OutR z) = z)
and (InL x1 = InL x2 equiv x1 = x2)
and (InR y1 = InR y2 equiv y1 = y2)
and not InL x1 = InR y1
and not InR y1 = InL x1
and OutL (InL x1) = x1
and OutR (InR y1) = y1
and (IsL z equiv InL (OutL z) = z)
and (IsR z equiv InR (OutR z) = z)

Theorems

sum_cases_thm turnstil forall xspot (exists yspot x = InL y) or (exists zspot x = InR z)
sum_fns_thm turnstil forall f gspot exists1 hspot h o InL = f and h o InR = g


HOME net links © RBJ created 1999/11/02 modified 1999/11/02