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
fill• ∀ x1 x2 y1 y2 z
fill• IsSumRep (inl x1)
fill∧ IsSumRep (inr y1)
fill∧ (IsSumRep z
fill⇒ inl (outl z) = z ∨ inr (outr z) = z)
fill∧ (inl x1 = inl x2 ⇔ x1 = x2)
fill∧ (inr y1 = inr y2 ⇔ y1 = y2)
fill∧ ¬ inl x1 = inr y1
fill∧ ¬ inr y1 = inl x1
fill∧ outl (inl x1) = x1
fill∧ outr (inr y1) = y1
fill∧ (IsSumRep z ⇒ (isl z ⇔ inl (outl z) = z))
fill∧ (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
fill• (InL (OutL z) = z ∨ InR (OutR z) = z)
fill∧ (InL x1 = InL x2 ⇔ x1 = x2)
fill∧ (InR y1 = InR y2 ⇔ y1 = y2)
fill∧ ¬ InL x1 = InR y1
fill∧ ¬ InR y1 = InL x1
fill∧ OutL (InL x1) = x1
fill∧ OutR (InR y1) = y1
fill∧ (IsL z ⇔ InL (OutL z) = z)
fill∧ (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

up quick index

privacy policy

Created:

V