Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: interface.ml Sprache: Isabelle

Original von: Isabelle^©

(*  Author:  Florian Haftmann, TUM
*)

section \<open>Proof(s) of concept for algebraically founded lists of bits\<close>

theory Bit_Lists
  imports
    "HOL-Library.Word" "HOL-Library.More_List"
begin

subsection \<open>Fragments of algebraic bit representations\<close>

context comm_semiring_1
begin

abbreviation (input) unsigned_of_bits :: "bool list \ 'a"
  where "unsigned_of_bits \ horner_sum of_bool 2"

lemma unsigned_of_bits_replicate_False [simp]:
  "unsigned_of_bits (replicate n False) = 0"
  by (induction n) simp_all

end

context unique_euclidean_semiring_with_bit_shifts
begin

lemma unsigned_of_bits_append [simp]:
  "unsigned_of_bits (bs @ cs) = unsigned_of_bits bs
    + push_bit (length bs) (unsigned_of_bits cs)"
  by (induction bs) (simp_all add: push_bit_double,
    simp_all add: algebra_simps)

lemma unsigned_of_bits_take [simp]:
  "unsigned_of_bits (take n bs) = take_bit n (unsigned_of_bits bs)"
proof (induction bs arbitrary: n)
  case Nil
  then show ?case
    by simp
next
  case (Cons b bs)
  then show ?case
    by (cases n) (simp_all add: ac_simps take_bit_Suc)
qed

lemma unsigned_of_bits_drop [simp]:
  "unsigned_of_bits (drop n bs) = drop_bit n (unsigned_of_bits bs)"
proof (induction bs arbitrary: n)
  case Nil
  then show ?case
    by simp
next
  case (Cons b bs)
  then show ?case
    by (cases n) (simp_all add: drop_bit_Suc)
qed

lemma bit_unsigned_of_bits_iff:
  \<open>bit (unsigned_of_bits bs) n \<longleftrightarrow> nth_default False bs n\<close>
proof (induction bs arbitrary: n)
  case Nil
  then show ?case
    by simp
next
  case (Cons b bs)
  then show ?case
    by (cases n) (simp_all add: bit_Suc)
qed

primrec n_bits_of :: "nat \ 'a \ bool list"
  where
    "n_bits_of 0 a = []"
  | "n_bits_of (Suc n) a = odd a # n_bits_of n (a div 2)"

lemma n_bits_of_eq_iff:
  "n_bits_of n a = n_bits_of n b \ take_bit n a = take_bit n b"
  apply (induction n arbitrary: a b)
   apply (auto elim!: evenE oddE simp add: take_bit_Suc mod_2_eq_odd)
    apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one)
   apply (metis dvd_triv_right even_plus_one_iff odd_iff_mod_2_eq_one)
  done

lemma take_n_bits_of [simp]:
  "take m (n_bits_of n a) = n_bits_of (min m n) a"
proof -
  define q and v and w where "q = min m n" and "v = m - q" and "w = n - q"
  then have "v = 0 \ w = 0"
    by auto
  then have "take (q + v) (n_bits_of (q + w) a) = n_bits_of q a"
    by (induction q arbitrary: a) auto
  with q_def v_def w_def show ?thesis
    by simp
qed

lemma unsigned_of_bits_n_bits_of [simp]:
  "unsigned_of_bits (n_bits_of n a) = take_bit n a"
  by (induction n arbitrary: a) (simp_all add: ac_simps take_bit_Suc mod_2_eq_odd)

end

subsection \<open>Syntactic bit representation\<close>

class bit_representation =
  fixes bits_of :: "'a \ bool list"
    and of_bits :: "bool list \ 'a"
  assumes of_bits_of [simp]: "of_bits (bits_of a) = a"

text \<open>Unclear whether a \<^typ>\<open>bool\<close> instantiation is needed or not\<close>

instantiation nat :: bit_representation
begin

