src/HOL/Code_Evaluation.thy
changeset 62597 b3f2b8c906a6
parent 61799 4cf66f21b764
child 62958 b41c1cb5e251
     1.1 --- a/src/HOL/Code_Evaluation.thy	Fri Mar 11 17:20:14 2016 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Sat Mar 12 22:04:52 2016 +0100
     1.3 @@ -105,12 +105,14 @@
     1.4    "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
     1.5    "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
     1.6  
     1.7 -lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
     1.8 -  "Code_Evaluation.term_of c = (case c of Char x y \<Rightarrow>
     1.9 -   Code_Evaluation.App (Code_Evaluation.App
    1.10 -    (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
    1.11 -      (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
    1.12 -  by (subst term_of_anything) rule 
    1.13 +definition case_char :: "'a \<Rightarrow> (num \<Rightarrow> 'a) \<Rightarrow> char \<Rightarrow> 'a"
    1.14 +  where "case_char f g c = (if c = 0 then f else g (num_of_nat (nat_of_char c)))"
    1.15 +
    1.16 +lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_num_def, code]:
    1.17 +  "term_of =
    1.18 +    case_char (Const (STR ''Groups.zero_class.zero'') (TYPEREP(char)))
    1.19 +    (\<lambda>k. App (Const (STR ''String.Char'') (TYPEREP(num \<Rightarrow> char))) (term_of k))"
    1.20 +  by (rule ext) (rule term_of_anything [THEN meta_eq_to_obj_eq])
    1.21  
    1.22  lemma term_of_string [code]:
    1.23     "term_of s = App (Const (STR ''STR'')
    1.24 @@ -133,7 +135,7 @@
    1.25     else
    1.26       App (Const (STR ''Groups.uminus_class.uminus'') TYPEREP(integer \<Rightarrow> integer))
    1.27         (term_of (- i)))"
    1.28 -by(rule term_of_anything[THEN meta_eq_to_obj_eq])
    1.29 +  by (rule term_of_anything [THEN meta_eq_to_obj_eq])
    1.30  
    1.31  code_reserved Eval HOLogic
    1.32