Theory state_transformer

⊢ ∀g f. monad_bind g f = UNCURRY f ∘ g

⊢ ∀f m. EXT f m = UNCURRY f ∘ m

⊢ 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 do u <- a h; FOREACH (t,a) od)

⊢ 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
                  do u <- a i; FOR (if i < j then i + 1 else i − 1,j,a) od))

⊢ ∀f g. do f; g od = do x <- f; g od

⊢ ∀z. JOIN z = monad_bind z I

⊢ ∀g f. MCOMP g f = EXT g ∘ f

⊢ ∀f m. MMAP f m = monad_bind m (UNIT ∘ f)

⊢ ∀g b.
    MWHILE g b = do gv <- g; if gv then do b; MWHILE g b od else UNIT () od

⊢ ∀v f. NARROW v f = (λs. (let (r,s1) = f (v,s) in (r,SND s1)))

⊢ ∀f. READ f = (λs. (f s,s))

⊢ ∀x. UNIT x = (λs. (x,s))

⊢ ∀f. WIDEN f = (λ(s1,s2). (let (r,s3) = f s2 in (r,s1,s3)))

⊢ ∀f. WRITE f = (λs. ((),f s))

⊢ ∀f. mapM f = sequence ∘ MAP f

⊢ sequence = FOLDR (λm ms. do x <- m; xs <- ms; UNIT (x::xs) od) (UNIT [])

⊢ ∀k m n. do a <- k; monad_bind (m a) n od = monad_bind (monad_bind k m) n

⊢ monad_bind m f = EXT f m

⊢ ∀k x. monad_bind (UNIT x) k = k x

⊢ ∀k. monad_bind k UNIT = k

⊢ EXT f = JOIN ∘ MMAP f

⊢ EXT (MCOMP g f) = EXT g ∘ EXT f

⊢ EXT UNIT = I

⊢ ∀f. EXT f ∘ JOIN = EXT (EXT f)

⊢ EXT f ∘ UNIT = f

⊢ (∀a. FOREACH ([],a) = UNIT ()) ∧
  ∀t h a. FOREACH (h::t,a) = do u <- a h; FOREACH (t,a) od

⊢ ∀P. (∀a. P ([],a)) ∧ (∀h t a. P (t,a) ⇒ P (h::t,a)) ⇒ ∀v v1. P (v,v1)

⊢ ∀j i a.
    FOR (i,j,a) =
    if i = j then a i
    else do u <- a i; FOR (if i < j then i + 1 else i − 1,j,a) od

⊢ ∀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)

⊢ ∀f g. FST ∘ MMAP f g = f ∘ FST ∘ g

⊢ ∀x. FST ∘ UNIT x = K x

⊢ JOIN = EXT I

⊢ ∀k m. monad_bind k m = JOIN (MMAP m k)

⊢ JOIN ∘ MMAP JOIN = JOIN ∘ JOIN

⊢ JOIN ∘ MMAP UNIT = I

⊢ JOIN ∘ UNIT = I

⊢ MCOMP g f = CURRY (UNCURRY g ∘ UNCURRY f)

⊢ MCOMP f (MCOMP g h) = MCOMP (MCOMP f g) h

⊢ MCOMP g UNIT = g ∧ MCOMP UNIT f = f

⊢ ∀f g. MMAP (f ∘ g) = MMAP f ∘ MMAP g

⊢ MMAP f = EXT (UNIT ∘ f)

⊢ MMAP I = I

⊢ ∀f. MMAP f ∘ JOIN = JOIN ∘ MMAP (MMAP f)

⊢ ∀f. MMAP f ∘ UNIT = UNIT ∘ f

⊢ ∀x. SND ∘ UNIT x = I

⊢ UNIT = CURRY I

⊢ ∀s. UNCURRY UNIT s = s

⊢ MCOMP (UNIT ∘ g) (UNIT ∘ f) = UNIT ∘ g ∘ f

⊢ mapM f (x::xs) = do y <- f x; ys <- mapM f xs; UNIT (y::ys) od

⊢ mapM f [] = UNIT []

⊢ sequence [] = UNIT []