# HG changeset patch # User haftmann # Date 1291304355 -3600 # Node ID 3c45d6753fd0e031255ab3906ba2a0ba9fa317a7 # Parent 7046acb44f7a41fc8b042947ca6f722406ba8215# Parent da4bdafeef7c5cd98e53eef44c5733529bc47a07 merged diff -r 7046acb44f7a -r 3c45d6753fd0 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Thu Dec 02 16:17:01 2010 +0100 +++ b/src/HOL/Code_Evaluation.thy Thu Dec 02 16:39:15 2010 +0100 @@ -138,28 +138,37 @@ subsubsection {* Numeric types *} -definition term_of_num :: "'a\{semiring_div} \ 'a\{semiring_div} \ term" where - "term_of_num two = (\_. dummy_term)" +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_code [code]: - "term_of_num two k = (if k = 0 then termify Int.Pls +lemma (in term_syntax) term_of_num_semiring_code [code]: + "term_of_num_semiring two k = (if k = 0 then termify Int.Pls else (if k mod two = 0 - then termify Int.Bit0 <\> term_of_num two (k div two) - else termify Int.Bit1 <\> term_of_num two (k div two)))" - by (auto simp add: term_of_anything Const_def App_def term_of_num_def Let_def) + then termify Int.Bit0 <\> term_of_num_semiring two (k div two) + else termify Int.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 Let_def) lemma (in term_syntax) term_of_nat_code [code]: - "term_of (n::nat) = termify (number_of :: int \ nat) <\> term_of_num (2::nat) n" + "term_of (n::nat) = termify (number_of :: int \ nat) <\> term_of_num_semiring (2::nat) n" + by (simp only: term_of_anything) + +lemma (in term_syntax) term_of_code_numeral_code [code]: + "term_of (k::code_numeral) = termify (number_of :: int \ code_numeral) <\> term_of_num_semiring (2::code_numeral) k" by (simp only: term_of_anything) +definition term_of_num_ring :: "'a\ring_div \ 'a \ term" where + "term_of_num_ring two = (\_. dummy_term)" + +lemma (in term_syntax) term_of_num_ring_code [code]: + "term_of_num_ring two k = (if k = 0 then termify Int.Pls + else if k = -1 then termify Int.Min + else if k mod two = 0 then termify Int.Bit0 <\> term_of_num_ring two (k div two) + else termify Int.Bit1 <\> term_of_num_ring two (k div two))" + by (auto simp add: term_of_anything Const_def App_def term_of_num_ring_def Let_def) + 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 (number_of :: int \ int) <\> term_of_num (2::int) k - else termify (uminus :: int \ int) <\> (termify (number_of :: int \ int) <\> term_of_num (2::int) (- k)))" - by (simp only: term_of_anything) - -lemma (in term_syntax) term_of_code_numeral_code [code]: - "term_of (k::code_numeral) = termify (number_of :: int \ code_numeral) <\> term_of_num (2::code_numeral) k" + else termify (number_of :: int \ int) <\> term_of_num_ring (2::int) k)" by (simp only: term_of_anything) @@ -188,6 +197,6 @@ hide_const dummy_term valapp -hide_const (open) Const App Abs termify valtermify term_of term_of_num tracing +hide_const (open) Const App Abs termify valtermify term_of term_of_num_semiring term_of_num_ring tracing end diff -r 7046acb44f7a -r 3c45d6753fd0 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Dec 02 16:17:01 2010 +0100 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Dec 02 16:39:15 2010 +0100 @@ -1272,7 +1272,7 @@ values [expected "{4::int}"] "{c. minus_int_test 9 5 c}" values [expected "{9::int}"] "{a. minus_int_test a 4 5}" -values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}" +values [expected "{-1::int}"] "{b. minus_int_test 4 b 5}" subsection {* minus on bool *}