(* Title: HOL/Library/Bit.thy

Author: Brian Huffman

*)

header {* The Field of Integers mod 2 *}

theory Bit

imports Main

begin

subsection {* Bits as a datatype *}

typedef bit = "UNIV :: bool set"

morphisms set Bit

..

instantiation bit :: "{zero, one}"

begin

definition zero_bit_def:

"0 = Bit False"

definition one_bit_def:

"1 = Bit True"

instance ..

end

rep_datatype "0::bit" "1::bit"

proof -

fix P and x :: bit

assume "P (0::bit)" and "P (1::bit)"

then have "∀b. P (Bit b)"

unfolding zero_bit_def one_bit_def

by (simp add: all_bool_eq)

then show "P x"

by (induct x) simp

next

show "(0::bit) ≠ (1::bit)"

unfolding zero_bit_def one_bit_def

by (simp add: Bit_inject)

qed

lemma Bit_set_eq [simp]:

"Bit (set b) = b"

by (fact set_inverse)

lemma set_Bit_eq [simp]:

"set (Bit P) = P"

by (rule Bit_inverse) rule

lemma bit_eq_iff:

"x = y <-> (set x <-> set y)"

by (auto simp add: set_inject)

lemma Bit_inject [simp]:

"Bit P = Bit Q <-> (P <-> Q)"

by (auto simp add: Bit_inject)

lemma set [iff]:

"¬ set 0"

"set 1"

by (simp_all add: zero_bit_def one_bit_def Bit_inverse)

lemma [code]:

"set 0 <-> False"

"set 1 <-> True"

by simp_all

lemma set_iff:

"set b <-> b = 1"

by (cases b) simp_all

lemma bit_eq_iff_set:

"b = 0 <-> ¬ set b"

"b = 1 <-> set b"

by (simp_all add: bit_eq_iff)

lemma Bit [simp, code]:

"Bit False = 0"

"Bit True = 1"

by (simp_all add: zero_bit_def one_bit_def)

lemma bit_not_0_iff [iff]:

"(x::bit) ≠ 0 <-> x = 1"

by (simp add: bit_eq_iff)

lemma bit_not_1_iff [iff]:

"(x::bit) ≠ 1 <-> x = 0"

by (simp add: bit_eq_iff)

lemma [code]:

"HOL.equal 0 b <-> ¬ set b"

"HOL.equal 1 b <-> set b"

by (simp_all add: equal set_iff)

subsection {* Type @{typ bit} forms a field *}

instantiation bit :: field_inverse_zero

begin

definition plus_bit_def:

"x + y = bit_case y (bit_case 1 0 y) x"

definition times_bit_def:

"x * y = bit_case 0 y x"

definition uminus_bit_def [simp]:

"- x = (x :: bit)"

definition minus_bit_def [simp]:

"x - y = (x + y :: bit)"

definition inverse_bit_def [simp]:

"inverse x = (x :: bit)"

definition divide_bit_def [simp]:

"x / y = (x * y :: bit)"

lemmas field_bit_defs =

plus_bit_def times_bit_def minus_bit_def uminus_bit_def

divide_bit_def inverse_bit_def

instance proof

qed (unfold field_bit_defs, auto split: bit.split)

end

lemma bit_add_self: "x + x = (0 :: bit)"

unfolding plus_bit_def by (simp split: bit.split)

lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) <-> x = 1 ∧ y = 1"

unfolding times_bit_def by (simp split: bit.split)

text {* Not sure whether the next two should be simp rules. *}

lemma bit_add_eq_0_iff: "x + y = (0 :: bit) <-> x = y"

unfolding plus_bit_def by (simp split: bit.split)

lemma bit_add_eq_1_iff: "x + y = (1 :: bit) <-> x ≠ y"

unfolding plus_bit_def by (simp split: bit.split)

subsection {* Numerals at type @{typ bit} *}

text {* All numerals reduce to either 0 or 1. *}

lemma bit_minus1 [simp]: "-1 = (1 :: bit)"

by (simp only: minus_one [symmetric] uminus_bit_def)

lemma bit_neg_numeral [simp]: "(neg_numeral w :: bit) = numeral w"

by (simp only: neg_numeral_def uminus_bit_def)

lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"

by (simp only: numeral_Bit0 bit_add_self)

lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"

by (simp only: numeral_Bit1 bit_add_self add_0_left)

subsection {* Conversion from @{typ bit} *}

context zero_neq_one

begin

definition of_bit :: "bit => 'a"

where

"of_bit b = bit_case 0 1 b"

lemma of_bit_eq [simp, code]:

"of_bit 0 = 0"

"of_bit 1 = 1"

by (simp_all add: of_bit_def)

lemma of_bit_eq_iff:

"of_bit x = of_bit y <-> x = y"

by (cases x) (cases y, simp_all)+

end

context semiring_1

begin

lemma of_nat_of_bit_eq:

"of_nat (of_bit b) = of_bit b"

by (cases b) simp_all

end

context ring_1

begin

lemma of_int_of_bit_eq:

"of_int (of_bit b) = of_bit b"

by (cases b) simp_all

end

hide_const (open) set

end