Changeset 10 for Csemantics/Mem.ma
 Timestamp:
 Jul 6, 2010, 11:53:23 AM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Mem.ma
r9 r10 25 25 *) 26 26 27 include "arithmetics/Z.ma". 27 include "arithmetics/nat.ma". 28 include "binary/Z.ma". 28 29 include "datatypes/sums.ma". 29 30 include "datatypes/list.ma". … … 127 128  Mfloat64 => 7]. 128 129 130 alias symbol "plus" (instance 2) = "integer plus". 129 131 nlemma size_chunk_pred: 130 132 ∀chunk. size_chunk chunk = 1 + pred_size_chunk chunk. … … 164 166 nlemma align_size_chunk_divides: 165 167 ∀chunk. (align_chunk chunk ∣ size_chunk chunk). 166 #chunk;ncases chunk;nnormalize; @;//;##[ napply 2; ## // ##]168 #chunk;ncases chunk;nnormalize;/3/; 167 169 nqed. 168 170 … … 176 178 (* The initial store. *) 177 179 178 ndefinition oneZ ≝ pos O.180 ndefinition oneZ ≝ pos one. 179 181 180 182 nremark one_pos: OZ < oneZ. … … 186 188 187 189 ndefinition empty: mem ≝ 188 mk_mem (λx.empty_block OZ OZ) (pos O) one_pos.190 mk_mem (λx.empty_block OZ OZ) (pos one) one_pos. 189 191 190 192 ndefinition nullptr: block ≝ OZ. … … 501 503 nchange in ⊢ (??(???%)?) with (update ????); 502 504 nwhd in ⊢(??%?);nrewrite > (update_s content …); 503 nwhd in ⊢(??%?);nrewrite > (not_eq_to_eqb_false … );//;napply sym_neq;//;505 nwhd in ⊢(??%?);nrewrite > (not_eq_to_eqb_false … (sym_neq … H));//; 504 506 nqed. 505 507 … … 512 514 nlapply (eqZb_to_Prop p1 p2); ncases (eqZb p1 p2); #Hp; 513 515 ##[nrewrite > Hp; 514 n lapply (eqb_to_Prop n1 n2);ncases (eqbn1 n2); #Hn;516 napply (eqb_elim n1 n2); #Hn; 515 517 ##[nrewrite > Hn;@; @; //; 516 518 ##@2;/2/] … … 1055 1057 ##nrewrite > (size_chunk_pred …) in H1;nrewrite > (size_chunk_pred …); 1056 1058 #H1;napply nmk;#Hfalse;nelim H1;#H4;napply H4; 1057 napply (eq_f ?? (λx. Z_of_nat (1 + x)) ???);//##]1059 napply (eq_f ?? (λx.1 + x) ???);//##] 1058 1060 nqed. 1059 1061 … … 1582 1584 ## napply (Zleb_true_to_Zle … H2) 1583 1585 ## nwhd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon 1584 ## n apply (witness ?? (abs ofs)); nnormalize; nrewrite > (Zplus_z_OZ ?); //1586 ## ncases ofs; /2/; 1585 1587 ##] 1586 1588 ## *; #Hval;#Hlo;#Hhi;#Hal; … … 1699 1701 ## #ineq; @1; @1; napply ineq; 1700 1702 ##] nqed. 1701 1703 (* XXX: reenable once I've sorted out performance a bit 1702 1704 ndefinition meminj_no_overlap ≝ λmi: meminj. λm: mem. 1703 1705 ∀b1,b1',delta1,b2,b2',delta2. … … 2365 2367 ##] 2366 2368 ##] nqed. 2367 (* XXX: reenable once I've sorted out Integers.ma a bit 2369 2368 2370 nlemma valid_pointer_inject_no_overflow: 2369 2371 ∀f,m1,m2,b,ofs,b',x.
Note: See TracChangeset
for help on using the changeset viewer.