# HG changeset patch # User haftmann # Date 1573313961 0 # Node ID a197532693a5d003be7e3bdb2f1b98a46737130b # Parent b7d481cdd54d11d2d81dc623a9ecda7dcd5fcdee bit shifts as class operations diff -r b7d481cdd54d -r a197532693a5 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Sat Nov 09 10:38:51 2019 +0000 +++ b/src/HOL/Code_Numeral.thy Sat Nov 09 15:39:21 2019 +0000 @@ -287,17 +287,30 @@ instance integer :: unique_euclidean_ring_with_nat by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def) -lemma [transfer_rule]: - "rel_fun (=) (rel_fun pcr_integer pcr_integer) (push_bit :: _ \ _ \ int) (push_bit :: _ \ _ \ integer)" - by (unfold push_bit_eq_mult [abs_def]) transfer_prover +instantiation integer :: semiring_bit_shifts +begin + +lift_definition push_bit_integer :: \nat \ integer \ integer\ + is \push_bit\ . + +lift_definition drop_bit_integer :: \nat \ integer \ integer\ + is \drop_bit\ . + +instance by (standard; transfer) + (fact bit_split_eq bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div)+ + +end lemma [transfer_rule]: "rel_fun (=) (rel_fun pcr_integer pcr_integer) (take_bit :: _ \ _ \ int) (take_bit :: _ \ _ \ integer)" by (unfold take_bit_eq_mod [abs_def]) transfer_prover -lemma [transfer_rule]: - "rel_fun (=) (rel_fun pcr_integer pcr_integer) (drop_bit :: _ \ _ \ int) (drop_bit :: _ \ _ \ integer)" - by (unfold drop_bit_eq_div [abs_def]) transfer_prover +instance integer :: unique_euclidean_semiring_with_bit_shifts .. + +lemma [code]: + \push_bit n k = k * 2 ^ n\ + \drop_bit n k = k div 2 ^ n\ for k :: integer + by (fact push_bit_eq_mult drop_bit_eq_div)+ instantiation integer :: unique_euclidean_semiring_numeral begin @@ -968,17 +981,30 @@ instance natural :: unique_euclidean_semiring_with_nat by (standard; transfer) simp_all -lemma [transfer_rule]: - "rel_fun (=) (rel_fun pcr_natural pcr_natural) (push_bit :: _ \ _ \ nat) (push_bit :: _ \ _ \ natural)" - by (unfold push_bit_eq_mult [abs_def]) transfer_prover +instantiation natural :: semiring_bit_shifts +begin + +lift_definition push_bit_natural :: \nat \ natural \ natural\ + is \push_bit\ . + +lift_definition drop_bit_natural :: \nat \ natural \ natural\ + is \drop_bit\ . + +instance by (standard; transfer) + (fact bit_split_eq bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div)+ + +end lemma [transfer_rule]: "rel_fun (=) (rel_fun pcr_natural pcr_natural) (take_bit :: _ \ _ \ nat) (take_bit :: _ \ _ \ natural)" by (unfold take_bit_eq_mod [abs_def]) transfer_prover -lemma [transfer_rule]: - "rel_fun (=) (rel_fun pcr_natural pcr_natural) (drop_bit :: _ \ _ \ nat) (drop_bit :: _ \ _ \ natural)" - by (unfold drop_bit_eq_div [abs_def]) transfer_prover +instance natural :: unique_euclidean_semiring_with_bit_shifts .. + +lemma [code]: + \push_bit n m = m * 2 ^ n\ + \drop_bit n m = m div 2 ^ n\ for m :: natural + by (fact push_bit_eq_mult drop_bit_eq_div)+ lift_definition natural_of_integer :: "integer \ natural" is "nat :: int \ nat" diff -r b7d481cdd54d -r a197532693a5 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Sat Nov 09 10:38:51 2019 +0000 +++ b/src/HOL/Parity.thy Sat Nov 09 15:39:21 2019 +0000 @@ -573,35 +573,6 @@ "n mod 2 \ Suc 0 \ n mod 2 = 0" using not_mod_2_eq_1_eq_0 [of n] by simp -lemma nat_bit_induct [case_names zero even odd]: - "P n" if zero: "P 0" - and even: "\n. P n \ n > 0 \ P (2 * n)" - and odd: "\n. P n \ P (Suc (2 * n))" -proof (induction n rule: less_induct) - case (less n) - show "P n" - proof (cases "n = 0") - case True with zero show ?thesis by simp - next - case False - with less have hyp: "P (n div 2)" by simp - show ?thesis - proof (cases "even n") - case True - then have "n \ 1" - by auto - with \n \ 0\ have "n div 2 > 0" - by simp - with \even n\ hyp even [of "n div 2"] show ?thesis - by simp - next - case False - with hyp odd [of "n div 2"] show ?thesis - by simp - qed - qed -qed - lemma odd_card_imp_not_empty: \A \ {}\ if \odd (card A)\ using that by auto @@ -774,6 +745,72 @@ lemma even_nat_iff: "0 \ k \ even (nat k) \ even k" by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric]) + +subsection \Abstract bit shifts\ + +class semiring_bits = semiring_parity + + assumes bit_split_eq: \\a. of_bool (odd a) + 2 * (a div 2) = a\ + and bit_eq_rec: \\a b. a = b \ (even a = even b) \ a div 2 = b div 2\ + and bit_induct [case_names stable rec]: + \(\a. a div 2 = a \ P a) + \ (\a b. P a \ (of_bool b + 2 * a) div 2 = a \ P (of_bool b + 2 * a)) + \ P a\ + +lemma nat_bit_induct [case_names zero even odd]: + "P n" if zero: "P 0" + and even: "\n. P n \ n > 0 \ P (2 * n)" + and odd: "\n. P n \ P (Suc (2 * n))" +proof (induction n rule: less_induct) + case (less n) + show "P n" + proof (cases "n = 0") + case True with zero show ?thesis by simp + next + case False + with less have hyp: "P (n div 2)" by simp + show ?thesis + proof (cases "even n") + case True + then have "n \ 1" + by auto + with \n \ 0\ have "n div 2 > 0" + by simp + with \even n\ hyp even [of "n div 2"] show ?thesis + by simp + next + case False + with hyp odd [of "n div 2"] show ?thesis + by simp + qed + qed +qed + +instance nat :: semiring_bits +proof + show \of_bool (odd n) + 2 * (n div 2) = n\ + for n :: nat + by simp + show \m = n \ (even m \ even n) \ m div 2 = n div 2\ + for m n :: nat + by (auto dest: odd_two_times_div_two_succ) + show \P n\ if stable: \\n. n div 2 = n \ P n\ + and rec: \\n b. P n \ (of_bool b + 2 * n) div 2 = n \ P (of_bool b + 2 * n)\ + for P and n :: nat + proof (induction n rule: nat_bit_induct) + case zero + from stable [of 0] show ?case + by simp + next + case (even n) + with rec [of n False] show ?case + by simp + next + case (odd n) + with rec [of n True] show ?case + by simp + qed +qed + lemma int_bit_induct [case_names zero minus even odd]: "P k" if zero_int: "P 0" and minus_int: "P (- 1)" @@ -831,27 +868,98 @@ qed qed +instance int :: semiring_bits +proof + show \of_bool (odd k) + 2 * (k div 2) = k\ + for k :: int + by (auto elim: oddE) + show \k = l \ (even k \ even l) \ k div 2 = l div 2\ + for k l :: int + by (auto dest: odd_two_times_div_two_succ) + show \P k\ if stable: \\k. k div 2 = k \ P k\ + and rec: \\k b. P k \ (of_bool b + 2 * k) div 2 = k \ P (of_bool b + 2 * k)\ + for P and k :: int + proof (induction k rule: int_bit_induct) + case zero + from stable [of 0] show ?case + by simp + next + case minus + from stable [of \- 1\] show ?case + by simp + next + case (even k) + with rec [of k False] show ?case + by (simp add: ac_simps) + next + case (odd k) + with rec [of k True] show ?case + by (simp add: ac_simps) + qed +qed -subsection \Abstract bit operations\ - -context semiring_parity +class semiring_bit_shifts = semiring_bits + + fixes push_bit :: \nat \ 'a \ 'a\ + assumes push_bit_eq_mult: \push_bit n a = a * 2 ^ n\ + fixes drop_bit :: \nat \ 'a \ 'a\ + assumes drop_bit_eq_div: \drop_bit n a = a div 2 ^ n\ begin -text \The primary purpose of the following operations is - to avoid ad-hoc simplification of concrete expressions \<^term>\2 ^ n\\ +definition take_bit :: \nat \ 'a \ 'a\ + where take_bit_eq_mod: \take_bit n a = a mod 2 ^ n\ -definition push_bit :: "nat \ 'a \ 'a" - where push_bit_eq_mult: "push_bit n a = a * 2 ^ n" - -definition take_bit :: "nat \ 'a \ 'a" - where take_bit_eq_mod: "take_bit n a = a mod 2 ^ n" - -definition drop_bit :: "nat \ 'a \ 'a" - where drop_bit_eq_div: "drop_bit n a = a div 2 ^ n" +text \ + Logically, \<^const>\push_bit\, + \<^const>\drop_bit\ and \<^const>\take_bit\ are just aliases; having them + as separate operations makes proofs easier, otherwise proof automation + would fiddle with concrete expressions \<^term>\2 ^ n\ in a way obfuscating the basic + algebraic relationships between those operations. + Having + \<^const>\push_bit\ and \<^const>\drop_bit\ as definitional class operations + takes into account that specific instances of these can be implemented + differently wrt. code generation. +\ end -context unique_euclidean_semiring_with_nat +instantiation nat :: semiring_bit_shifts +begin + +definition push_bit_nat :: \nat \ nat \ nat\ + where \push_bit_nat n m = m * 2 ^ n\ + +definition drop_bit_nat :: \nat \ nat \ nat\ + where \drop_bit_nat n m = m div 2 ^ n\ + +instance proof + show \push_bit n m = m * 2 ^ n\ for n m :: nat + by (simp add: push_bit_nat_def) + show \drop_bit n m = m div 2 ^ n\ for n m :: nat + by (simp add: drop_bit_nat_def) +qed + +end + +instantiation int :: semiring_bit_shifts +begin + +definition push_bit_int :: \nat \ int \ int\ + where \push_bit_int n k = k * 2 ^ n\ + +definition drop_bit_int :: \nat \ int \ int\ + where \drop_bit_int n k = k div 2 ^ n\ + +instance proof + show \push_bit n k = k * 2 ^ n\ for n :: nat and k :: int + by (simp add: push_bit_int_def) + show \drop_bit n k = k div 2 ^ n\ for n :: nat and k :: int + by (simp add: drop_bit_int_def) +qed + +end + +class unique_euclidean_semiring_with_bit_shifts = + unique_euclidean_semiring_with_nat + semiring_bit_shifts begin lemma bit_ident: @@ -1081,6 +1189,10 @@ end +instance nat :: unique_euclidean_semiring_with_bit_shifts .. + +instance int :: unique_euclidean_semiring_with_bit_shifts .. + lemma push_bit_of_Suc_0 [simp]: "push_bit n (Suc 0) = 2 ^ n" using push_bit_of_1 [where ?'a = nat] by simp diff -r b7d481cdd54d -r a197532693a5 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Sat Nov 09 10:38:51 2019 +0000 +++ b/src/HOL/Set_Interval.thy Sat Nov 09 15:39:21 2019 +0000 @@ -2041,7 +2041,7 @@ by (subst sum_subtractf_nat) auto -context unique_euclidean_semiring_with_nat +context unique_euclidean_semiring_with_bit_shifts begin lemma take_bit_sum: diff -r b7d481cdd54d -r a197532693a5 src/HOL/String.thy --- a/src/HOL/String.thy Sat Nov 09 10:38:51 2019 +0000 +++ b/src/HOL/String.thy Sat Nov 09 15:39:21 2019 +0000 @@ -45,7 +45,7 @@ end -context unique_euclidean_semiring_with_nat +context unique_euclidean_semiring_with_bit_shifts begin definition char_of :: "'a \ char" diff -r b7d481cdd54d -r a197532693a5 src/HOL/ex/Bit_Lists.thy --- a/src/HOL/ex/Bit_Lists.thy Sat Nov 09 10:38:51 2019 +0000 +++ b/src/HOL/ex/Bit_Lists.thy Sat Nov 09 15:39:21 2019 +0000 @@ -26,7 +26,7 @@ end -context unique_euclidean_semiring_with_nat +context unique_euclidean_semiring_with_bit_shifts begin lemma unsigned_of_bits_append [simp]: @@ -285,7 +285,7 @@ of_bits bs OR of_bits cs = of_bits (map2 (\) bs cs)" and xor_eq: "length bs = length cs \ of_bits bs XOR of_bits cs = of_bits (map2 (\) bs cs)" - and shift_bit_eq: "shift_bit n a = of_bits (replicate n False @ bits_of a)" + and push_bit_eq: "push_bit n a = of_bits (replicate n False @ bits_of a)" and drop_bit_eq: "n < length (bits_of a) \ drop_bit n a = of_bits (drop n (bits_of a))" class ring_bit_representation = ring_bit_operations + semiring_bit_representation + @@ -314,7 +314,7 @@ instance nat :: semiring_bit_representation apply standard apply (simp_all only: and_nat.of_bits or_nat.of_bits xor_nat.of_bits) - apply (simp_all add: drop_bit_eq_div Parity.drop_bit_eq_div shift_bit_eq_mult push_bit_eq_mult) + apply simp_all done context zip_int @@ -359,10 +359,9 @@ show "(of_bits \ map Not \ bits_of) k = NOT k" by (induction k rule: int_bit_induct) (simp_all add: not_int_def) qed - show "shift_bit n k = of_bits (replicate n False @ bits_of k)" + show "push_bit n k = of_bits (replicate n False @ bits_of k)" for k :: int and n :: nat - by (cases "n = 0") (simp_all add: shift_bit_eq_push_bit) -qed (simp_all add: and_int.of_bits or_int.of_bits xor_int.of_bits - drop_bit_eq_drop_bit) + by (cases "n = 0") simp_all +qed (simp_all add: and_int.of_bits or_int.of_bits xor_int.of_bits) end diff -r b7d481cdd54d -r a197532693a5 src/HOL/ex/Bit_Operations.thy --- a/src/HOL/ex/Bit_Operations.thy Sat Nov 09 10:38:51 2019 +0000 +++ b/src/HOL/ex/Bit_Operations.thy Sat Nov 09 15:39:21 2019 +0000 @@ -9,248 +9,6 @@ Word begin -hide_const (open) drop_bit take_bit - -subsection \Algebraic structures with bits\ - -class semiring_bits = semiring_parity + - assumes bit_split_eq: \\a. of_bool (odd a) + 2 * (a div 2) = a\ - and bit_eq_rec: \\a b. a = b \ (even a = even b) \ a div 2 = b div 2\ - and bit_induct [case_names stable rec]: - \(\a. a div 2 = a \ P a) - \ (\a b. P a \ (of_bool b + 2 * a) div 2 = a \ P (of_bool b + 2 * a)) - \ P a\ - - -subsubsection \Instance \<^typ>\nat\\ - -instance nat :: semiring_bits -proof - show \of_bool (odd n) + 2 * (n div 2) = n\ - for n :: nat - by simp - show \m = n \ (even m \ even n) \ m div 2 = n div 2\ - for m n :: nat - by (auto dest: odd_two_times_div_two_succ) - show \P n\ if stable: \\n. n div 2 = n \ P n\ - and rec: \\n b. P n \ (of_bool b + 2 * n) div 2 = n \ P (of_bool b + 2 * n)\ - for P and n :: nat - proof (induction n rule: nat_bit_induct) - case zero - from stable [of 0] show ?case - by simp - next - case (even n) - with rec [of n False] show ?case - by simp - next - case (odd n) - with rec [of n True] show ?case - by simp - qed -qed - - -subsubsection \Instance \<^typ>\int\\ - -instance int :: semiring_bits -proof - show \of_bool (odd k) + 2 * (k div 2) = k\ - for k :: int - by (auto elim: oddE) - show \k = l \ (even k \ even l) \ k div 2 = l div 2\ - for k l :: int - by (auto dest: odd_two_times_div_two_succ) - show \P k\ if stable: \\k. k div 2 = k \ P k\ - and rec: \\k b. P k \ (of_bool b + 2 * k) div 2 = k \ P (of_bool b + 2 * k)\ - for P and k :: int - proof (induction k rule: int_bit_induct) - case zero - from stable [of 0] show ?case - by simp - next - case minus - from stable [of \- 1\] show ?case - by simp - next - case (even k) - with rec [of k False] show ?case - by (simp add: ac_simps) - next - case (odd k) - with rec [of k True] show ?case - by (simp add: ac_simps) - qed -qed - - -subsubsection \Instance \<^typ>\'a word\\ - -instance word :: (len) semiring_bits -proof - show \of_bool (odd a) + 2 * (a div 2) = a\ - for a :: \'a word\ - apply (cases \even a\; simp, transfer; cases rule: length_cases [where ?'a = 'a]) - apply auto - apply (auto simp add: take_bit_eq_mod) - apply (metis add.commute even_take_bit_eq len_not_eq_0 mod_mod_trivial odd_two_times_div_two_succ take_bit_eq_mod) - done - show \a = b \ (even a \ even b) \ a div 2 = b div 2\ - for a b :: \'a word\ - apply transfer - apply (cases rule: length_cases [where ?'a = 'a]) - apply auto - apply (metis even_take_bit_eq len_not_eq_0) - apply (metis even_take_bit_eq len_not_eq_0) - apply (metis (no_types, hide_lams) diff_add_cancel dvd_div_mult_self even_take_bit_eq mult_2_right take_bit_add take_bit_minus) - apply (metis bit_ident drop_bit_eq_div drop_bit_half even_take_bit_eq even_two_times_div_two mod_div_trivial odd_two_times_div_two_succ take_bit_eq_mod) - done - show \P a\ if stable: \\a. a div 2 = a \ P a\ - and rec: \\a b. P a \ (of_bool b + 2 * a) div 2 = a \ P (of_bool b + 2 * a)\ - for P and a :: \'a word\ - proof (induction a rule: word_bit_induct) - case zero - from stable [of 0] show ?case - by simp - next - case (even a) - with rec [of a False] show ?case - using bit_word_half_eq [of a False] by (simp add: ac_simps) - next - case (odd a) - with rec [of a True] show ?case - using bit_word_half_eq [of a True] by (simp add: ac_simps) - qed -qed - - -subsection \Bit shifts in suitable algebraic structures\ - -class semiring_bit_shifts = semiring_bits + - fixes shift_bit :: \nat \ 'a \ 'a\ - assumes shift_bit_eq_mult: \shift_bit n a = a * 2 ^ n\ - fixes drop_bit :: \nat \ 'a \ 'a\ - assumes drop_bit_eq_div: \drop_bit n a = a div 2 ^ n\ -begin - -definition take_bit :: \nat \ 'a \ 'a\ - where take_bit_eq_mod: \take_bit n a = a mod 2 ^ n\ - -text \ - Logically, \<^const>\shift_bit\, - \<^const>\drop_bit\ and \<^const>\take_bit\ are just aliases; having them - as separate operations makes proofs easier, otherwise proof automation - would fiddle with concrete expressions \<^term>\2 ^ n\ in a way obfuscating the basic - algebraic relationships between those operations; having - \<^const>\push_bit\ and \<^const>\drop_bit\ as definitional class operations - takes into account that specific instances of these can be implemented - differently wrt. code generation. -\ - -end - -subsubsection \Instance \<^typ>\nat\\ - -instantiation nat :: semiring_bit_shifts -begin - -definition shift_bit_nat :: \nat \ nat \ nat\ - where \shift_bit_nat n m = m * 2 ^ n\ - -definition drop_bit_nat :: \nat \ nat \ nat\ - where \drop_bit_nat n m = m div 2 ^ n\ - -instance proof - show \shift_bit n m = m * 2 ^ n\ for n m :: nat - by (simp add: shift_bit_nat_def) - show \drop_bit n m = m div 2 ^ n\ for n m :: nat - by (simp add: drop_bit_nat_def) -qed - -end - - -subsubsection \Instance \<^typ>\int\\ - -instantiation int :: semiring_bit_shifts -begin - -definition shift_bit_int :: \nat \ int \ int\ - where \shift_bit_int n k = k * 2 ^ n\ - -definition drop_bit_int :: \nat \ int \ int\ - where \drop_bit_int n k = k div 2 ^ n\ - -instance proof - show \shift_bit n k = k * 2 ^ n\ for n :: nat and k :: int - by (simp add: shift_bit_int_def) - show \drop_bit n k = k div 2 ^ n\ for n :: nat and k :: int - by (simp add: drop_bit_int_def) -qed - -end - -lemma shift_bit_eq_push_bit: - \shift_bit = (push_bit :: nat \