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"