--- a/src/HOL/Code_Numeral.thy Mon Feb 06 20:56:37 2017 +0100
+++ b/src/HOL/Code_Numeral.thy Mon Feb 06 20:56:38 2017 +0100
@@ -342,6 +342,26 @@
code_datatype "0::integer" Pos Neg
+
+text \<open>A further pair of constructors for generated computations\<close>
+
+context
+begin
+
+qualified definition positive :: "num \<Rightarrow> integer"
+ where [simp]: "positive = numeral"
+
+qualified definition negative :: "num \<Rightarrow> integer"
+ where [simp]: "negative = uminus \<circ> numeral"
+
+lemma [code_computation_unfold]:
+ "numeral = positive"
+ "Pos = positive"
+ "Neg = negative"
+ by (simp_all add: fun_eq_iff)
+
+end
+
text \<open>Auxiliary operations\<close>
--- a/src/HOL/String.thy Mon Feb 06 20:56:37 2017 +0100
+++ b/src/HOL/String.thy Mon Feb 06 20:56:38 2017 +0100
@@ -375,6 +375,17 @@
lifting_update literal.lifting
lifting_forget literal.lifting
+
+subsection \<open>Dedicated conversion for generated computations\<close>
+
+definition char_of_num :: "num \<Rightarrow> char"
+ where "char_of_num = char_of_nat o nat_of_num"
+
+lemma [code_computation_unfold]:
+ "Char = char_of_num"
+ by (simp add: fun_eq_iff char_of_num_def nat_of_num_numeral Char_def)
+
+
subsection \<open>Code generator\<close>
ML_file "Tools/string_code.ML"