a sophisticated char/nibble conversion combinator
authorhaftmann
Tue Sep 16 16:13:09 2008 +0200 (2008-09-16)
changeset 28244f433e544a855
parent 28243 84d90ec67059
child 28245 9767dd8e1e54
a sophisticated char/nibble conversion combinator
src/HOL/Library/Code_Char.thy
src/HOL/List.thy
src/HOL/ex/Codegenerator_Pretty.thy
     1.1 --- a/src/HOL/Library/Code_Char.thy	Tue Sep 16 16:13:06 2008 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Tue Sep 16 16:13:09 2008 +0200
     1.3 @@ -9,8 +9,6 @@
     1.4  imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
     1.5  begin
     1.6  
     1.7 -declare char.recs [code func del] char.cases [code func del]
     1.8 -
     1.9  code_type char
    1.10    (SML "char")
    1.11    (OCaml "char")
    1.12 @@ -35,9 +33,6 @@
    1.13    (OCaml "!((_ : char) = _)")
    1.14    (Haskell infixl 4 "==")
    1.15  
    1.16 -lemma [code func, code func del]:
    1.17 -  "(Code_Eval.term_of :: char \<Rightarrow> term) = Code_Eval.term_of" ..
    1.18 -
    1.19  code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
    1.20    (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
    1.21  
     2.1 --- a/src/HOL/List.thy	Tue Sep 16 16:13:06 2008 +0200
     2.2 +++ b/src/HOL/List.thy	Tue Sep 16 16:13:09 2008 +0200
     2.3 @@ -3376,6 +3376,32 @@
     2.4  lemma char_size [code, simp]:
     2.5    "char_size (c::char) = 0" by (cases c) simp
     2.6  
     2.7 +primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
     2.8 +  "nibble_pair_of_char (Char n m) = (n, m)"
     2.9 +
    2.10 +declare nibble_pair_of_char.simps [code func del]
    2.11 +
    2.12 +setup {*
    2.13 +let
    2.14 +  val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
    2.15 +  val thms = map_product
    2.16 +   (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
    2.17 +      nibbles nibbles;
    2.18 +in
    2.19 +  PureThy.note_thmss Thm.lemmaK [((Name.binding "nibble_pair_of_char_simps", []), [(thms, [])])]
    2.20 +  #-> (fn [(_, thms)] => fold_rev Code.add_func thms)
    2.21 +end
    2.22 +*}
    2.23 +
    2.24 +lemma char_case_nibble_pair [code func, code inline]:
    2.25 +  "char_case f = split f o nibble_pair_of_char"
    2.26 +  by (simp add: expand_fun_eq split: char.split)
    2.27 +
    2.28 +lemma char_rec_nibble_pair [code func, code inline]:
    2.29 +  "char_rec f = split f o nibble_pair_of_char"
    2.30 +  unfolding char_case_nibble_pair [symmetric]
    2.31 +  by (simp add: expand_fun_eq split: char.split)
    2.32 +
    2.33  types string = "char list"
    2.34  
    2.35  syntax
     3.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy	Tue Sep 16 16:13:06 2008 +0200
     3.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy	Tue Sep 16 16:13:09 2008 +0200
     3.3 @@ -11,12 +11,6 @@
     3.4  
     3.5  declare isnorm.simps [code func del]
     3.6  
     3.7 -lemma [code func, code func del]:
     3.8 -  "(Code_Eval.term_of :: char \<Rightarrow> term) = Code_Eval.term_of" ..
     3.9 -
    3.10 -declare char.recs [code func del]
    3.11 -  char.cases [code func del]
    3.12 -
    3.13  ML {* (*FIXME get rid of this*)
    3.14  nonfix union;
    3.15  nonfix inter;