fun bits_of_nat :: "nat \ bool list"
  where "bits_of (n::nat) =
    (if n = 0 then [] else odd n # bits_of (n div 2))"

lemma bits_of_nat_simps [simp]:
  "bits_of (0::nat) = []"
  "n > 0 \ bits_of n = odd n # bits_of (n div 2)" for n :: nat
  by simp_all

declare bits_of_nat.simps [simp del]

definition of_bits_nat :: "bool list \ nat"
  where [simp]: "of_bits_nat = unsigned_of_bits"
  \<comment> \<open>remove simp\<close>

instance proof
  show "of_bits (bits_of n) = n" for n :: nat
    by (induction n rule: nat_bit_induct) simp_all
qed

end

lemma bit_of_bits_nat_iff:
  \<open>bit (of_bits bs :: nat) n \<longleftrightarrow> nth_default False bs n\<close>
  by (simp add: bit_unsigned_of_bits_iff)

lemma bits_of_Suc_0 [simp]:
  "bits_of (Suc 0) = [True]"
  by simp

lemma bits_of_1_nat [simp]:
  "bits_of (1 :: nat) = [True]"
  by simp

lemma bits_of_nat_numeral_simps [simp]:
  "bits_of (numeral Num.One :: nat) = [True]" (is ?One)
  "bits_of (numeral (Num.Bit0 n) :: nat) = False # bits_of (numeral n :: nat)" (is ?Bit0)
  "bits_of (numeral (Num.Bit1 n) :: nat) = True # bits_of (numeral n :: nat)" (is ?Bit1)
proof -
  show ?One
    by simp
  define m :: nat where "m = numeral n"
  then have "m > 0" and *: "numeral n = m" "numeral (Num.Bit0 n) = 2 * m" "numeral (Num.Bit1 n) = Suc (2 * m)"
    by simp_all
  from \<open>m > 0\<close> show ?Bit0 ?Bit1
    by (simp_all add: *)
qed

lemma unsigned_of_bits_of_nat [simp]:
  "unsigned_of_bits (bits_of n) = n" for n :: nat
  using of_bits_of [of n] by simp

instantiation int :: bit_representation
begin

fun bits_of_int :: "int \ bool list"
  where "bits_of_int k = odd k #
    (if k = 0 \<or> k = - 1 then [] else bits_of_int (k div 2))"

lemma bits_of_int_simps [simp]:
  "bits_of (0 :: int) = [False]"
  "bits_of (- 1 :: int) = [True]"
  "k \ 0 \ k \ - 1 \ bits_of k = odd k # bits_of (k div 2)" for k :: int
  by simp_all

lemma bits_of_not_Nil [simp]:
  "bits_of k \ []" for k :: int
  by simp

declare bits_of_int.simps [simp del]

definition of_bits_int :: "bool list \ int"
  where "of_bits_int bs = (if bs = [] \ \ last bs then unsigned_of_bits bs
    else unsigned_of_bits bs - 2 ^ length bs)"

lemma of_bits_int_simps [simp]:
  "of_bits [] = (0 :: int)"
  "of_bits [False] = (0 :: int)"
  "of_bits [True] = (- 1 :: int)"
  "of_bits (bs @ [b]) = (unsigned_of_bits bs :: int) - (2 ^ length bs) * of_bool b"
  "of_bits (False # bs) = 2 * (of_bits bs :: int)"
  "bs \ [] \ of_bits (True # bs) = 1 + 2 * (of_bits bs :: int)"
  by (simp_all add: of_bits_int_def push_bit_of_1)

instance proof
  show "of_bits (bits_of k) = k" for k :: int
    by (induction k rule: int_bit_induct) simp_all
qed

lemma bits_of_1_int [simp]:
  "bits_of (1 :: int) = [True, False]"
  by simp

lemma bits_of_int_numeral_simps [simp]:
  "bits_of (numeral Num.One :: int) = [True, False]" (is ?One)
  "bits_of (numeral (Num.Bit0 n) :: int) = False # bits_of (numeral n :: int)" (is ?Bit0)
  "bits_of (numeral (Num.Bit1 n) :: int) = True # bits_of (numeral n :: int)" (is ?Bit1)
  "bits_of (- numeral (Num.Bit0 n) :: int) = False # bits_of (- numeral n :: int)" (is ?nBit0)
  "bits_of (- numeral (Num.Bit1 n) :: int) = True # bits_of (- numeral (Num.inc n) :: int)" (is ?nBit1)
proof -
  show ?One
    by simp
  define k :: int where "k = numeral n"
  then have "k > 0" and *: "numeral n = k" "numeral (Num.Bit0 n) = 2 * k" "numeral (Num.Bit1 n) = 2 * k + 1"
    "numeral (Num.inc n) = k + 1"
    by (simp_all add: add_One)
  have "- (2 * k) div 2 = - k" "(- (2 * k) - 1) div 2 = - k - 1"
    by simp_all
  with \<open>k > 0\<close> show ?Bit0 ?Bit1 ?nBit0 ?nBit1
    by (simp_all add: *)
qed

lemma bit_of_bits_int_iff:
  \<open>bit (of_bits bs :: int) n \<longleftrightarrow> nth_default (bs \<noteq> [] \<and> last bs) bs n\<close>
proof (induction bs arbitrary: n)
  case Nil
  then show ?case
    by simp
next
  case (Cons b bs)
  then show ?case
    by (cases n; cases b; cases bs) (simp_all add: bit_Suc)
qed

lemma of_bits_append [simp]:
  "of_bits (bs @ cs) = of_bits bs + push_bit (length bs) (of_bits cs :: int)"
    if "bs \ []" "\ last bs"
using that proof (induction bs rule: list_nonempty_induct)
  case (single b)
  then show ?case
    by simp
next
  case (cons b bs)
  then show ?case
    by (cases b) (simp_all add: push_bit_double)
qed

