Changeset 2044 for src/RTLabs/semantics.ma
- Timestamp:
- Jun 12, 2012, 10:52:37 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/semantics.ma
r2025 r2044 256 256 . 257 257 258 lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Prop.258 lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Type[0]. 259 259 (∀a. e = OK A a → f a = OK ? v → P v) → 260 260 (match e with [ OK v ⇒ f v | Error m ⇒ Error ? m ] = OK ? v → P v). … … 305 305 ] qed. 306 306 307 (* Show that, in principle at least, we can calculate which function we called 308 on a transition. The proof is a functional inversion similar to eval_preserves, 309 above. *) 310 311 definition func_block_of_exec : ∀ge,s,t,fd,args,dst,fs,m. 312 eval_statement ge s = Value ??? 〈t,Callstate fd args dst fs m〉 → 313 Σb:block. find_funct_ptr … ge b = Some ? fd. 314 #ge * 315 [ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m' 316 whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); 317 cases (lookup_present … nok) 318 (* Function call cases. *) 319 [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs #E normalize in E; destruct 320 [ %{v} @Efd 321 | cases v in Efd; 322 [ 5: * #pty #b #pc #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd; 323 [ #E @E | #E normalize in E; destruct ] 324 | *: normalize #A try #B try #C destruct 325 ] 326 ] 327 (* and everything else cannot occur, but we need to work through the 328 definition to find the resulting state to demonstrate that. *) 329 | #l #LP whd in ⊢ (??%? → ?); #E destruct 330 | #c #l #LP whd in ⊢ (??%? → ?); #E destruct 331 | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct 332 | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct 333 | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct 334 | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct 335 | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct 336 | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct 337 | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct ] | *: #vl #E whd in E:(??%?); destruct ] 338 | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct 339 ] 340 | * #fn #args #retdst #stk #m #tr #fd' #args' #dst' #fs' #m' 341 whd in ⊢ (??%? → ?); 342 [ @bind_res_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?); 343 #E destruct 344 | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct 345 ] 346 | #v #r * [2: #f #fs ] #m #tr #fd' #args' #dst' #fs' #m' 347 whd in ⊢ (??%? → ?); 348 [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct 349 | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct | *: normalize #a try #b destruct ] ] 350 ] 351 | #r #tr #fd' #args' #dst' #fs' #m' 352 normalize #E destruct 353 ] qed. 354 307 355 308 356 lemma initial_state_is_not_final : ∀p,s.
Note: See TracChangeset
for help on using the changeset viewer.