Library ibw_def

Set Implicit Arguments.

Require Import Bool.
Require Import Omega.
Require Import misc.

Coercion Local Z_of_nat : nat >-> Z.

Definition ibw := nat -> bool.

Fixpoint ones (w:ibw) (i:nat) { struct i } :=
match i with
| 0 => 0
| S i' =>
let w_i := if w i then 1 else 0 in
w_i + ones w i'
end.

Fixpoint zeros (w:ibw) (i:nat) { struct i } :=
match i with
| 0 => 0
| S i' =>
let not_w_i := if w i then 0 else 1 in
not_w_i + zeros w i'
end.

Definition ibw_of_ones (ones_w: nat -> nat): ibw :=
fun i =>
match i with
| O => false
| S i' => negb (beq_nat (ones_w i) (ones_w i'))
end.

Definition on (w1:ibw) (w2:ibw) : ibw :=
(fun i =>
match w1 i with
| true => w2 (ones w1 i)
| false => false
end).

Definition not (w:ibw) : ibw :=
(fun n =>
match n with
| 0 => false
| _ => negb (w n)
end).

Definition prec (w1 w2: ibw) : Prop :=
forall i,
ones w1 i >= ones w2 i.

Definition ones_supremum (w1 w2: ibw) : nat -> nat :=
fun i => Arith.Min.min (ones w1 i) (ones w2 i).

Definition ones_infimum (w1 w2: ibw) : nat -> nat :=
fun i => Arith.Max.max (ones w1 i) (ones w2 i).

Definition supremum (w1 w2: ibw) : ibw :=
ibw_of_ones (ones_supremum w1 w2).

Definition infimum (w1 w2: ibw) : ibw :=
ibw_of_ones (ones_infimum w1 w2).

Definition sync (w1 w2: ibw) : Prop :=
exists b1: Z,
exists b2: Z,
forall i, (b1 <= ones w1 i - ones w2 i <= b2)%Z.

Definition adaptability (w1 w2: ibw) : Prop :=
prec w1 w2 /\ sync w1 w2.

Definition sizei (w1 w2: ibw) (i: nat) :=
((ones w1 i) - (ones w2 i))%Z.

Definition size (w1 w2: ibw) (s: Z) :=
(forall i, (sizei w1 w2 i <= s)%Z)
/\
(exists i, sizei w1 w2 i = s).