equal
deleted
inserted
replaced
4 |
4 |
5 section \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close> |
5 section \<open>Combinator syntax for generic, open state monads (single-threaded monads)\<close> |
6 |
6 |
7 theory Open_State_Syntax |
7 theory Open_State_Syntax |
8 imports Main |
8 imports Main |
|
9 begin |
|
10 |
|
11 context |
|
12 includes state_combinator_syntax |
9 begin |
13 begin |
10 |
14 |
11 subsection \<open>Motivation\<close> |
15 subsection \<open>Motivation\<close> |
12 |
16 |
13 text \<open> |
17 text \<open> |
52 We aim to assert that values of any state type \<open>\<sigma>\<close> are used |
56 We aim to assert that values of any state type \<open>\<sigma>\<close> are used |
53 in a single-threaded way: after application of a transformation on a |
57 in a single-threaded way: after application of a transformation on a |
54 value of type \<open>\<sigma>\<close>, the former value should not be used |
58 value of type \<open>\<sigma>\<close>, the former value should not be used |
55 again. To achieve this, we use a set of monad combinators: |
59 again. To achieve this, we use a set of monad combinators: |
56 \<close> |
60 \<close> |
57 |
|
58 notation fcomp (infixl "\<circ>>" 60) |
|
59 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
60 |
61 |
61 text \<open> |
62 text \<open> |
62 Given two transformations \<^term>\<open>f\<close> and \<^term>\<open>g\<close>, they may be |
63 Given two transformations \<^term>\<open>f\<close> and \<^term>\<open>g\<close>, they may be |
63 directly composed using the \<^term>\<open>(\<circ>>)\<close> combinator, forming a |
64 directly composed using the \<^term>\<open>(\<circ>>)\<close> combinator, forming a |
64 forward composition: \<^prop>\<open>(f \<circ>> g) s = f (g s)\<close>. |
65 forward composition: \<^prop>\<open>(f \<circ>> g) s = f (g s)\<close>. |
109 Evaluation of monadic expressions by force: |
110 Evaluation of monadic expressions by force: |
110 \<close> |
111 \<close> |
111 |
112 |
112 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta |
113 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta |
113 |
114 |
|
115 end |
|
116 |
114 |
117 |
115 subsection \<open>Do-syntax\<close> |
118 subsection \<open>Do-syntax\<close> |
116 |
119 |
117 nonterminal sdo_binds and sdo_bind |
120 nonterminal sdo_binds and sdo_bind |
118 |
121 |