src/HOL/Library/Bit.thy
author haftmann
Sun, 18 Aug 2013 15:29:50 +0200
changeset 53063 8f7ac535892f
parent 49834 b27bbb021df1
child 54489 03ff4d1e6784
permissions -rw-r--r--
explicit conversion from and to bool, and into algebraic structures with 0 and 1
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 36409
diff changeset
     1
(*  Title:      HOL/Library/Bit.thy
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
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
     5
header {* The Field of Integers mod 2 *}
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
     6
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
     7
theory Bit
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
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    11
subsection {* Bits as a datatype *}
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    12
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    13
typedef bit = "UNIV :: bool set"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    14
  morphisms set Bit
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    15
  ..
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    16
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    17
instantiation bit :: "{zero, one}"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    18
begin
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    19
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    20
definition zero_bit_def:
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    21
  "0 = Bit False"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    22
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    23
definition one_bit_def:
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    24
  "1 = Bit True"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    25
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    26
instance ..
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    27
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    28
end
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    29
45701
615da8b8d758 discontinued obsolete datatype "alt_names";
wenzelm
parents: 41959
diff changeset
    30
rep_datatype "0::bit" "1::bit"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    31
proof -
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    32
  fix P and x :: bit
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    33
  assume "P (0::bit)" and "P (1::bit)"
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    34
  then have "\<forall>b. P (Bit b)"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    35
    unfolding zero_bit_def one_bit_def
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    36
    by (simp add: all_bool_eq)
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    37
  then show "P x"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    38
    by (induct x) simp
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    39
next
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    40
  show "(0::bit) \<noteq> (1::bit)"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    41
    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
    42
    by (simp add: Bit_inject)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    43
qed
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    44
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    45
lemma Bit_set_eq [simp]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    46
  "Bit (set b) = b"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    47
  by (fact set_inverse)
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    48
  
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    49
lemma set_Bit_eq [simp]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    50
  "set (Bit P) = P"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    51
  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
    52
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    53
lemma bit_eq_iff:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    54
  "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    55
  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
    56
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    57
lemma Bit_inject [simp]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    58
  "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
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: Bit_inject)  
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
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    71
lemma set_iff:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    72
  "set b \<longleftrightarrow> b = 1"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    73
  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
    74
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    75
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
    76
  "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
    77
  "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
    78
  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
    79
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    80
lemma Bit [simp, code]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    81
  "Bit False = 0"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    82
  "Bit True = 1"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    83
  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
    84
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    85
lemma bit_not_0_iff [iff]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    86
  "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    87
  by (simp add: bit_eq_iff)
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    88
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    89
lemma bit_not_1_iff [iff]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    90
  "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    91
  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
    92
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    93
lemma [code]:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    94
  "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
    95
  "HOL.equal 1 b \<longleftrightarrow> set b"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    96
  by (simp_all add: equal set_iff)  
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    97
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
    98
  
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
    99
subsection {* Type @{typ bit} forms a field *}
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   100
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36349
diff changeset
   101
instantiation bit :: field_inverse_zero
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   102
begin
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   103
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   104
definition plus_bit_def:
31212
a94aea0cef76 eliminated case input syntax on bits
haftmann
parents: 30129
diff changeset
   105
  "x + y = bit_case y (bit_case 1 0 y) x"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   106
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   107
definition times_bit_def:
31212
a94aea0cef76 eliminated case input syntax on bits
haftmann
parents: 30129
diff changeset
   108
  "x * y = bit_case 0 y x"
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   109
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   110
definition uminus_bit_def [simp]:
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   111
  "- x = (x :: bit)"
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
definition minus_bit_def [simp]:
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   114
  "x - y = (x + y :: bit)"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   115
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   116
definition inverse_bit_def [simp]:
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   117
  "inverse x = (x :: bit)"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   118
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   119
definition divide_bit_def [simp]:
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   120
  "x / y = (x * y :: bit)"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   121
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   122
lemmas field_bit_defs =
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   123
  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
   124
  divide_bit_def inverse_bit_def
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   125
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   126
instance proof
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   127
qed (unfold field_bit_defs, auto split: bit.split)
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   128
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   129
end
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   130
30129
419116f1157a remove unnecessary simp rules
huffman
parents: 29995
diff changeset
   131
lemma bit_add_self: "x + x = (0 :: bit)"
419116f1157a remove unnecessary simp rules
huffman
parents: 29995
diff changeset
   132
  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
   133
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   134
lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   135
  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
   136
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   137
text {* Not sure whether the next two should be simp rules. *}
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   138
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   139
lemma bit_add_eq_0_iff: "x + y = (0 :: bit) \<longleftrightarrow> x = y"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   140
  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
   141
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   142
lemma bit_add_eq_1_iff: "x + y = (1 :: bit) \<longleftrightarrow> x \<noteq> y"
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   143
  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
   144
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   145
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   146
subsection {* Numerals at type @{typ bit} *}
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   147
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   148
text {* All numerals reduce to either 0 or 1. *}
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   149
29995
62efbd0ef132 add rule for minus 1 at type bit
huffman
parents: 29994
diff changeset
   150
lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   151
  by (simp only: minus_one [symmetric] uminus_bit_def)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   152
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   153
lemma bit_neg_numeral [simp]: "(neg_numeral w :: bit) = numeral w"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   154
  by (simp only: neg_numeral_def uminus_bit_def)
29995
62efbd0ef132 add rule for minus 1 at type bit
huffman
parents: 29994
diff changeset
   155
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   156
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
   157
  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
   158
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45701
diff changeset
   159
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
   160
  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
   161
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   162
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   163
subsection {* Conversion from @{typ bit} *}
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   164
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   165
context zero_neq_one
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   166
begin
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   167
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   168
definition of_bit :: "bit \<Rightarrow> 'a"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   169
where
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   170
  "of_bit b = bit_case 0 1 b" 
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   171
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   172
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
   173
  "of_bit 0 = 0"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   174
  "of_bit 1 = 1"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   175
  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
   176
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   177
lemma of_bit_eq_iff:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   178
  "of_bit x = of_bit y \<longleftrightarrow> x = y"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   179
  by (cases x) (cases y, simp_all)+
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   180
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   181
end  
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   182
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   183
context semiring_1
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   184
begin
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   185
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   186
lemma of_nat_of_bit_eq:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   187
  "of_nat (of_bit b) = of_bit b"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   188
  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
   189
29994
6ca6b6bd6e15 add formalization of a type of integers mod 2 to Library
huffman
parents:
diff changeset
   190
end
53063
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   191
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   192
context ring_1
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   193
begin
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   194
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   195
lemma of_int_of_bit_eq:
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   196
  "of_int (of_bit b) = of_bit b"
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   197
  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
   198
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   199
end
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   200
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   201
hide_const (open) set
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   202
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   203
end
8f7ac535892f explicit conversion from and to bool, and into algebraic structures with 0 and 1
haftmann
parents: 49834
diff changeset
   204