src/HOL/Library/Z2.thy
author haftmann
Tue, 04 Aug 2020 09:33:05 +0000
changeset 72082 41393ecb57ac
parent 71988 ace45a11a45e
permissions -rw-r--r--
uniform mask operation
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
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    17
typedef bit = \<open>UNIV :: bool set\<close> ..
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    18
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    19
instantiation bit :: zero_neq_one
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    20
begin
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    21
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    22
definition zero_bit :: bit
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    23
  where \<open>0 = Abs_bit False\<close>
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    24
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    25
definition one_bit :: bit
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    26
  where \<open>1 = Abs_bit True\<close>
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    27
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    28
instance
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    29
  by standard (simp add: zero_bit_def one_bit_def Abs_bit_inject)
29994
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
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    33
free_constructors case_bit for \<open>0::bit\<close> | \<open>1::bit\<close>
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    34
proof -
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    35
  fix P :: bool
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    36
  fix a :: bit
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    37
  assume \<open>a = 0 \<Longrightarrow> P\<close> and \<open>a = 1 \<Longrightarrow> P\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    38
  then show P
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    39
    by (cases a) (auto simp add: zero_bit_def one_bit_def Abs_bit_inject)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    40
qed simp
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    41
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    42
lemma bit_not_zero_iff [simp]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    43
  \<open>a \<noteq> 0 \<longleftrightarrow> a = 1\<close> for a :: bit
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    44
  by (cases a) simp_all
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    45
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    46
lemma bit_not_one_imp [simp]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    47
  \<open>a \<noteq> 1 \<longleftrightarrow> a = 0\<close> for a :: bit
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    48
  by (cases a) simp_all
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    49
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    50
instantiation bit :: semidom_modulo
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    51
begin
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    52
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    53
definition plus_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    54
  where \<open>a + b = Abs_bit (Rep_bit a \<noteq> Rep_bit b)\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    55
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    56
definition minus_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    57
  where [simp]: \<open>minus_bit = plus\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    58
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    59
definition times_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    60
  where \<open>a * b = Abs_bit (Rep_bit a \<and> Rep_bit b)\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    61
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    62
definition divide_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    63
  where [simp]: \<open>divide_bit = times\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    64
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    65
definition modulo_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    66
  where \<open>a mod b = Abs_bit (Rep_bit a \<and> \<not> Rep_bit b)\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    67
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    68
instance
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    69
  by standard
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    70
    (auto simp flip: Rep_bit_inject
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    71
    simp add: zero_bit_def one_bit_def plus_bit_def times_bit_def modulo_bit_def Abs_bit_inverse Rep_bit_inverse)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    72
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    73
end
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    74
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    75
lemma bit_2_eq_0 [simp]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    76
  \<open>2 = (0::bit)\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    77
  by (simp flip: one_add_one add: zero_bit_def plus_bit_def)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    78
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    79
instance bit :: semiring_parity
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    80
  apply standard
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    81
    apply (auto simp flip: Rep_bit_inject simp add: modulo_bit_def Abs_bit_inverse Rep_bit_inverse)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    82
         apply (auto simp add: zero_bit_def one_bit_def Abs_bit_inverse Rep_bit_inverse)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    83
  done
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    84
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    85
lemma Abs_bit_eq_of_bool [code_abbrev]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    86
  \<open>Abs_bit = of_bool\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    87
  by (simp add: fun_eq_iff zero_bit_def one_bit_def)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    88
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    89
lemma Rep_bit_eq_odd:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    90
  \<open>Rep_bit = odd\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    91
proof -
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    92
  have \<open>\<not> Rep_bit 0\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    93
    by (simp only: zero_bit_def) (subst Abs_bit_inverse, auto)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    94
  then show ?thesis
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    95
    by (auto simp flip: Rep_bit_inject simp add: fun_eq_iff)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    96
