src/HOL/Library/Z2.thy
author haftmann
Sat, 20 Jun 2020 05:56:28 +0000
changeset 71965 d45f5d4c41bd
parent 71957 3e162c63371a
child 71988 ace45a11a45e
permissions -rw-r--r--
more class operations for the sake of efficient generated code
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
71957
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
     8
imports Main "HOL-Library.Bit_Operations"
29994
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
70351
32b4e1aec5ca make latex happy
haftmann
parents: 70342
diff changeset
    13
  type provided here, for historical reasons named \<^text>\<open>bit\<close>, is only needed if proper
70342
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
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
    55
context
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
    56
begin
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
    57
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
    58
qualified 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
    59
  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
    60
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
    61
end
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
    62
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    63
lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    64
  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
    65
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    66
lemma set [iff]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    67
  "\<not> set 0"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    68
  "set 1"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    69
  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
    70
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    71
lemma [code]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    72
  "set 0 \<longleftrightarrow> False"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    73
  "set 1 \<longleftrightarrow> True"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    74
  by simp_all
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    75
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    76
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
    77
  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
    78
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    79
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
    80
  "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
    81
  "b = 1 \<longleftrightarrow> set b"
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
    82
  by (simp_all add: Z2.bit_eq_iff)
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    83
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    84
lemma Bit [simp, code]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    85
  "Bit False = 0"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    86
  "Bit True = 1"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    87
  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
    88
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    89
lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
    90
  by (simp add: Z2.bit_eq_iff)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    91
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    92
lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
    93
  by (simp add: Z2.bit_eq_iff)
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    94
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    95
lemma [code]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    96
  "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
    97
  "HOL.equal 1 b \<longleftrightarrow> set b"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
    98
  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
    99
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   100
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 63462
diff changeset
   101
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
   102
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 58881
diff changeset
   103
instantiation bit :: field
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   104
begin
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   105
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   106
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
   107
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   108
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
   109
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   110
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
   111
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   112
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
   113
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   114
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
   115
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   116
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
   117
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   118
lemmas field_bit_defs =
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   119
  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
   120
  divide_bit_def inverse_bit_def
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   121
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   122
instance
71942
d2654b30f7bd eliminated warnings
haftmann
parents: 70351
diff changeset
   123
  by standard (auto simp: plus_bit_def times_bit_def split: bit.split)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   124
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   125
end
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   126
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   127
lemma bit_add_self: "x + x = 0" for x :: bit
30129
419116f1157a remove unnecessary simp rules
huffman
parents: 29995
diff changeset
   128
  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
   129
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   130
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
   131
  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
   132
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   133
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
   134
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   135
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
   136
  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
   137
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   138
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
   139
  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
   140
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   141
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 63462
diff changeset
   142
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
   143
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60429
diff changeset
   144
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
   145
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 53063
diff changeset
   146
lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 53063
diff changeset
   147
  by (simp only: uminus_bit_def)
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   148
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 53063
diff changeset
   149
lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 53063
diff changeset
   150
  by (simp only: uminus_bit_def)
29995
62efbd0ef132 add rule for minus 1 at type bit
huffman
parents: 29994
diff changeset
   151
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   152
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
   153
  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
   154
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   155
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
   156
  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
   157
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   158
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 63462
diff changeset
   159
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
   160
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   161
context zero_neq_one
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   162
begin
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   163
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   164
definition of_bit :: "bit \<Rightarrow> 'a"
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   165
  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
   166
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   167
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
   168
  "of_bit 0 = 0"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   169
  "of_bit 1 = 1"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   170
  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
   171
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   172
lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y"
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   173
  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
   174
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   175
end
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   176
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   177
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
   178
  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
   179
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   180
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
   181
  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
   182
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   183
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   184
subsection \<open>Bit structure\<close>
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   185
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   186
instantiation bit :: semidom_modulo
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   187
begin
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   188
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   189
definition modulo_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   190
  where [simp]: \<open>a mod b = a * of_bool (b = 0)\<close> for a b :: bit
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   191
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   192
instance
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   193
  by standard simp
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   194
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   195
end
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   196
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   197
instantiation bit :: semiring_bits
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   198
begin
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   199
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   200
definition bit_bit :: \<open>bit \<Rightarrow> nat \<Rightarrow> bool\<close>
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   201
  where [simp]: \<open>bit_bit b n \<longleftrightarrow> b = 1 \<and> n = 0\<close>
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   202
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   203
instance
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   204
  apply standard
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   205
                apply (auto simp add: power_0_left power_add set_iff)
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   206
   apply (metis bit_not_1_iff of_bool_eq(2))
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   207
  done
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   208
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   209
end
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   210
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   211
instantiation bit :: semiring_bit_shifts
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   212
begin
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   213
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   214
definition push_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   215
  where \<open>push_bit n b = (if n = 0 then b else 0)\<close> for b :: bit
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   216
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   217
definition drop_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   218
  where \<open>drop_bit n b = (if n = 0 then b else 0)\<close> for b :: bit
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   219
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   220
definition take_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   221
  where \<open>take_bit n b = (if n = 0 then 0 else b)\<close> for b :: bit
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   222
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   223
instance
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   224
  by standard (simp_all add: push_bit_bit_def drop_bit_bit_def take_bit_bit_def)
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   225
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   226
end
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   227
71957
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   228
instantiation bit :: ring_bit_operations
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   229
begin
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   230
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   231
definition not_bit :: \<open>bit \<Rightarrow> bit\<close>
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   232
  where \<open>NOT b = of_bool (even b)\<close> for b :: bit
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   233
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   234
definition and_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   235
  where \<open>b AND c = of_bool (odd b \<and> odd c)\<close> for b c :: bit
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   236
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   237
definition or_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   238
  where \<open>b OR c = of_bool (odd b \<or> odd c)\<close> for b c :: bit
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   239
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   240
definition xor_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   241
  where \<open>b XOR c = of_bool (odd b \<noteq> odd c)\<close> for b c :: bit
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   242
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   243
instance
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   244
  by standard (auto simp add: and_bit_def or_bit_def xor_bit_def not_bit_def add_eq_0_iff)
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   245
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   246
end
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   247
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   248
lemma add_bit_eq_xor:
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   249
  \<open>(+) = ((XOR) :: bit \<Rightarrow> _)\<close>
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   250
  by (auto simp add: fun_eq_iff plus_bit_def xor_bit_def)
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   251
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   252
lemma mult_bit_eq_and:
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   253
  \<open>(*) = ((AND) :: bit \<Rightarrow> _)\<close>
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   254
  by (simp add: fun_eq_iff times_bit_def and_bit_def split: bit.split)
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   255
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   256
lemma bit_NOT_eq_1_iff [simp]: "NOT b = 1 \<longleftrightarrow> b = 0"
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   257
  for b :: bit
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   258
  by (cases b) simp_all
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   259
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   260
lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   261
  for a b :: bit
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   262
  by (cases a; cases b) simp_all
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   263
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   264
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   265
hide_const (open) set
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   266
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   267
end