(*  Title:      HOL/Library/State_Monad.thy    Author:     Florian Haftmann, TU Muenchen*)header {* Combinator syntax for generic, open state monads (single-threaded monads) *}theory State_Monadimports Main Monad_Syntaxbeginsubsection {* Motivation *}text {*  The logic HOL has no notion of constructor classes, so it is not  possible to model monads the Haskell way in full genericity in  Isabelle/HOL.    However, this theory provides substantial support for a very common  class of monads: \emph{state monads} (or \emph{single-threaded  monads}, since a state is transformed single-threadedly).  To enter from the Haskell world,  \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} makes  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 @{text "σ => σ'"},      transforming a state.    \item[yielding'' transformations] with type signature @{text "σ      => α × σ'"}, yielding'' a side result while transforming a      state.    \item[queries] with type signature @{text "σ => α"}, computing a      result dependent on a state.  \end{description}  By convention we write @{text "σ"} for types representing states and  @{text "α"}, @{text "β"}, @{text "γ"}, @{text "…"} 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 @{text "σ"} are used  in a single-threaded way: after application of a transformation on a  value of type @{text "σ"}, the former value should not be used  again.  To achieve this, we use a set of monad combinators:*}notation fcomp (infixl "o>" 60)notation scomp (infixl "o->" 60)text {*  Given two transformations @{term f} and @{term g}, they may be  directly composed using the @{term "op o>"} combinator, forming a  forward composition: @{prop "(f o> 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 o->"} combinator: @{prop "(f o-> (λ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}*}subsection {* Monad laws *}text {*  The common monadic laws hold and may also be used as normalization  rules for monadic expressions:*}lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id  scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoctext {*  Evaluation of monadic expressions by force:*}lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_betasubsection {* Do-syntax *}nonterminal sdo_binds and sdo_bindsyntax  "_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 (xsymbols)  "_sdo_bind"  :: "[pttrn, 'a] => sdo_bind" ("(_ \<leftarrow>/ _)" 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 @{text "HOL/Proofs/Extraction/Higman.thy"}.*}end