Changeset 2145 for src/common


Ignore:
Timestamp:
Jul 2, 2012, 4:12:12 PM (7 years ago)
Author:
campbell
Message:

Cost labelling doesn't affect interaction.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r2044 r2145  
    385385] qed.
    386386
     387lemma bindIO_res_interact : ∀O,I,A,B,e,f,o,k. ∀P:∀o:O. (I o → IO O I B) → Type[0].
     388  (∀v. e = OK A v → f v = Interact … o k → P o k) →
     389  bindIO O I A B (err_to_io … e) f = Interact … o k → P o k.
     390#O #I #A #B *
     391[ #a #f #o #k #P #H #E @(H … E) @refl
     392| #m #f #o #k #P #_ #E whd in E:(??%?); destruct
     393] qed.
     394
     395lemma bindIO_opt_interact : ∀O,I,A,B,m,e,f,o,k. ∀P:∀o:O. (I o → IO O I B) → Type[0].
     396  (∀v. e = Some A v → f v = Interact … o k → P o k) →
     397  bindIO O I A B (opt_to_io … m e) f = Interact … o k → P o k.
     398#O #I #A #B #m *
     399[ #f #o #k #P #_ #E whd in E:(??%?); destruct
     400| #a #f #o #k #P #H #E @(H … E) @refl
     401] qed.
     402
    387403lemma bindIO_inversion: ∀O,I.
    388404  ∀A,B: Type[0]. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
  • src/common/SmallstepExec.ma

    r2118 r2145  
    112112] qed.
    113113
     114lemma extract_interact : ∀O,I,TS,ge,s,o,k.
     115  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
     116  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
     117#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
     118cases (step … s)
     119[ #o' #k' normalize #E destruct %{k'} /2/
     120| * #x #y normalize cases (is_final ?????) normalize
     121  #X try #Y destruct
     122| normalize #m #E destruct
     123] qed.
     124
    114125lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
    115126  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
Note: See TracChangeset for help on using the changeset viewer.