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