# Theory BitVector

```section ‹Formalization of Bit Vectors›

theory BitVector imports Main begin

type_synonym bit_vector = "bool list"

fun bv_leqs :: "bit_vector ⇒ bit_vector ⇒ bool" ("_ ≼⇩b _" 99)
where bv_Nils:"[] ≼⇩b [] = True"
| bv_Cons:"(x#xs) ≼⇩b (y#ys) = ((x ⟶ y) ∧ xs ≼⇩b ys)"
| bv_rest:"xs ≼⇩b ys = False"

subsection ‹Some basic properties›

lemma bv_length: "xs ≼⇩b ys ⟹ length xs = length ys"
by(induct rule:bv_leqs.induct)auto

lemma [dest!]: "xs ≼⇩b [] ⟹ xs = []"
by(induct xs) auto

lemma bv_leqs_AppendI:
"⟦xs ≼⇩b ys; xs' ≼⇩b ys'⟧ ⟹ (xs@xs') ≼⇩b (ys@ys')"
by(induct xs ys rule:bv_leqs.induct,auto)

lemma bv_leqs_AppendD:
"⟦(xs@xs') ≼⇩b (ys@ys'); length xs = length ys⟧
⟹ xs ≼⇩b ys ∧ xs' ≼⇩b ys'"
by(induct xs ys rule:bv_leqs.induct,auto)

lemma bv_leqs_eq:
"xs ≼⇩b ys = ((∀i < length xs. xs ! i ⟶ ys ! i) ∧ length xs = length ys)"
proof(induct xs ys rule:bv_leqs.induct)
case (2 x xs y ys)
note eq = ‹xs ≼⇩b ys =
((∀i < length xs. xs ! i ⟶ ys ! i) ∧ length xs = length ys)›
show ?case
proof
assume leqs:"x#xs ≼⇩b y#ys"
with eq have "x ⟶ y" and "∀i < length xs. xs ! i ⟶ ys ! i"
and "length xs = length ys" by simp_all
from ‹x ⟶ y› have "(x#xs) ! 0 ⟶ (y#ys) ! 0" by simp
{ fix i assume "i > 0" and "i < length (x#xs)"
then obtain j where "i = Suc j" and "j < length xs" by(cases i) auto
with ‹∀i < length xs. xs ! i ⟶ ys ! i›
have "(x#xs) ! i ⟶ (y#ys) ! i" by auto }
hence "∀i < length (x#xs). i > 0 ⟶ (x#xs) ! i ⟶ (y#ys) ! i" by simp
with ‹(x#xs) ! 0 ⟶ (y#ys) ! 0› ‹length xs = length ys›
show "(∀i < length (x#xs). (x#xs) ! i ⟶ (y#ys) ! i) ∧
length (x#xs) = length (y#ys)"
by clarsimp(case_tac "i>0",auto)
next
assume "(∀i < length (x#xs). (x#xs) ! i ⟶ (y#ys) ! i) ∧
length (x#xs) = length (y#ys)"
hence "∀i < length (x#xs). (x#xs) ! i ⟶ (y#ys) ! i"
and "length (x#xs) = length (y#ys)" by simp_all
from ‹∀i < length (x#xs). (x#xs) ! i ⟶ (y#ys) ! i›
have "∀i < length xs. xs ! i ⟶ ys ! i"
by clarsimp(erule_tac x="Suc i" in allE,auto)
with eq ‹length (x#xs) = length (y#ys)› have "xs ≼⇩b ys" by simp
from ‹∀i < length (x#xs). (x#xs) ! i ⟶ (y#ys) ! i›
have "x ⟶ y" by(erule_tac x="0" in allE) simp
with ‹xs ≼⇩b ys› show "x#xs ≼⇩b y#ys" by simp
qed
qed simp_all

subsection ‹\$\preceq_b\$ is an order on bit vectors with minimal and
maximal element›

lemma minimal_element:
"replicate (length xs) False ≼⇩b xs"
by(induct xs) auto

lemma maximal_element:
"xs ≼⇩b replicate (length xs) True"
by(induct xs) auto

lemma bv_leqs_refl:"xs ≼⇩b xs"
by(induct xs) auto

lemma bv_leqs_trans:"⟦xs ≼⇩b ys; ys ≼⇩b zs⟧ ⟹ xs ≼⇩b zs"
proof(induct xs ys arbitrary:zs rule:bv_leqs.induct)
case (2 x xs y ys)
note IH = ‹⋀zs. ⟦xs ≼⇩b ys; ys ≼⇩b zs⟧ ⟹ xs ≼⇩b zs›
from ‹(x#xs) ≼⇩b (y#ys)› have "xs ≼⇩b ys" and "x ⟶ y" by simp_all
from ‹(y#ys) ≼⇩b zs› obtain z zs' where "zs = z#zs'" by(cases zs) auto
with ‹(y#ys) ≼⇩b zs› have "ys ≼⇩b zs'" and "y ⟶ z" by simp_all
from IH[OF ‹xs ≼⇩b ys› ‹ys ≼⇩b zs'›] have "xs ≼⇩b zs'" .
with ‹x ⟶ y› ‹y ⟶ z› ‹zs = z#zs'› show ?case by simp
qed simp_all

lemma bv_leqs_antisym:"⟦xs ≼⇩b ys; ys ≼⇩b xs⟧ ⟹ xs = ys"
by(induct xs ys rule:bv_leqs.induct)auto

definition bv_less :: "bit_vector ⇒ bit_vector ⇒ bool" ("_ ≺⇩b _" 99)
where "xs ≺⇩b ys ≡ xs ≼⇩b ys ∧ xs ≠ ys"

interpretation order "bv_leqs" "bv_less"
by(unfold_locales,
auto intro:bv_leqs_refl bv_leqs_trans bv_leqs_antisym simp:bv_less_def)

end
```