# HG changeset patch # User haftmann # Date 1288874556 -3600 # Node ID 84388bba911d20d30e22b13d2f4e644d7c43f8e2 # Parent b6ed3364753d737adaa09363dce8dc8ad184c2aa dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document diff -r b6ed3364753d -r 84388bba911d src/HOL/Library/State_Monad.thy --- a/src/HOL/Library/State_Monad.thy Thu Nov 04 13:42:36 2010 +0100 +++ b/src/HOL/Library/State_Monad.thy Thu Nov 04 13:42:36 2010 +0100 @@ -2,7 +2,7 @@ Author: Florian Haftmann, TU Muenchen *) -header {* Combinator syntax for generic, open state monads (single threaded monads) *} +header {* Combinator syntax for generic, open state monads (single-threaded monads) *} theory State_Monad imports Main Monad_Syntax @@ -11,19 +11,18 @@ subsection {* 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. + 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-threaded). + 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. + \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 *} @@ -32,64 +31,66 @@ We classify functions operating on states into two categories: \begin{description} - \item[transformations] - with type signature @{text "\ \ \'"}, + + \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. + + \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. + 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: + 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 "\>" 60) notation scomp (infixl "\\" 60) -abbreviation (input) - "return \ Pair" - 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)"}. + 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')"}. + 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. + 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: + 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 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} *} @@ -97,8 +98,8 @@ subsection {* Monad laws *} text {* - The common monadic laws hold and may also be used - as normalization rules for monadic expressions: + 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 @@ -145,7 +146,7 @@ "_sdo_block (_sdo_final e)" => "e" text {* - For an example, see HOL/Extraction/Higman.thy. + For an example, see @{text HOL/Proofs/Extraction/Higman.thy}. *} end diff -r b6ed3364753d -r 84388bba911d src/HOL/Proofs/Extraction/Higman.thy --- a/src/HOL/Proofs/Extraction/Higman.thy Thu Nov 04 13:42:36 2010 +0100 +++ b/src/HOL/Proofs/Extraction/Higman.thy Thu Nov 04 13:42:36 2010 +0100 @@ -352,11 +352,11 @@ function mk_word_aux :: "nat \ Random.seed \ letter list \ Random.seed" where "mk_word_aux k = exec { i \ Random.range 10; - (if i > 7 \ k > 2 \ k > 1000 then return [] + (if i > 7 \ k > 2 \ k > 1000 then Pair [] else exec { let l = (if i mod 2 = 0 then A else B); ls \ mk_word_aux (Suc k); - return (l # ls) + Pair (l # ls) })}" by pat_completeness auto termination by (relation "measure ((op -) 1001)") auto