Changeset 724


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.

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r712 r724  
    114114  λb: BitVector n.
    115115    \fst (sub_with_borrows n b (zero n) true).
    116    
     116
     117let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝
     118  match m with
     119  [ O ⇒ v
     120  | S m' ⇒ bitvector_of_nat_aux n m' (increment n v)
     121  ].
     122
     123definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝
     124  λn,m. bitvector_of_nat_aux n m (zero n).
     125
     126let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝
     127match v with
     128[ VEmpty ⇒ m
     129| VCons n' hd tl ⇒ nat_of_bitvector_aux n' (if hd then 2*m +1 else 2*m) tl
     130].
     131
     132definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
     133  λn,v. nat_of_bitvector_aux n O v.
     134
    117135definition two_complement_negation ≝
    118136  λn: nat.
  • 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:
  • src/ASM/I8051.ma

    r698 r724  
    44include "ASM/String.ma".
    55include "ASM/ASM.ma".
     6include "ASM/Arithmetic.ma".
    67include "utilities/Compare.ma".
    78
Note: See TracChangeset for help on using the changeset viewer.