Theory Native_Word.Word_Type_Copies

(*  Title:      Word_Type_Copies.thy
    Author:     Florian Haftmann, TU Muenchen

chapter ‹Systematic approach towards type copies of word type›

theory Word_Type_Copies

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

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
    ― ‹Use an abstract type for code generation to disable pattern matching on termof_word.›
  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)

lemma eq_iff_word_of:
  p = q  word_of p = word_of q
  by (auto intro: word_of_eqI)


bundle constraintless

declaration let
    val cs = map (rpair NONE o fst o dest_Const)
      [term0, term(+), termuminus, term(-),
       term1, term(*), term(div), term(mod),
       termHOL.equal, term(≤), term(<),
       term(dvd), termof_bool, termnumeral, termof_nat,
       termBit_Operations.not, termBit_Operations.and, termBit_Operations.or, termBit_Operations.xor, termmask,
       termpush_bit, termdrop_bit, termtake_bit,
       termBit_Operations.set_bit, termunset_bit, termflip_bit,
       termmsb, termlsb, termsize, termGeneric_set_bit.set_bit, termset_bits]
    K (Context.mapping I (fold Proof_Context.add_const_constraint cs))


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

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

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)


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)

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

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)
  assume ?P
  then obtain q where p = 2 * q ..
  then show ?Q by (simp add: word_of_mult)
  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

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)
      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 .
    finally show P p .
  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
  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
              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)
  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_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)
  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)

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)


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)

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)


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)

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)