lemma of_bits_replicate_False [simp]:
  "of_bits (replicate n False) = (0 :: int)"
  by (auto simp add: of_bits_int_def)

lemma of_bits_drop [simp]:
  "of_bits (drop n bs) = drop_bit n (of_bits bs :: int)"
    if "n < length bs"
using that proof (induction bs arbitrary: n)
  case Nil
  then show ?case
    by simp
next
  case (Cons b bs)
  show ?case
  proof (cases n)
    case 0
    then show ?thesis
      by simp
  next
    case (Suc n)
    with Cons.prems have "bs \ []"
      by auto
    with Suc Cons.IH [of n] Cons.prems show ?thesis
      by (cases b) (simp_all add: drop_bit_Suc)
  qed
qed

end

lemma unsigned_of_bits_eq_of_bits:
  "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)"
  by (simp add: of_bits_int_def)

unbundle word.lifting

instantiation word :: (len) bit_representation
begin

lift_definition bits_of_word :: "'a word \ bool list"
  is "n_bits_of LENGTH('a)"
  by (simp add: n_bits_of_eq_iff)

lift_definition of_bits_word :: "bool list \ 'a word"
  is unsigned_of_bits .

instance proof
  fix a :: "'a word"
  show "of_bits (bits_of a) = a"
    by transfer simp
qed

end

lifting_update word.lifting
lifting_forget word.lifting

subsection \<open>Bit representations with bit operations\<close>

class semiring_bit_representation = semiring_bit_operations + bit_representation +
  assumes and_eq: "length bs = length cs \
      of_bits bs AND of_bits cs = of_bits (map2 (\<and>) bs cs)"
    and or_eq: "length bs = length cs \
      of_bits bs OR of_bits cs = of_bits (map2 (\<or>) bs cs)"
    and xor_eq: "length bs = length cs \
      of_bits bs XOR of_bits cs = of_bits (map2 (\<noteq>) bs cs)"
    and push_bit_eq: "push_bit n a = of_bits (replicate n False @ bits_of a)"
    and drop_bit_eq: "n < length (bits_of a) \ drop_bit n a = of_bits (drop n (bits_of a))"

class ring_bit_representation = ring_bit_operations + semiring_bit_representation +
  assumes not_eq: "not = of_bits \ map Not \ bits_of"

instance nat :: semiring_bit_representation
  by standard (simp_all add: bit_eq_iff bit_unsigned_of_bits_iff nth_default_map2 [of _ _ _ False False]
    bit_and_iff bit_or_iff bit_xor_iff)

instance int :: ring_bit_representation
proof
  {
    fix bs cs :: \<open>bool list\<close>
    assume \<open>length bs = length cs\<close>
    then have \<open>cs = [] \<longleftrightarrow> bs = []\<close>
      by auto
    with \<open>length bs = length cs\<close> have \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<and>) bs cs) \<longleftrightarrow> (bs \<noteq> [] \<and> last bs) \<and> (cs \<noteq> [] \<and> last cs)\<close>
      and \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<or>) bs cs) \<longleftrightarrow> (bs \<noteq> [] \<and> last bs) \<or> (cs \<noteq> [] \<and> last cs)\<close>
      and \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<noteq>) bs cs) \<longleftrightarrow> ((bs \<noteq> [] \<and> last bs) \<noteq> (cs \<noteq> [] \<and> last cs))\<close>
      by (auto simp add: last_map last_zip zip_eq_Nil_iff prod_eq_iff)
    then show \<open>of_bits bs AND of_bits cs = (of_bits (map2 (\<and>) bs cs) :: int)\<close>
      and \<open>of_bits bs OR of_bits cs = (of_bits (map2 (\<or>) bs cs) :: int)\<close>
      and \<open>of_bits bs XOR of_bits cs = (of_bits (map2 (\<noteq>) bs cs) :: int)\<close>
      by (simp_all add: fun_eq_iff bit_eq_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff bit_of_bits_int_iff \<open>length bs = length cs\<close> nth_default_map2 [of bs cs _ \<open>bs \<noteq> [] \<and> last bs\<close> \<open>cs \<noteq> [] \<and> last cs\<close>])
  }
  show \<open>push_bit n k = of_bits (replicate n False @ bits_of k)\<close>
    for k :: int and n :: nat
    by (cases "n = 0") simp_all
  show \<open>drop_bit n k = of_bits (drop n (bits_of k))\<close>
    if \<open>n < length (bits_of k)\<close> for k :: int and n :: nat
    using that by simp
  show \<open>(not :: int \<Rightarrow> _) = of_bits \<circ> map Not \<circ> bits_of\<close>
  proof (rule sym, rule ext)
    fix k :: int
    show \<open>(of_bits \<circ> map Not \<circ> bits_of) k = NOT k\<close>
      by (induction k rule: int_bit_induct) (simp_all add: not_int_def)
  qed
qed

end

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.