Changeset 10 for C-semantics/Integers.ma


Ignore:
Timestamp:
Jul 6, 2010, 11:53:23 AM (9 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:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Integers.ma

    r9 r10  
    1717
    1818include "arithmetics/nat.ma".
    19 include "arithmetics/Z.ma".
     19include "binary/Z.ma".
    2020include "extralib.ma".
    2121
     
    6262*)
    6363
    64 naxiom two_power_nat : nat → Z.
     64(*naxiom two_power_nat : nat → Z.*)
    6565
    6666ndefinition wordsize : nat ≝ 32.
    67 ndefinition modulus : Z ≝ two_power_nat wordsize.
     67ndefinition modulus : Z ≝ Z_two_power_nat wordsize.
    6868ndefinition half_modulus : Z ≝ modulus / 2.
    6969ndefinition max_unsigned : Z ≝ modulus - 1.
     
    7575nnormalize; //; nqed.
    7676
    77 (*
    78 Remark modulus_power:
     77nremark modulus_power:
    7978  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
     81nremark modulus_pos:
    8582  modulus > 0.
    86 Proof.
    87   rewrite modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega.
    88 Qed.
    89 *)
     83//; nqed.
     84
    9085(* * Representation of machine integers *)
    9186
Note: See TracChangeset for help on using the changeset viewer.