src/HOL/Library/Bit.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 55416 dd7992d4a61a child 58881 b9556a055632 permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
```     1 (*  Title:      HOL/Library/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 bit = "UNIV :: bool set"
```
```    14   morphisms set Bit
```
```    15   ..
```
```    16
```
```    17 instantiation bit :: "{zero, one}"
```
```    18 begin
```
```    19
```
```    20 definition zero_bit_def:
```
```    21   "0 = Bit False"
```
```    22
```
```    23 definition one_bit_def:
```
```    24   "1 = Bit True"
```
```    25
```
```    26 instance ..
```
```    27
```
```    28 end
```
```    29
```
```    30 old_rep_datatype "0::bit" "1::bit"
```
```    31 proof -
```
```    32   fix P and x :: bit
```
```    33   assume "P (0::bit)" and "P (1::bit)"
```
```    34   then have "\<forall>b. P (Bit b)"
```
```    35     unfolding zero_bit_def one_bit_def
```
```    36     by (simp add: all_bool_eq)
```
```    37   then show "P x"
```
```    38     by (induct x) simp
```
```    39 next
```
```    40   show "(0::bit) \<noteq> (1::bit)"
```
```    41     unfolding zero_bit_def one_bit_def
```
```    42     by (simp add: Bit_inject)
```
```    43 qed
```
```    44
```
```    45 lemma Bit_set_eq [simp]:
```
```    46   "Bit (set b) = b"
```
```    47   by (fact set_inverse)
```
```    48
```
```    49 lemma set_Bit_eq [simp]:
```
```    50   "set (Bit P) = P"
```
```    51   by (rule Bit_inverse) rule
```
```    52
```
```    53 lemma bit_eq_iff:
```
```    54   "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
```
```    55   by (auto simp add: set_inject)
```
```    56
```
```    57 lemma Bit_inject [simp]:
```
```    58   "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
```
```    59   by (auto simp add: Bit_inject)
```
```    60
```
```    61 lemma set [iff]:
```
```    62   "\<not> set 0"
```
```    63   "set 1"
```
```    64   by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
```
```    65
```
```    66 lemma [code]:
```
```    67   "set 0 \<longleftrightarrow> False"
```
```    68   "set 1 \<longleftrightarrow> True"
```
```    69   by simp_all
```
```    70
```
```    71 lemma set_iff:
```
```    72   "set b \<longleftrightarrow> b = 1"
```
```    73   by (cases b) simp_all
```
```    74
```
```    75 lemma bit_eq_iff_set:
```
```    76   "b = 0 \<longleftrightarrow> \<not> set b"
```
```    77   "b = 1 \<longleftrightarrow> set b"
```
```    78   by (simp_all add: bit_eq_iff)
```
```    79
```
```    80 lemma Bit [simp, code]:
```
```    81   "Bit False = 0"
```
```    82   "Bit True = 1"
```
```    83   by (simp_all add: zero_bit_def one_bit_def)
```
```    84
```
```    85 lemma bit_not_0_iff [iff]:
```
```    86   "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
```
```    87   by (simp add: bit_eq_iff)
```
```    88
```
```    89 lemma bit_not_1_iff [iff]:
```
```    90   "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
```
```    91   by (simp add: bit_eq_iff)
```
```    92
```
```    93 lemma [code]:
```
```    94   "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
```
```    95   "HOL.equal 1 b \<longleftrightarrow> set b"
```
```    96   by (simp_all add: equal set_iff)
```
```    97
```
```    98
```
```    99 subsection {* Type @{typ bit} forms a field *}
```
```   100
```
```   101 instantiation bit :: field_inverse_zero
```
```   102 begin
```
```   103
```
```   104 definition plus_bit_def:
```
```   105   "x + y = case_bit y (case_bit 1 0 y) x"
```
```   106
```
```   107 definition times_bit_def:
```
```   108   "x * y = case_bit 0 y x"
```
```   109
```
```   110 definition uminus_bit_def [simp]:
```
```   111   "- x = (x :: bit)"
```
```   112
```
```   113 definition minus_bit_def [simp]:
```
```   114   "x - y = (x + y :: bit)"
```
```   115
```
```   116 definition inverse_bit_def [simp]:
```
```   117   "inverse x = (x :: bit)"
```
```   118
```
```   119 definition divide_bit_def [simp]:
```
```   120   "x / y = (x * y :: bit)"
```
```   121
```
```   122 lemmas field_bit_defs =
```
```   123   plus_bit_def times_bit_def minus_bit_def uminus_bit_def
```
```   124   divide_bit_def inverse_bit_def
```
```   125
```
```   126 instance proof
```
```   127 qed (unfold field_bit_defs, auto split: bit.split)
```
```   128
```
```   129 end
```
```   130
```
```   131 lemma bit_add_self: "x + x = (0 :: bit)"
```
```   132   unfolding plus_bit_def by (simp split: bit.split)
```
```   133
```
```   134 lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
```
```   135   unfolding times_bit_def by (simp split: bit.split)
```
```   136
```
```   137 text {* Not sure whether the next two should be simp rules. *}
```
```   138
```
```   139 lemma bit_add_eq_0_iff: "x + y = (0 :: bit) \<longleftrightarrow> x = y"
```
```   140   unfolding plus_bit_def by (simp split: bit.split)
```
```   141
```
```   142 lemma bit_add_eq_1_iff: "x + y = (1 :: bit) \<longleftrightarrow> x \<noteq> y"
```
```   143   unfolding plus_bit_def by (simp split: bit.split)
```
```   144
```
```   145
```
```   146 subsection {* Numerals at type @{typ bit} *}
```
```   147
```
```   148 text {* All numerals reduce to either 0 or 1. *}
```
```   149
```
```   150 lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
```
```   151   by (simp only: uminus_bit_def)
```
```   152
```
```   153 lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
```
```   154   by (simp only: uminus_bit_def)
```
```   155
```
```   156 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
```
```   157   by (simp only: numeral_Bit0 bit_add_self)
```
```   158
```
```   159 lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
```
```   160   by (simp only: numeral_Bit1 bit_add_self add_0_left)
```
```   161
```
```   162
```
```   163 subsection {* Conversion from @{typ bit} *}
```
```   164
```
```   165 context zero_neq_one
```
```   166 begin
```
```   167
```
```   168 definition of_bit :: "bit \<Rightarrow> 'a"
```
```   169 where
```
```   170   "of_bit b = case_bit 0 1 b"
```
```   171
```
```   172 lemma of_bit_eq [simp, code]:
```
```   173   "of_bit 0 = 0"
```
```   174   "of_bit 1 = 1"
```
```   175   by (simp_all add: of_bit_def)
```
```   176
```
```   177 lemma of_bit_eq_iff:
```
```   178   "of_bit x = of_bit y \<longleftrightarrow> x = y"
```
```   179   by (cases x) (cases y, simp_all)+
```
```   180
```
```   181 end
```
```   182
```
```   183 context semiring_1
```
```   184 begin
```
```   185
```
```   186 lemma of_nat_of_bit_eq:
```
```   187   "of_nat (of_bit b) = of_bit b"
```
```   188   by (cases b) simp_all
```
```   189
```
```   190 end
```
```   191
```
```   192 context ring_1
```
```   193 begin
```
```   194
```
```   195 lemma of_int_of_bit_eq:
```
```   196   "of_int (of_bit b) = of_bit b"
```
```   197   by (cases b) simp_all
```
```   198
```
```   199 end
```
```   200
```
```   201 hide_const (open) set
```
```   202
```
```   203 end
```
```   204
```