Require Export Arith_compl.
Require Export Bool_compl.
Require Export Lists_replace.

Definition BV := list bool.
Definition nilbv : BV := nil.
Definition consbv : bool -> BV -> BV := cons (A:=bool).
Definition appbv : BV -> BV -> BV := app (A:=bool).
Definition lengthbv : BV -> nat := length (A:=bool).
Definition lenbv : BV -> nat -> Prop := len bool.
Definition BV_null (n : nat) : BV := list_const bool n false.
Definition truncbv : BV -> nat -> BV := trunc bool.
Definition stripbv : BV -> nat -> BV := strip bool.
Definition field : BV -> nat -> nat -> BV := sublist bool.
Definition abit : BV -> nat -> BV := elemlist bool.
Definition bitset : BV -> nat -> bool -> BV := replace bool.
Definition BVnot (v : BV) : BV := map bool bool v negb.

Fixpoint BV_to_nat (v : BV) : nat :=
  match v return nat with
  | nil => 0
  | b :: w => bool_to_nat b + (BV_to_nat w + BV_to_nat w)
  end.

Lemma BV_to_nat_eq1 : BV_to_nat nilbv = 0.
auto with v62. Qed.
Lemma BV_to_nat_eq2 :
 forall (b : bool) (w : BV),
 BV_to_nat (consbv b w) = bool_to_nat b + (BV_to_nat w + BV_to_nat w).
auto with v62. Qed.



Lemma BV_to_nat_app :
 forall (l n : BV) (ll : nat),
 
 lenbv l ll -> BV_to_nat (appbv l n) = BV_to_nat l + power2 ll * BV_to_nat n.
unfold BV, lenbv, appbv in |- *. simple induction l. intros. inversion H. simpl in |- *. auto with v62.
intros. simpl in |- *. inversion H0. simpl in |- *.
rewrite (H n l1). rewrite mult_plus_distr_r. repeat rewrite plus_assoc.
rewrite
 (plus_permute2 (bool_to_nat a + BV_to_nat l0) (power2 l1 * BV_to_nat n)
    (BV_to_nat l0)).
auto with v62.
exact H4.
Qed. Hint Resolve BV_to_nat_app.

Lemma BV_to_nat_app2 :
 forall l n : BV,
 
 BV_to_nat (appbv l n) = BV_to_nat l + power2 (lengthbv l) * BV_to_nat n.
intros. apply BV_to_nat_app. auto with v62. unfold lenbv, lengthbv in |- *. apply len_length.
Qed. Hint Resolve BV_to_nat_app2.

Lemma BV_null_nat : forall n : nat, BV_to_nat (BV_null n) = 0.
unfold BV_null in |- *.
simple induction n; auto with v62.
intros. simpl in |- *. rewrite H. auto with v62.
Qed. Hint Resolve BV_null_nat.

Lemma length_BV_null : forall n : nat, lengthbv (BV_null n) = n.
unfold lengthbv, BV_null in |- *. intro. apply length_list_const.
Qed. Hint Resolve length_BV_null.