src/HOL/Library/Z2.thy
author haftmann
Fri, 14 Jun 2019 08:34:27 +0000
changeset 70342 e4d626692640
parent 69593 src/HOL/Library/Bit.thy@3dda49e08b9d
child 70351 32b4e1aec5ca
permissions -rw-r--r--
clear separation of types for bits (False / True) and Z2 (0 / 1)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
70342
e4d626692640 clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents: 69593
diff changeset
     1
(*  Title:      HOL/Library/Z2.thy
41959
b460124855b8 tuned headers;
wenzelm
parents: 36409
diff changeset
     2
    Author:     Brian Huffman
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
     3
*)
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
     5
section \<open>The Field of Integers mod 2\<close>
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
     6
70342
e4d626692640 clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents: 69593
diff changeset
     7
theory Z2
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
     8
imports Main
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
     9
begin
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    10
70342
e4d626692640 clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents: 69593
diff changeset
    11
text \<open>
e4d626692640 clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents: 69593
diff changeset
    12
  Note that in most cases \<^typ>\<open>bool\<close> is appropriate hen a binary type is needed; the
e4d626692640 clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents: 69593
diff changeset
    13
  type provided here, for historical reasons named \<guillemotright>bit\<guillemotleft>, is only needed if proper
e4d626692640 clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents: 69593
diff changeset
    14
  field operations are required.
e4d626692640 clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents: 69593
diff changeset
    15
\<close>
e4d626692640 clear separation of types for bits (False / True) and Z2 (0 / 1)
haftmann
parents: 69593
diff changeset
    16
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
    17
subsection \<open>Bits as a datatype\<close>
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    18
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    19
typedef bit = "UNIV :: bool set"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    20
  morphisms set Bit ..
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    21
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    22
instantiation bit :: "{zero, one}"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    23
begin
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    24
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    25
definition zero_bit_def: "0 = Bit False"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    26
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    27
definition one_bit_def: "1 = Bit True"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    28
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    29
instance ..
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    30
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    31
end
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    32
58306
117ba6cbe414 renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
blanchet
parents: 55416
diff changeset
    33
old_rep_datatype "0::bit" "1::bit"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    34
proof -
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    35
  fix P :: "bit \<Rightarrow> bool"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    36
  fix x :: bit
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    37
  assume "P 0" and "P 1"
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    38
  then have "\<forall>b. P (Bit b)"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    39
    unfolding zero_bit_def one_bit_def
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    40
    by (simp add: all_bool_eq)
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    41
  then show "P x"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    42
    by (induct x) simp
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    43
next
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    44
  show "(0::bit) \<noteq> (1::bit)"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    45
    unfolding zero_bit_def one_bit_def
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    46
    by (simp add: Bit_inject)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    47
qed
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    48
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    49
lemma Bit_set_eq [simp]: "Bit (set b) = b"
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    50
  by (fact set_inverse)
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    51
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    52
lemma set_Bit_eq [simp]: "set (Bit P) = P"
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    53
  by (rule Bit_inverse) rule
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    54
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    55
lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    56
  by (auto simp add: set_inject)
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    57
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    58
lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    59
  by (auto simp add: Bit_inject)
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    60
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    61
lemma set [iff]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    62
  "\<not> set 0"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    63
  "set 1"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    64
  by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    65
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    66
lemma [code]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    67
  "set 0 \<longleftrightarrow> False"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    68
  "set 1 \<longleftrightarrow> True"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    69
  by simp_all
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    70
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    71
lemma set_iff: "set b \<longleftrightarrow> b = 1"
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    72
  by (cases b) simp_all
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    73
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    74
lemma bit_eq_iff_set:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    75
  "b = 0 \<longleftrightarrow> \<not> set b"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    76
  "b = 1 \<longleftrightarrow> set b"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    77
  by (simp_all add: bit_eq_iff)
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    78
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    79
lemma Bit [simp, code]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    80
  "Bit False = 0"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    81
  "Bit True = 1"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    82
  by (simp_all add: zero_bit_def one_bit_def)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    83
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    84
lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    85
  by (simp add: bit_eq_iff)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    86
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    87
lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    88
  by (simp add: bit_eq_iff)
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    89
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    90
lemma [code]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    91
  "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    92
  "HOL.equal 1 b \<longleftrightarrow> set b"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    93
  by (simp_all add: equal set_iff)
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    94
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    95
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 63462
diff changeset
    96
