Theory Native_Word.Word_Type_Copies
chapter ‹Systematic approach towards type copies of word type›
theory Word_Type_Copies
imports
"HOL-Library.Word"
"Word_Lib.Most_significant_bit"
"Word_Lib.Least_significant_bit"
"Word_Lib.Generic_set_bit"
"Word_Lib.Bit_Comprehension"
"Code_Target_Word_Base"
begin
section ‹Establishing type class instances for type copies of word type›
text ‹The lifting machinery is not localized, hence the abstract proofs are carried out using morphisms.›
locale word_type_copy =
fixes of_word :: ‹'b::len word ⇒ 'a›
and word_of :: ‹'a ⇒ 'b word›
assumes type_definition: ‹type_definition word_of of_word UNIV›
begin
lemma word_of_word:
‹word_of (of_word w) = w›
using type_definition by (simp add: type_definition_def)
lemma of_word_of [code abstype]:
‹of_word (word_of p) = p›
using type_definition by (simp add: type_definition_def)
lemma word_of_eqI:
‹p = q› if ‹word_of p = word_of q›
proof -
from that have ‹of_word (word_of p) = of_word (word_of q)›
by simp
then show ?thesis
by (simp add: of_word_of)
qed
lemma eq_iff_word_of:
‹p = q ⟷ word_of p = word_of q›
by (auto intro: word_of_eqI)
end
bundle constraintless
begin
declaration ‹
let
val cs = map (rpair NONE o fst o dest_Const)
[\<^term>‹0›, \<^term>‹(+)›, \<^term>‹uminus›, \<^term>‹(-)›,
\<^term>‹1›, \<^term>‹(*)›, \<^term>‹(div)›, \<^term>‹(mod)›,
\<^term>‹HOL.equal›, \<^term>‹(≤)›, \<^term>‹(<)›,
\<^term>‹(dvd)›, \<^term>‹of_bool›, \<^term>‹numeral›, \<^term>‹of_nat›,
\<^term>‹bit›,
\<^term>‹Bit_Operations.not›, \<^term>‹Bit_Operations.and›, \<^term>‹Bit_Operations.or›, \<^term>‹Bit_Operations.xor›, \<^term>‹mask›,
\<^term>‹push_bit›, \<^term>‹drop_bit›, \<^term>‹take_bit›,
\<^term>‹Bit_Operations.set_bit›, \<^term>‹unset_bit›, \<^term>‹flip_bit›,
\<^term>‹msb›, \<^term>‹size›, \<^term>‹Generic_set_bit.set_bit›, \<^term>‹set_bits›]
in
K (Context.mapping I (fold Proof_Context.add_const_constraint cs))
end
›
end
locale word_type_copy_ring = word_type_copy
opening constraintless +
constrains word_of :: ‹'a ⇒ 'b::len word›
assumes word_of_0 [code]: ‹word_of 0 = 0›
and word_of_1 [code]: ‹word_of 1 = 1›
and word_of_add [code]: ‹word_of (p + q) = word_of p + word_of q›
and word_of_minus [code]: ‹word_of (- p) = - (word_of p)›
and word_of_diff [code]: ‹word_of (p - q) = word_of p - word_of q›
and word_of_mult [code]: ‹word_of (p * q) = word_of p * word_of q›
and word_of_div [code]: ‹word_of (p div q) = word_of p div word_of q›
and word_of_mod [code]: ‹word_of (p mod q) = word_of p mod word_of q›
and equal_iff_word_of [code]: ‹HOL.equal p q ⟷ HOL.equal (word_of p) (word_of q)›
and less_eq_iff_word_of [code]: ‹p ≤ q ⟷ word_of p ≤ word_of q›
and less_iff_word_of [code]: ‹p < q ⟷ word_of p < word_of q›
begin
lemma of_class_comm_ring_1:
‹OFCLASS('a, comm_ring_1_class)›
by standard (simp_all add: eq_iff_word_of word_of_0 word_of_1
word_of_add word_of_minus word_of_diff word_of_mult algebra_simps)
lemma of_class_semiring_modulo:
‹OFCLASS('a, semiring_modulo_class)›
by standard (simp_all add: eq_iff_word_of word_of_0 word_of_1
word_of_add word_of_minus word_of_diff word_of_mult word_of_mod word_of_div algebra_simps
mod_mult_div_eq)
lemma of_class_equal:
‹OFCLASS('a, equal_class)›
by standard (simp add: eq_iff_word_of equal_iff_word_of equal)
lemma of_class_linorder:
‹OFCLASS('a, linorder_class)›
by standard (auto simp add: eq_iff_word_of less_eq_iff_word_of less_iff_word_of)
end
locale word_type_copy_bits = word_type_copy_ring
opening constraintless and bit_operations_syntax +
constrains word_of :: ‹'a::{comm_ring_1, semiring_modulo, equal, linorder} ⇒ 'b::len word›
fixes signed_drop_bit :: ‹nat ⇒ 'a ⇒ 'a›
assumes bit_eq_word_of [code]: ‹bit p = bit (word_of p)›
and word_of_not [code]: ‹word_of (NOT p) = NOT (word_of p)›
and word_of_and [code]: ‹word_of (p AND q) = word_of p AND word_of q›
and word_of_or [code]: ‹word_of (p OR q) = word_of p OR word_of q›
and word_of_xor [code]: ‹word_of (p XOR q) = word_of p XOR word_of q›
and word_of_mask [code]: ‹word_of (mask n) = mask n›
and word_of_push_bit [code]: ‹word_of (push_bit n p) = push_bit n (word_of p)›
and word_of_drop_bit [code]: ‹word_of (drop_bit n p) = drop_bit n (word_of p)›
and word_of_signed_drop_bit [code]: ‹word_of (signed_drop_bit n p) = Word.signed_drop_bit n (word_of p)›
and word_of_take_bit [code]: ‹word_of (take_bit n p) = take_bit n (word_of p)›
and word_of_set_bit [code]: ‹word_of (Bit_Operations.set_bit n p) = Bit_Operations.set_bit n (word_of p)›
and word_of_unset_bit [code]: ‹word_of (unset_bit n p) = unset_bit n (word_of p)›
and word_of_flip_bit [code]: ‹word_of (flip_bit n p) = flip_bit n (word_of p)›
begin
lemma word_of_bool:
‹word_of (of_bool n) = of_bool n›
by (simp add: word_of_0 word_of_1)
lemma word_of_nat:
‹word_of (of_nat n) = of_nat n›
by (induction n) (simp_all add: word_of_0 word_of_1 word_of_add)
lemma word_of_numeral [simp]:
‹word_of (numeral n) = numeral n›
proof -
have ‹word_of (of_nat (numeral n)) = of_nat (numeral n)›
by (simp only: word_of_nat)
then show ?thesis by simp
qed
lemma word_of_power:
‹word_of (p ^ n) = word_of p ^ n›
by (induction n) (simp_all add: word_of_1 word_of_mult)
lemma even_iff_word_of:
‹2 dvd p ⟷ 2 dvd word_of p› (is ‹?P ⟷ ?Q›)
proof
assume ?P
then obtain q where ‹p = 2 * q› ..
then show ?Q by (simp add: word_of_mult)
next
assume ?Q
then obtain w where ‹word_of p = 2 * w› ..
then have ‹of_word (word_of p) = of_word (2 * w)›
by simp
then have ‹p = 2 * of_word w›
by (simp add: eq_iff_word_of word_of_word word_of_mult)
then show ?P
by simp
qed
lemma of_class_ring_bit_operations:
‹OFCLASS('a, ring_bit_operations_class)›
proof -
have induct: ‹P p› if stable: ‹(⋀p. p div 2 = p ⟹ P p)›
and rec: ‹(⋀p b. P p ⟹ (of_bool b + 2 * p) div 2 = p ⟹ P (of_bool b + 2 * p))›
for p :: 'a and P
proof -
from stable have stable': ‹(⋀p. word_of p div 2 = word_of p ⟹ P p)›
by (simp add: eq_iff_word_of word_of_div)
from rec have rec': ‹(⋀p b. P p ⟹ (of_bool b + 2 * word_of p) div 2 = word_of p ⟹ P (of_bool b + 2 * p))›
by (simp add: eq_iff_word_of word_of_add word_of_bool word_of_mult word_of_div)
define w where ‹w = word_of p›
then have ‹p = of_word w›
by (simp add: of_word_of)
also have ‹P (of_word w)›
proof (induction w rule: bit_induct)
case (stable w)
show ?case
by (rule stable') (simp add: word_of_word stable)
next
case (rec w b)
have ‹P (of_bool b + 2 * of_word w)›
by (rule rec') (simp_all add: word_of_word rec)
also have ‹of_bool b + 2 * of_word w = of_word (of_bool b + 2 * w)›
by (simp add: eq_iff_word_of word_of_word word_of_add word_of_1 word_of_mult word_of_0)
finally show ?case .
qed
finally show ‹P p› .
qed
have ‹class.semiring_parity_axioms (+) (0::'a) (*) 1 (div) (mod)›
by standard
(simp_all add: eq_iff_word_of word_of_0 word_of_1 even_iff_word_of word_of_add word_of_div word_of_mod even_iff_mod_2_eq_zero)
with of_class_semiring_modulo have ‹OFCLASS('a, semiring_parity_class)›
by (rule semiring_parity_class.intro)
moreover have ‹OFCLASS('a, semiring_modulo_trivial_class)›
apply standard
apply (simp_all only: eq_iff_word_of word_of_0 word_of_1 word_of_div)
apply simp_all
done
moreover have ‹class.semiring_bits_axioms (+) (0::'a) (*) 1 (div) (mod) bit›
apply standard
apply (fact induct)
apply (simp_all only: eq_iff_word_of word_of_0 word_of_1 word_of_bool word_of_numeral
word_of_add word_of_diff word_of_mult word_of_div word_of_mod word_of_power
bit_eq_word_of push_bit_take_bit drop_bit_take_bit even_iff_word_of
fold_possible_bit
flip: push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod mask_eq_exp_minus_1 drop_bit_Suc)
apply (simp_all add: bit_simps even_drop_bit_iff_not_bit not_less)
done
ultimately have ‹OFCLASS('a, semiring_bits_class)›
by (rule semiring_bits_class.intro)
moreover have ‹class.semiring_bit_operations_axioms (+) (-) (0::'a) (*) (1::'a) (div) (mod) (AND) (OR) (XOR) mask Bit_Operations.set_bit unset_bit flip_bit push_bit drop_bit take_bit›
apply standard
apply (simp_all add: eq_iff_word_of word_of_add word_of_push_bit word_of_power
bit_eq_word_of word_of_and word_of_or word_of_xor word_of_mask word_of_diff
word_of_0 word_of_1 bit_simps
word_of_set_bit set_bit_eq_or word_of_unset_bit unset_bit_eq_or_xor word_of_flip_bit flip_bit_eq_xor
word_of_mult
word_of_drop_bit word_of_div word_of_take_bit word_of_mod
and_rec [of ‹word_of a› ‹word_of b› for a b]
or_rec [of ‹word_of a› ‹word_of b› for a b]
xor_rec [of ‹word_of a› ‹word_of b› for a b] even_iff_word_of
flip: mask_eq_exp_minus_1 push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod)
done
ultimately have ‹OFCLASS('a, semiring_bit_operations_class)›
by (rule semiring_bit_operations_class.intro)
moreover have ‹OFCLASS('a, ring_parity_class)›
using ‹OFCLASS('a, semiring_parity_class)› by (rule ring_parity_class.intro) standard
moreover have ‹class.ring_bit_operations_axioms (-) (1::'a) uminus NOT›
by standard
(simp add: eq_iff_word_of word_of_not word_of_diff word_of_minus word_of_1 not_eq_complement)
ultimately show ‹OFCLASS('a, ring_bit_operations_class)›
by (rule ring_bit_operations_class.intro)
qed
lemma [code]:
‹take_bit n a = a AND mask n› for a :: 'a
by (simp add: eq_iff_word_of word_of_take_bit word_of_and word_of_mask take_bit_eq_mask)
lemma [code]:
‹mask (Suc n) = push_bit n (1 :: 'a) OR mask n›
‹mask 0 = (0 :: 'a)›
by (simp_all add: eq_iff_word_of word_of_mask word_of_or word_of_push_bit word_of_0 word_of_1 mask_Suc_exp)
lemma [code]:
‹Bit_Operations.set_bit n w = w OR push_bit n 1› for w :: 'a
by (simp add: eq_iff_word_of word_of_set_bit word_of_or word_of_push_bit word_of_1 set_bit_eq_or)
lemma [code]:
‹unset_bit n w = w AND NOT (push_bit n 1)› for w :: 'a
by (simp add: eq_iff_word_of word_of_unset_bit word_of_and word_of_not word_of_push_bit word_of_1 unset_bit_eq_and_not)
lemma [code]:
‹flip_bit n w = w XOR push_bit n 1› for w :: 'a
by (simp add: eq_iff_word_of word_of_flip_bit word_of_xor word_of_push_bit word_of_1 flip_bit_eq_xor)
end
locale word_type_copy_more = word_type_copy_bits +
constrains word_of :: ‹'a::{ring_bit_operations, equal, linorder} ⇒ 'b::len word›
fixes of_nat :: ‹nat ⇒ 'a› and nat_of :: ‹'a ⇒ nat›
and of_int :: ‹int ⇒ 'a› and int_of :: ‹'a ⇒ int›
and of_integer :: ‹integer ⇒ 'a› and integer_of :: ‹'a ⇒ integer›
assumes word_of_nat_eq: ‹word_of (of_nat n) = word_of_nat n›
and nat_of_eq_word_of: ‹nat_of p = unat (word_of p)›
and word_of_int_eq: ‹word_of (of_int k) = word_of_int k›
and int_of_eq_word_of: ‹int_of p = uint (word_of p)›
and word_of_integer_eq: ‹word_of (of_integer l) = word_of_integer l›
and integer_of_eq_word_of: ‹integer_of p = unsigned (word_of p)›
begin
lemma of_word_numeral [code_post]:
‹of_word (numeral n) = numeral n›
by (simp add: eq_iff_word_of word_of_word)
lemma of_word_0 [code_post]:
‹of_word 0 = 0›
by (simp add: eq_iff_word_of word_of_0 word_of_word)
lemma of_word_1 [code_post]:
‹of_word 1 = 1›
by (simp add: eq_iff_word_of word_of_1 word_of_word)
text ‹Use pretty numerals from integer for pretty printing›
lemma numeral_eq_integer [code_unfold]:
‹numeral n = of_integer (numeral n)›
by (simp add: eq_iff_word_of word_of_integer_eq)
lemma neg_numeral_eq_integer [code_unfold]:
‹- numeral n = of_integer (- numeral n)›
by (simp add: eq_iff_word_of word_of_integer_eq word_of_minus)
end
locale word_type_copy_misc = word_type_copy_more
opening constraintless and bit_operations_syntax +
constrains word_of :: ‹'a::{ring_bit_operations, equal, linorder} ⇒ 'b::len word›
fixes size :: nat and set_bits_aux :: ‹(nat ⇒ bool) ⇒ nat ⇒ 'a ⇒ 'a›
assumes size_eq_length: ‹size = LENGTH('b::len)›
and msb_iff_word_of [code]: ‹msb p ⟷ msb (word_of p)›
and size_eq_word_of: ‹Nat.size (p :: 'a) = Nat.size (word_of p)›
and word_of_generic_set_bit [code]: ‹word_of (Generic_set_bit.set_bit p n b) = Generic_set_bit.set_bit (word_of p) n b›
and word_of_set_bits: ‹word_of (set_bits P) = set_bits P›
and word_of_set_bits_aux: ‹word_of (set_bits_aux P n p) = Bit_Comprehension.set_bits_aux P n (word_of p)›
begin
lemma size_eq [code]:
‹Nat.size p = size› for p :: 'a
by (simp add: size_eq_length size_eq_word_of word_size)
lemma set_bits_aux_code [code]:
‹set_bits_aux f n w =
(if n = 0 then w
else let n' = n - 1 in set_bits_aux f n' (push_bit 1 w OR (if f n' then 1 else 0)))›
by (simp add: eq_iff_word_of word_of_set_bits_aux Let_def word_of_mult word_of_or word_of_0 word_of_1 set_bits_aux_rec [of f n])
lemma set_bits_code [code]: ‹set_bits P = set_bits_aux P size 0›
by (simp add: fun_eq_iff eq_iff_word_of word_of_set_bits word_of_set_bits_aux word_of_0 size_eq_length set_bits_conv_set_bits_aux)
lemma of_class_set_bit:
‹OFCLASS('a, set_bit_class)›
by standard (simp add: eq_iff_word_of word_of_generic_set_bit bit_eq_word_of word_of_power word_of_0 bit_simps linorder_not_le)
lemma of_class_bit_comprehension:
‹OFCLASS('a, bit_comprehension_class)›
by standard (simp add: eq_iff_word_of word_of_set_bits bit_eq_word_of set_bits_bit_eq)
end
section ‹Establishing operation variants tailored towards target languages›
locale word_type_copy_target_language = word_type_copy_misc +
constrains word_of :: ‹'a::{ring_bit_operations, equal, linorder, Generic_set_bit.set_bit} ⇒ 'b::len word›
fixes size_integer :: integer
and almost_size :: nat
assumes size_integer_eq_length: ‹size_integer = Nat.of_nat LENGTH('b::len)›
and almost_size_eq_decr_length: ‹almost_size = LENGTH('b::len) - Suc 0›
begin
definition shiftl :: ‹'a ⇒ integer ⇒ 'a›
where ‹shiftl w k = (if k < 0 ∨ size_integer ≤ k then undefined (push_bit :: nat ⇒ 'a ⇒ 'a) w k
else push_bit (nat_of_integer k) w)›
lemma word_of_shiftl [code abstract]:
‹word_of (shiftl w k) =
(if k < 0 ∨ size_integer ≤ k then word_of (undefined (push_bit :: _ ⇒ _ ⇒ 'a) w k)
else push_bit (nat_of_integer k) (word_of w))›
by (simp add: shiftl_def word_of_push_bit)
lemma push_bit_code [code]:
‹push_bit k w = (if k < size then shiftl w (integer_of_nat k) else 0)›
by (rule word_of_eqI)
(simp add: integer_of_nat_eq_of_nat word_of_push_bit word_of_0 shiftl_def, simp add: size_eq_length size_integer_eq_length)
definition shiftr :: ‹'a ⇒ integer ⇒ 'a›
where ‹shiftr w k = (if k < 0 ∨ size_integer ≤ k then undefined (drop_bit :: nat ⇒ 'a ⇒ 'a) w k
else drop_bit (nat_of_integer k) w)›
lemma word_of_shiftr [code abstract]:
‹word_of (shiftr w k) =
(if k < 0 ∨ size_integer ≤ k then word_of (undefined (drop_bit :: _ ⇒ _ ⇒ 'a) w k)
else drop_bit (nat_of_integer k) (word_of w))›
by (simp add: shiftr_def word_of_drop_bit)
lemma drop_bit_code [code]:
‹drop_bit k w = (if k < size then shiftr w (integer_of_nat k) else 0)›
by (rule word_of_eqI)
(simp add: integer_of_nat_eq_of_nat word_of_drop_bit word_of_0 shiftr_def, simp add: size_eq_length size_integer_eq_length)
definition sshiftr :: ‹'a ⇒ integer ⇒ 'a›
where ‹sshiftr w k = (if k < 0 ∨ size_integer ≤ k then undefined (signed_drop_bit :: _ ⇒ _ ⇒ 'a) w k
else signed_drop_bit (nat_of_integer k) w)›
lemma word_of_sshiftr [code abstract]:
‹word_of (sshiftr w k) =
(if k < 0 ∨ size_integer ≤ k then word_of (undefined (signed_drop_bit :: _ ⇒ _ ⇒ 'a) w k)
else Word.signed_drop_bit (nat_of_integer k) (word_of w))›
by (simp add: sshiftr_def word_of_signed_drop_bit)
lemma signed_drop_bit_code [code]:
‹signed_drop_bit k w = (if k < size then sshiftr w (integer_of_nat k)
else if (bit w almost_size) then - 1 else 0)›
by (rule word_of_eqI)
(simp add: integer_of_nat_eq_of_nat word_of_signed_drop_bit
word_of_0 word_of_1 word_of_minus sshiftr_def bit_eq_word_of not_less,
simp add: size_eq_length size_integer_eq_length almost_size_eq_decr_length signed_drop_bit_beyond)
definition test_bit :: ‹'a ⇒ integer ⇒ bool›
where ‹test_bit w k = (if k < 0 ∨ size_integer ≤ k then undefined (bit :: 'a ⇒ _) w k
else bit w (nat_of_integer k))›
lemma test_bit_eq [code]:
‹test_bit w k = (if k < 0 ∨ size_integer ≤ k then undefined (bit :: 'a ⇒ _) w k
else bit (word_of w) (nat_of_integer k))›
by (simp add: test_bit_def bit_eq_word_of)
lemma bit_code [code]:
‹bit w n ⟷ n < size ∧ test_bit w (integer_of_nat n)›
by (simp add: test_bit_def integer_of_nat_eq_of_nat)
(simp add: bit_eq_word_of size_eq_length size_integer_eq_length impossible_bit)
definition set_bit :: ‹'a ⇒ integer ⇒ bool ⇒ 'a›
where ‹set_bit w k b =
(if k < 0 ∨ size_integer ≤ k then undefined (Generic_set_bit.set_bit :: 'a ⇒ _) w k b
else Generic_set_bit.set_bit w (nat_of_integer k) b)›
lemma word_of_gen_set_bit [code abstract]:
‹word_of (set_bit w k b) =
(if k < 0 ∨ size_integer ≤ k then word_of (undefined (Generic_set_bit.set_bit :: 'a ⇒ _) w k b)
else Generic_set_bit.set_bit (word_of w) (nat_of_integer k) b)›
by (simp add: set_bit_def word_of_generic_set_bit)
lemma generic_set_bit_code [code]:
‹Generic_set_bit.set_bit w n b = (if n < size then set_bit w (integer_of_nat n) b else w)›
by (rule word_of_eqI)
(simp add: set_bit_def word_of_generic_set_bit, simp add: integer_of_nat_eq_of_nat
size_eq_length size_integer_eq_length set_bit_beyond word_size)
end
end