- WRITE_def
-
⊢ ∀f. WRITE f = (λs. SOME ((),f s))
- WIDEN_def
-
⊢ ∀f.
WIDEN f =
(λ(s1,s2). case f s2 of NONE => NONE | SOME (r,s3) => SOME (r,s1,s3))
- UNIT_DEF
-
⊢ ∀x. UNIT x = (λs. SOME (x,s))
- sequence_def
-
⊢ sequence = FOLDR (λm ms. BIND m (λx. BIND ms (λxs. UNIT (x::xs)))) (UNIT [])
- READ_def
-
⊢ ∀f. READ f = (λs. SOME (f s,s))
- NARROW_def
-
⊢ ∀v f.
NARROW v f =
(λs. case f (v,s) of NONE => NONE | SOME (r,s1) => SOME (r,SND s1))
- MMAP_DEF
-
⊢ ∀f m. MMAP f m = BIND m (UNIT ∘ f)
- MCOMP_DEF
-
⊢ ∀g f. MCOMP g f = CURRY (OPTION_MCOMP (UNCURRY g) (UNCURRY f))
- mapM_def
-
⊢ ∀f. mapM f = sequence ∘ MAP f
- JOIN_DEF
-
⊢ ∀z. JOIN z = BIND z I
- IGNORE_BIND_DEF
-
⊢ ∀f g. IGNORE_BIND f g = BIND f (λx. g)
- FOREACH_primitive_def
-
⊢ FOREACH =
WFREC (@R. WF R ∧ ∀h a t. R (t,a) (h::t,a))
(λFOREACH a'.
case a' of
([],a) => I (UNIT ())
| (h::t,a) => I (BIND (a h) (λu. FOREACH (t,a))))
- FOR_primitive_def
-
⊢ FOR =
WFREC
(@R. WF R ∧ ∀a j i. i ≠ j ⇒ R (if i < j then i + 1 else i − 1,j,a) (i,j,a))
(λFOR a'.
case a' of
(i,j,a) =>
I
(if i = j then a i
else BIND (a i) (λu. FOR (if i < j then i + 1 else i − 1,j,a))))
- EXT_DEF
-
⊢ ∀g m. EXT g m = BIND m g
- ES_LIFT2_DEF
-
⊢ ∀f xM yM. ES_LIFT2 f xM yM = MMAP f xM <*> yM
- ES_GUARD_DEF
-
⊢ ∀b. ES_GUARD b = if b then UNIT () else ES_FAIL
- ES_FAIL_DEF
-
⊢ ∀s. ES_FAIL s = NONE
- ES_CHOICE_DEF
-
⊢ ∀xM yM s. ES_CHOICE xM yM s = case xM s of NONE => yM s | SOME v1 => SOME v1
- ES_APPLY_DEF
-
⊢ ∀fM xM. fM <*> xM = BIND fM (λf. BIND xM (λx. UNIT (f x)))
- BIND_DEF
-
⊢ ∀g f s0. BIND g f s0 = case g s0 of NONE => NONE | SOME (b,s) => f b s
- UNIT_CURRY
-
⊢ UNIT = CURRY SOME
- sequence_nil
-
⊢ sequence [] = UNIT []
- MMAP_UNIT
-
⊢ ∀f. MMAP f ∘ UNIT = UNIT ∘ f
- MMAP_JOIN
-
⊢ ∀f. MMAP f ∘ JOIN = JOIN ∘ MMAP (MMAP f)
- MMAP_ID
-
⊢ MMAP I = I
- MMAP_COMP
-
⊢ ∀f g. MMAP (f ∘ g) = MMAP f ∘ MMAP g
- MCOMP_THM
-
⊢ MCOMP g f = EXT g ∘ f
- MCOMP_ID
-
⊢ (MCOMP g UNIT = g) ∧ (MCOMP UNIT f = f)
- MCOMP_ASSOC
-
⊢ MCOMP f (MCOMP g h) = MCOMP (MCOMP f g) h
- mapM_nil
-
⊢ mapM f [] = UNIT []
- mapM_cons
-
⊢ mapM f (x::xs) = BIND (f x) (λy. BIND (mapM f xs) (λys. UNIT (y::ys)))
- JOIN_UNIT
-
⊢ JOIN ∘ UNIT = I
- JOIN_MMAP_UNIT
-
⊢ JOIN ∘ MMAP UNIT = I
- JOIN_MAP_JOIN
-
⊢ JOIN ∘ MMAP JOIN = JOIN ∘ JOIN
- JOIN_MAP
-
⊢ ∀k m. BIND k m = JOIN (MMAP m k)
- IGNORE_BIND_FAIL
-
⊢ (IGNORE_BIND ES_FAIL xM = ES_FAIL) ∧ (IGNORE_BIND xM ES_FAIL = ES_FAIL)
- IGNORE_BIND_ESGUARD
-
⊢ (IGNORE_BIND (ES_GUARD F) xM = ES_FAIL) ∧ (IGNORE_BIND (ES_GUARD T) xM = xM)
- FOREACH_ind
-
⊢ ∀P. (∀a. P ([],a)) ∧ (∀h t a. P (t,a) ⇒ P (h::t,a)) ⇒ ∀v v1. P (v,v1)
- FOREACH_def
-
⊢ (∀a. FOREACH ([],a) = UNIT ()) ∧
∀t h a. FOREACH (h::t,a) = BIND (a h) (λu. FOREACH (t,a))
- FOR_ind
-
⊢ ∀P.
(∀i j a. (i ≠ j ⇒ P (if i < j then i + 1 else i − 1,j,a)) ⇒ P (i,j,a)) ⇒
∀v v1 v2. P (v,v1,v2)
- FOR_def
-
⊢ ∀j i a.
FOR (i,j,a) =
if i = j then a i
else BIND (a i) (λu. FOR (if i < j then i + 1 else i − 1,j,a))
- ES_CHOICE_FAIL_RID
-
⊢ ES_CHOICE xM ES_FAIL = xM
- ES_CHOICE_FAIL_LID
-
⊢ ES_CHOICE ES_FAIL xM = xM
- ES_CHOICE_ASSOC
-
⊢ ES_CHOICE xM (ES_CHOICE yM zM) = ES_CHOICE (ES_CHOICE xM yM) zM
- BIND_RIGHT_UNIT
-
⊢ ∀k. BIND k UNIT = k
- BIND_LEFT_UNIT
-
⊢ ∀k x. BIND (UNIT x) k = k x
- BIND_FAIL_L
-
⊢ BIND ES_FAIL fM = ES_FAIL
- BIND_ESGUARD
-
⊢ (BIND (ES_GUARD F) fM = ES_FAIL) ∧ (BIND (ES_GUARD T) fM = fM ())
- BIND_ASSOC
-
⊢ ∀k m n. BIND k (λa. BIND (m a) n) = BIND (BIND k m) n
- APPLY_UNIT_UNIT
-
⊢ UNIT f <*> UNIT x = UNIT (f x)
- APPLY_UNIT
-
⊢ UNIT f <*> xM = MMAP f xM