# HG changeset patch # User haftmann # Date 1360913491 -3600 # Node ID 0ede9e2266a8cd60f66fbad15ace387ce368d1c1 # Parent 0a2371e7ced3a13eb4247f3c3b0651c10e5173cf less customary term_of conversions; spurious side effect on method reflection diff -r 0a2371e7ced3 -r 0ede9e2266a8 src/HOL/Code_Evaluation.thy --- 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 \ integer \ term" + (Eval "HOLogic.mk'_number/ HOLogic.code'_integerT") + code_const "term_of \ String.literal \ term" (Eval "HOLogic.mk'_literal") code_reserved Eval HOLogic -subsubsection {* Numeric types *} - -definition term_of_num_semiring :: "'a\semiring_div \ 'a \ term" where - "term_of_num_semiring two = (\_. 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 <\> term_of_num_semiring two (k div two) - else termify Num.Bit1 <\> 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 \ nat) <\> 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 \ natural) <\> 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 \ integer) <\> term_of_num_semiring (2::integer) (- k) - else termify (numeral :: num \ integer) <\> 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 \ int) <\> term_of_num_semiring (2::int) (- k) - else termify (numeral :: num \ int) <\> 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 diff -r 0a2371e7ced3 -r 0ede9e2266a8 src/HOL/Predicate_Compile_Examples/Examples.thy --- 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 \ 'a) \ nat \ 'a list" where "list s n = map s [0 ..< n]" -values [expected "{[42, (43 :: nat)]}"] "{list s 2|s. (SKIP, nth [42, 43]) \ 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]) \ s}" subsection {* CCS *} diff -r 0a2371e7ced3 -r 0ede9e2266a8 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- 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 *} diff -r 0a2371e7ced3 -r 0ede9e2266a8 src/HOL/ex/Reflection_Examples.thy --- 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 \ B \ (B \ A \ (B \ C \ (B \ A \ D))) \ A \ B \ D" apply (reflection Ifm.simps only: "B \ C \ (B \ A \ D)") - apply code_simp oops