Changeset 1516 for src/common/Mem.ma


Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Mem.ma

    r891 r1516  
    6666  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
    6767  update_block … x v f x = v.
    68 #A * * #ix #v #f whd in ⊢ (??%?)
     68#A * * #ix #v #f whd in ⊢ (??%?);
    6969>eq_block_b_b //
    7070qed.
     
    192192lemma align_size_chunk_divides:
    193193  ∀chunk. (align_chunk chunk ∣ size_chunk chunk).
    194 #chunk cases chunk;[8:#r cases r ]normalize;/3/;
     194#chunk cases chunk;[8:#r cases r ]normalize;/3 by witness/;
    195195qed.
    196196
     
    735735lemma valid_not_valid_diff:
    736736  ∀m,b,b'. valid_block m b →  ¬(valid_block m b') → b ≠ b'.
    737 #m #b #b' #H #H' @nmk #e >e in H #H
     737#m #b #b' #H #H' @nmk #e >e in H; #H
    738738@(absurd ? H H')
    739739qed.
     
    759759#m #chunk #chunk2 #r #b #ofs #H1 #H2
    760760elim H2;#H3 #H4 #H5 #H6 #H7
    761 >H1 in H5 #H5
     761>H1 in H5; #H5
    762762% //;
    763763<(align_chunk_compat … H1) //;
     
    807807#b' cases (store_inv … STORE)
    808808#H1 #H2 >H2
    809 whd in ⊢ (??(?%?)?) whd in ⊢ (??%?)
    810 whd in ⊢ (??(?%)?) @eq_block_elim #E
     809whd in ⊢ (??(?%?)?); whd in ⊢ (??%?);
     810whd in ⊢ (??(?%)?); @eq_block_elim #E
    811811normalize //
    812812qed.
     
    864864#chunk #m1 #r #b #ofs #v #m2 #STORE
    865865#chunk' #r' #b' #ofs'
    866 * Hv;
     866* as Hv
    867867#Hvb #Hl #Hr #Halign #Hptr
    868868% //;
     
    878878#chunk #m1 #r #b #ofs #v #m2 #STORE
    879879#chunk' #r' #b' #ofs'
    880 * Hv;
     880* as Hv
    881881#Hvb #Hl #Hr #Halign #Hcompat
    882882% //;
     
    35143514  ∀m,a,v.
    35153515  storev Mint8signed m a v = storev Mint8unsigned m a v.
    3516 #m #a #v whd in ⊢ (??%%) elim a //
    3517 #r #b #p #ofs whd in ⊢ (??%%)
     3516#m #a #v whd in ⊢ (??%%); elim a //
     3517#r #b #p #ofs whd in ⊢ (??%%);
    35183518>(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //
    35193519qed.
     
    35223522  ∀m,a,v.
    35233523  storev Mint16signed m a v = storev Mint16unsigned m a v.
    3524 #m #a #v whd in ⊢ (??%%) elim a //
    3525 #r #b #p #ofs whd in ⊢ (??%%)
     3524#m #a #v whd in ⊢ (??%%); elim a //
     3525#r #b #p #ofs whd in ⊢ (??%%);
    35263526>(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //
    35273527qed.
Note: See TracChangeset for help on using the changeset viewer.