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