src/HOL/Library/Bit.thy
 author haftmann Wed Apr 22 19:09:21 2009 +0200 (2009-04-22) changeset 30960 fec1a04b7220 parent 30129 419116f1157a child 31212 a94aea0cef76 permissions -rw-r--r--
power operation defined generic
```     1 (* Title:      Bit.thy
```
```     2    Author:     Brian Huffman
```
```     3 *)
```
```     4
```
```     5 header {* The Field of Integers mod 2 *}
```
```     6
```
```     7 theory Bit
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 subsection {* Bits as a datatype *}
```
```    12
```
```    13 typedef (open) bit = "UNIV :: bool set" ..
```
```    14
```
```    15 instantiation bit :: "{zero, one}"
```
```    16 begin
```
```    17
```
```    18 definition zero_bit_def:
```
```    19   "0 = Abs_bit False"
```
```    20
```
```    21 definition one_bit_def:
```
```    22   "1 = Abs_bit True"
```
```    23
```
```    24 instance ..
```
```    25
```
```    26 end
```
```    27
```
```    28 rep_datatype (bit) "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
```
```    34     by (simp add: all_bool_eq)
```
```    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
```
```    40     by (simp add: Abs_bit_inject)
```
```    41 qed
```
```    42
```
```    43 lemma bit_not_0_iff [iff]: "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
```
```    44   by (induct x) simp_all
```
```    45
```
```    46 lemma bit_not_1_iff [iff]: "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
```
```    47   by (induct x) simp_all
```
```    48
```
```    49
```
```    50 subsection {* Type @{typ bit} forms a field *}
```
```    51
```
```    52 instantiation bit :: "{field, division_by_zero}"
```
```    53 begin
```
```    54
```
```    55 definition plus_bit_def:
```
```    56   "x + y = (case x of 0 \<Rightarrow> y | 1 \<Rightarrow> (case y of 0 \<Rightarrow> 1 | 1 \<Rightarrow> 0))"
```
```    57
```
```    58 definition times_bit_def:
```
```    59   "x * y = (case x of 0 \<Rightarrow> 0 | 1 \<Rightarrow> y)"
```
```    60
```
```    61 definition uminus_bit_def [simp]:
```
```    62   "- x = (x :: bit)"
```
```    63
```
```    64 definition minus_bit_def [simp]:
```
```    65   "x - y = (x + y :: bit)"
```
```    66
```
```    67 definition inverse_bit_def [simp]:
```
```    68   "inverse x = (x :: bit)"
```
```    69
```
```    70 definition divide_bit_def [simp]:
```
```    71   "x / y = (x * y :: bit)"
```
```    72
```
```    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
```
```    76
```
```    77 instance proof
```
```    78 qed (unfold field_bit_defs, auto split: bit.split)
```
```    79
```
```    80 end
```
```    81
```
```    82 lemma bit_add_self: "x + x = (0 :: bit)"
```
```    83   unfolding plus_bit_def by (simp split: bit.split)
```
```    84
```
```    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)
```
```    87
```
```    88 text {* Not sure whether the next two should be simp rules. *}
```
```    89
```
```    90 lemma bit_add_eq_0_iff: "x + y = (0 :: bit) \<longleftrightarrow> x = y"
```
```    91   unfolding plus_bit_def by (simp split: bit.split)
```
```    92
```
```    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)
```
```    95
```
```    96
```
```    97 subsection {* Numerals at type @{typ bit} *}
```
```    98
```
```    99 instantiation bit :: number_ring
```
```   100 begin
```
```   101
```
```   102 definition number_of_bit_def:
```
```   103   "(number_of w :: bit) = of_int w"
```
```   104
```
```   105 instance proof
```
```   106 qed (rule number_of_bit_def)
```
```   107
```
```   108 end
```
```   109
```
```   110 text {* All numerals reduce to either 0 or 1. *}
```
```   111
```
```   112 lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
```
```   113   by (simp only: number_of_Min uminus_bit_def)
```
```   114
```
```   115 lemma bit_number_of_even [simp]: "number_of (Int.Bit0 w) = (0 :: bit)"
```
```   116   by (simp only: number_of_Bit0 add_0_left bit_add_self)
```
```   117
```
```   118 lemma bit_number_of_odd [simp]: "number_of (Int.Bit1 w) = (1 :: bit)"
```
```   119   by (simp only: number_of_Bit1 add_assoc bit_add_self
```
```   120                  monoid_add_class.add_0_right)
```
```   121
```
```   122 end
```