subsection \<open>Type \<^typ>\<open>bit\<close> forms a field\<close>
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    97
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 58881
diff changeset
    98
instantiation bit :: field
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    99
begin
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   100
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   101
definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   102
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   103
definition times_bit_def: "x * y = case_bit 0 y x"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   104
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   105
definition uminus_bit_def [simp]: "- x = x" for x :: bit
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   106
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   107
definition minus_bit_def [simp]: "x - y = x + y" for x y :: bit
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   108
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   109
definition inverse_bit_def [simp]: "inverse x = x" for x :: bit
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   110
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   111
definition divide_bit_def [simp]: "x div y = x * y" for x y :: bit
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   112
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   113
lemmas field_bit_defs =
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   114
  plus_bit_def times_bit_def minus_bit_def uminus_bit_def
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   115
  divide_bit_def inverse_bit_def
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   116
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   117
instance
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   118
  by standard (auto simp: field_bit_defs split: bit.split)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   119
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   120
end
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   121
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   122
lemma bit_add_self: "x + x = 0" for x :: bit
30129
419116f1157a remove unnecessary simp rules
huffman
parents: 29995
diff changeset
   123
  unfolding plus_bit_def by (simp split: bit.split)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   124
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   125
lemma bit_mult_eq_1_iff [simp]: "x * y = 1 \<longleftrightarrow> x = 1 \<and> y = 1" for x y :: bit
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   126
  unfolding times_bit_def by (simp split: bit.split)
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   127
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   128
text \<open>Not sure whether the next two should be simp rules.\<close>
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   129
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   130
lemma bit_add_eq_0_iff: "x + y = 0 \<longleftrightarrow> x = y" for x y :: bit
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   131
  unfolding plus_bit_def by (simp split: bit.split)
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   132
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   133
lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   134
  unfolding plus_bit_def by (simp split: bit.split)
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   135
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   136
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 63462
diff changeset
   137
subsection \<open>Numerals at type \<^typ>\<open>bit\<close>\<close>
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   138
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   139
text \<open>All numerals reduce to either 0 or 1.\<close>
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   140
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 53063
diff changeset
   141
lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 53063
diff changeset
   142
  by (simp only: uminus_bit_def)
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   143
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 53063
diff changeset
   144
lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 53063
diff changeset
   145
  by (simp only: uminus_bit_def)
29995
62efbd0ef132 add rule for minus 1 at type bit
huffman
parents: 29994
diff changeset
   146
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   147
lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   148
  by (simp only: numeral_Bit0 bit_add_self)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   149
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   150
lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   151
  by (simp only: numeral_Bit1 bit_add_self add_0_left)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   152
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   153
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 63462
diff changeset
   154
subsection \<open>Conversion from \<^typ>\<open>bit\<close>\<close>
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   155
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   156
context zero_neq_one
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   157
begin
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   158
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   159
definition of_bit :: "bit \<Rightarrow> 'a"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   160
  where "of_bit b = case_bit 0 1 b"
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   161
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   162
lemma of_bit_eq [simp, code]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   163
  "of_bit 0 = 0"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   164
  "of_bit 1 = 1"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   165
  by (simp_all add: of_bit_def)
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   166
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   167
lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   168
  by (cases x) (cases y; simp)+
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   169
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   170
end
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   171
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   172
lemma (in semiring_1) of_nat_of_bit_eq: "of_nat (of_bit b) = of_bit b"
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   173
  by (cases b) simp_all
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   174
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   175
lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   176
  by (cases b) simp_all
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   177
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   178
hide_const (open) set
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   179
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   180
end