Ignore:
Timestamp:
Oct 13, 2010, 4:27:18 PM (9 years ago)
Author:
campbell
Message:

Sort out some axioms.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Integers.ma

    r15 r181  
    156156ndefinition neg : int → int ≝ λx. repr (- unsigned x).
    157157
    158 (*
    159 ndefinition zero_ext : Z → int → int ≝
    160 λn,x. repr (modZ (unsigned x) (two_p n)).
    161 ndefinition sign_ext : Z → int → int ≝
    162 λn,x. repr (let p ≝ two_p n in
    163         let y ≝ modZ (unsigned x) p in
    164         if Zltb y (two_p (n-1)) then y else y - p).
    165 *)
    166158nlet rec zero_ext (n:Z) (x:int) on x : int ≝
    167159  repr (modZ (unsigned x) (two_p n)).
     
    204196ndefinition Z_shift_add ≝ λb: bool. λx: Z.
    205197  if b then 2 * x + 1 else 2 * x.
    206 (*
    207 Definition Z_bin_decomp (x: Z) : bool * Z :=
    208   match x with
    209   | Z0 => (false, 0)
    210   | Zpos p =>
    211       match p with
    212       | xI q => (true, Zpos q)
    213       | xO q => (false, Zpos q)
    214       | xH => (true, 0)
    215       end
    216   | Zneg p =>
    217       match p with
    218       | xI q => (true, Zneg q - 1)
    219       | xO q => (false, Zneg q)
    220       | xH => (true, -1)
    221       end
    222   end.
    223 *)
    224 naxiom bits_of_Z : nat → Z → Z → bool.
    225 naxiom Z_of_bits : nat → (Z → bool) → Z.
    226 (*
    227 Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool :=
    228   match n with
    229   | O =>
    230       (fun i: Z => false)
    231   | S m =>
    232       let (b, y) := Z_bin_decomp x in
    233       let f := bits_of_Z m y in
    234       (fun i: Z => if zeq i 0 then b else f (i - 1))
    235   end.
    236 
    237 Fixpoint Z_of_bits (n: nat) (f: Z -> bool) {struct n}: Z :=
    238   match n with
    239   | O => 0
    240   | S m => Z_shift_add (f 0) (Z_of_bits m (fun i => f (i + 1)))
    241   end.
    242 *)
     198
     199ndefinition Z_bin_decomp : Z → bool × Z ≝
     200λx.match x with
     201[ OZ ⇒ 〈false, OZ〉
     202| pos p ⇒
     203  match p with
     204  [ p1 q ⇒ 〈true, pos q〉
     205  | p0 q ⇒ 〈false, pos q〉
     206  | one ⇒ 〈true, OZ〉
     207  ]
     208| neg p ⇒
     209  match p with
     210  [ p1 q ⇒ 〈true, Zpred (neg q)〉
     211  | p0 q ⇒ 〈false, neg q〉
     212  | one ⇒ 〈true, neg one〉
     213  ]
     214].
     215
     216nlet rec bits_of_Z (n:nat) (x:Z) on n : Z → bool ≝
     217match n with
     218[ O ⇒ λi:Z. false
     219| S m ⇒
     220    match Z_bin_decomp x with [ mk_pair b y ⇒
     221      let f ≝ bits_of_Z m y in
     222      λi:Z. if eqZb i 0 then b else f (Zpred i) ]
     223].
     224
     225nlet rec Z_of_bits (n:nat) (f:Z → bool) on n : Z ≝
     226match n with
     227[ O ⇒ OZ
     228| S m ⇒ Z_shift_add (f OZ) (Z_of_bits m (λi. f (Zsucc i)))
     229].
     230
    243231(* * Bitwise logical ``and'', ``or'' and ``xor'' operations. *)
    244232
     
    744732  apply eqmod_refl. red; exists (-1); ring.
    745733Qed.
    746 
    747 Theorem unsigned_range:
    748   forall i, 0 <= unsigned i < modulus.
    749 Proof.
    750   destruct i; simpl. auto.
    751 Qed.
    752 Hint Resolve unsigned_range: ints.
    753 
    754 Theorem unsigned_range_2:
    755   forall i, 0 <= unsigned i <= max_unsigned.
    756 Proof.
    757   intro; unfold max_unsigned.
    758   generalize (unsigned_range i). omega.
    759 Qed.
    760 Hint Resolve unsigned_range_2: ints.
    761734*)
     735
     736ntheorem unsigned_range: ∀i. 0 ≤ unsigned i ∧ unsigned i < modulus.
     737#i; ncases i; #i' H; ncases H; /2/;
     738nqed.
     739
     740ntheorem unsigned_range_2:
     741  ∀i. 0 ≤ unsigned i ∧ unsigned i ≤ max_unsigned.
     742#i; nrewrite > (?:max_unsigned = modulus - 1); //; (* unfold *)
     743nlapply (unsigned_range i); *; #Hz Hm; @;
     744##[ //;
     745##| nrewrite < (Zpred_Zsucc (unsigned i));
     746    nrewrite < (Zpred_Zplus_neg_O modulus);
     747    napply monotonic_Zle_Zpred;
     748    /2/;
     749##] nqed.
     750
    762751naxiom signed_range:
    763752  ∀i. min_signed ≤ signed i ∧ signed i ≤ max_signed.
    764753(*
     754#i; nwhd in ⊢ (?(??%)(?%?));
     755nlapply (unsigned_range i); *; nletin n ≝ (unsigned i); #H1 H2;
     756napply (Zltb_elim_Type0); #H3;
     757##[ @; ##[ napply (transitive_Zle ? OZ); //;
     758       ##| nrewrite < (Zpred_Zsucc n);
     759           nrewrite < (Zpred_Zplus_neg_O half_modulus);
     760           napply monotonic_Zle_Zpred; /2/;
     761       ##]
     762##| @; ##[ nrewrite > half_modulus_modulus;
     763
    765764Theorem signed_range:
    766765  forall i, min_signed <= signed i <= max_signed.
Note: See TracChangeset for help on using the changeset viewer.