# HG changeset patch
# User haftmann
# Date 1221574389 -7200
# Node ID f433e544a855503a84f4356ee4a9095f3106e58a
# Parent  84d90ec6705967aed07c41e612c902a80daeb5e4
a sophisticated char/nibble conversion combinator

diff -r 84d90ec67059 -r f433e544a855 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Tue Sep 16 16:13:06 2008 +0200
+++ b/src/HOL/Library/Code_Char.thy	Tue Sep 16 16:13:09 2008 +0200
@@ -9,8 +9,6 @@
 imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
 begin
 
-declare char.recs [code func del] char.cases [code func del]
-
 code_type char
   (SML "char")
   (OCaml "char")
@@ -35,9 +33,6 @@
   (OCaml "!((_ : char) = _)")
   (Haskell infixl 4 "==")
 
-lemma [code func, code func del]:
-  "(Code_Eval.term_of :: char \<Rightarrow> term) = Code_Eval.term_of" ..
-
 code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
   (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
 
diff -r 84d90ec67059 -r f433e544a855 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Sep 16 16:13:06 2008 +0200
+++ b/src/HOL/List.thy	Tue Sep 16 16:13:09 2008 +0200
@@ -3376,6 +3376,32 @@
 lemma char_size [code, simp]:
   "char_size (c::char) = 0" by (cases c) simp
 
+primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
+  "nibble_pair_of_char (Char n m) = (n, m)"
+
+declare nibble_pair_of_char.simps [code func del]
+
+setup {*
+let
+  val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
+  val thms = map_product
+   (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
+      nibbles nibbles;
+in
+  PureThy.note_thmss Thm.lemmaK [((Name.binding "nibble_pair_of_char_simps", []), [(thms, [])])]
+  #-> (fn [(_, thms)] => fold_rev Code.add_func thms)
+end
+*}
+
+lemma char_case_nibble_pair [code func, code inline]:
+  "char_case f = split f o nibble_pair_of_char"
+  by (simp add: expand_fun_eq split: char.split)
+
+lemma char_rec_nibble_pair [code func, code inline]:
+  "char_rec f = split f o nibble_pair_of_char"
+  unfolding char_case_nibble_pair [symmetric]
+  by (simp add: expand_fun_eq split: char.split)
+
 types string = "char list"
 
 syntax
diff -r 84d90ec67059 -r f433e544a855 src/HOL/ex/Codegenerator_Pretty.thy
--- a/src/HOL/ex/Codegenerator_Pretty.thy	Tue Sep 16 16:13:06 2008 +0200
+++ b/src/HOL/ex/Codegenerator_Pretty.thy	Tue Sep 16 16:13:09 2008 +0200
@@ -11,12 +11,6 @@
 
 declare isnorm.simps [code func del]
 
-lemma [code func, code func del]:
-  "(Code_Eval.term_of :: char \<Rightarrow> term) = Code_Eval.term_of" ..
-
-declare char.recs [code func del]
-  char.cases [code func del]
-
 ML {* (*FIXME get rid of this*)
 nonfix union;
 nonfix inter;