267 declare nat_of_char_simps [code] |
267 declare nat_of_char_simps [code] |
268 |
268 |
269 lemma nibble_of_nat_of_char_div_16: |
269 lemma nibble_of_nat_of_char_div_16: |
270 "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)" |
270 "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)" |
271 by (cases c) |
271 by (cases c) |
272 (simp add: nat_of_char_def add_commute nat_of_nibble_less_16) |
272 (simp add: nat_of_char_def add.commute nat_of_nibble_less_16) |
273 |
273 |
274 lemma nibble_of_nat_nat_of_char: |
274 lemma nibble_of_nat_nat_of_char: |
275 "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)" |
275 "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)" |
276 proof (cases c) |
276 proof (cases c) |
277 case (Char x y) |
277 case (Char x y) |
278 then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y" |
278 then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y" |
279 by (simp add: nibble_of_nat_mod_16) |
279 by (simp add: nibble_of_nat_mod_16) |
280 then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y" |
280 then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y" |
281 by (simp only: nibble_of_nat_mod_16) |
281 by (simp only: nibble_of_nat_mod_16) |
282 with Char show ?thesis by (simp add: nat_of_char_def add_commute) |
282 with Char show ?thesis by (simp add: nat_of_char_def add.commute) |
283 qed |
283 qed |
284 |
284 |
285 code_datatype Char -- {* drop case certificate for char *} |
285 code_datatype Char -- {* drop case certificate for char *} |
286 |
286 |
287 lemma case_char_code [code]: |
287 lemma case_char_code [code]: |
301 proof - |
301 proof - |
302 from mod_mult2_eq [of n 16 16] |
302 from mod_mult2_eq [of n 16 16] |
303 have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp |
303 have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp |
304 then show ?thesis |
304 then show ?thesis |
305 by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble |
305 by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble |
306 card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add_commute) |
306 card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add.commute) |
307 qed |
307 qed |
308 |
308 |
309 lemma char_of_nat_of_char [simp]: |
309 lemma char_of_nat_of_char [simp]: |
310 "char_of_nat (nat_of_char c) = c" |
310 "char_of_nat (nat_of_char c) = c" |
311 by (cases c) |
311 by (cases c) |