isabelle: src/HOL/ex/Word_Computations.thy@89347c0cc6a3 (annotated)

82523 e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	1	(* Author: Florian Haftmann, TU Muenchen *)
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	2
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	3	section \<open>Tests for simplifying word operations on ground terms\<close>
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	4
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	5	theory Word_Computations
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	6	imports
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	7	"HOL.Bit_Operations"
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	8	"HOL-Library.Word"
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	9	begin
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	10
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	11	unbundle bit_operations_syntax
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	12
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	13	named_theorems eval
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	14
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	15	declare mask_numeral [eval]
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	16
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	17	type_synonym word16 = \<open>16 word\<close>
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	18	type_synonym word32 = \<open>32 word\<close>
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	19
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	20	definition computations_arith where
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	21	[eval]: \<open>computations_arith = (
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	22	[473514 + - 763, - 5324 - 7892 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	23	[3131 * - 42, - 2342 div 1213, 2152 mod - 235 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	24	[12323 \<le> (- 12132 :: word16), - 123 < (321312 :: word16), 12323 \<le>s (- 12132 :: word16), - 123 <s (321312 :: word16)]
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	25	)\<close>
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	26
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	27	definition results_arith where
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	28	[eval]: \<open>results_arith = (
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	29	[472751, - 13216 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	30	[- 131502, 52, 2152 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	31	[True, False, False, False]
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	32	)\<close>
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	33
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	34	lemma \<open>computations_arith = results_arith\<close>
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	35	by (simp add: eval)
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	36
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	37	definition computations_bit where
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	38	[eval]: \<open>computations_bit = (
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	39	[bit (473514 :: word16) 5, bit (- 805167 :: word16) 7],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	40	[NOT 473513, NOT (- 805167) :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	41	[473514 AND 767063, - 805167 AND 767063, 473514 AND - 314527, - 805167 AND - 314527 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	42	[473514 OR 767063, - 805167 OR 767063, 473514 OR - 314527, - 805167 OR - 314527 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	43	[473514 XOR 767063, - 805167 XOR 767063, 473514 XOR - 314527, - 805167 XOR - 314527 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	44	mask 11 :: word16,
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	45	[set_bit 15 473514, set_bit 11 (- 805167) :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	46	[unset_bit 13 473514, unset_bit 12 (- 805167) :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	47	[flip_bit 15 473514, flip_bit 12 (- 805167) :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	48	[push_bit 12 473514, push_bit 12 (- 805167) :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	49	[drop_bit 12 65344, drop_bit 12 (- 17405) :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	50	[signed_drop_bit 12 (- 17405) :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	51	[take_bit 12 473514, take_bit 12 (- 805167) :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	52	[signed_take_bit 12 473514, signed_take_bit 12 (- 805167) :: word16]
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	53	)\<close>
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	54
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	55	definition results_bit where
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	56	[eval]: \<open>results_bit = (
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	57	[True, True],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	58	[- 473514, 805166 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	59	[208898, 242769, 209184, - 839103 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	60	[1031679, - 280873, - 50197, - 280591 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	61	[822781, - 523642, - 259381, 558512 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	62	2047 :: word16,
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	63	[506282, - 803119 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	64	[465322, - 809263 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	65	[506282, - 809263 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	66	[1939513344, - 3297964032 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	67	[15, 11 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	68	[- 5 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	69	[2474, 1745 :: word16],
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	70	[- 1622, - 2351 :: word16]
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	71	)\<close>
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	72
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	73	lemma \<open>computations_bit = results_bit\<close>
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	74	by (simp add: eval)
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	75
e4207dfa36b5 explicit check for computations on word type haftmann parents: diff changeset	76	end

author	haftmann
	Thu, 19 Jun 2025 17:15:40 +0200
changeset 82734	89347c0cc6a3
parent 82523	e4207dfa36b5
permissions	-rw-r--r--