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.
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 w2 i - ones w1 i <= b2)%Z.
Definition subtyping (w1 w2: ibw) : Prop :=
prec w1 w2 /\ sync w1 w2.
Definition size (w1 w2: ibw) (s: nat) :=
forall i,
(ones w1 i) - (ones w2 i) <= s
/\
exists i, (ones w1 i) - (ones w2 i) = s.