1.1 --- a/src/HOL/List.thy	Tue Sep 16 16:13:06 2008 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Sep 16 16:13:09 2008 +0200
     1.3 @@ -3376,6 +3376,32 @@
     1.4  lemma char_size [code, simp]:
     1.5    "char_size (c::char) = 0" by (cases c) simp
     1.6  
     1.7 +primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
     1.8 +  "nibble_pair_of_char (Char n m) = (n, m)"
     1.9 +
    1.10 +declare nibble_pair_of_char.simps [code func del]
    1.11 +
    1.12 +setup {*
    1.13 +let
    1.14 +  val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
    1.15 +  val thms = map_product
    1.16 +   (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
    1.17 +      nibbles nibbles;
    1.18 +in
    1.19 +  PureThy.note_thmss Thm.lemmaK [((Name.binding "nibble_pair_of_char_simps", []), [(thms, [])])]
    1.20 +  #-> (fn [(_, thms)] => fold_rev Code.add_func thms)
    1.21 +end
    1.22 +*}
    1.23 +
    1.24 +lemma char_case_nibble_pair [code func, code inline]:
    1.25 +  "char_case f = split f o nibble_pair_of_char"
    1.26 +  by (simp add: expand_fun_eq split: char.split)
    1.27 +
    1.28 +lemma char_rec_nibble_pair [code func, code inline]:
    1.29 +  "char_rec f = split f o nibble_pair_of_char"
    1.30 +  unfolding char_case_nibble_pair [symmetric]
    1.31 +  by (simp add: expand_fun_eq split: char.split)
    1.32 +
    1.33  types string = "char list"
    1.34  
    1.35  syntax