--- 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/ _))")
--- 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
--- 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;