--- 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