58 notation fcomp (infixl "\<circ>>" 60) |
58 notation fcomp (infixl "\<circ>>" 60) |
59 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
59 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
60 |
60 |
61 text \<open> |
61 text \<open> |
62 Given two transformations @{term f} and @{term g}, they may be |
62 Given two transformations @{term f} and @{term g}, they may be |
63 directly composed using the @{term "op \<circ>>"} combinator, forming a |
63 directly composed using the @{term "(\<circ>>)"} combinator, forming a |
64 forward composition: @{prop "(f \<circ>> g) s = f (g s)"}. |
64 forward composition: @{prop "(f \<circ>> g) s = f (g s)"}. |
65 |
65 |
66 After any yielding transformation, we bind the side result |
66 After any yielding transformation, we bind the side result |
67 immediately using a lambda abstraction. This is the purpose of the |
67 immediately using a lambda abstraction. This is the purpose of the |
68 @{term "op \<circ>\<rightarrow>"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') |
68 @{term "(\<circ>\<rightarrow>)"} combinator: @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') |
69 = f s in g s')"}. |
69 = f s in g s')"}. |
70 |
70 |
71 For queries, the existing @{term "Let"} is appropriate. |
71 For queries, the existing @{term "Let"} is appropriate. |
72 |
72 |
73 Naturally, a computation may yield a side result by pairing it to |
73 Naturally, a computation may yield a side result by pairing it to |