(*  Title:      HOL/Library/State_Monad.thy
Author:     Florian Haftmann, TU Muenchen
*)

begin

subsection ‹Motivation›

text ‹
The logic HOL has no notion of constructor classes, so it is not
Isabelle/HOL.

However, this theory provides substantial support for a very common

To enter from the Haskell world,
a good motivating start.  Here we just sketch briefly how those
monads enter the game of Isabelle/HOL.
›

subsection ‹State transformations and combinators›

text ‹
We classify functions operating on states into two categories:

\begin{description}

\item[transformations] with type signature ‹σ ⇒ σ'›,
transforming a state.

\item[yielding'' transformations] with type signature ‹σ
⇒ α × σ'›, yielding'' a side result while transforming a
state.

\item[queries] with type signature ‹σ ⇒ α›, computing a
result dependent on a state.

\end{description}

By convention we write ‹σ› for types representing states and
‹α›, ‹β›, ‹γ›, ‹…› for types
representing side results.  Type changes due to transformations are
not excluded in our scenario.

We aim to assert that values of any state type ‹σ› are used
in a single-threaded way: after application of a transformation on a
value of type ‹σ›, the former value should not be used
again.  To achieve this, we use a set of monad combinators:
›

notation fcomp (infixl "∘>" 60)
notation scomp (infixl "∘→" 60)

text ‹
Given two transformations @{term f} and @{term g}, they may be
directly composed using the @{term "op ∘>"} combinator, forming a
forward composition: @{prop "(f ∘> g) s = f (g s)"}.

After any yielding transformation, we bind the side result
immediately using a lambda abstraction.  This is the purpose of the
@{term "op ∘→"} combinator: @{prop "(f ∘→ (λx. g)) s = (let (x, s')
= f s in g s')"}.

For queries, the existing @{term "Let"} is appropriate.

Naturally, a computation may yield a side result by pairing it to
the state from the left; we introduce the suggestive abbreviation
@{term return} for this purpose.

The most crucial distinction to Haskell is that we do not need to
introduce distinguished type constructors for different kinds of
state.  This has two consequences:

\begin{itemize}

\item The monad model does not state anything about the kind of
state; the model for the state is completely orthogonal and may
be specified completely independently.

\item There is no distinguished type constructor encapsulating
away the state transformation, i.e.~transformations may be
applied directly without using any lifting or providing and
dropping units (open monad'').

\item The type of states may change due to a transformation.

\end{itemize}
›

text ‹
The common monadic laws hold and may also be used as normalization
›

lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc

text ‹
Evaluation of monadic expressions by force:
›

subsection ‹Do-syntax›

nonterminal sdo_binds and sdo_bind

syntax
"_sdo_block" :: "sdo_binds ⇒ 'a" ("exec {//(2  _)//}" [12] 62)
"_sdo_bind"  :: "[pttrn, 'a] ⇒ sdo_bind" ("(_ ←/ _)" 13)
"_sdo_let" :: "[pttrn, 'a] ⇒ sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
"_sdo_then" :: "'a ⇒ sdo_bind" ("_" [14] 13)
"_sdo_final" :: "'a ⇒ sdo_binds" ("_")
"_sdo_cons" :: "[sdo_bind, sdo_binds] ⇒ sdo_binds" ("_;//_" [13, 12] 12)

syntax (ASCII)
"_sdo_bind" :: "[pttrn, 'a] ⇒ sdo_bind" ("(_ <-/ _)" 13)

translations
"_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
== "CONST scomp t (λp. e)"
"_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
=> "CONST fcomp t e"
"_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))"
<= "_sdo_final (CONST fcomp t e)"
"_sdo_block (_sdo_cons (_sdo_then t) e)"
<= "CONST fcomp t (_sdo_block e)"
"_sdo_block (_sdo_cons (_sdo_let p t) bs)"
== "let p = t in _sdo_block bs"
"_sdo_block (_sdo_cons b (_sdo_cons c cs))"
== "_sdo_block (_sdo_cons b (_sdo_final (_sdo_block (_sdo_cons c cs))))"
"_sdo_cons (_sdo_let p t) (_sdo_final s)"
== "_sdo_final (let p = t in s)"
"_sdo_block (_sdo_final e)" => "e"

text ‹
For an example, see 🗏‹~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy›.
›

end