The Theory sum
 Parents
 combin
 Children
 hol
 Constants
 IsSumRep 'a × 'b × BOOL → BOOL InL 'a → 'a + 'b InR 'b → 'a + 'b OutL 'a + 'b → 'a OutR 'a + 'b → 'b IsL 'a + 'b → BOOL IsR 'a + 'b → BOOL
 Types
 '1 + '2
 Fixity
 Right Infix 300: +
 Definitions
 IsSumRep is_sum_rep_def ⊢ ∃ inl inr outl outr isl isr • ∀ x1 x2 y1 y2 z • IsSumRep (inl x1) ∧ IsSumRep (inr y1) ∧ (IsSumRep z ⇒ inl (outl z) = z ∨ inr (outr z) = z) ∧ (inl x1 = inl x2 ⇔ x1 = x2) ∧ (inr y1 = inr y2 ⇔ y1 = y2) ∧ ¬ inl x1 = inr y1 ∧ ¬ inr y1 = inl x1 ∧ outl (inl x1) = x1 ∧ outr (inr y1) = y1 ∧ (IsSumRep z ⇒ (isl z ⇔ inl (outl z) = z)) ∧ (IsSumRep z ⇒ (isr z ⇔ inr (outr z) = z)) + sum_def ⊢ ∃ f• TypeDefn IsSumRep f InL InR OutL OutR IsL IsR sum_clauses ⊢ ∀ x1 x2 y1 y2 z • (InL (OutL z) = z ∨ InR (OutR z) = z) ∧ (InL x1 = InL x2 ⇔ x1 = x2) ∧ (InR y1 = InR y2 ⇔ y1 = y2) ∧ ¬ InL x1 = InR y1 ∧ ¬ InR y1 = InL x1 ∧ OutL (InL x1) = x1 ∧ OutR (InR y1) = y1 ∧ (IsL z ⇔ InL (OutL z) = z) ∧ (IsR z ⇔ InR (OutR z) = z)
 Theorems
 sum_cases_thm ⊢ ∀ x• (∃ y• x = InL y) ∨ (∃ z• x = InR z) sum_fns_thm ⊢ ∀ f g• ∃1 h• h o InL = f ∧ h o InR = g