author | haftmann |

Thu Nov 04 13:42:36 2010 +0100 (2010-11-04) | |

changeset 40359 | 84388bba911d |

parent 40358 | b6ed3364753d |

child 40360 | 1a73b5b90a3c |

dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document

src/HOL/Library/State_Monad.thy | file | annotate | diff | revisions | |

src/HOL/Proofs/Extraction/Higman.thy | file | annotate | diff | revisions |

1.1 --- a/src/HOL/Library/State_Monad.thy Thu Nov 04 13:42:36 2010 +0100 1.2 +++ b/src/HOL/Library/State_Monad.thy Thu Nov 04 13:42:36 2010 +0100 1.3 @@ -2,7 +2,7 @@ 1.4 Author: Florian Haftmann, TU Muenchen 1.5 *) 1.6 1.7 -header {* Combinator syntax for generic, open state monads (single threaded monads) *} 1.8 +header {* Combinator syntax for generic, open state monads (single-threaded monads) *} 1.9 1.10 theory State_Monad 1.11 imports Main Monad_Syntax 1.12 @@ -11,19 +11,18 @@ 1.13 subsection {* Motivation *} 1.14 1.15 text {* 1.16 - The logic HOL has no notion of constructor classes, so 1.17 - it is not possible to model monads the Haskell way 1.18 - in full genericity in Isabelle/HOL. 1.19 + The logic HOL has no notion of constructor classes, so it is not 1.20 + possible to model monads the Haskell way in full genericity in 1.21 + Isabelle/HOL. 1.22 1.23 - However, this theory provides substantial support for 1.24 - a very common class of monads: \emph{state monads} 1.25 - (or \emph{single-threaded monads}, since a state 1.26 - is transformed single-threaded). 1.27 + However, this theory provides substantial support for a very common 1.28 + class of monads: \emph{state monads} (or \emph{single-threaded 1.29 + monads}, since a state is transformed single-threadedly). 1.30 1.31 To enter from the Haskell world, 1.32 - \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} 1.33 - makes a good motivating start. Here we just sketch briefly 1.34 - how those monads enter the game of Isabelle/HOL. 1.35 + \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} makes 1.36 + a good motivating start. Here we just sketch briefly how those 1.37 + monads enter the game of Isabelle/HOL. 1.38 *} 1.39 1.40 subsection {* State transformations and combinators *} 1.41 @@ -32,64 +31,66 @@ 1.42 We classify functions operating on states into two categories: 1.43 1.44 \begin{description} 1.45 - \item[transformations] 1.46 - with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"}, 1.47 + 1.48 + \item[transformations] with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"}, 1.49 transforming a state. 1.50 - \item[``yielding'' transformations] 1.51 - with type signature @{text "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"}, 1.52 - ``yielding'' a side result while transforming a state. 1.53 - \item[queries] 1.54 - with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, 1.55 - computing a result dependent on a state. 1.56 + 1.57 + \item[``yielding'' transformations] with type signature @{text "\<sigma> 1.58 + \<Rightarrow> \<alpha> \<times> \<sigma>'"}, ``yielding'' a side result while transforming a 1.59 + state. 1.60 + 1.61 + \item[queries] with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"}, computing a 1.62 + result dependent on a state. 1.63 + 1.64 \end{description} 1.65 1.66 - By convention we write @{text "\<sigma>"} for types representing states 1.67 - and @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} 1.68 - for types representing side results. Type changes due 1.69 - to transformations are not excluded in our scenario. 1.70 + By convention we write @{text "\<sigma>"} for types representing states and 1.71 + @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} for types 1.72 + representing side results. Type changes due to transformations are 1.73 + not excluded in our scenario. 1.74 1.75 - We aim to assert that values of any state type @{text "\<sigma>"} 1.76 - are used in a single-threaded way: after application 1.77 - of a transformation on a value of type @{text "\<sigma>"}, the 1.78 - former value should not be used again. To achieve this, 1.79 - we use a set of monad combinators: 1.80 + We aim to assert that values of any state type @{text "\<sigma>"} are used 1.81 + in a single-threaded way: after application of a transformation on a 1.82 + value of type @{text "\<sigma>"}, the former value should not be used 1.83 + again. To achieve this, we use a set of monad combinators: 1.84 *} 1.85 1.86 notation fcomp (infixl "\<circ>>" 60) 1.87 notation scomp (infixl "\<circ>\<rightarrow>" 60) 1.88 1.89 -abbreviation (input) 1.90 - "return \<equiv> Pair" 1.91 - 1.92 text {* 1.93 - Given two transformations @{term f} and @{term g}, they 1.94 - may be directly composed using the @{term "op \<circ>>"} combinator, 1.95 - forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}. 1.96 + Given two transformations @{term f} and @{term g}, they may be 1.97 + directly composed using the @{term "op \<circ>>"} combinator, forming a 1.98 + forward composition: @{prop "(f \<circ>> g) s = f (g s)"}. 1.99 1.100 After any yielding transformation, we bind the side result 1.101 - immediately using a lambda abstraction. This 1.102 - is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator: 1.103 - @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}. 1.104 + immediately using a lambda abstraction. This is the purpose of the 1.105 + @{term "op \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') 1.106 + = f s in g s')"}. 1.107 1.108 For queries, the existing @{term "Let"} is appropriate. 1.109 1.110 - Naturally, a computation may yield a side result by pairing 1.111 - it to the state from the left; we introduce the 1.112 - suggestive abbreviation @{term return} for this purpose. 1.113 + Naturally, a computation may yield a side result by pairing it to 1.114 + the state from the left; we introduce the suggestive abbreviation 1.115 + @{term return} for this purpose. 1.116 1.117 - The most crucial distinction to Haskell is that we do 1.118 - not need to introduce distinguished type constructors 1.119 - for different kinds of state. This has two consequences: 1.120 + The most crucial distinction to Haskell is that we do not need to 1.121 + introduce distinguished type constructors for different kinds of 1.122 + state. This has two consequences: 1.123 + 1.124 \begin{itemize} 1.125 - \item The monad model does not state anything about 1.126 - the kind of state; the model for the state is 1.127 - completely orthogonal and may be 1.128 - specified completely independently. 1.129 - \item There is no distinguished type constructor 1.130 - encapsulating away the state transformation, i.e.~transformations 1.131 - may be applied directly without using any lifting 1.132 - or providing and dropping units (``open monad''). 1.133 + 1.134 + \item The monad model does not state anything about the kind of 1.135 + state; the model for the state is completely orthogonal and may 1.136 + be specified completely independently. 1.137 + 1.138 + \item There is no distinguished type constructor encapsulating 1.139 + away the state transformation, i.e.~transformations may be 1.140 + applied directly without using any lifting or providing and 1.141 + dropping units (``open monad''). 1.142 + 1.143 \item The type of states may change due to a transformation. 1.144 + 1.145 \end{itemize} 1.146 *} 1.147 1.148 @@ -97,8 +98,8 @@ 1.149 subsection {* Monad laws *} 1.150 1.151 text {* 1.152 - The common monadic laws hold and may also be used 1.153 - as normalization rules for monadic expressions: 1.154 + The common monadic laws hold and may also be used as normalization 1.155 + rules for monadic expressions: 1.156 *} 1.157 1.158 lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id 1.159 @@ -145,7 +146,7 @@ 1.160 "_sdo_block (_sdo_final e)" => "e" 1.161 1.162 text {* 1.163 - For an example, see HOL/Extraction/Higman.thy. 1.164 + For an example, see @{text HOL/Proofs/Extraction/Higman.thy}. 1.165 *} 1.166 1.167 end

2.1 --- a/src/HOL/Proofs/Extraction/Higman.thy Thu Nov 04 13:42:36 2010 +0100 2.2 +++ b/src/HOL/Proofs/Extraction/Higman.thy Thu Nov 04 13:42:36 2010 +0100 2.3 @@ -352,11 +352,11 @@ 2.4 function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where 2.5 "mk_word_aux k = exec { 2.6 i \<leftarrow> Random.range 10; 2.7 - (if i > 7 \<and> k > 2 \<or> k > 1000 then return [] 2.8 + (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair [] 2.9 else exec { 2.10 let l = (if i mod 2 = 0 then A else B); 2.11 ls \<leftarrow> mk_word_aux (Suc k); 2.12 - return (l # ls) 2.13 + Pair (l # ls) 2.14 })}" 2.15 by pat_completeness auto 2.16 termination by (relation "measure ((op -) 1001)") auto