Changeset 724 for src/ASM/BitVector.ma
 Timestamp:
 Mar 30, 2011, 2:03:05 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVector.ma
r700 r724 93 93 (* ===================================== *) 94 94 95 let rec bitvector_of_nat_aux (n: nat) (bound: nat) on bound ≝96 match bound with97 [ O ⇒ [ ] (* IT WILL NOT HAPPEN *)98  S bound' ⇒99 let divrem ≝ divide_with_remainder n (S (S O)) in100 let div ≝ fst nat nat divrem in101 let rem ≝ snd nat nat divrem in102 match div with103 [ O ⇒104 match rem with105 [ O ⇒ [ ]106  S r ⇒ true :: (bitvector_of_nat_aux O bound')107 ]108  S d ⇒109 match rem with110 [ O ⇒ false :: (bitvector_of_nat_aux (S d) bound')111  S r ⇒ true :: (bitvector_of_nat_aux (S d) bound')112 ]113 ]114 ].115 116 95 definition eq_bv ≝ 117 96 λn: nat. … … 130 109 #Q * *; normalize /3/ 131 110 qed. 132 133 let rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝134 let biglist ≝ rev ? (bitvector_of_nat_aux m m) in135 let size ≝ length ? biglist in136 let bitvector ≝ vector_of_list ? biglist in137 let difference ≝ n  size in138 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_m142 //143 assumption144 qed.145 146 let rec nat_of_bitvector (n: nat) (b: BitVector n) on b: nat ≝147 match b with148 [ VEmpty ⇒ O149  VCons o hd tl ⇒150 let hdval ≝ match hd with [ true ⇒ S O  false ⇒ O ] in151 plus ((2^o) * hdval) (nat_of_bitvector o tl)152 ].153 111 154 112 axiom bitvector_of_string:
Note: See TracChangeset
for help on using the changeset viewer.