# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1499786553 -7200
# Node ID 403d84138c5c5ab5877802bfaec33031e168a893
# Parent  0820c83683203fa81cdef956387c0389c6c2b8d2
State_Monad ~> Open_State_Syntax

diff -r 0820c8368320 -r 403d84138c5c src/HOL/Library/Library.thy
--- 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
diff -r 0820c8368320 -r 403d84138c5c src/HOL/Library/Open_State_Syntax.thy
--- /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
diff -r 0820c8368320 -r 403d84138c5c src/HOL/Library/State_Monad.thy
--- 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
diff -r 0820c8368320 -r 403d84138c5c src/HOL/Proofs/Extraction/Higman_Extraction.thy
--- 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]
diff -r 0820c8368320 -r 403d84138c5c src/HOL/ROOT
--- 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