author | haftmann |
Tue, 19 Nov 2013 10:05:53 +0100 | |
changeset 54489 | 03ff4d1e6784 |
parent 53063 | 8f7ac535892f |
child 55416 | dd7992d4a61a |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Library/Bit.thy |
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 | 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 | 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 | 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 | 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 | 131 |
lemma bit_add_self: "x + x = (0 :: bit)" |
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 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
53063
diff
changeset
|
150 |
lemma bit_minus1 [simp]: "- 1 = (1 :: bit)" |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
53063
diff
changeset
|
151 |
by (simp only: uminus_bit_def) |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45701
diff
changeset
|
152 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
53063
diff
changeset
|
153 |
lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w" |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
53063
diff
changeset
|
154 |
by (simp only: uminus_bit_def) |
29995 | 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 |