Changeset 2288 for src/RTLabs/Traces.ma
 Timestamp:
 Aug 2, 2012, 5:04:36 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2226 r2288 102 102 match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with 103 103 [ St_cond _ _ _ ⇒ cl_jump 104  St_jumptable _ _ ⇒ cl_jump 104 (*  St_jumptable _ _ ⇒ cl_jump*) 105 105  _ ⇒ cl_other 106 106 ] … … 666 666 ∃f,fs,m. s = State f fs m ∧ 667 667 let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in 668 (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).668 (∃r,l1,l2. stmt = St_cond r l1 l2) (*∨ (∃r,ls. stmt = St_jumptable r ls)*). 669 669 * 670 670 [ #f #fs #m #E … … 673 673  whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %; 674 674 try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct) 675 [ %1%{A} %{B} %{C} @refl676  %2 %{A} %{B} @refl677 ] 675 (*[ %1*) %{A} %{B} %{C} @refl 676 (*  %2 %{A} %{B} @refl 677 ]*) 678 678 ] 679 679  normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct … … 689 689 #ge #s #tr #s' #EV #H #CL 690 690 cases (rtlabs_jump_inv s CL) 691 #fr * #fs * #m * #Es *692 [ * #r * #l1 * #l2 #Estmt691 #fr * #fs * #m * #Es(* * 692 [*) * #r * #l1 * #l2 #Estmt 693 693 >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs 694 694 >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); … … 701 701 whd in ⊢ (% → ?); 702 702 * #H1 #H2 [ @H1  @H2 ] 703  * #r * #ls #Estmt703 (* * #r * #ls #Estmt 704 704 >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs 705 705 >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); … … 719 719 #H1 #H2 @H2 720 720 ] 721 ] qed.721 ]*) qed. 722 722 723 723 lemma rtlabs_call_inv : ∀s. … … 1344 1344  #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1345 1345  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1}  %{l2} ] % // [ %  %2 %] // 1346  #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev1346 (* #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev 1347 1347 cases v [ #E normalize in E; destruct  #sz #i  #f #E normalize in E; destruct  #E normalize in E; destruct  #p #E normalize in E; destruct ] 1348 1348 whd in ⊢ (??%? → ?); … … 1351 1351 [ #e #E normalize in E; destruct 1352 1352  #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El) 1353 ] 1353 ]*) 1354 1354  #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl 1355 1355 ] qed. … … 1423 1423  #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl 1424 1424  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl 1425  #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev1425 (* #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev 1426 1426 cases v [ #E normalize in E; destruct  #sz #i  #f #E normalize in E; destruct  #E normalize in E; destruct  #p #E normalize in E; destruct ] 1427 1427 whd in ⊢ (??%? → ?); … … 1430 1430 [ #e #E normalize in E; destruct 1431 1431  #l #El whd in ⊢ (??%? → ?); #E destruct @refl 1432 ] 1432 ]*) 1433 1433  #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl 1434 1434 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.