qed
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    97
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    98
lemma Rep_bit_iff_odd [code_abbrev]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
    99
  \<open>Rep_bit b \<longleftrightarrow> odd b\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   100
  by (simp add: Rep_bit_eq_odd)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   101
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   102
lemma Not_Rep_bit_iff_even [code_abbrev]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   103
  \<open>\<not> Rep_bit b \<longleftrightarrow> even b\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   104
  by (simp add: Rep_bit_eq_odd)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   105
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   106
lemma Not_Not_Rep_bit [code_unfold]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   107
  \<open>\<not> \<not> Rep_bit b \<longleftrightarrow> Rep_bit b\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   108
  by simp
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   109
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   110
code_datatype \<open>0::bit\<close> \<open>1::bit\<close>
63462
c1fe30f2bc32 misc tuning and modernization;
wenzelm
parents: 60679
diff changeset
   111
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   112
lemma Abs_bit_code [code]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   113
  \<open>Abs_bit False = 0\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   114
  \<open>Abs_bit True = 1\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   115
  by (simp_all add: Abs_bit_eq_of_bool)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   116
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   117
lemma Rep_bit_code [code]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   118
  \<open>Rep_bit 0 \<longleftrightarrow> False\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   119
  \<open>Rep_bit 1 \<longleftrightarrow> True\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   120
  by (simp_all add: Rep_bit_eq_odd)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   121
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   122
context zero_neq_one
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   123
begin
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   124
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   125
abbreviation of_bit :: \<open>bit \<Rightarrow> 'a\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   126
  where \<open>of_bit b \<equiv> of_bool (odd b)\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   127
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   128
end
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   129
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   130
context
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   131
begin
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   132
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   133
qualified lemma bit_eq_iff:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   134
  \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b)\<close> for a b :: bit
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   135
  by (cases a; cases b) simp_all
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   136
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   137
end
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   138
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   139
lemma modulo_bit_unfold [simp, code]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   140
  \<open>a mod b = of_bool (odd a \<and> even b)\<close> for a b :: bit
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   141
  by (simp add: modulo_bit_def Abs_bit_eq_of_bool Rep_bit_eq_odd)
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   142
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   143
lemma power_bit_unfold [simp, code]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   144
  \<open>a ^ n = of_bool (odd a \<or> n = 0)\<close> for a :: bit
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   145
  by (cases a) simp_all
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   146
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   147
instantiation bit :: semiring_bits
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   148
begin
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   149
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   150
definition bit_bit :: \<open>bit \<Rightarrow> nat \<Rightarrow> bool\<close>
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   151
  where [simp]: \<open>bit_bit b n \<longleftrightarrow> odd b \<and> n = 0\<close>
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   152
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   153
instance
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   154
  apply standard
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   155
              apply auto
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   156
  apply (metis bit.exhaust of_bool_eq(2))
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   157
  done
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   158
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   159
end
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   160
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   161
instantiation bit :: semiring_bit_shifts
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   162
begin
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   163
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   164
definition push_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   165
  where [simp]: \<open>push_bit n b = of_bool (odd b \<and> n = 0)\<close> for b :: bit
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   166
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   167
definition drop_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   168
  where [simp]: \<open>drop_bit_bit = push_bit\<close>
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   169
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   170
definition take_bit_bit :: \<open>nat \<Rightarrow> bit \<Rightarrow> bit\<close>
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   171
  where [simp]: \<open>take_bit n b = of_bool (odd b \<and> n > 0)\<close> for b :: bit
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   172
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   173
instance
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   174
  by standard simp_all
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   175
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   176
end
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   177
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   178
instantiation bit :: semiring_bit_operations
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   179
begin
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   180
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   181
definition and_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   182
  where [simp]: \<open>b AND c = of_bool (odd b \<and> odd c)\<close> for b c :: bit
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   183
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   184
definition or_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   185
  where [simp]: \<open>b OR c = of_bool (odd b \<or> odd c)\<close> for b c :: bit
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   186
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   187
definition xor_bit :: \<open>bit \<Rightarrow> bit \<Rightarrow> bit\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   188
  where [simp]: \<open>b XOR c = of_bool (odd b \<noteq> odd c)\<close> for b c :: bit
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71957
diff changeset
   189
72082
41393ecb57ac uniform mask operation
haftmann
parents: 71988
diff changeset
   190
definition mask_bit :: \<open>nat \<Rightarrow> bit\<close>
41393ecb57ac uniform mask operation
haftmann
parents: 71988
diff changeset
   191
  where [simp]: \<open>mask_bit n = of_bool (n > 0)\<close>
41393ecb57ac uniform mask operation
haftmann
parents: 71988
diff changeset
   192
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   193
instance
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   194
  by standard auto
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   195
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   196
end
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   197
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   198
lemma add_bit_eq_xor [simp, code]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   199
  \<open>(+) = ((XOR) :: bit \<Rightarrow> _)\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   200
  by (auto simp add: fun_eq_iff)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   201
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   202
lemma mult_bit_eq_and [simp, code]:
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   203
  \<open>(*) = ((AND) :: bit \<Rightarrow> _)\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   204
  by (simp add: fun_eq_iff)
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   205
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   206
instantiation bit :: field
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   207
begin
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   208
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   209
definition uminus_bit :: \<open>bit \<Rightarrow> bit\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   210
  where [simp]: \<open>uminus_bit = id\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   211
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   212
definition inverse_bit :: \<open>bit \<Rightarrow> bit\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   213
  where [simp]: \<open>inverse_bit = id\<close>
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   214
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   215
instance
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   216
  by standard simp_all
71953
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   217
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   218
end
428609096812 more lemmas and less name space pollution
haftmann
parents: 71942
diff changeset
   219
71957
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   220
instantiation bit :: ring_bit_operations
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   221
begin
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   222
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   223
definition not_bit :: \<open>bit \<Rightarrow> bit\<close>
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   224
  where [simp]: \<open>NOT b = of_bool (even b)\<close> for b :: bit
71957
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   225
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   226
instance
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   227
  by standard simp_all
71957
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   228
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   229
end
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   230
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   231
lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   232
  by (simp only: Z2.bit_eq_iff even_numeral) simp
71957
3e162c63371a build bit operations on word on library theory on bit operations
haftmann
parents: 71953
diff changeset
   233
71988
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   234
lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
ace45a11a45e a small aggiornamento for Z2
haftmann
parents: 71965
diff changeset
   235
  by (simp only: Z2.bit_eq_iff odd_numeral)  simp
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   236
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   237
end