src/HOL/Library/Bit.thy
 author wenzelm Thu Feb 16 22:53:24 2012 +0100 (2012-02-16) changeset 46507 1b24c24017dd parent 45701 615da8b8d758 child 47108 2a1953f0d20d permissions -rw-r--r--
tuned proofs;
1 (*  Title:      HOL/Library/Bit.thy
2     Author:     Brian Huffman
3 *)
5 header {* The Field of Integers mod 2 *}
7 theory Bit
8 imports Main
9 begin
11 subsection {* Bits as a datatype *}
13 typedef (open) bit = "UNIV :: bool set" ..
15 instantiation bit :: "{zero, one}"
16 begin
18 definition zero_bit_def:
19   "0 = Abs_bit False"
21 definition one_bit_def:
22   "1 = Abs_bit True"
24 instance ..
26 end
28 rep_datatype "0::bit" "1::bit"
29 proof -
30   fix P and x :: bit
31   assume "P (0::bit)" and "P (1::bit)"
32   then have "\<forall>b. P (Abs_bit b)"
33     unfolding zero_bit_def one_bit_def
35   then show "P x"
36     by (induct x) simp
37 next
38   show "(0::bit) \<noteq> (1::bit)"
39     unfolding zero_bit_def one_bit_def
41 qed
43 lemma bit_not_0_iff [iff]: "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
44   by (induct x) simp_all
46 lemma bit_not_1_iff [iff]: "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
47   by (induct x) simp_all
50 subsection {* Type @{typ bit} forms a field *}
52 instantiation bit :: field_inverse_zero
53 begin
55 definition plus_bit_def:
56   "x + y = bit_case y (bit_case 1 0 y) x"
58 definition times_bit_def:
59   "x * y = bit_case 0 y x"
61 definition uminus_bit_def [simp]:
62   "- x = (x :: bit)"
64 definition minus_bit_def [simp]:
65   "x - y = (x + y :: bit)"
67 definition inverse_bit_def [simp]:
68   "inverse x = (x :: bit)"
70 definition divide_bit_def [simp]:
71   "x / y = (x * y :: bit)"
73 lemmas field_bit_defs =
74   plus_bit_def times_bit_def minus_bit_def uminus_bit_def
75   divide_bit_def inverse_bit_def
77 instance proof
78 qed (unfold field_bit_defs, auto split: bit.split)
80 end
82 lemma bit_add_self: "x + x = (0 :: bit)"
83   unfolding plus_bit_def by (simp split: bit.split)
85 lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
86   unfolding times_bit_def by (simp split: bit.split)
88 text {* Not sure whether the next two should be simp rules. *}
90 lemma bit_add_eq_0_iff: "x + y = (0 :: bit) \<longleftrightarrow> x = y"
91   unfolding plus_bit_def by (simp split: bit.split)
93 lemma bit_add_eq_1_iff: "x + y = (1 :: bit) \<longleftrightarrow> x \<noteq> y"
94   unfolding plus_bit_def by (simp split: bit.split)
97 subsection {* Numerals at type @{typ bit} *}
99 instantiation bit :: number_ring
100 begin
102 definition number_of_bit_def:
103   "(number_of w :: bit) = of_int w"
105 instance proof
106 qed (rule number_of_bit_def)
108 end
110 text {* All numerals reduce to either 0 or 1. *}
112 lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
113   by (simp only: number_of_Min uminus_bit_def)
115 lemma bit_number_of_even [simp]: "number_of (Int.Bit0 w) = (0 :: bit)"