Changeset 2722 for src/Clight/labelSimulation.ma
 Timestamp:
 Feb 23, 2013, 5:05:03 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r2682 r2722 87 87 ] 88 88  #v #ty #b #o #tr #EX #u %{tr} % [ 89 whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %;89 whd in EX:(??%?) ⊢ (??%?); cases (lookup SymbolTag ?? v) in EX ⊢ %; 90 90 [ whd in ⊢ (??%? → ??%?); >(rgg_find_symbol … RG) // 91 91  #b // ] … … 407 407 qed. 408 408 409 lemma opt_find_funct : ∀ge,ge',m,vf,fd .409 lemma opt_find_funct : ∀ge,ge',m,vf,fd,id. 410 410 related_globals_gen … label_fundef ge ge' → 411 opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd→412 ∃u. opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (\fst (label_fundef u fd)).413 #ge #ge' #m #vf #fd # RG414 lapply (rgg_find_funct … RG … vf fd)415 cases (find_funct … vf)411 opt_to_io io_out io_in … m (find_funct_id … ge vf) = Value … 〈fd,id〉 → 412 ∃u. opt_to_io io_out io_in … m (find_funct_id … ge' vf) = Value … 〈\fst (label_fundef u fd), id〉. 413 #ge #ge' #m #vf #fd #id #RG 414 lapply (rgg_find_funct_id … RG … vf fd) 415 cases (find_funct_id … vf) 416 416 [ #_ #E normalize in E; destruct 417  #fd' #H #E normalize in E; destruct cases (H(refl ??)) #u #FF %{u} >FF //417  * #fd' #id' #H #E normalize in E; destruct cases (H ? (refl ??)) #u #FF %{u} >FF // 418 418 ] qed. 419 419 … … 768 768 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX 769 769 cases (bindIO_inversion ??????? EX) EX * #args' #tr2 * #EX2 #EX 770 cases (bindIO_inversion ??????? EX) EX #fd * #EX3 #EX770 cases (bindIO_inversion ??????? EX) EX * #fd #fid * #EX3 #EX 771 771 cases (bindIO_inversion ??????? EX) EX #E4 * #EX4 #EX 772 772 whd in EX:(??%%); … … 910 910 cases v1 in EX1 EX; 911 911 [ 2: #sz #i #EX1 #EX 912  *: normalize #A #B try #Cdestruct912  *: [ 3: #x ] #A whd in ⊢ (??%% → ?); #B destruct 913 913 ] 914 914 whd in EX:(??%%); cases ty in EX1 EX ⊢ %; normalize nodelta #sz' try #sg try #EX1 try #EX destruct
Note: See TracChangeset
for help on using the changeset viewer.