
wenzelm@41959: (*  Title:      HOL/Library/Bit.thy
wenzelm@41959:     Author:     Brian Huffman
huffman@29994: *)
huffman@29994: 
huffman@29994: header {* The Field of Integers mod 2 *}
huffman@29994: 
huffman@29994: theory Bit
huffman@29994: imports Main
huffman@29994: begin
huffman@29994: 
huffman@29994: subsection {* Bits as a datatype *}
huffman@29994: 
haftmann@53063: typedef bit = "UNIV :: bool set"
haftmann@53063:   morphisms set Bit
haftmann@53063:   ..
huffman@29994: 
huffman@29994: instantiation bit :: "{zero, one}"
huffman@29994: begin
huffman@29994: 
huffman@29994: definition zero_bit_def:
haftmann@53063:   "0 = Bit False"
huffman@29994: 
huffman@29994: definition one_bit_def:
haftmann@53063:   "1 = Bit True"
huffman@29994: 
huffman@29994: instance ..
huffman@29994: 
huffman@29994: end
huffman@29994: 
blanchet@58306: old_rep_datatype "0::bit" "1::bit"
huffman@29994: proof -
huffman@29994:   fix P and x :: bit
huffman@29994:   assume "P (0::bit)" and "P (1::bit)"
haftmann@53063:   then have "\<forall>b. P (Bit b)"
huffman@29994:     unfolding zero_bit_def one_bit_def
huffman@29994:     by (simp add: all_bool_eq)
huffman@29994:   then show "P x"
huffman@29994:     by (induct x) simp
huffman@29994: next
huffman@29994:   show "(0::bit) \<noteq> (1::bit)"
huffman@29994:     unfolding zero_bit_def one_bit_def
haftmann@53063:     by (simp add: Bit_inject)
huffman@29994: qed
huffman@29994: 
haftmann@53063: lemma Bit_set_eq [simp]:
haftmann@53063:   "Bit (set b) = b"
haftmann@53063:   by (fact set_inverse)
haftmann@53063:   
haftmann@53063: lemma set_Bit_eq [simp]:
haftmann@53063:   "set (Bit P) = P"
haftmann@53063:   by (rule Bit_inverse) rule
haftmann@53063: 
haftmann@53063: lemma bit_eq_iff:
haftmann@53063:   "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
haftmann@53063:   by (auto simp add: set_inject)
haftmann@53063: 
haftmann@53063: lemma Bit_inject [simp]:
haftmann@53063:   "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
haftmann@53063:   by (auto simp add: Bit_inject)  
haftmann@53063: 
haftmann@53063: lemma set [iff]:
haftmann@53063:   "\<not> set 0"
haftmann@53063:   "set 1"
haftmann@53063:   by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
haftmann@53063: 
haftmann@53063: lemma [code]:
haftmann@53063:   "set 0 \<longleftrightarrow> False"
haftmann@53063:   "set 1 \<longleftrightarrow> True"
haftmann@53063:   by simp_all
huffman@29994: 
haftmann@53063: lemma set_iff:
haftmann@53063:   "set b \<longleftrightarrow> b = 1"
haftmann@53063:   by (cases b) simp_all
haftmann@53063: 
haftmann@53063: lemma bit_eq_iff_set:
haftmann@53063:   "b = 0 \<longleftrightarrow> \<not> set b"
haftmann@53063:   "b = 1 \<longleftrightarrow> set b"
haftmann@53063:   by (simp_all add: bit_eq_iff)
haftmann@53063: 
haftmann@53063: lemma Bit [simp, code]:
haftmann@53063:   "Bit False = 0"
haftmann@53063:   "Bit True = 1"
haftmann@53063:   by (simp_all add: zero_bit_def one_bit_def)
huffman@29994: 
haftmann@53063: lemma bit_not_0_iff [iff]:
haftmann@53063:   "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
haftmann@53063:   by (simp add: bit_eq_iff)
huffman@29994: 
haftmann@53063: lemma bit_not_1_iff [iff]:
haftmann@53063:   "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
haftmann@53063:   by (simp add: bit_eq_iff)
haftmann@53063: 
haftmann@53063: lemma [code]:
haftmann@53063:   "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
haftmann@53063:   "HOL.equal 1 b \<longleftrightarrow> set b"
haftmann@53063:   by (simp_all add: equal set_iff)  
haftmann@53063: 
haftmann@53063:   
huffman@29994: subsection {* Type @{typ bit} forms a field *}
huffman@29994: 
haftmann@36409: instantiation bit :: field_inverse_zero
huffman@29994: begin
huffman@29994: 
huffman@29994: definition plus_bit_def:
blanchet@55416:   "x + y = case_bit y (case_bit 1 0 y) x"
huffman@29994: 
huffman@29994: definition times_bit_def:
blanchet@55416:   "x * y = case_bit 0 y x"
huffman@29994: 
huffman@29994: definition uminus_bit_def [simp]:
huffman@29994:   "- x = (x :: bit)"
huffman@29994: 
huffman@29994: definition minus_bit_def [simp]:
huffman@29994:   "x - y = (x + y :: bit)"
huffman@29994: 
huffman@29994: definition inverse_bit_def [simp]:
huffman@29994:   "inverse x = (x :: bit)"
huffman@29994: 
huffman@29994: definition divide_bit_def [simp]:
huffman@29994:   "x / y = (x * y :: bit)"
huffman@29994: 
huffman@29994: lemmas field_bit_defs =
huffman@29994:   plus_bit_def times_bit_def minus_bit_def uminus_bit_def
huffman@29994:   divide_bit_def inverse_bit_def
huffman@29994: 
huffman@29994: instance proof
huffman@29994: qed (unfold field_bit_defs, auto split: bit.split)
huffman@29994: 
huffman@29994: end
huffman@29994: 
huffman@30129: lemma bit_add_self: "x + x = (0 :: bit)"
huffman@30129:   unfolding plus_bit_def by (simp split: bit.split)
huffman@29994: 
huffman@29994: lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
huffman@29994:   unfolding times_bit_def by (simp split: bit.split)
huffman@29994: 
huffman@29994: text {* Not sure whether the next two should be simp rules. *}
huffman@29994: 
huffman@29994: lemma bit_add_eq_0_iff: "x + y = (0 :: bit) \<longleftrightarrow> x = y"
huffman@29994:   unfolding plus_bit_def by (simp split: bit.split)
huffman@29994: 
huffman@29994: lemma bit_add_eq_1_iff: "x + y = (1 :: bit) \<longleftrightarrow> x \<noteq> y"
huffman@29994:   unfolding plus_bit_def by (simp split: bit.split)
huffman@29994: 
huffman@29994: 
huffman@29994: subsection {* Numerals at type @{typ bit} *}
huffman@29994: 
huffman@29994: text {* All numerals reduce to either 0 or 1. *}
huffman@29994: 
haftmann@54489: lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
haftmann@54489:   by (simp only: uminus_bit_def)
huffman@47108: 
haftmann@54489: lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
haftmann@54489:   by (simp only: uminus_bit_def)
huffman@29995: 
huffman@47108: lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
huffman@47108:   by (simp only: numeral_Bit0 bit_add_self)
huffman@29994: 
huffman@47108: lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
huffman@47108:   by (simp only: numeral_Bit1 bit_add_self add_0_left)
huffman@29994: 
haftmann@53063: 
haftmann@53063: subsection {* Conversion from @{typ bit} *}
haftmann@53063: 
haftmann@53063: context zero_neq_one
haftmann@53063: begin
haftmann@53063: 
haftmann@53063: definition of_bit :: "bit \<Rightarrow> 'a"
haftmann@53063: where
blanchet@55416:   "of_bit b = case_bit 0 1 b" 
haftmann@53063: 
haftmann@53063: lemma of_bit_eq [simp, code]:
haftmann@53063:   "of_bit 0 = 0"
haftmann@53063:   "of_bit 1 = 1"
haftmann@53063:   by (simp_all add: of_bit_def)
haftmann@53063: 
haftmann@53063: lemma of_bit_eq_iff:
haftmann@53063:   "of_bit x = of_bit y \<longleftrightarrow> x = y"
haftmann@53063:   by (cases x) (cases y, simp_all)+
haftmann@53063: 
haftmann@53063: end  
haftmann@53063: 
haftmann@53063: context semiring_1
haftmann@53063: begin
haftmann@53063: 
haftmann@53063: lemma of_nat_of_bit_eq:
haftmann@53063:   "of_nat (of_bit b) = of_bit b"
haftmann@53063:   by (cases b) simp_all
haftmann@53063: 
huffman@29994: end
haftmann@53063: 
haftmann@53063: context ring_1
haftmann@53063: begin
haftmann@53063: 
haftmann@53063: lemma of_int_of_bit_eq:
haftmann@53063:   "of_int (of_bit b) = of_bit b"
haftmann@53063:   by (cases b) simp_all
haftmann@53063: 
haftmann@53063: end
haftmann@53063: 
haftmann@53063: hide_const (open) set
haftmann@53063: 
haftmann@53063: end
haftmann@53063: 




