computation preprocessing rules to allow literals as input for computations
authorhaftmann
Mon Feb 06 20:56:38 2017 +0100 (2017-02-06)
changeset 649946e4c05e8edbb
parent 64993 4fb84597ec5a
child 64995 a7af4045f873
computation preprocessing rules to allow literals as input for computations
src/HOL/Code_Numeral.thy
src/HOL/String.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Mon Feb 06 20:56:37 2017 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Mon Feb 06 20:56:38 2017 +0100
     1.3 @@ -342,6 +342,26 @@
     1.4  
     1.5  code_datatype "0::integer" Pos Neg
     1.6  
     1.7 +  
     1.8 +text \<open>A further pair of constructors for generated computations\<close>
     1.9 +
    1.10 +context
    1.11 +begin  
    1.12 +
    1.13 +qualified definition positive :: "num \<Rightarrow> integer"
    1.14 +  where [simp]: "positive = numeral"
    1.15 +
    1.16 +qualified definition negative :: "num \<Rightarrow> integer"
    1.17 +  where [simp]: "negative = uminus \<circ> numeral"
    1.18 +
    1.19 +lemma [code_computation_unfold]:
    1.20 +  "numeral = positive"
    1.21 +  "Pos = positive"
    1.22 +  "Neg = negative"
    1.23 +  by (simp_all add: fun_eq_iff)
    1.24 +
    1.25 +end
    1.26 +
    1.27  
    1.28  text \<open>Auxiliary operations\<close>
    1.29  
     2.1 --- a/src/HOL/String.thy	Mon Feb 06 20:56:37 2017 +0100
     2.2 +++ b/src/HOL/String.thy	Mon Feb 06 20:56:38 2017 +0100
     2.3 @@ -375,6 +375,17 @@
     2.4  lifting_update literal.lifting
     2.5  lifting_forget literal.lifting
     2.6  
     2.7 +  
     2.8 +subsection \<open>Dedicated conversion for generated computations\<close>
     2.9 +
    2.10 +definition char_of_num :: "num \<Rightarrow> char"
    2.11 +  where "char_of_num = char_of_nat o nat_of_num"
    2.12 +
    2.13 +lemma [code_computation_unfold]:
    2.14 +  "Char = char_of_num"
    2.15 +  by (simp add: fun_eq_iff char_of_num_def nat_of_num_numeral Char_def)
    2.16 +
    2.17 +
    2.18  subsection \<open>Code generator\<close>
    2.19  
    2.20  ML_file "Tools/string_code.ML"