Changeset 724 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Mar 30, 2011, 2:03:05 PM (9 years ago)
Author:
campbell
Message:

More tractable version of bitvector_of_nat / nat_of_bitvector.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r700 r724  
    9393(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    9494
    95 let rec bitvector_of_nat_aux (n: nat) (bound: nat) on bound ≝
    96  match bound with
    97   [ O ⇒ [ ] (* IT WILL NOT HAPPEN *)
    98   | S bound' ⇒
    99     let divrem ≝ divide_with_remainder n (S (S O)) in
    100     let div ≝ fst nat nat divrem in
    101     let rem ≝ snd nat nat divrem in
    102       match div with
    103         [ O ⇒
    104           match rem with
    105             [ O ⇒ [ ]
    106             | S r ⇒ true :: (bitvector_of_nat_aux O bound')
    107             ]
    108         | S d ⇒
    109           match rem with
    110             [ O ⇒ false :: (bitvector_of_nat_aux (S d) bound')
    111             | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound')
    112             ]
    113         ]
    114   ].
    115 
    11695definition eq_bv ≝
    11796  λn: nat.
     
    130109#Q * *; normalize /3/
    131110qed.
    132 
    133 let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
    134   let biglist ≝ rev ? (bitvector_of_nat_aux m m) in
    135   let size ≝ length ? biglist in
    136   let bitvector ≝ vector_of_list ? biglist in
    137   let difference ≝ n - size in
    138    less_than_or_equal_b_elim …
    139     (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector (difference+size) ↦ BitVector n⌉))
    140     (λH:¬(size ≤ n). maximum n).
    141   < plus_minus_m_m
    142   //
    143   assumption
    144 qed.
    145 
    146 let rec nat_of_bitvector (n: nat) (b: BitVector n) on b: nat ≝
    147   match b with
    148     [ VEmpty ⇒ O
    149     | VCons o hd tl ⇒
    150       let hdval ≝ match hd with [ true ⇒ S O | false ⇒ O ] in
    151         plus ((2^o) * hdval) (nat_of_bitvector o tl)
    152     ].
    153111   
    154112axiom bitvector_of_string:
Note: See TracChangeset for help on using the changeset viewer.