19 \<^item> Byte values from 128 to 255 are uninterpreted blobs. |
19 \<^item> Byte values from 128 to 255 are uninterpreted blobs. |
20 \<close> |
20 \<close> |
21 |
21 |
22 subsubsection \<open>Bytes as datatype\<close> |
22 subsubsection \<open>Bytes as datatype\<close> |
23 |
23 |
|
24 context unique_euclidean_semiring_with_bit_shifts |
|
25 begin |
|
26 |
|
27 lemma bit_horner_sum_iff: |
|
28 \<open>bit (foldr (\<lambda>b k. of_bool b + k * 2) bs 0) n \<longleftrightarrow> n < length bs \<and> bs ! n\<close> |
|
29 proof (induction bs arbitrary: n) |
|
30 case Nil |
|
31 then show ?case |
|
32 by simp |
|
33 next |
|
34 case (Cons b bs) |
|
35 show ?case |
|
36 proof (cases n) |
|
37 case 0 |
|
38 then show ?thesis |
|
39 by simp |
|
40 next |
|
41 case (Suc m) |
|
42 with bit_rec [of _ n] Cons.prems Cons.IH [of m] |
|
43 show ?thesis by simp |
|
44 qed |
|
45 qed |
|
46 |
|
47 lemma take_bit_horner_sum_eq: |
|
48 \<open>take_bit n (foldr (\<lambda>b k. of_bool b + k * 2) bs 0) = foldr (\<lambda>b k. of_bool b + k * 2) (take n bs) 0\<close> |
|
49 proof (induction bs arbitrary: n) |
|
50 case Nil |
|
51 then show ?case |
|
52 by simp |
|
53 next |
|
54 case (Cons b bs) |
|
55 show ?case |
|
56 proof (cases n) |
|
57 case 0 |
|
58 then show ?thesis |
|
59 by simp |
|
60 next |
|
61 case (Suc m) |
|
62 with take_bit_rec [of n] Cons.prems Cons.IH [of m] |
|
63 show ?thesis by (simp add: ac_simps) |
|
64 qed |
|
65 qed |
|
66 |
|
67 lemma (in semiring_bit_shifts) take_bit_eq_horner_sum: |
|
68 \<open>take_bit n a = foldr (\<lambda>b k. of_bool b + k * 2) (map (bit a) [0..<n]) 0\<close> |
|
69 proof (induction a arbitrary: n rule: bits_induct) |
|
70 case (stable a) |
|
71 have *: \<open>((\<lambda>k. k * 2) ^^ n) 0 = 0\<close> |
|
72 by (induction n) simp_all |
|
73 from stable have \<open>bit a = (\<lambda>_. odd a)\<close> |
|
74 by (simp add: stable_imp_bit_iff_odd fun_eq_iff) |
|
75 then have \<open>map (bit a) [0..<n] = replicate n (odd a)\<close> |
|
76 by (simp add: map_replicate_const) |
|
77 with stable show ?case |
|
78 by (simp add: stable_imp_take_bit_eq mask_eq_seq_sum *) |
|
79 next |
|
80 case (rec a b) |
|
81 show ?case |
|
82 proof (cases n) |
|
83 case 0 |
|
84 then show ?thesis |
|
85 by simp |
|
86 next |
|
87 case (Suc m) |
|
88 have \<open>map (bit (of_bool b + 2 * a)) [0..<Suc m] = b # map (bit (of_bool b + 2 * a)) [Suc 0..<Suc m]\<close> |
|
89 by (simp only: upt_conv_Cons) simp |
|
90 also have \<open>\<dots> = b # map (bit a) [0..<m]\<close> |
|
91 by (simp only: flip: map_Suc_upt) (simp add: bit_Suc rec.hyps) |
|
92 finally show ?thesis |
|
93 using Suc rec.IH [of m] by (simp add: take_bit_Suc rec.hyps, simp add: ac_simps) |
|
94 qed |
|
95 qed |
|
96 |
|
97 end |
|
98 |
24 datatype char = |
99 datatype char = |
25 Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool) |
100 Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool) |
26 (digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool) |
101 (digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool) |
27 |
102 |
28 context comm_semiring_1 |
103 context comm_semiring_1 |
29 begin |
104 begin |
30 |
105 |
31 definition of_char :: "char \<Rightarrow> 'a" |
106 definition of_char :: \<open>char \<Rightarrow> 'a\<close> |
32 where "of_char c = ((((((of_bool (digit7 c) * 2 |
107 where \<open>of_char c = foldr (\<lambda>b k. of_bool b + k * 2) |
33 + of_bool (digit6 c)) * 2 |
108 [digit0 c, digit1 c, digit2 c, digit3 c, digit4 c, digit5 c, digit6 c, digit7 c] 0\<close> |
34 + of_bool (digit5 c)) * 2 |
|
35 + of_bool (digit4 c)) * 2 |
|
36 + of_bool (digit3 c)) * 2 |
|
37 + of_bool (digit2 c)) * 2 |
|
38 + of_bool (digit1 c)) * 2 |
|
39 + of_bool (digit0 c)" |
|
40 |
109 |
41 lemma of_char_Char [simp]: |
110 lemma of_char_Char [simp]: |
42 "of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) = |
111 \<open>of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) = |
43 foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0" |
112 foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0\<close> |
44 by (simp add: of_char_def ac_simps) |
113 by (simp add: of_char_def) |
45 |
114 |
46 end |
115 end |
47 |
116 |
48 context unique_euclidean_semiring_with_bit_shifts |
117 context unique_euclidean_semiring_with_bit_shifts |
49 begin |
118 begin |
50 |
119 |
51 definition char_of :: "'a \<Rightarrow> char" |
120 definition char_of :: \<open>'a \<Rightarrow> char\<close> |
52 where "char_of n = Char (odd n) (odd (drop_bit 1 n)) |
121 where \<open>char_of n = Char (odd n) (bit n 1) (bit n 2) (bit n 3) (bit n 4) (bit n 5) (bit n 6) (bit n 7)\<close> |
53 (odd (drop_bit 2 n)) (odd (drop_bit 3 n)) |
122 |
54 (odd (drop_bit 4 n)) (odd (drop_bit 5 n)) |
123 lemma char_of_take_bit_eq: |
55 (odd (drop_bit 6 n)) (odd (drop_bit 7 n))" |
124 \<open>char_of (take_bit n m) = char_of m\<close> if \<open>n \<ge> 8\<close> |
|
125 using that by (simp add: char_of_def bit_take_bit_iff) |
56 |
126 |
57 lemma char_of_char [simp]: |
127 lemma char_of_char [simp]: |
58 "char_of (of_char c) = c" |
128 \<open>char_of (of_char c) = c\<close> |
59 proof (cases c) |
129 by (simp only: of_char_def char_of_def bit_horner_sum_iff) simp |
60 have **: "drop_bit n (q * 2 + of_bool d) = drop_bit (n - 1) q + drop_bit n (of_bool d)" |
|
61 if "n > 0" for q :: 'a and n :: nat and d :: bool |
|
62 using that by (cases n) simp_all |
|
63 case (Char d0 d1 d2 d3 d4 d5 d6 d7) |
|
64 then show ?thesis |
|
65 by (simp only: of_char_def char_of_def char.simps char.sel drop_bit_of_bool **) simp |
|
66 qed |
|
67 |
130 |
68 lemma char_of_comp_of_char [simp]: |
131 lemma char_of_comp_of_char [simp]: |
69 "char_of \<circ> of_char = id" |
132 "char_of \<circ> of_char = id" |
70 by (simp add: fun_eq_iff) |
133 by (simp add: fun_eq_iff) |
71 |
134 |
72 lemma inj_of_char: |
135 lemma inj_of_char: |
73 "inj of_char" |
136 \<open>inj of_char\<close> |
74 proof (rule injI) |
137 proof (rule injI) |
75 fix c d |
138 fix c d |
76 assume "of_char c = of_char d" |
139 assume "of_char c = of_char d" |
77 then have "char_of (of_char c) = char_of (of_char d)" |
140 then have "char_of (of_char c) = char_of (of_char d)" |
78 by simp |
141 by simp |
79 then show "c = d" |
142 then show "c = d" |
80 by simp |
143 by simp |
81 qed |
144 qed |
82 |
145 |
|
146 lemma of_char_eqI: |
|
147 \<open>c = d\<close> if \<open>of_char c = of_char d\<close> |
|
148 using that inj_of_char by (simp add: inj_eq) |
|
149 |
83 lemma of_char_eq_iff [simp]: |
150 lemma of_char_eq_iff [simp]: |
84 "of_char c = of_char d \<longleftrightarrow> c = d" |
151 \<open>of_char c = of_char d \<longleftrightarrow> c = d\<close> |
85 by (simp add: inj_eq inj_of_char) |
152 by (auto intro: of_char_eqI) |
86 |
153 |
87 lemma of_char_of [simp]: |
154 lemma of_char_of [simp]: |
88 "of_char (char_of a) = a mod 256" |
155 \<open>of_char (char_of a) = a mod 256\<close> |
89 proof - |
156 proof - |
90 have *: "{0::nat..<8} = {0, 1, 2, 3, 4, 5, 6, 7}" |
157 have \<open>[0..<8] = [0, Suc 0, 2, 3, 4, 5, 6, 7 :: nat]\<close> |
91 by auto |
158 by (simp add: upt_eq_Cons_conv) |
92 have "of_char (char_of (take_bit 8 a)) = |
159 then have \<open>[odd a, bit a 1, bit a 2, bit a 3, bit a 4, bit a 5, bit a 6, bit a 7] = map (bit a) [0..<8]\<close> |
93 (\<Sum>k\<in>{0, 1, 2, 3, 4, 5, 6, 7}. push_bit k (of_bool (odd (drop_bit k a))))" |
160 by simp |
94 by (simp add: of_char_def char_of_def push_bit_of_1 drop_bit_take_bit) |
161 then have \<open>of_char (char_of a) = take_bit 8 a\<close> |
95 also have "\<dots> = take_bit 8 a" |
162 by (simp only: char_of_def of_char_def char.sel take_bit_eq_horner_sum) |
96 using * take_bit_sum [of 8 a] by simp |
163 then show ?thesis |
97 also have "char_of(take_bit 8 a) = char_of a" |
|
98 by (simp add: char_of_def drop_bit_take_bit) |
|
99 finally show ?thesis |
|
100 by (simp add: take_bit_eq_mod) |
164 by (simp add: take_bit_eq_mod) |
101 qed |
165 qed |
102 |
166 |
103 lemma char_of_mod_256 [simp]: |
167 lemma char_of_mod_256 [simp]: |
104 "char_of (n mod 256) = char_of n" |
168 \<open>char_of (n mod 256) = char_of n\<close> |
105 by (metis char_of_char of_char_of) |
169 by (rule of_char_eqI) simp |
106 |
170 |
107 lemma of_char_mod_256 [simp]: |
171 lemma of_char_mod_256 [simp]: |
108 "of_char c mod 256 = of_char c" |
172 \<open>of_char c mod 256 = of_char c\<close> |
109 by (metis char_of_char of_char_of) |
173 proof - |
|
174 have \<open>of_char (char_of (of_char c)) mod 256 = of_char (char_of (of_char c))\<close> |
|
175 by (simp only: of_char_of) simp |
|
176 then show ?thesis |
|
177 by simp |
|
178 qed |
110 |
179 |
111 lemma char_of_quasi_inj [simp]: |
180 lemma char_of_quasi_inj [simp]: |
112 "char_of m = char_of n \<longleftrightarrow> m mod 256 = n mod 256" |
181 \<open>char_of m = char_of n \<longleftrightarrow> m mod 256 = n mod 256\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>) |
113 by (metis char_of_mod_256 of_char_of) |
182 proof |
114 |
183 assume ?Q |
115 lemma char_of_nat_eq_iff: |
184 then show ?P |
116 "char_of n = c \<longleftrightarrow> take_bit 8 n = of_char c" |
185 by (auto intro: of_char_eqI) |
117 by (simp add: take_bit_eq_mod) (use of_char_eq_iff in fastforce) |
186 next |
|
187 assume ?P |
|
188 then have \<open>of_char (char_of m) = of_char (char_of n)\<close> |
|
189 by simp |
|
190 then show ?Q |
|
191 by simp |
|
192 qed |
|
193 |
|
194 lemma char_of_eq_iff: |
|
195 \<open>char_of n = c \<longleftrightarrow> take_bit 8 n = of_char c\<close> |
|
196 by (auto intro: of_char_eqI simp add: take_bit_eq_mod) |
118 |
197 |
119 lemma char_of_nat [simp]: |
198 lemma char_of_nat [simp]: |
120 "char_of (of_nat n) = char_of n" |
199 \<open>char_of (of_nat n) = char_of n\<close> |
121 by (simp add: char_of_def String.char_of_def drop_bit_of_nat) |
200 by (simp add: char_of_def String.char_of_def drop_bit_of_nat) |
122 |
201 |
123 end |
202 end |
124 |
203 |
125 lemma inj_on_char_of_nat [simp]: |
204 lemma inj_on_char_of_nat [simp]: |