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
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>‹lsb›, \<^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 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 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 lsb_iff_word_of [code]: ‹lsb p ⟷ lsb (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_lsb:
‹OFCLASS('a, lsb_class)›
by standard (simp add: fun_eq_iff lsb_iff_word_of even_iff_word_of lsb_odd)
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
end