Theory Z2

(*  Title:      HOL/Library/Z2.thy
    Author:     Brian Huffman
*)

section The Field of Integers mod 2

theory Z2
imports Main
begin

text 
  Note that in most cases typbool is appropriate when a binary type is needed; the
  type provided here, for historical reasons named text‹bit›, is only needed if proper
  field operations are required.


typedef bit = UNIV :: bool set ..

instantiation bit :: zero_neq_one
begin

definition zero_bit :: bit
  where 0 = Abs_bit False

definition one_bit :: bit
  where 1 = Abs_bit True

instance
  by standard (simp add: zero_bit_def one_bit_def Abs_bit_inject)

end

free_constructors case_bit for 0::bit | 1::bit
proof -
  fix P :: bool
  fix a :: bit
  assume a = 0  P and a = 1  P
  then show P
    by (cases a) (auto simp add: zero_bit_def one_bit_def Abs_bit_inject)
qed simp

lemma bit_not_zero_iff [simp]:
  a  0  a = 1 for a :: bit
  by (cases a) simp_all

lemma bit_not_one_iff [simp]:
  a  1  a = 0 for a :: bit
  by (cases a) simp_all

instantiation bit :: semidom_modulo
begin

definition plus_bit :: bit  bit  bit
  where a + b = Abs_bit (Rep_bit a  Rep_bit b)

definition minus_bit :: bit  bit  bit
  where [simp]: minus_bit = plus

definition times_bit :: bit  bit  bit
  where a * b = Abs_bit (Rep_bit a  Rep_bit b)

definition divide_bit :: bit  bit  bit
  where [simp]: divide_bit = times

definition modulo_bit :: bit  bit  bit
  where a mod b = Abs_bit (Rep_bit a  ¬ Rep_bit b)

instance
  by standard
    (auto simp flip: Rep_bit_inject
    simp add: zero_bit_def one_bit_def plus_bit_def times_bit_def modulo_bit_def Abs_bit_inverse Rep_bit_inverse)

end

lemma bit_2_eq_0 [simp]:
  2 = (0::bit)
  by (simp flip: one_add_one add: zero_bit_def plus_bit_def)

instance bit :: semiring_parity
  apply standard
    apply (auto simp flip: Rep_bit_inject simp add: modulo_bit_def Abs_bit_inverse Rep_bit_inverse)
         apply (auto simp add: zero_bit_def one_bit_def Abs_bit_inverse Rep_bit_inverse)
  done

lemma Abs_bit_eq_of_bool [code_abbrev]:
  Abs_bit = of_bool
  by (simp add: fun_eq_iff zero_bit_def one_bit_def)

lemma Rep_bit_eq_odd:
  Rep_bit = odd
proof -
  have ¬ Rep_bit 0
    by (simp only: zero_bit_def) (subst Abs_bit_inverse, auto)
  then show ?thesis
    by (auto simp flip: Rep_bit_inject simp add: fun_eq_iff)
qed

lemma Rep_bit_iff_odd [code_abbrev]:
  Rep_bit b  odd b
  by (simp add: Rep_bit_eq_odd)

lemma Not_Rep_bit_iff_even [code_abbrev]:
  ¬ Rep_bit b  even b
  by (simp add: Rep_bit_eq_odd)

lemma Not_Not_Rep_bit [code_unfold]:
  ¬ ¬ Rep_bit b  Rep_bit b
  by simp

code_datatype 0::bit 1::bit

lemma Abs_bit_code [code]:
  Abs_bit False = 0
  Abs_bit True = 1
  by (simp_all add: Abs_bit_eq_of_bool)

lemma Rep_bit_code [code]:
  Rep_bit 0  False
  Rep_bit 1  True
  by (simp_all add: Rep_bit_eq_odd)

context zero_neq_one
begin

abbreviation of_bit :: bit  'a
  where of_bit b  of_bool (odd b)

end

context
begin

qualified lemma bit_eq_iff:
  a = b  (even a  even b) for a b :: bit
  by (cases a; cases b) simp_all

end

lemma modulo_bit_unfold [simp, code]:
  a mod b = of_bool (odd a  even b) for a b :: bit
  by (simp add: modulo_bit_def Abs_bit_eq_of_bool Rep_bit_eq_odd)

lemma power_bit_unfold [simp, code]:
  a ^ n = of_bool (odd a  n = 0) for a :: bit
  by (cases a) simp_all

instantiation bit :: field
begin

definition uminus_bit :: bit  bit
  where [simp]: uminus_bit = id

definition inverse_bit :: bit  bit
  where [simp]: inverse_bit = id

instance
  apply standard
  apply simp_all
  apply (simp only: Z2.bit_eq_iff even_add)
  apply simp
  done

end

instantiation bit :: semiring_bits
begin

definition bit_bit :: bit  nat  bool
  where [simp]: bit_bit b n  odd b  n = 0

instance
  apply standard
              apply auto
  apply (metis bit.exhaust of_bool_eq(2))
  done

end

instantiation bit :: ring_bit_operations
begin

context
  includes bit_operations_syntax
begin

definition not_bit :: bit  bit
  where [simp]: NOT b = of_bool (even b) for b :: bit

definition and_bit :: bit  bit  bit
  where [simp]: b AND c = of_bool (odd b  odd c) for b c :: bit

definition or_bit :: bit  bit  bit
  where [simp]: b OR c = of_bool (odd b  odd c) for b c :: bit

definition xor_bit :: bit  bit  bit
  where [simp]: b XOR c = of_bool (odd b  odd c) for b c :: bit

definition mask_bit :: nat  bit
  where [simp]: mask n = (of_bool (n > 0) :: bit)

definition set_bit_bit :: nat  bit  bit
  where [simp]: set_bit n b = of_bool (n = 0  odd b) for b :: bit

definition unset_bit_bit :: nat  bit  bit
  where [simp]: unset_bit n b = of_bool (n > 0  odd b) for b :: bit

definition flip_bit_bit :: nat  bit  bit
  where [simp]: flip_bit n b = of_bool ((n = 0)  odd b) for b :: bit

definition push_bit_bit :: nat  bit  bit
  where [simp]: push_bit n b = of_bool (odd b  n = 0) for b :: bit

definition drop_bit_bit :: nat  bit  bit
  where [simp]: drop_bit n b = of_bool (odd b  n = 0) for b :: bit

definition take_bit_bit :: nat  bit  bit
  where [simp]: take_bit n b = of_bool (odd b  n > 0) for b :: bit

end

instance
  apply standard
             apply auto
  apply (simp only: Z2.bit_eq_iff even_add even_zero)
  done

end

lemma add_bit_eq_xor [simp, code]:
  (+) = (Bit_Operations.xor :: bit  _)
  by (auto simp add: fun_eq_iff)

lemma mult_bit_eq_and [simp, code]:
  (*) = (Bit_Operations.and :: bit  _)
  by (simp add: fun_eq_iff)


lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
  by (simp only: Z2.bit_eq_iff even_numeral) simp

lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
  by (simp only: Z2.bit_eq_iff odd_numeral)  simp

end