Changeset 582 for Deliverables/D3.1/Csemantics/Integers.ma
 Timestamp:
 Feb 22, 2011, 11:35:16 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Integers.ma
r547 r582 131 131 132 132 definition eq : int → int → bool ≝ eq_bv wordsize. 133 definition lt : int → int → bool ≝ λx,y:int. 134 if Zltb (signed x) (signed y) then true else false. 135 definition ltu : int → int → bool ≝ λx,y: int. 136 if Zltb (unsigned x) (unsigned y) then true else false. 137 138 definition neg : int → int ≝ λx. repr ( unsigned x). 133 definition lt : int → int → bool ≝ lt_s wordsize. 134 definition ltu : int → int → bool ≝ lt_u wordsize. 135 136 definition neg : int → int ≝ negation_bv wordsize. 139 137 140 138 let rec zero_ext (n:Z) (x:int) on x : int ≝ … … 145 143 if Zltb y (two_p (n1)) then y else y  p). 146 144 147 definition add ≝ λx,y: int. 148 repr (unsigned x + unsigned y). 149 definition sub ≝ λx,y: int. 150 repr (unsigned x  unsigned y). 151 definition mul ≝ λx,y: int. 152 repr (unsigned x * unsigned y). 145 definition add ≝ addition_n wordsize. 146 definition sub ≝ subtraction wordsize. 147 definition mul ≝ λx,y. \fst (split ? wordsize wordsize (multiplication wordsize x y)). 153 148 definition Zdiv_round : Z → Z → Z ≝ λx,y: Z. 154 149 if Zltb x 0 then … … 218 213 repr (Z_of_bits wordsize (λi. f (fx i) (fy i))). 219 214 220 definition i_and : int → int → int ≝ λx,y. bitwise_binop andb x y.221 definition or : int → int → int ≝ λx,y. bitwise_binop orb x y.222 definition xor : int → int → int ≝ λx,y. bitwise_binop xorb x y.223 224 definition not : int → int ≝ λx.xor x mone.215 definition i_and : int → int → int ≝ conjunction_bv wordsize. 216 definition or : int → int → int ≝ inclusive_disjunction_bv wordsize. 217 definition xor : int → int → int ≝ exclusive_disjunction_bv wordsize. 218 219 definition not : int → int ≝ negation_bv wordsize. 225 220 226 221 (* * Shifts and rotates. *) … … 490 485 Qed. 491 486 *) 492 axiom one_not_zero: one ≠ zero. 487 theorem one_not_zero: one ≠ zero. 488 % #H 489 lapply (refl ? (get_index' ? 31 0 one)) 490 >H in ⊢ (???% → ?) 491 normalize #E destruct 492 qed. 493 493 494 (* 494 Theorem one_not_zero: one <> zero.495 Proof.496 assert (unsigned one <> unsigned zero).497 rewrite unsigned_one; rewrite unsigned_zero; congruence.498 congruence.499 Qed.500 501 495 Theorem unsigned_repr_wordsize: 502 496 unsigned iwordsize = Z_of_nat wordsize.
Note: See TracChangeset
for help on using the changeset viewer.