Quelle Note_on_signed_division_on_words.thy Sprache: Isabelle

theory Note_on_signed_division_on_words
  imports "HOL-Library.Word" "HOL-Library.Centered_Division"
begin

unbundle bit_operations_syntax

context semiring_bit_operations
begin

lemma take_bit_Suc_from_most:
  \<open>take_bit (Suc n) a = 2 ^ n * of_bool (bit a n) OR take_bit n a\<close>
  by (rule bit_eqI) (auto simp add: bit_simps less_Suc_eq)

end

context ring_bit_operations
begin

lemma signed_take_bit_exp_eq_int:
  \<open>signed_take_bit m (2 ^ n) =
    (if n < m then 2 ^ n else if n = m then - (2 ^ n) else 0)\<close>
  by (rule bit_eqI) (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)

end

lift_definition signed_divide_word :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>  (infixl \<open>wdiv\<close> 70)
  is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a cdiv signed_take_bit (LENGTH('a) - Suc 0) b\<close>
  by (simp flip: signed_take_bit_decr_length_iff)

lift_definition signed_modulo_word :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>  (infixl \<open>wmod\<close> 70)
  is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a cmod signed_take_bit (LENGTH('a) - Suc 0) b\<close>
  by (simp flip: signed_take_bit_decr_length_iff)

lemma signed_take_bit_eq_wmod:
  \<open>signed_take_bit n w = w wmod (2 ^ Suc n)\<close>
proof (transfer fixing: n)
  show \<open>take_bit LENGTH('a) (signed_take_bit n (take_bit LENGTH('a) k)) =
    take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k cmod signed_take_bit (LENGTH('a) - Suc 0) (2 ^ Suc n))\ for k :: int
  proof (cases \<open>LENGTH('a) = Suc (Suc n)\<close>)
    case True
    then show ?thesis
      by (simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit cmod_minus_eq flip: power_Suc signed_take_bit_eq_cmod)
  next
    case False
    then show ?thesis
      by (auto simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit take_bit_signed_take_bit simp flip: power_Suc signed_take_bit_eq_cmod)
  qed
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.