Theory BitVector

header {* \isaheader{Formalization of Bit Vectors} *}

theory BitVector imports Main begin

type_synonym bit_vector = "bool list"

fun bv_leqs :: "bit_vector => bit_vector => bool" ("_ \<preceq>⇣b _" 99)
  where bv_Nils:"[] \<preceq>⇣b [] = True"
  | bv_Cons:"(x#xs) \<preceq>⇣b (y#ys) = ((x --> y) ∧ xs \<preceq>⇣b ys)"
  | bv_rest:"xs \<preceq>⇣b ys = False"


subsection {* Some basic properties *}

lemma bv_length: "xs \<preceq>⇣b ys ==> length xs = length ys"
by(induct rule:bv_leqs.induct)auto


lemma [dest!]: "xs \<preceq>⇣b [] ==> xs = []"
by(induct xs) auto


lemma bv_leqs_AppendI:
  "[|xs \<preceq>⇣b ys; xs' \<preceq>⇣b ys'|] ==> (xs@xs') \<preceq>⇣b (ys@ys')"
by(induct xs ys rule:bv_leqs.induct,auto)


lemma bv_leqs_AppendD:
  "[|(xs@xs') \<preceq>⇣b (ys@ys'); length xs = length ys|]
  ==> xs \<preceq>⇣b ys ∧ xs' \<preceq>⇣b ys'"
by(induct xs ys rule:bv_leqs.induct,auto)


lemma bv_leqs_eq:
  "xs \<preceq>⇣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 \<preceq>⇣b ys = 
    ((∀i < length xs. xs ! i --> ys ! i) ∧ length xs = length ys)`
  show ?case
  proof
    assume leqs:"x#xs \<preceq>⇣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 \<preceq>⇣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 \<preceq>⇣b ys` show "x#xs \<preceq>⇣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 \<preceq>⇣b xs"
by(induct xs) auto

lemma maximal_element:
  "xs \<preceq>⇣b replicate (length xs) True"
by(induct xs) auto

lemma bv_leqs_refl:"xs \<preceq>⇣b xs"
  by(induct xs) auto


lemma bv_leqs_trans:"[|xs \<preceq>⇣b ys; ys \<preceq>⇣b zs|] ==> xs \<preceq>⇣b zs"
proof(induct xs ys arbitrary:zs rule:bv_leqs.induct)
  case (2 x xs y ys)
  note IH = `!!zs. [|xs \<preceq>⇣b ys; ys \<preceq>⇣b zs|] ==> xs \<preceq>⇣b zs`
  from `(x#xs) \<preceq>⇣b (y#ys)` have "xs \<preceq>⇣b ys" and "x --> y" by simp_all
  from `(y#ys) \<preceq>⇣b zs` obtain z zs' where "zs = z#zs'" by(cases zs) auto
  with `(y#ys) \<preceq>⇣b zs` have "ys \<preceq>⇣b zs'" and "y --> z" by simp_all
  from IH[OF `xs \<preceq>⇣b ys` `ys \<preceq>⇣b zs'`] have "xs \<preceq>⇣b zs'" .
  with `x --> y` `y --> z` `zs = z#zs'` show ?case by simp
qed simp_all


lemma bv_leqs_antisym:"[|xs \<preceq>⇣b ys; ys \<preceq>⇣b xs|] ==> xs = ys"
  by(induct xs ys rule:bv_leqs.induct)auto


definition bv_less :: "bit_vector => bit_vector => bool" ("_ \<prec>⇣b _" 99)
  where "xs \<prec>⇣b ys ≡ xs \<preceq>⇣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