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 "\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) \ (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 \ (set x \ set y)" haftmann@53063: by (auto simp add: set_inject) haftmann@53063: haftmann@53063: lemma Bit_inject [simp]: haftmann@53063: "Bit P = Bit Q \ (P \ Q)" haftmann@53063: by (auto simp add: Bit_inject) haftmann@53063: haftmann@53063: lemma set [iff]: haftmann@53063: "\ 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 \ False" haftmann@53063: "set 1 \ True" haftmann@53063: by simp_all huffman@29994: haftmann@53063: lemma set_iff: haftmann@53063: "set b \ b = 1" haftmann@53063: by (cases b) simp_all haftmann@53063: haftmann@53063: lemma bit_eq_iff_set: haftmann@53063: "b = 0 \ \ set b" haftmann@53063: "b = 1 \ 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) \ 0 \ x = 1" haftmann@53063: by (simp add: bit_eq_iff) huffman@29994: haftmann@53063: lemma bit_not_1_iff [iff]: haftmann@53063: "(x::bit) \ 1 \ x = 0" haftmann@53063: by (simp add: bit_eq_iff) haftmann@53063: haftmann@53063: lemma [code]: haftmann@53063: "HOL.equal 0 b \ \ set b" haftmann@53063: "HOL.equal 1 b \ 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) \ x = 1 \ 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) \ 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) \ x \ 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 \ '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 \ 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: