Theory HOL-Library.Z2
section ‹The Field of Integers mod 2›
theory Z2
imports Main
begin
text ‹
Note that in most cases \<^typ>‹bool› 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]:
‹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 even_zero refl)
done
end
instantiation bit :: semiring_bits
begin
definition bit_bit :: ‹bit ⇒ nat ⇒ bool›
where [simp]: ‹bit_bit b n ⟷ odd b ∧ n = 0›
instance
by standard
(auto intro: Abs_bit_induct simp add: Abs_bit_eq_of_bool)
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
by standard auto
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 n) = (0 :: bit)›
by (simp only: Z2.bit_eq_iff even_numeral) simp
lemma bit_numeral_odd [simp]:
‹numeral (Num.Bit1 n) = (1 :: bit)›
by (simp only: Z2.bit_eq_iff odd_numeral) simp
end