Changeset 2608 for src/Clight/switchRemoval.ma
 Timestamp:
 Feb 6, 2013, 1:01:34 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/switchRemoval.ma
r2588 r2608 1188 1188 beloadv (free m1 block) ptr = Some ? res → beloadv (free m2 block) ptr = Some ? res. 1189 1189 * #contents1 #nextblock1 #nextpos1 * #contents2 #nextblock2 #nextpos2 #writeable 1190 * #br #bid * * #pr#pid #poff #res #Hext1190 * (* #br *) #bid * * (* #pr *) #pid #poff #res #Hext 1191 1191 (*#Hme_nonempty #Hme_writeable #Hme_nonempty #Hvalid_conserv*) 1192 1192 #Hload … … 1223 1223 [ 1: lapply Hvalid normalize // 1224 1224  2: lapply Hlh normalize 1225 cases (block_region b) normalize nodelta1226 cases (block_region bl) normalize nodelta try //1227 1225 @(eqZb_elim … (block_id b) (block_id bl)) 1228 1226 [ 1,3: * normalize * … … 1232 1230 lemma eqb_to_eq_block : ∀a,b : block. a == b = eq_block a b. 1233 1231 #a #b lapply (eqb_true ? a b) @(eq_block_elim … a b) 1234 /2 by neq_block_eq_block_false, true_to_andb_true/ 1232 #H #I 1233 try /2 by neq_block_eq_block_false, true_to_andb_true/ 1234 cases I #J #K @K @H 1235 1235 qed. 1236 1236 … … 1362 1362 #b normalize >Hcontents_eq @refl 1363 1363  5: #x1 #x2 #acc normalize @conj try @refl 1364 * *#id normalize nodelta cases (block_region x1)1364 * (* * *) #id normalize nodelta cases (block_region x1) 1365 1365 cases (block_region x2) normalize nodelta 1366 1366 @(eqZb_elim id (block_id x1)) #Hx1 normalize nodelta 1367 1367 @(eqZb_elim id (block_id x2)) #Hx2 normalize nodelta try @refl 1368  6: * #r#i * #contents #nextblock #Hpos @conj1368  6: * (* #r *) #i * #contents #nextblock #Hpos @conj 1369 1369 [ 1: @refl 1370  2: #b normalize cases (block_region b) normalize1371 cases r normalize cases (eqZb (block_id b) i)1370  2: #b normalize (* cases (block_region b) normalize 1371 cases r normalize *) cases (eqZb (block_id b) i) 1372 1372 normalize @refl 1373 1373 ] … … 1650 1650 [ 1: normalize cases H // 1651 1651  2: cases H normalize #Hb_lt #Hb_nonempty2 1652 cases (block_region b)1653 cases (block_region wb) normalize nodelta1654 //1652 (* 1653 cases (block_region b) 1654 cases (block_region wb) *) 1655 1655 @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta 1656 1656 // ] … … 1705 1705 (nextblock m) (nextblock_pos m)) b. 1706 1706 #m #b #wb #offset #v * #Hvalid #Hnonempty % // 1707 cases b in Hvalid Hnonempty; #br #bid cases wb #wbr#wbid normalize1708 cases br normalize nodelta cases wbr normalize nodelta // 1707 cases b in Hvalid Hnonempty; (* #br *) #bid cases wb (* #wbr *) #wbid normalize 1708 (* cases br *) normalize nodelta (* cases wbr normalize nodelta // *) 1709 1709 @(eqZb_elim … bid wbid) // #Heq #Hlt normalize // 1710 1710 qed. … … 1720 1720 nonempty_block m b. 1721 1721 #m #b #wb #offset #v * #Hvalid #Hnonempty % // 1722 cases b in Hvalid Hnonempty; #br #bid cases wb #wbr#wbid normalize1723 cases br normalize nodelta cases wbr normalize nodelta // 1722 cases b in Hvalid Hnonempty; (* #br *) #bid cases wb (* #wbr *) #wbid normalize 1723 (* cases br normalize nodelta cases wbr normalize nodelta // *) 1724 1724 @(eqZb_elim … bid wbid) // #Heq #Hlt normalize // 1725 1725 qed. … … 1764 1764 @conj 1765 1765 [ 1: @nonempty_block_update_ok // 1766  2: normalize cases b in HB; #br #bid cases wb #wbr #wbid 1767 cases br cases wbr normalize nodelta 1768 @(eqZb_elim … bid wbid) normalize nodelta // 1769 #Hid_eq >Hid_eq #Hblock_eq >Hblock_eq @refl ] 1766  2: normalize (* cases b in HB; #br #bid cases wb #wbr #wbid 1767 cases br cases wbr normalize nodelta *) 1768 @(eqZb_elim … (block_id b) (block_id wb)) normalize nodelta // 1769 #Hid_eq cut (b = wb) 1770 [ cases b in Hid_eq; cases wb #wid #bid #H >H @refl ] 1771 #Hblock_eq destruct (Hblock_eq) >HB @refl ] 1770 1772  2: #b #Hmem lapply (me_writeable_valid … Hext … Hmem) @nonempty_block_update_ok 1771 1773  3: #b #Hnonempty lapply (nonempty_block_update_ok2 … Hnonempty)
Note: See TracChangeset
for help on using the changeset viewer.