source: src/utilities/state.ma @ 2896

Last change on this file since 2896 was 2708, checked in by tranquil, 7 years ago

fixed linearise and LINToASM
LINToASM has now correct transformation of idents and labels to Identifier

File size: 1.5 KB
Line 
1include "utilities/monad.ma".
2
3definition state_monad ≝
4  λS : Type[0].MakeSetoidMonadProps
5  (* the monad *)
6  (λX.S → S × X)
7  (* return *)
8  (λX,x,s.〈s,x〉)
9  (* bind *)
10  (λX,Y,m,f,s. let 〈s', x〉 ≝ m s in f x s')
11  (* monad eq *)
12  (λX,c1,c2.∀s.c1 s = c2 s)
13  ????????.
14// normalize
15#X
16[ (* bind_proper *)
17  #Y #m #n #f #g #H #G #s >H elim (n s) #s' #x normalize @G
18| #m#s @pair_elim //
19| #Y#Z #m #f #g #s elim (m s) //
20]
21qed.
22
23definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉.
24definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉.
25definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s).
26definition state_update : ∀S.(S → S) → state_monad S unit ≝ λS,f,s.〈f s, it〉.
27
28definition state_pred ≝ λS.λPs : S → Prop.mk_MonadPred (state_monad S)
29  (λX,P,m.∀s.Ps s → let m' ≝ m s in Ps (\fst m') ∧ P (\snd m')) ???.
30[ normalize /2 by conj/
31| normalize #X#Y#P1#P2 #m #H #f #G #s #Ps lapply (H … Ps)
32  elim (m s) #s' #x normalize * /2/
33| #X #P #Q #H #m normalize #G #s #Ps elim (G … Ps) /3/
34]
35qed.
36
37definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (state_monad S) (state_monad T)
38  (λX,Y,P,m,n.∀s,t.Ps s t → let m' ≝ m s in let n' ≝ n t in
39    Ps (\fst m') (\fst n') ∧ P (\snd m') (\snd n')) ???.
40[ normalize /2/
41| normalize #X#Y#Z#W#P1#P2 #m #n #H #f #g #G #s #t #Ps lapply (H … Ps)
42  * elim (m s) elim (n t) /2/
43| #X #Y #P #Q #H #m #n normalize #G #s #t #Ps elim (G … Ps) /3/
44]
45qed.
46
Note: See TracBrowser for help on using the repository browser.