Ignore:
Timestamp:
May 21, 2012, 7:04:21 PM (8 years ago)
Author:
tranquil
Message:
  • monads: just changed some defs, which had to be propagated in some files
  • ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
  • added a library for permutations of lists (useful with fold AC ops on lists)
  • first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/state.ma

    r1882 r1976  
    11include "utilities/monad.ma".
    22
    3 definition State
     3definition state_monad
    44  λS : Type[0].MakeSetoidMonadProps
    55  (* the monad *)
     
    2121qed.
    2222
    23 definition state_monad ≝ λS.monad (State S).
    24 
    2523definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉.
    2624definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉.
    2725definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s).
    2826
    29 include "hints_declaration.ma".
    30 unification hint 0 ≔ S,X;
    31 N ≟ State S, M ≟ smax_def N
    32 (*---------------*) ⊢
    33 state_monad S X ≡ monad M X
    34 .
    35 
    36 definition StatePred ≝ λS.λPs : S → Prop.mk_MonadPred (State S)
     27definition state_pred ≝ λS.λPs : S → Prop.mk_MonadPred (state_monad S)
    3728  (λX,P,m.∀s.Ps s → let m' ≝ m s in Ps (\fst m') ∧ P (\snd m')) ???.
    38 [ normalize /2/
     29[ normalize /2 by conj/
    3930| normalize #X#Y#P1#P2 #m #H #f #G #s #Ps lapply (H … Ps)
    4031  elim (m s) #s' #x normalize * /2/
     
    4334qed.
    4435
    45 definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (State S) (State T)
     36definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (state_monad S) (state_monad T)
    4637  (λX,Y,P,m,n.∀s,t.Ps s t → let m' ≝ m s in let n' ≝ n t in
    4738    Ps (\fst m') (\fst n') ∧ P (\snd m') (\snd n')) ???.
Note: See TracChangeset for help on using the changeset viewer.