Theory "state_transformer"

Parents list

Signature

Constant	Type
BIND	:(α -> β # α) -> (β -> α -> γ # α) -> α -> γ # α
EXT	:(β -> σ -> γ # σ) -> (σ -> β # σ) -> σ -> γ # σ
FOR	:num # num # (num -> 'state -> unit # 'state) -> 'state -> unit # 'state
FOREACH	:α list # (α -> 'state -> unit # 'state) -> 'state -> unit # 'state
IGNORE_BIND	:(α -> γ # α) -> (α -> β # α) -> α -> β # α
JOIN	:(α -> (α -> β # α) # α) -> α -> β # α
MCOMP	:(β -> σ -> γ # σ) -> (α -> σ -> β # σ) -> α -> σ -> γ # σ
MMAP	:(γ -> β) -> (α -> γ # α) -> α -> β # α
MWHILE	:(α -> bool # α) -> (α -> β # α) -> α -> unit # α
NARROW	:β -> (β # 'state -> α # β # 'state) -> 'state -> α # 'state
READ	:('state -> α) -> 'state -> α # 'state
UNIT	:β -> α -> β # α
WIDEN	:('state -> α # 'state) -> β # 'state -> α # β # 'state
WRITE	:('state -> 'state) -> 'state -> unit # 'state
mapM	:(α -> β -> γ # β) -> α list -> β -> γ list # β
sequence	:(α -> β # α) list -> α -> β list # α

Definitions

BIND_DEF

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

EXT_DEF

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

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

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

IGNORE_BIND_DEF

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

JOIN_DEF

⊢ ∀z. JOIN z = monad_bind z I

MCOMP_DEF

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

MMAP_DEF

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

MWHILE_DEF

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

NARROW_def

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

READ_def

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

UNIT_DEF

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

WIDEN_def

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

WRITE_def

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

mapM_def

⊢ ∀f. mapM f = sequence ∘ MAP f

sequence_def

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

Theorems

BIND_ASSOC

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

BIND_EXT

⊢ monad_bind m f = EXT f m

BIND_LEFT_UNIT

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

BIND_RIGHT_UNIT

⊢ ∀k. monad_bind k UNIT = k

EXT_JM

⊢ EXT f = JOIN ∘ MMAP f

EXT_MCOMP

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

EXT_UNIT

⊢ EXT UNIT = I

EXT_o_JOIN

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

EXT_o_UNIT

⊢ EXT f ∘ UNIT = f

FOREACH_def

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

FOREACH_ind

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

FOR_def

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

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)

FST_o_MMAP

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

FST_o_UNIT

⊢ ∀x. FST ∘ UNIT x = K x

JOIN_EXT

⊢ JOIN = EXT I

JOIN_MAP

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

JOIN_MAP_JOIN

⊢ JOIN ∘ MMAP JOIN = JOIN ∘ JOIN

JOIN_MMAP_UNIT

⊢ JOIN ∘ MMAP UNIT = I

JOIN_UNIT

⊢ JOIN ∘ UNIT = I

MCOMP_ALT

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

MCOMP_ASSOC

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

MCOMP_ID

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

MMAP_COMP

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

MMAP_EXT

⊢ MMAP f = EXT (UNIT ∘ f)

MMAP_ID

⊢ MMAP I = I

MMAP_JOIN

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

MMAP_UNIT

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

SND_o_UNIT

⊢ ∀x. SND ∘ UNIT x = I

UNIT_CURRY

⊢ UNIT = CURRY I

UNIT_UNCURRY

⊢ ∀s. UNITᴾ s = s

UNIT_o_MCOMP

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

mapM_cons

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

mapM_nil

⊢ mapM f [] = UNIT []

sequence_nil

⊢ sequence [] = UNIT []