summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | Lars Hupel <lars.hupel@mytum.de> |

Tue, 11 Jul 2017 17:22:33 +0200 | |

changeset 66270 | 403d84138c5c |

parent 66269 | 0820c8368320 |

child 66271 | d157195a468a |

State_Monad ~> Open_State_Syntax

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

src/HOL/Library/Open_State_Syntax.thy | file | annotate | diff | comparison | revisions | |

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

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

src/HOL/ROOT | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Library/Library.thy Tue Jul 11 17:11:37 2017 +0200 +++ b/src/HOL/Library/Library.thy Tue Jul 11 17:22:33 2017 +0200 @@ -48,6 +48,7 @@ Nonpos_Ints Numeral_Type Omega_Words_Fun + Open_State_Syntax Option_ord Order_Continuity Parallel @@ -70,7 +71,6 @@ Rewrite Saturated Set_Algebras - State_Monad Stirling Stream Sublist

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Open_State_Syntax.thy Tue Jul 11 17:22:33 2017 +0200 @@ -0,0 +1,151 @@ +(* Title: HOL/Library/Open_State_Syntax.thy + Author: Florian Haftmann, TU Muenchen +*) + +section \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close> + +theory Open_State_Syntax +imports Main +begin + +subsection \<open>Motivation\<close> + +text \<open> + 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>\<open>http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes + a good motivating start. Here we just sketch briefly how those + monads enter the game of Isabelle/HOL. +\<close> + +subsection \<open>State transformations and combinators\<close> + +text \<open> + We classify functions operating on states into two categories: + + \begin{description} + + \item[transformations] with type signature \<open>\<sigma> \<Rightarrow> \<sigma>'\<close>, + transforming a state. + + \item[``yielding'' transformations] with type signature \<open>\<sigma> + \<Rightarrow> \<alpha> \<times> \<sigma>'\<close>, ``yielding'' a side result while transforming a + state. + + \item[queries] with type signature \<open>\<sigma> \<Rightarrow> \<alpha>\<close>, computing a + result dependent on a state. + + \end{description} + + By convention we write \<open>\<sigma>\<close> for types representing states and + \<open>\<alpha>\<close>, \<open>\<beta>\<close>, \<open>\<gamma>\<close>, \<open>\<dots>\<close> 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 \<open>\<sigma>\<close> are used + in a single-threaded way: after application of a transformation on a + value of type \<open>\<sigma>\<close>, the former value should not be used + again. To achieve this, we use a set of monad combinators: +\<close> + +notation fcomp (infixl "\<circ>>" 60) +notation scomp (infixl "\<circ>\<rightarrow>" 60) + +text \<open> + Given two transformations @{term f} and @{term g}, they may be + directly composed using the @{term "op \<circ>>"} combinator, forming a + forward composition: @{prop "(f \<circ>> 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 \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>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} +\<close> + + +subsection \<open>Monad laws\<close> + +text \<open> + The common monadic laws hold and may also be used as normalization + rules for monadic expressions: +\<close> + +lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id + scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc + +text \<open> + Evaluation of monadic expressions by force: +\<close> + +lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta + + +subsection \<open>Do-syntax\<close> + +nonterminal sdo_binds and sdo_bind + +syntax + "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2 _)//}" [12] 62) + "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13) + "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13) + "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13) + "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_") + "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12) + +syntax (ASCII) + "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13) + +translations + "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))" + == "CONST scomp t (\<lambda>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 \<open> + For an example, see \<^file>\<open>~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy\<close>. +\<close> + +end

--- a/src/HOL/Library/State_Monad.thy Tue Jul 11 17:11:37 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,151 +0,0 @@ -(* Title: HOL/Library/State_Monad.thy - Author: Florian Haftmann, TU Muenchen -*) - -section \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close> - -theory State_Monad -imports Main -begin - -subsection \<open>Motivation\<close> - -text \<open> - 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>\<open>http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes - a good motivating start. Here we just sketch briefly how those - monads enter the game of Isabelle/HOL. -\<close> - -subsection \<open>State transformations and combinators\<close> - -text \<open> - We classify functions operating on states into two categories: - - \begin{description} - - \item[transformations] with type signature \<open>\<sigma> \<Rightarrow> \<sigma>'\<close>, - transforming a state. - - \item[``yielding'' transformations] with type signature \<open>\<sigma> - \<Rightarrow> \<alpha> \<times> \<sigma>'\<close>, ``yielding'' a side result while transforming a - state. - - \item[queries] with type signature \<open>\<sigma> \<Rightarrow> \<alpha>\<close>, computing a - result dependent on a state. - - \end{description} - - By convention we write \<open>\<sigma>\<close> for types representing states and - \<open>\<alpha>\<close>, \<open>\<beta>\<close>, \<open>\<gamma>\<close>, \<open>\<dots>\<close> 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 \<open>\<sigma>\<close> are used - in a single-threaded way: after application of a transformation on a - value of type \<open>\<sigma>\<close>, the former value should not be used - again. To achieve this, we use a set of monad combinators: -\<close> - -notation fcomp (infixl "\<circ>>" 60) -notation scomp (infixl "\<circ>\<rightarrow>" 60) - -text \<open> - Given two transformations @{term f} and @{term g}, they may be - directly composed using the @{term "op \<circ>>"} combinator, forming a - forward composition: @{prop "(f \<circ>> 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 \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>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} -\<close> - - -subsection \<open>Monad laws\<close> - -text \<open> - The common monadic laws hold and may also be used as normalization - rules for monadic expressions: -\<close> - -lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id - scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc - -text \<open> - Evaluation of monadic expressions by force: -\<close> - -lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta - - -subsection \<open>Do-syntax\<close> - -nonterminal sdo_binds and sdo_bind - -syntax - "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2 _)//}" [12] 62) - "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13) - "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13) - "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13) - "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_") - "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12) - -syntax (ASCII) - "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13) - -translations - "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))" - == "CONST scomp t (\<lambda>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 \<open> - For an example, see \<^file>\<open>~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy\<close>. -\<close> - -end

--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy Tue Jul 11 17:11:37 2017 +0200 +++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy Tue Jul 11 17:22:33 2017 +0200 @@ -6,7 +6,7 @@ subsection \<open>Extracting the program\<close> theory Higman_Extraction -imports Higman Old_Datatype "~~/src/HOL/Library/State_Monad" +imports Higman Old_Datatype "~~/src/HOL/Library/Open_State_Syntax" begin declare R.induct [ind_realizer]

--- a/src/HOL/ROOT Tue Jul 11 17:11:37 2017 +0200 +++ b/src/HOL/ROOT Tue Jul 11 17:22:33 2017 +0200 @@ -448,7 +448,7 @@ "~~/src/HOL/Library/Code_Target_Numeral" "~~/src/HOL/Library/Monad_Syntax" "~~/src/HOL/Computational_Algebra/Primes" - "~~/src/HOL/Library/State_Monad" + "~~/src/HOL/Library/Open_State_Syntax" theories Greatest_Common_Divisor Warshall