# HG changeset patch
# User haftmann
# Date 1486410998 -3600
# Node ID 6e4c05e8edbb7357a1f670ef2d48fabadfb672c7
# Parent  4fb84597ec5a03a3f8d7cdca9626e1856dadb808
computation preprocessing rules to allow literals as input for computations

diff -r 4fb84597ec5a -r 6e4c05e8edbb src/HOL/Code_Numeral.thy
--- 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>
 
diff -r 4fb84597ec5a -r 6e4c05e8edbb src/HOL/String.thy
--- 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"