Changeset 1920 for src/common/IOMonad.ma


Ignore:
Timestamp:
May 8, 2012, 11:16:18 AM (8 years ago)
Author:
campbell
Message:

Most of the labelling simulation. Still need to sort out switch statements
and function calls.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r1882 r1920  
    218218] qed.
    219219*)
     220
     221(* Inversion when injecting errors into IO monad. *)
     222lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
     223  (∀a. e = OK A a → f a = OK B v → P v) →
     224  (match e »= f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v).
     225#O #I #A #B *
     226[ #a #f #v #P #H #E @H [ @a | @refl | normalize in E; cases (f a) in E ⊢ %;
     227  [ #v' #E normalize in E; destruct @refl | #m #E normalize in E; destruct ] ]
     228| #m #f #v #P #H #E whd in E:(??%?); destruct
     229] qed.
     230
     231lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
     232  (∀a. e = Value ??? a → f a = Value ??? v → P v) →
     233  (bindIO O I A B e f = Value ??? v → P v).
     234#O #I #A #B *
     235[ #o #k #f #v #P #H #E whd in E:(??%?); destruct
     236| #a #f #v #P #H #E @H [ @a | @refl | @E ]
     237| #m #f #v #P #H #E whd in E:(??%?); destruct
     238] qed.
Note: See TracChangeset for help on using the changeset viewer.