Changeset 10 for C-semantics/Integers.ma

Timestamp:

Jul 6, 2010, 11:53:23 AM (10 years ago)

Author:

campbell

Message:

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

File:

• C-semantics/Integers.ma (modified) (3 diffs)

C-semantics/Integers.ma

@@ -17 +17 @@
 
 include "arithmetics/nat.ma".
-include "arithmetics/Z.ma".
+include "binary/Z.ma".
 include "extralib.ma".
 
@@ -62 +62 @@
 *)
 
-naxiom two_power_nat : nat → Z.
+(*naxiom two_power_nat : nat → Z.*)
 
 ndefinition wordsize : nat ≝ 32.
-ndefinition modulus : Z ≝ two_power_nat wordsize.
+ndefinition modulus : Z ≝ Z_two_power_nat wordsize.
 ndefinition half_modulus : Z ≝ modulus / 2.
 ndefinition max_unsigned : Z ≝ modulus - 1.
@@ -75 +75 @@
 nnormalize; //; nqed.
 
-(*
-Remark modulus_power:
+nremark modulus_power:
   modulus = two_p (Z_of_nat wordsize).
-Proof.
-  unfold modulus. apply two_power_nat_two_p.
-Qed.
-
-Remark modulus_pos:
+//; nqed.
+
+nremark modulus_pos:
   modulus > 0.
-Proof.
-  rewrite modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega.
-Qed.
-*)
+//; nqed.
+
 (* * Representation of machine integers *)