# HG changeset patch # User haftmann # Date 1597040844 -7200 # Node ID 9e0321263eb321eda92ad03392af535b4d56e9c8 # Parent 3707cf7b370b6c56ad750dda847939bf089791be consolidated names diff -r 3707cf7b370b -r 9e0321263eb3 src/HOL/ex/Word_Conversions.thy --- a/src/HOL/ex/Word_Conversions.thy Mon Aug 10 08:27:17 2020 +0200 +++ b/src/HOL/ex/Word_Conversions.thy Mon Aug 10 08:27:24 2020 +0200 @@ -103,42 +103,40 @@ abbreviation word_of_int :: \int \ 'a::len word\ where \word_of_int \ of_int\ -text \TODO rework names from here\ - lemma unsigned_of_nat [simp]: - \unsigned (of_nat n :: 'a::len word) = take_bit LENGTH('a) n\ + \unsigned (of_nat n :: 'a::len word) = of_nat (take_bit LENGTH('a) n)\ by transfer (simp add: nat_eq_iff take_bit_of_nat) -lemma of_nat_unsigned [simp]: - \of_nat (unsigned w) = w\ +lemma of_nat_of_word [simp]: + \of_nat (nat_of_word w) = unsigned w\ by transfer simp lemma of_int_unsigned [simp]: - \of_int (unsigned w) = w\ + \of_int (unsigned_int w) = unsigned w\ by transfer simp lemma unsigned_int_greater_eq: - \(0::int) \ unsigned w\ for w :: \'a::len word\ + \0 \ unsigned_int w\ for w :: \'a::len word\ by transfer simp -lemma unsigned_nat_less: - \unsigned w < (2 ^ LENGTH('a) :: nat)\ for w :: \'a::len word\ +lemma nat_of_word_less: + \nat_of_word w < 2 ^ LENGTH('a)\ for w :: \'a::len word\ by transfer (simp add: take_bit_eq_mod) lemma unsigned_int_less: - \unsigned w < (2 ^ LENGTH('a) :: int)\ for w :: \'a::len word\ + \unsigned_int w < 2 ^ LENGTH('a)\ for w :: \'a::len word\ by transfer (simp add: take_bit_eq_mod) lemma signed_of_int [simp]: - \signed (of_int k :: 'a::len word) = signed_take_bit (LENGTH('a) - 1) k\ + \signed (word_of_int k :: 'a::len word) = of_int (signed_take_bit (LENGTH('a) - 1) k)\ by transfer simp lemma of_int_signed [simp]: - \of_int (signed a) = a\ + \of_int (signed_int a) = signed a\ by transfer (simp_all add: take_bit_signed_take_bit) lemma signed_int_greater_eq: - \- ((2::int) ^ (LENGTH('a) - 1)) \ signed w\ for w :: \'a::len word\ + \- (2 ^ (LENGTH('a) - 1)) \ signed_int w\ for w :: \'a::len word\ proof (cases \bit w (LENGTH('a) - 1)\) case True then show ?thesis @@ -152,7 +150,7 @@ qed lemma signed_int_less: - \signed w < (2 ^ (LENGTH('a) - 1) :: int)\ for w :: \'a::len word\ + \signed_int w < 2 ^ (LENGTH('a) - 1)\ for w :: \'a::len word\ by (cases \bit w (LENGTH('a) - 1)\; transfer) (simp_all add: signed_take_bit_eq signed_take_bit_eq_or take_bit_int_less_exp not_eq_complement mask_eq_exp_minus_1 OR_upper) @@ -169,36 +167,36 @@ end -lemma of_nat_word_eq_iff: - \of_nat m = (of_nat n :: 'a::len word) \ take_bit LENGTH('a) m = take_bit LENGTH('a) n\ +lemma word_of_nat_eq_iff: + \word_of_nat m = (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m = take_bit LENGTH('a) n\ by transfer (simp add: take_bit_of_nat) -lemma of_nat_word_less_eq_iff: - \of_nat m \ (of_nat n :: 'a::len word) \ take_bit LENGTH('a) m \ take_bit LENGTH('a) n\ +lemma word_of_nat_less_eq_iff: + \word_of_nat m \ (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m \ take_bit LENGTH('a) n\ by transfer (simp add: take_bit_of_nat) -lemma of_nat_word_less_iff: - \of_nat m < (of_nat n :: 'a::len word) \ take_bit LENGTH('a) m < take_bit LENGTH('a) n\ +lemma word_of_nat_less_iff: + \word_of_nat m < (word_of_nat n :: 'a::len word) \ take_bit LENGTH('a) m < take_bit LENGTH('a) n\ by transfer (simp add: take_bit_of_nat) -lemma of_nat_word_eq_0_iff: - \of_nat n = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd n\ +lemma word_of_nat_eq_0_iff: + \word_of_nat n = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd n\ using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) -lemma of_int_word_eq_iff: - \of_int k = (of_int l :: 'a::len word) \ take_bit LENGTH('a) k = take_bit LENGTH('a) l\ +lemma word_of_int_eq_iff: + \word_of_int k = (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k = take_bit LENGTH('a) l\ by transfer rule -lemma of_int_word_less_eq_iff: - \of_int k \ (of_int l :: 'a::len word) \ take_bit LENGTH('a) k \ take_bit LENGTH('a) l\ +lemma word_of_int_less_eq_iff: + \word_of_int k \ (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k \ take_bit LENGTH('a) l\ by transfer rule -lemma of_int_word_less_iff: - \of_int k < (of_int l :: 'a::len word) \ take_bit LENGTH('a) k < take_bit LENGTH('a) l\ +lemma word_of_int_less_iff: + \word_of_int k < (word_of_int l :: 'a::len word) \ take_bit LENGTH('a) k < take_bit LENGTH('a) l\ by transfer rule -lemma of_int_word_eq_0_iff: - \of_int k = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd k\ +lemma word_of_int_eq_0_iff: + \word_of_int k = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd k\ using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) end