Changeset 724

Timestamp:

Mar 30, 2011, 2:03:05 PM (10 years ago)

Author:

campbell

Message:

More tractable version of bitvector_of_nat / nat_of_bitvector.

Location:

src/ASM

Files:

• Arithmetic.ma (modified) (1 diff)
• BitVector.ma (modified) (2 diffs)
• I8051.ma (modified) (1 diff)

src/ASM/Arithmetic.ma

@@ -114 +114 @@
   λb: BitVector n.
     \fst (sub_with_borrows n b (zero n) true).
-    
+
+let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝
+  match m with
+  [ O ⇒ v
+  | S m' ⇒ bitvector_of_nat_aux n m' (increment n v)
+  ].
+
+definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝
+  λn,m. bitvector_of_nat_aux n m (zero n).
+
+let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝
+match v with
+[ VEmpty ⇒ m
+| VCons n' hd tl ⇒ nat_of_bitvector_aux n' (if hd then 2*m +1 else 2*m) tl
+].
+
+definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
+  λn,v. nat_of_bitvector_aux n O v.
+
 definition two_complement_negation ≝
   λn: nat.

src/ASM/BitVector.ma

@@ -93 +93 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
 
-let rec bitvector_of_nat_aux (n: nat) (bound: nat) on bound ≝
- match bound with
-  [ O ⇒ [ ] (* IT WILL NOT HAPPEN *)
-  | S bound' ⇒ 
-    let divrem ≝ divide_with_remainder n (S (S O)) in
-    let div ≝ fst nat nat divrem in
-    let rem ≝ snd nat nat divrem in
-      match div with
-        [ O ⇒
-          match rem with
-            [ O ⇒ [ ]
-            | S r ⇒ true :: (bitvector_of_nat_aux O bound')
-            ]
-        | S d ⇒
-          match rem with
-            [ O ⇒ false :: (bitvector_of_nat_aux (S d) bound')
-            | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound')
-            ]
-        ]
-  ].
-
 definition eq_bv ≝
   λn: nat.
@@ -130 +109 @@
 #Q * *; normalize /3/
 qed.
-
-let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
-  let biglist ≝ rev ? (bitvector_of_nat_aux m m) in
-  let size ≝ length ? biglist in
-  let bitvector ≝ vector_of_list ? biglist in
-  let difference ≝ n - size in
-   less_than_or_equal_b_elim …
-    (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector (difference+size) ↦ BitVector n⌉)) 
-    (λH:¬(size ≤ n). maximum n).
-  < plus_minus_m_m
-  //
-  assumption
-qed.
-
-let rec nat_of_bitvector (n: nat) (b: BitVector n) on b: nat ≝
-  match b with
-    [ VEmpty ⇒ O
-    | VCons o hd tl ⇒
-      let hdval ≝ match hd with [ true ⇒ S O | false ⇒ O ] in
-        plus ((2^o) * hdval) (nat_of_bitvector o tl)
-    ].
     
 axiom bitvector_of_string:

src/ASM/I8051.ma

@@ -4 +4 @@
 include "ASM/String.ma".
 include "ASM/ASM.ma".
+include "ASM/Arithmetic.ma".
 include "utilities/Compare.ma".