Theory errorStateMonad

⊢ ∀g f s0. BIND g f s0 = case g s0 of NONE => NONE | SOME (b,s) => f b s

⊢ ∀fM xM. fM <*> xM = BIND fM (λf. BIND xM (λx. UNIT (f x)))

⊢ ∀xM yM s.
    ES_CHOICE xM yM s = case xM s of NONE => yM s | SOME v1 => SOME v1

⊢ ∀s. ES_FAIL s = NONE

⊢ ∀b. ES_GUARD b = if b then UNIT () else ES_FAIL

⊢ ∀f xM yM. ES_LIFT2 f xM yM = MMAP f xM <*> yM

⊢ ∀g m. EXT g m = BIND m g

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

⊢ ∀f g. IGNORE_BIND f g = BIND f (λx. g)

⊢ ∀z. JOIN z = BIND z I

⊢ ∀g f. MCOMP g f = CURRY (OPTION_MCOMP (UNCURRY g) (UNCURRY f))

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

⊢ ∀P g x s.
    MWHILE P g x s =
    BIND (P x) (λb. if b then BIND (g x) (MWHILE P g) else UNIT x) s

⊢ ∀P g s.
    MWHILE_UNIT P g s =
    BIND P (λb. if b then IGNORE_BIND g (MWHILE_UNIT P g) else UNIT ()) s

⊢ ∀v f.
    NARROW v f =
    (λs. case f (v,s) of NONE => NONE | SOME (r,s1) => SOME (r,SND s1))

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

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

⊢ ∀f. WIDEN f =
      (λ(s1,s2). case f s2 of NONE => NONE | SOME (r,s3) => SOME (r,s1,s3))

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

⊢ ∀f. mapM f = sequence ∘ MAP f

⊢ (∀P g x s. mwhile_step P g x 0 s = BIND (P x) (λb. UNIT (b,x)) s) ∧
  ∀P g x n s.
    mwhile_step P g x (SUC n) s =
    BIND (P x)
      (λb. if b then BIND (g x) (λgx. mwhile_step P g gx n) else UNIT (b,x))
      s

⊢ (∀P g s. mwhile_unit_step P g 0 s = P s) ∧
  ∀P g n s.
    mwhile_unit_step P g (SUC n) s =
    BIND P
      (λb. if b then IGNORE_BIND g (mwhile_unit_step P g n) else UNIT b) s

⊢ sequence =
  FOLDR (λm ms. BIND m (λx. BIND ms (λxs. UNIT (x::xs)))) (UNIT [])

⊢ UNIT f <*> xM = MMAP f xM

⊢ UNIT f <*> UNIT x = UNIT (f x)

⊢ ∀k m n. BIND k (λa. BIND (m a) n) = BIND (BIND k m) n

⊢ BIND (ES_GUARD F) fM = ES_FAIL ∧ BIND (ES_GUARD T) fM = fM ()

⊢ BIND ES_FAIL fM = ES_FAIL

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

⊢ ∀k. BIND k UNIT = k

⊢ ES_CHOICE xM (ES_CHOICE yM zM) = ES_CHOICE (ES_CHOICE xM yM) zM

⊢ ES_CHOICE ES_FAIL xM = xM

⊢ ES_CHOICE xM ES_FAIL = xM

⊢ (∀a. FOREACH ([],a) = UNIT ()) ∧
  ∀t h a. FOREACH (h::t,a) = BIND (a h) (λu. FOREACH (t,a))

⊢ ∀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 BIND (a i) (λu. FOR (if i < j then i + 1 else i − 1,j,a))

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

⊢ IGNORE_BIND (ES_GUARD F) xM = ES_FAIL ∧ IGNORE_BIND (ES_GUARD T) xM = xM

⊢ IGNORE_BIND ES_FAIL xM = ES_FAIL ∧ IGNORE_BIND xM ES_FAIL = ES_FAIL

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

⊢ JOIN ∘ MMAP JOIN = JOIN ∘ JOIN

⊢ JOIN ∘ MMAP UNIT = I

⊢ JOIN ∘ UNIT = I

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

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

⊢ MCOMP g f = EXT g ∘ f

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

⊢ MMAP I = I

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

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

⊢ UNIT = CURRY SOME

⊢ mapM f (x::xs) = BIND (f x) (λy. BIND (mapM f xs) (λys. UNIT (y::ys)))

⊢ mapM f [] = UNIT []

⊢ (∀P g x s. mwhile_step P g x 0 s = BIND (P x) (λb. UNIT (b,x)) s) ∧
  (∀P g x n s.
     mwhile_step P g x (NUMERAL (BIT1 n)) s =
     BIND (P x)
       (λb.
            if b then
              BIND (g x) (λgx. mwhile_step P g gx (NUMERAL (BIT1 n) − 1))
            else UNIT (b,x)) s) ∧
  ∀P g x n s.
    mwhile_step P g x (NUMERAL (BIT2 n)) s =
    BIND (P x)
      (λb.
           if b then
             BIND (g x) (λgx. mwhile_step P g gx (NUMERAL (BIT1 n)))
           else UNIT (b,x)) s

⊢ (∀P g s. mwhile_unit_step P g 0 s = P s) ∧
  (∀P g n s.
     mwhile_unit_step P g (NUMERAL (BIT1 n)) s =
     BIND P
       (λb.
            if b then
              IGNORE_BIND g (mwhile_unit_step P g (NUMERAL (BIT1 n) − 1))
            else UNIT b) s) ∧
  ∀P g n s.
    mwhile_unit_step P g (NUMERAL (BIT2 n)) s =
    BIND P
      (λb.
           if b then
             IGNORE_BIND g (mwhile_unit_step P g (NUMERAL (BIT1 n)))
           else UNIT b) s

⊢ sequence [] = UNIT []