src/HOL/Library/Open_State_Syntax.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (19 months ago)
changeset 67951 655aa11359dc
parent 67399 eab6ce8368fa
child 68224 1f7308050349
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
lars@66270
     1
(*  Title:      HOL/Library/Open_State_Syntax.thy
haftmann@21192
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@21192
     3
*)
haftmann@21192
     4
wenzelm@60500
     5
section \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close>
haftmann@21192
     6
lars@66270
     7
theory Open_State_Syntax
haftmann@66258
     8
imports Main
haftmann@21192
     9
begin
haftmann@21192
    10
wenzelm@60500
    11
subsection \<open>Motivation\<close>
haftmann@21192
    12
wenzelm@60500
    13
text \<open>
haftmann@40359
    14
  The logic HOL has no notion of constructor classes, so it is not
haftmann@40359
    15
  possible to model monads the Haskell way in full genericity in
haftmann@40359
    16
  Isabelle/HOL.
haftmann@21192
    17
  
haftmann@40359
    18
  However, this theory provides substantial support for a very common
haftmann@40359
    19
  class of monads: \emph{state monads} (or \emph{single-threaded
haftmann@40359
    20
  monads}, since a state is transformed single-threadedly).
haftmann@21192
    21
haftmann@21192
    22
  To enter from the Haskell world,
wenzelm@63680
    23
  \<^url>\<open>http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes
haftmann@40359
    24
  a good motivating start.  Here we just sketch briefly how those
haftmann@40359
    25
  monads enter the game of Isabelle/HOL.
wenzelm@60500
    26
\<close>
haftmann@21192
    27
wenzelm@60500
    28
subsection \<open>State transformations and combinators\<close>
haftmann@21192
    29
wenzelm@60500
    30
text \<open>
haftmann@21192
    31
  We classify functions operating on states into two categories:
haftmann@21192
    32
haftmann@21192
    33
  \begin{description}
haftmann@40359
    34
wenzelm@61585
    35
    \item[transformations] with type signature \<open>\<sigma> \<Rightarrow> \<sigma>'\<close>,
haftmann@21192
    36
      transforming a state.
haftmann@40359
    37
wenzelm@61585
    38
    \item[``yielding'' transformations] with type signature \<open>\<sigma>
wenzelm@61585
    39
      \<Rightarrow> \<alpha> \<times> \<sigma>'\<close>, ``yielding'' a side result while transforming a
haftmann@40359
    40
      state.
haftmann@40359
    41
wenzelm@61585
    42
    \item[queries] with type signature \<open>\<sigma> \<Rightarrow> \<alpha>\<close>, computing a
haftmann@40359
    43
      result dependent on a state.
haftmann@40359
    44
haftmann@21192
    45
  \end{description}
haftmann@21192
    46
wenzelm@61585
    47
  By convention we write \<open>\<sigma>\<close> for types representing states and
wenzelm@61585
    48
  \<open>\<alpha>\<close>, \<open>\<beta>\<close>, \<open>\<gamma>\<close>, \<open>\<dots>\<close> for types
haftmann@40359
    49
  representing side results.  Type changes due to transformations are
haftmann@40359
    50
  not excluded in our scenario.
haftmann@21192
    51
wenzelm@61585
    52
  We aim to assert that values of any state type \<open>\<sigma>\<close> are used
haftmann@40359
    53
  in a single-threaded way: after application of a transformation on a
wenzelm@61585
    54
  value of type \<open>\<sigma>\<close>, the former value should not be used
haftmann@40359
    55
  again.  To achieve this, we use a set of monad combinators:
wenzelm@60500
    56
\<close>
haftmann@21192
    57
haftmann@37751
    58
notation fcomp (infixl "\<circ>>" 60)
haftmann@37817
    59
notation scomp (infixl "\<circ>\<rightarrow>" 60)
wenzelm@21404
    60
wenzelm@60500
    61
text \<open>
haftmann@40359
    62
  Given two transformations @{term f} and @{term g}, they may be
nipkow@67399
    63
  directly composed using the @{term "(\<circ>>)"} combinator, forming a
haftmann@40359
    64
  forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
haftmann@21192
    65
haftmann@21192
    66
  After any yielding transformation, we bind the side result
haftmann@40359
    67
  immediately using a lambda abstraction.  This is the purpose of the
