# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1500302959 -7200
# Node ID adf3155c57e2123b65311ecd1ee2306f5856bb46
# Parent  e5ba49a72ab9c8725aa42c266e9527de8e59363a
Printing natural numbers as numerals in evaluation

diff -r e5ba49a72ab9 -r adf3155c57e2 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Sun Jul 16 23:47:21 2017 +0200
+++ b/src/HOL/Num.thy	Mon Jul 17 16:49:19 2017 +0200
@@ -1253,4 +1253,14 @@
 code_identifier
   code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
+subsection \<open>Printing of evaluated natural numbers as numerals\<close>
+
+lemma [code_post]:
+  "Suc 0 = 1"
+  "Suc 1 = 2"
+  "Suc (numeral n) = numeral (Num.inc n)"
+  by (simp_all add: numeral_inc)
+
+lemmas [code_post] = Num.inc.simps
+
 end
diff -r e5ba49a72ab9 -r adf3155c57e2 src/HOL/Predicate_Compile_Examples/Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Sun Jul 16 23:47:21 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Mon Jul 17 16:49:19 2017 +0200
@@ -311,14 +311,7 @@
 definition list :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list" where
   "list s n = map s [0 ..< n]"
 
-values [expected "{[Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
-     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
-     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)
-     )))))))))))))))))))))))))))))))))))))))),
-   Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc   (Suc (Suc (Suc (Suc
-     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
-     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)
-     )))))))))))))))))))))))))))))))))))))))))]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
+values [expected "{[42::nat, 43]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
 
 
 subsection \<open>CCS\<close>
diff -r e5ba49a72ab9 -r adf3155c57e2 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Sun Jul 16 23:47:21 2017 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Mon Jul 17 16:49:19 2017 +0200
@@ -379,7 +379,7 @@
 code_pred [dseq] one_or_two .
 code_pred [random_dseq] one_or_two .
 thm one_or_two.dseq_equation
-values [expected "{Suc 0, Suc (Suc 0)}"] "{x. one_or_two x}"
+values [expected "{1::nat, 2}"] "{x. one_or_two x}"
 values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
 
 inductive one_or_two' :: "nat => bool"
@@ -432,9 +432,9 @@
 
 values [expected "{}" dseq 0] 8 "{x. even x}"
 values [expected "{0::nat}" dseq 1] 8 "{x. even x}"
-values [expected "{0, Suc (Suc 0)}" dseq 3] 8 "{x. even x}"
-values [expected "{0, Suc (Suc 0)}" dseq 4] 8 "{x. even x}"
-values [expected "{0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))}" dseq 6] 8 "{x. even x}"
+values [expected "{0::nat, 2}" dseq 3] 8 "{x. even x}"
+values [expected "{0::nat, 2}" dseq 4] 8 "{x. even x}"
+values [expected "{0::nat, 2, 4}" dseq 6] 8 "{x. even x}"
 
 values [random_dseq 1, 1, 0] 8 "{x. even x}"
 values [random_dseq 1, 1, 1] 8 "{x. even x}"
@@ -487,7 +487,7 @@
 values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}"
 
 values [expected "{}" dseq 0] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
-values [expected "{(([]::nat list), [Suc 0, Suc (Suc 0), Suc (Suc (Suc 0)), Suc (Suc (Suc (Suc 0))), Suc (Suc (Suc (Suc (Suc 0))))])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
+values [expected "{(([]::nat list), [1::nat, 2, 3, 4, 5])}" dseq 1] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
 values [dseq 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
 values [dseq 6] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
 values [random_dseq 1, 1, 4] 10 "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}"
@@ -598,9 +598,9 @@
 
 thm filter1.equation
 
-values [expected "{[0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
+values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
 values [expected "{}" dseq 9] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
-values [expected "{[0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
+values [expected "{[0::nat, 2, 4]}" dseq 10] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
 
 inductive filter2
 where
@@ -1278,21 +1278,16 @@
 thm plus_nat_test.equation
 thm plus_nat_test.new_random_dseq_equation
 
-values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))}"] "{z. plus_nat_test 4 5 z}"
-values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))}"] "{z. plus_nat_test 7 2 z}"
-values [expected "{Suc (Suc (Suc (Suc 0)))}"] "{y. plus_nat_test 5 y 9}"
+values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}"
+values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}"
+values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}"
 values [expected "{}"] "{y. plus_nat_test 9 y 8}"
-values [expected "{Suc (Suc (Suc (Suc (Suc (Suc 0)))))}"] "{y. plus_nat_test 1 y 7}"
-values [expected "{Suc (Suc 0)}"] "{x. plus_nat_test x 7 9}"
+values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}"
+values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"
 values [expected "{}"] "{x. plus_nat_test x 9 7}"
 values [expected "{(0::nat, 0::nat)}"] "{(x, y). plus_nat_test x y 0}"
-values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}"
-values [expected "{(0, Suc (Suc (Suc (Suc (Suc 0))))),
-                  (Suc 0, Suc (Suc (Suc (Suc 0)))),
-                  (Suc (Suc 0), Suc (Suc (Suc 0))),
-                  (Suc (Suc (Suc 0)), Suc (Suc 0)),
-                  (Suc (Suc (Suc (Suc 0))), Suc 0),
-                  (Suc (Suc (Suc (Suc (Suc 0)))), 0)}"]
+values [expected "{(0, 1), (1::nat, 0::nat)}"] "{(x, y). plus_nat_test x y 1}"
+values [expected "{(0::nat, 5::nat), (1, 4), (2, 3), (3, 2), (4, 1), (5, 0)}"]
   "{(x, y). plus_nat_test x y 5}"
 
 inductive minus_nat_test :: "nat => nat => nat => bool"
@@ -1306,10 +1301,10 @@
 thm minus_nat_test.new_random_dseq_equation
 
 values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"
-values [expected "{Suc (Suc (Suc (Suc (Suc 0))))}"] "{z. minus_nat_test 7 2 z}"
-values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))}"] "{x. minus_nat_test x 7 9}"
-values [expected "{Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))}"] "{x. minus_nat_test x 9 7}"
-values [expected "{0, Suc 0, Suc (Suc 0), Suc (Suc (Suc 0))}"] "{x. minus_nat_test x 3 0}"
+values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}"
+values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}"
+values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}"
+values [expected "{0::nat, 1, 2, 3}"] "{x. minus_nat_test x 3 0}"
 values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"
 
 subsection \<open>Examples on int\<close>