(* Author: Florian Haftmann, TU Muenchen *) \<open>Tests for simplifying bit operations on ground terms\<close> theory Bit_Operation_Computationsimports "HOL.Bit_Operations" "HOL-Library.Word" begin \<open>Generic unsigned computations\<close> locale unsigned_computations =fixes type :: \<open>'a::semiring_bit_operations itself\<close> begin definition computations where \<open>computations = ( 'a) 5], AND 767063 :: 'a], 'a], 'a], 'a, 'a], 'a], 'a], 'a], 'a], 'a] \<close> definition results where \<open>results = ( 'a::semiring_bit_operations], 'a], 'a], 'a, 'a], 'a], 'a], 'a], 'a], 'a] \<close> lemmas evaluation_simps = computations_def results_def mask_numeral\<comment> \<open>Expressions like \<term>\<open>mask 42\<close> are deliberately not simplified by default\<close> end \<open>TYPE(nat)\<close> defines unsigned_computations_nat = unsigned_computations_nat.computationsand unsigned_results_nat = unsigned_computations_nat.results .lemma \<open>unsigned_computations_nat.computations = unsigned_computations_nat.results\<close> by (simp add: unsigned_computations_nat.evaluation_simps)\<open>TYPE(int)\<close> defines unsigned_computations_int = unsigned_computations_int.computationsand unsigned_results_int = unsigned_computations_int.results .lemma \<open>unsigned_computations_int.computations = unsigned_computations_int.results\<close> by (simp add: unsigned_computations_int.evaluation_simps)\<open>TYPE(16 word)\<close> defines unsigned_computations_word16 = unsigned_computations_word16.computationsand unsigned_results_word16 = unsigned_computations_word16.results .lemma \<open>unsigned_computations_word16 = unsigned_results_word16\<close> by (simp add: unsigned_computations_word16.evaluation_simps)\<open>Generic unsigned computations\<close> locale signed_computations =fixes type :: \<open>'a::ring_bit_operations itself\<close> begin definition computations where \<open>computations = ( 'a) 7], AND 767063, 473514 AND - 314527, - 805167 AND - 314527 :: 'a], 'a], 'a], 'a], 'a], 'a], 'a], 'a], 'a], 'a] \<close> definition results where \<open>results = ( 'a], 'a], 'a], 'a], 'a], 'a], 'a], 'a], 'a], 'a] \<close> lemmas evaluation_simps = computations_def results_defend \<open>TYPE(int)\<close> defines signed_computations_int = signed_computations_int.computationsand signed_results_int = signed_computations_int.results .lemma \<open>signed_computations_int.computations = signed_computations_int.results\<close> by (simp add: signed_computations_int.evaluation_simps)\<open>TYPE(16 word)\<close> defines signed_computations_word16 = signed_computations_word16.computationsand signed_results_word16 = signed_computations_word16.results .lemma \<open>signed_computations_word16 = signed_results_word16\<close> by (simp add: signed_computations_word16.evaluation_simps)\<open>Special cases on particular type instances\<close> lemma \<open>drop_bit 12 (- 17405 :: int) = - 5\<close> by simplemma \<open>signed_drop_bit 12 (- 17405 :: 16 word) = - 5\<close> by simplemma \<open>drop_bit 12 (- 17405 :: 16 word) = 11\<close> by simpend quality 93%
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
