67909
|
1 |
(* Author: Florian Haftmann, TUM
|
|
2 |
*)
|
|
3 |
|
|
4 |
section \<open>Proof of concept for algebraically founded lists of bits\<close>
|
|
5 |
|
|
6 |
theory Bit_Lists
|
|
7 |
imports Main
|
|
8 |
begin
|
|
9 |
|
|
10 |
context comm_semiring_1
|
|
11 |
begin
|
|
12 |
|
|
13 |
primrec of_unsigned :: "bool list \<Rightarrow> 'a"
|
|
14 |
where "of_unsigned [] = 0"
|
|
15 |
| "of_unsigned (b # bs) = of_bool b + 2 * of_unsigned bs"
|
|
16 |
|
|
17 |
end
|
|
18 |
|
|
19 |
context comm_ring_1
|
|
20 |
begin
|
|
21 |
|
|
22 |
definition of_signed :: "bool list \<Rightarrow> 'a"
|
|
23 |
where "of_signed bs = (if bs = [] then 0 else if last bs
|
|
24 |
then - (of_unsigned (map Not bs) + 1) else of_unsigned bs)"
|
|
25 |
|
|
26 |
end
|
|
27 |
|
|
28 |
class semiring_bits = semiring_parity +
|
|
29 |
assumes half_measure: "a div 2 \<noteq> a \<Longrightarrow> euclidean_size (a div 2) < euclidean_size a"
|
|
30 |
\<comment> \<open>It is not clear whether this could be derived from already existing assumptions.\<close>
|
|
31 |
begin
|
|
32 |
|
|
33 |
function bits_of :: "'a \<Rightarrow> bool list"
|
|
34 |
where "bits_of a = odd a # (let b = a div 2 in if a = b then [] else bits_of b)"
|
|
35 |
by auto
|
|
36 |
|
|
37 |
termination
|
|
38 |
by (relation "measure euclidean_size") (auto intro: half_measure)
|
|
39 |
|
|
40 |
lemma bits_of_not_empty [simp]:
|
|
41 |
"bits_of a \<noteq> []"
|
|
42 |
by (induction a rule: bits_of.induct) simp_all
|
|
43 |
|
|
44 |
lemma bits_of_0 [simp]:
|
|
45 |
"bits_of 0 = [False]"
|
|
46 |
by simp
|
|
47 |
|
|
48 |
lemma bits_of_1 [simp]:
|
|
49 |
"bits_of 1 = [True, False]"
|
|
50 |
by simp
|
|
51 |
|
|
52 |
lemma bits_of_double [simp]:
|
|
53 |
"bits_of (a * 2) = False # (if a = 0 then [] else bits_of a)"
|
|
54 |
by simp (simp add: mult_2_right)
|
|
55 |
|
|
56 |
lemma bits_of_add_1_double [simp]:
|
|
57 |
"bits_of (1 + a * 2) = True # (if a + 1 = 0 then [] else bits_of a)"
|
|
58 |
by simp (simp add: mult_2_right algebra_simps)
|
|
59 |
|
|
60 |
declare bits_of.simps [simp del]
|
|
61 |
|
|
62 |
lemma not_last_bits_of_nat [simp]:
|
|
63 |
"\<not> last (bits_of (of_nat n))"
|
|
64 |
by (induction n rule: parity_induct)
|
|
65 |
(use of_nat_neq_0 in \<open>simp_all add: algebra_simps\<close>)
|
|
66 |
|
|
67 |
lemma of_unsigned_bits_of_nat:
|
|
68 |
"of_unsigned (bits_of (of_nat n)) = of_nat n"
|
|
69 |
by (induction n rule: parity_induct)
|
|
70 |
(use of_nat_neq_0 in \<open>simp_all add: algebra_simps\<close>)
|
|
71 |
|
|
72 |
end
|
|
73 |
|
|
74 |
instance nat :: semiring_bits
|
|
75 |
by standard simp
|
|
76 |
|
|
77 |
lemma bits_of_Suc_double [simp]:
|
|
78 |
"bits_of (Suc (n * 2)) = True # bits_of n"
|
|
79 |
using bits_of_add_1_double [of n] by simp
|
|
80 |
|
|
81 |
lemma of_unsigned_bits_of:
|
|
82 |
"of_unsigned (bits_of n) = n" for n :: nat
|
|
83 |
using of_unsigned_bits_of_nat [of n, where ?'a = nat] by simp
|
|
84 |
|
|
85 |
class ring_bits = ring_parity + semiring_bits
|
|
86 |
begin
|
|
87 |
|
|
88 |
lemma bits_of_minus_1 [simp]:
|
|
89 |
"bits_of (- 1) = [True]"
|
|
90 |
using bits_of.simps [of "- 1"] by simp
|
|
91 |
|
|
92 |
lemma bits_of_double [simp]:
|
|
93 |
"bits_of (- (a * 2)) = False # (if a = 0 then [] else bits_of (- a))"
|
|
94 |
using bits_of.simps [of "- (a * 2)"] nonzero_mult_div_cancel_right [of 2 "- a"]
|
|
95 |
by simp (simp add: mult_2_right)
|
|
96 |
|
|
97 |
lemma bits_of_minus_1_diff_double [simp]:
|
|
98 |
"bits_of (- 1 - a * 2) = True # (if a = 0 then [] else bits_of (- 1 - a))"
|
|
99 |
proof -
|
|
100 |
have [simp]: "- 1 - a = - a - 1"
|
|
101 |
by (simp add: algebra_simps)
|
|
102 |
show ?thesis
|
|
103 |
using bits_of.simps [of "- 1 - a * 2"] div_mult_self1 [of 2 "- 1" "- a"]
|
|
104 |
by simp (simp add: mult_2_right algebra_simps)
|
|
105 |
qed
|
|
106 |
|
|
107 |
lemma last_bits_of_neg_of_nat [simp]:
|
|
108 |
"last (bits_of (- 1 - of_nat n))"
|
|
109 |
proof (induction n rule: parity_induct)
|
|
110 |
case zero
|
|
111 |
then show ?case
|
|
112 |
by simp
|
|
113 |
next
|
|
114 |
case (even n)
|
|
115 |
then show ?case
|
|
116 |
by (simp add: algebra_simps)
|
|
117 |
next
|
|
118 |
case (odd n)
|
|
119 |
then have "last (bits_of ((- 1 - of_nat n) * 2))"
|
|
120 |
by auto
|
|
121 |
also have "(- 1 - of_nat n) * 2 = - 1 - (1 + 2 * of_nat n)"
|
|
122 |
by (simp add: algebra_simps)
|
|
123 |
finally show ?case
|
|
124 |
by simp
|
|
125 |
qed
|
|
126 |
|
|
127 |
lemma of_signed_bits_of_nat:
|
|
128 |
"of_signed (bits_of (of_nat n)) = of_nat n"
|
|
129 |
by (simp add: of_signed_def of_unsigned_bits_of_nat)
|
|
130 |
|
|
131 |
lemma of_signed_bits_neg_of_nat:
|
|
132 |
"of_signed (bits_of (- 1 - of_nat n)) = - 1 - of_nat n"
|
|
133 |
proof -
|
|
134 |
have "of_unsigned (map Not (bits_of (- 1 - of_nat n))) = of_nat n"
|
|
135 |
proof (induction n rule: parity_induct)
|
|
136 |
case zero
|
|
137 |
then show ?case
|
|
138 |
by simp
|
|
139 |
next
|
|
140 |
case (even n)
|
|
141 |
then show ?case
|
|
142 |
by (simp add: algebra_simps)
|
|
143 |
next
|
|
144 |
case (odd n)
|
|
145 |
have *: "- 1 - (1 + of_nat n * 2) = - 2 - of_nat n * 2"
|
|
146 |
by (simp add: algebra_simps) (metis add_assoc one_add_one)
|
|
147 |
from odd show ?case
|
|
148 |
using bits_of_double [of "of_nat (Suc n)"] of_nat_neq_0
|
|
149 |
by (simp add: algebra_simps *)
|
|
150 |
qed
|
|
151 |
then show ?thesis
|
|
152 |
by (simp add: of_signed_def algebra_simps)
|
|
153 |
qed
|
|
154 |
|
|
155 |
lemma of_signed_bits_of_int:
|
|
156 |
"of_signed (bits_of (of_int k)) = of_int k"
|
|
157 |
by (cases k rule: int_cases)
|
|
158 |
(simp_all add: of_signed_bits_of_nat of_signed_bits_neg_of_nat)
|
|
159 |
|
|
160 |
end
|
|
161 |
|
|
162 |
instance int :: ring_bits
|
|
163 |
by standard auto
|
|
164 |
|
|
165 |
lemma of_signed_bits_of:
|
|
166 |
"of_signed (bits_of k) = k" for k :: int
|
|
167 |
using of_signed_bits_of_int [of k, where ?'a = int] by simp
|
|
168 |
|
|
169 |
end
|