Theory "state_transformer"

Parents list

Signature

Constant	Type
BIND	:(α -> β # α) -> (β -> α -> γ # α) -> α -> γ # α
FOR	:num # num # (num -> 'state -> unit # 'state) -> 'state -> unit # 'state
FOREACH	:α list # (α -> 'state -> unit # 'state) -> 'state -> unit # 'state
IGNORE_BIND	:(α -> γ # α) -> (α -> β # α) -> α -> β # α
JOIN	:(α -> (α -> β # α) # α) -> α -> β # α
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

UNIT_DEF

|- ∀x. UNIT x = (λs. (x,s))

BIND_DEF

|- ∀g f. BIND g f = UNCURRY f o g

IGNORE_BIND_DEF

|- ∀f g. IGNORE_BIND f g = BIND f (λx. g)

MMAP_DEF

|- ∀f m. MMAP f m = BIND m (UNIT o f)

JOIN_DEF

|- ∀z. JOIN z = BIND z I

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

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

READ_def

|- ∀f. READ f = (λs. (f s,s))

WRITE_def

|- ∀f. WRITE f = (λs. ((),f s))

NARROW_def

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

WIDEN_def

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

sequence_def

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

mapM_def

|- ∀f. mapM f = sequence o MAP f

MWHILE_DEF

|- ∀g b.
     MWHILE g b =
     BIND g (λgv. if gv then IGNORE_BIND b (MWHILE g b) else UNIT ())

Theorems

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

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

BIND_LEFT_UNIT

|- ∀k x. BIND (UNIT x) k = k x

UNIT_UNCURRY

|- ∀s. UNCURRY UNIT s = s

BIND_RIGHT_UNIT

|- ∀k. BIND k UNIT = k

BIND_ASSOC

|- ∀k m n. BIND k (λa. BIND (m a) n) = BIND (BIND k m) n

MMAP_ID

|- MMAP I = I

MMAP_COMP

|- ∀f g. MMAP (f o g) = MMAP f o MMAP g

MMAP_UNIT

|- ∀f. MMAP f o UNIT = UNIT o f

MMAP_JOIN

|- ∀f. MMAP f o JOIN = JOIN o MMAP (MMAP f)

JOIN_UNIT

|- JOIN o UNIT = I

JOIN_MMAP_UNIT

|- JOIN o MMAP UNIT = I

JOIN_MAP_JOIN

|- JOIN o MMAP JOIN = JOIN o JOIN

JOIN_MAP

|- ∀k m. BIND k m = JOIN (MMAP m k)

FST_o_UNIT

|- ∀x. FST o UNIT x = K x

SND_o_UNIT

|- ∀x. SND o UNIT x = I

FST_o_MMAP

|- ∀f g. FST o MMAP f g = f o FST o g

sequence_nil

|- sequence [] = UNIT []

mapM_nil

|- mapM f [] = UNIT []

mapM_cons

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