less customary term_of conversions;
spurious side effect on method reflection

--- a/src/HOL/Code_Evaluation.thy	Fri Feb 15 08:31:31 2013 +0100
+++ b/src/HOL/Code_Evaluation.thy	Fri Feb 15 08:31:31 2013 +0100
@@ -133,50 +133,15 @@
   (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))"
      and "Term.Free/ ((_), (_))")
 
+code_const "term_of \<Colon> integer \<Rightarrow> term"
+  (Eval "HOLogic.mk'_number/ HOLogic.code'_integerT")
+  
 code_const "term_of \<Colon> String.literal \<Rightarrow> term"
   (Eval "HOLogic.mk'_literal")
 
 code_reserved Eval HOLogic
 
 
-subsubsection {* Numeric types *}
-
-definition term_of_num_semiring :: "'a\<Colon>semiring_div \<Rightarrow> 'a \<Rightarrow> term" where
-  "term_of_num_semiring two = (\<lambda>_. dummy_term)"
-
-lemma (in term_syntax) term_of_num_semiring_code [code]:
-  "term_of_num_semiring two k = (
-    if k = 1 then termify Num.One
-    else (if k mod two = 0
-      then termify Num.Bit0 <\<cdot>> term_of_num_semiring two (k div two)
-      else termify Num.Bit1 <\<cdot>> term_of_num_semiring two (k div two)))"
-  by (auto simp add: term_of_anything Const_def App_def term_of_num_semiring_def)
-
-lemma (in term_syntax) term_of_nat_code [code]:
-  "term_of (n::nat) = (
-    if n = 0 then termify (0 :: nat)
-    else termify (numeral :: num \<Rightarrow> nat) <\<cdot>> term_of_num_semiring (2::nat) n)"
-  by (simp only: term_of_anything)
-
-lemma (in term_syntax) term_of_natural_code [code]:
-  "term_of (k::natural) = (
-    if k = 0 then termify (0 :: natural)
-    else termify (numeral :: num \<Rightarrow> natural) <\<cdot>> term_of_num_semiring (2::natural) k)"
-  by (simp only: term_of_anything)
-
-lemma (in term_syntax) term_of_integer_code [code]:
-  "term_of (k::integer) = (if k = 0 then termify (0 :: integer)
-    else if k < 0 then termify (neg_numeral :: num \<Rightarrow> integer) <\<cdot>> term_of_num_semiring (2::integer) (- k)
-    else termify (numeral :: num \<Rightarrow> integer) <\<cdot>> term_of_num_semiring (2::integer) k)"
-  by (simp only: term_of_anything)
-
-lemma (in term_syntax) term_of_int_code [code]:
-  "term_of (k::int) = (if k = 0 then termify (0 :: int)
-    else if k < 0 then termify (neg_numeral :: num \<Rightarrow> int) <\<cdot>> term_of_num_semiring (2::int) (- k)
-    else termify (numeral :: num \<Rightarrow> int) <\<cdot>> term_of_num_semiring (2::int) k)"
-  by (simp only: term_of_anything)
-
-
 subsubsection {* Obfuscation *}
 
 print_translation {*
@@ -202,7 +167,7 @@
 
 
 hide_const dummy_term valapp
-hide_const (open) Const App Abs Free termify valtermify term_of term_of_num_semiring tracing
+hide_const (open) Const App Abs Free termify valtermify term_of tracing
 
 end
 

--- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Feb 15 08:31:31 2013 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Feb 15 08:31:31 2013 +0100
@@ -309,7 +309,14 @@
 definition list :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list" where
   "list s n = map s [0 ..< n]"
 
-values [expected "{[42, (43 :: nat)]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
+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}"
 
 
 subsection {* CCS *}

--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Feb 15 08:31:31 2013 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Feb 15 08:31:31 2013 +0100
@@ -334,7 +334,7 @@
 code_pred [dseq] one_or_two .
 code_pred [random_dseq] one_or_two .
 thm one_or_two.dseq_equation
-values [expected "{1::nat, 2::nat}"] "{x. one_or_two x}"
+values [expected "{Suc 0, Suc (Suc 0)}"] "{x. one_or_two x}"
 values [random_dseq 0,0,10] 3 "{x. one_or_two x}"
 
 inductive one_or_two' :: "nat => bool"
@@ -387,9 +387,9 @@
 
 values [expected "{}" dseq 0] 8 "{x. even x}"
 values [expected "{0::nat}" dseq 1] 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 [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 [random_dseq 1, 1, 0] 8 "{x. even x}"
 values [random_dseq 1, 1, 1] 8 "{x. even x}"
@@ -442,7 +442,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), [1, 2, 3, 4, (5::nat)])}" dseq 1] 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 [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)]}"
@@ -553,9 +553,9 @@
 
 thm filter1.equation
 
-values [expected "{[0::nat, 2, 4]}"] "{xs. filter1 even [0, 1, 2, 3, 4] xs}"
+values [expected "{[0, Suc (Suc 0), Suc (Suc (Suc (Suc 0)))]}"] "{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::nat, 2, 4]}" dseq 10] "{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}"
 
 inductive filter2
 where
@@ -1233,16 +1233,21 @@
 thm plus_nat_test.equation
 thm plus_nat_test.new_random_dseq_equation
 
-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 "{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 "{}"] "{y. plus_nat_test 9 y 8}"
-values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}"
-values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"
+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 "{}"] "{x. plus_nat_test x 9 7}"
-values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}"
-values [expected "{(0::nat, 1::nat), (1, 0)}"] "{(x, y). plus_nat_test x y 1}"
-values [expected "{(0::nat, 5::nat), (4, 1), (3, 2), (2, 3), (1, 4), (5, 0)}"]
+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)}"]
   "{(x, y). plus_nat_test x y 5}"
 
 inductive minus_nat_test :: "nat => nat => nat => bool"
@@ -1256,10 +1261,10 @@
 thm minus_nat_test.new_random_dseq_equation
 
 values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"
-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 "{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 "{0::nat}"] "{x. minus_nat_test x 0 0}"
 
 subsection {* Examples on int *}

--- a/src/HOL/ex/Reflection_Examples.thy	Fri Feb 15 08:31:31 2013 +0100
+++ b/src/HOL/ex/Reflection_Examples.thy	Fri Feb 15 08:31:31 2013 +0100
@@ -129,7 +129,6 @@
 text {* Now we specify on which subterm it should be applied *}
 lemma "A \<noteq> B \<and> (B \<longrightarrow> A \<noteq> (B \<or> C \<and> (B \<longrightarrow> A \<or> D))) \<longrightarrow> A \<or> B \<and> D"
   apply (reflection Ifm.simps only: "B \<or> C \<and> (B \<longrightarrow> A \<or> D)")
-  apply code_simp
 oops