src/HOL/Library/Bit.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 63462 c1fe30f2bc32 child 69593 3dda49e08b9d permissions -rw-r--r--
executable domain membership checks
```     1 (*  Title:      HOL/Library/Bit.thy
```
```     2     Author:     Brian Huffman
```
```     3 *)
```
```     4
```
```     5 section \<open>The Field of Integers mod 2\<close>
```
```     6
```
```     7 theory Bit
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 subsection \<open>Bits as a datatype\<close>
```
```    12
```
```    13 typedef bit = "UNIV :: bool set"
```
```    14   morphisms set Bit ..
```
```    15
```
```    16 instantiation bit :: "{zero, one}"
```
```    17 begin
```
```    18
```
```    19 definition zero_bit_def: "0 = Bit False"
```
```    20
```
```    21 definition one_bit_def: "1 = Bit True"
```
```    22
```
```    23 instance ..
```
```    24
```
```    25 end
```
```    26
```
```    27 old_rep_datatype "0::bit" "1::bit"
```
```    28 proof -
```
```    29   fix P :: "bit \<Rightarrow> bool"
```
```    30   fix x :: bit
```
```    31   assume "P 0" and "P 1"
```
```    32   then have "\<forall>b. P (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: Bit_inject)
```
```    41 qed
```
```    42
```
```    43 lemma Bit_set_eq [simp]: "Bit (set b) = b"
```
```    44   by (fact set_inverse)
```
```    45
```
```    46 lemma set_Bit_eq [simp]: "set (Bit P) = P"
```
```    47   by (rule Bit_inverse) rule
```
```    48
```
```    49 lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
```
```    50   by (auto simp add: set_inject)
```
```    51
```
```    52 lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
```
```    53   by (auto simp add: Bit_inject)
```
```    54
```
```    55 lemma set [iff]:
```
```    56   "\<not> set 0"
```
```    57   "set 1"
```
```    58   by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
```
```    59
```
```    60 lemma [code]:
```
```    61   "set 0 \<longleftrightarrow> False"
```
```    62   "set 1 \<longleftrightarrow> True"
```
```    63   by simp_all
```
```    64
```
```    65 lemma set_iff: "set b \<longleftrightarrow> b = 1"
```
```    66   by (cases b) simp_all
```
```    67
```
```    68 lemma bit_eq_iff_set:
```
```    69   "b = 0 \<longleftrightarrow> \<not> set b"
```
```    70   "b = 1 \<longleftrightarrow> set b"
```
```    71   by (simp_all add: bit_eq_iff)
```
```    72
```
```    73 lemma Bit [simp, code]:
```
```    74   "Bit False = 0"
```
```    75   "Bit True = 1"
```
```    76   by (simp_all add: zero_bit_def one_bit_def)
```
```    77
```
```    78 lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit
```
```    79   by (simp add: bit_eq_iff)
```
```    80
```
```    81 lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit
```
```    82   by (simp add: bit_eq_iff)
```
```    83
```
```    84 lemma [code]:
```
```    85   "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
```
```    86   "HOL.equal 1 b \<longleftrightarrow> set b"
```
```    87   by (simp_all add: equal set_iff)
```
```    88
```
```    89
```
```    90 subsection \<open>Type @{typ bit} forms a field\<close>
```
```    91
```
```    92 instantiation bit :: field
```
```    93 begin
```
```    94
```
```    95 definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x"
```
```    96
```
```    97 definition times_bit_def: "x * y = case_bit 0 y x"
```
```    98
```
```    99 definition uminus_bit_def [simp]: "- x = x" for x :: bit
```
```   100
```
```   101 definition minus_bit_def [simp]: "x - y = x + y" for x y :: bit
```
```   102
```
```   103 definition inverse_bit_def [simp]: "inverse x = x" for x :: bit
```
```   104
```
```   105 definition divide_bit_def [simp]: "x div y = x * y" for x y :: bit
```
```   106
```
```   107 lemmas field_bit_defs =
```
```   108   plus_bit_def times_bit_def minus_bit_def uminus_bit_def
```
```   109   divide_bit_def inverse_bit_def
```
```   110
```
```   111 instance
```
```   112   by standard (auto simp: field_bit_defs split: bit.split)
```
```   113
```
```   114 end
```
```   115
```
```   116 lemma bit_add_self: "x + x = 0" for x :: bit
```
```   117   unfolding plus_bit_def by (simp split: bit.split)
```
```   118
```
```   119 lemma bit_mult_eq_1_iff [simp]: "x * y = 1 \<longleftrightarrow> x = 1 \<and> y = 1" for x y :: bit
```
```   120   unfolding times_bit_def by (simp split: bit.split)
```
```   121
```
```   122 text \<open>Not sure whether the next two should be simp rules.\<close>
```
```   123
```
```   124 lemma bit_add_eq_0_iff: "x + y = 0 \<longleftrightarrow> x = y" for x y :: bit
```
```   125   unfolding plus_bit_def by (simp split: bit.split)
```
```   126
```
```   127 lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit
```
```   128   unfolding plus_bit_def by (simp split: bit.split)
```
```   129
```
```   130
```
```   131 subsection \<open>Numerals at type @{typ bit}\<close>
```
```   132
```
```   133 text \<open>All numerals reduce to either 0 or 1.\<close>
```
```   134
```
```   135 lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
```
```   136   by (simp only: uminus_bit_def)
```
```   137
```
```   138 lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
```
```   139   by (simp only: uminus_bit_def)
```
```   140
```
```   141 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
```
```   142   by (simp only: numeral_Bit0 bit_add_self)
```
```   143
```
```   144 lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
```
```   145   by (simp only: numeral_Bit1 bit_add_self add_0_left)
```
```   146
```
```   147
```
```   148 subsection \<open>Conversion from @{typ bit}\<close>
```
```   149
```
```   150 context zero_neq_one
```
```   151 begin
```
```   152
```
```   153 definition of_bit :: "bit \<Rightarrow> 'a"
```
```   154   where "of_bit b = case_bit 0 1 b"
```
```   155
```
```   156 lemma of_bit_eq [simp, code]:
```
```   157   "of_bit 0 = 0"
```
```   158   "of_bit 1 = 1"
```
```   159   by (simp_all add: of_bit_def)
```
```   160
```
```   161 lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y"
```
```   162   by (cases x) (cases y; simp)+
```
```   163
```
```   164 end
```
```   165
```
```   166 lemma (in semiring_1) of_nat_of_bit_eq: "of_nat (of_bit b) = of_bit b"
```
```   167   by (cases b) simp_all
```
```   168
```
```   169 lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b"
```
```   170   by (cases b) simp_all
```
```   171
```
```   172 hide_const (open) set
```
```   173
```
```   174 end
```