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