Changeset 10 for C-semantics/Integers.ma
- Timestamp:
- Jul 6, 2010, 11:53:23 AM (11 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/Integers.ma
r9 r10 17 17 18 18 include "arithmetics/nat.ma". 19 include " arithmetics/Z.ma".19 include "binary/Z.ma". 20 20 include "extralib.ma". 21 21 … … 62 62 *) 63 63 64 naxiom two_power_nat : nat → Z. 64 (*naxiom two_power_nat : nat → Z.*) 65 65 66 66 ndefinition wordsize : nat ≝ 32. 67 ndefinition modulus : Z ≝ two_power_nat wordsize.67 ndefinition modulus : Z ≝ Z_two_power_nat wordsize. 68 68 ndefinition half_modulus : Z ≝ modulus / 2. 69 69 ndefinition max_unsigned : Z ≝ modulus - 1. … … 75 75 nnormalize; //; nqed. 76 76 77 (* 78 Remark modulus_power: 77 nremark modulus_power: 79 78 modulus = two_p (Z_of_nat wordsize). 80 Proof. 81 unfold modulus. apply two_power_nat_two_p. 82 Qed. 83 84 Remark modulus_pos: 79 //; nqed. 80 81 nremark modulus_pos: 85 82 modulus > 0. 86 Proof. 87 rewrite modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega. 88 Qed. 89 *) 83 //; nqed. 84 90 85 (* * Representation of machine integers *) 91 86
Note: See TracChangeset
for help on using the changeset viewer.