nipkow@67399
    68
  @{term "(\<circ>\<rightarrow>)"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s')
haftmann@40359
    69
  = f s in g s')"}.
haftmann@21192
    70
haftmann@21192
    71
  For queries, the existing @{term "Let"} is appropriate.
haftmann@21192
    72
haftmann@40359
    73
  Naturally, a computation may yield a side result by pairing it to
haftmann@40359
    74
  the state from the left; we introduce the suggestive abbreviation
haftmann@40359
    75
  @{term return} for this purpose.
haftmann@21192
    76
haftmann@40359
    77
  The most crucial distinction to Haskell is that we do not need to
haftmann@40359
    78
  introduce distinguished type constructors for different kinds of
haftmann@40359
    79
  state.  This has two consequences:
haftmann@40359
    80
haftmann@21192
    81
  \begin{itemize}
haftmann@40359
    82
haftmann@40359
    83
    \item The monad model does not state anything about the kind of
haftmann@40359
    84
       state; the model for the state is completely orthogonal and may
haftmann@40359
    85
       be specified completely independently.
haftmann@40359
    86
haftmann@40359
    87
    \item There is no distinguished type constructor encapsulating
haftmann@40359
    88
       away the state transformation, i.e.~transformations may be
haftmann@40359
    89
       applied directly without using any lifting or providing and
haftmann@40359
    90
       dropping units (``open monad'').
haftmann@40359
    91
haftmann@21192
    92
    \item The type of states may change due to a transformation.
haftmann@40359
    93
haftmann@21192
    94
  \end{itemize}
wenzelm@60500
    95
\<close>
haftmann@21192
    96
haftmann@21192
    97
wenzelm@60500
    98
subsection \<open>Monad laws\<close>
haftmann@21192
    99
wenzelm@60500
   100
text \<open>
haftmann@40359
   101
  The common monadic laws hold and may also be used as normalization
haftmann@40359
   102
  rules for monadic expressions:
wenzelm@60500
   103
\<close>
haftmann@21192
   104
haftmann@28145
   105
lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
haftmann@28145
   106
  scomp_scomp scomp_fcomp fcomp_scomp fcomp_assoc
haftmann@21192
   107
wenzelm@60500
   108
text \<open>
haftmann@21192
   109
  Evaluation of monadic expressions by force:
wenzelm@60500
   110
\<close>
haftmann@21192
   111
haftmann@28145
   112
lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
haftmann@26260
   113
haftmann@37817
   114
wenzelm@60500
   115
subsection \<open>Do-syntax\<close>
haftmann@37817
   116
wenzelm@41229
   117
nonterminal sdo_binds and sdo_bind
haftmann@37932
   118
haftmann@37932
   119
syntax
haftmann@37932
   120
  "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
wenzelm@61955
   121
  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
haftmann@37932
   122
  "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
haftmann@37932
   123
  "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13)
haftmann@37932
   124
  "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_")
haftmann@37932
   125
  "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12)
haftmann@21192
   126
wenzelm@61955
   127
syntax (ASCII)
wenzelm@61955
   128
  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
haftmann@37932
   129
haftmann@37932
   130
translations
haftmann@37932
   131
  "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
haftmann@37932
   132
    == "CONST scomp t (\<lambda>p. e)"
haftmann@37932
   133
  "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
haftmann@38345
   134
    => "CONST fcomp t e"
haftmann@38345
   135
  "_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))"
haftmann@38345
   136
    <= "_sdo_final (CONST fcomp t e)"
haftmann@38345
   137
  "_sdo_block (_sdo_cons (_sdo_then t) e)"
haftmann@38345
   138
    <= "CONST fcomp t (_sdo_block e)"
haftmann@37932
   139
  "_sdo_block (_sdo_cons (_sdo_let p t) bs)"
haftmann@37932
   140
    == "let p = t in _sdo_block bs"
haftmann@37932
   141
  "_sdo_block (_sdo_cons b (_sdo_cons c cs))"
haftmann@37932
   142
    == "_sdo_block (_sdo_cons b (_sdo_final (_sdo_block (_sdo_cons c cs))))"
haftmann@37932
   143
  "_sdo_cons (_sdo_let p t) (_sdo_final s)"
haftmann@37932
   144
    == "_sdo_final (let p = t in s)"
haftmann@37932
   145
  "_sdo_block (_sdo_final e)" => "e"
haftmann@37817
   146
wenzelm@60500
   147
text \<open>
wenzelm@63680
   148
  For an example, see \<^file>\<open>~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy\<close>.
wenzelm@60500
   149
\<close>
haftmann@21192
   150
wenzelm@22664
   151
end