--- a/src/HOL/Code_Numeral.thy Wed Nov 27 16:54:33 2019 +0000
+++ b/src/HOL/Code_Numeral.thy Sun Dec 01 08:00:59 2019 +0000
@@ -299,7 +299,7 @@
instance by (standard; transfer)
(fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
- div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
+ exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
end
@@ -995,7 +995,7 @@
instance by (standard; transfer)
(fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
- div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
+ exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
end
--- a/src/HOL/Parity.thy Wed Nov 27 16:54:33 2019 +0000
+++ b/src/HOL/Parity.thy Sun Dec 01 08:00:59 2019 +0000
@@ -577,6 +577,7 @@
and bits_div_by_1 [simp]: \<open>a div 1 = a\<close>
and bit_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close>
and even_succ_div_2 [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
+ and exp_div_exp_eq: \<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close>
and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
and mod_exp_eq: \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
and mult_exp_mod_exp_eq: \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close>
@@ -750,6 +751,10 @@
apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq)
done
+lemma bit_exp_iff:
+ \<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close>
+ by (auto simp add: bit_def exp_div_exp_eq)
+
end
lemma nat_bit_induct [case_names zero even odd]:
@@ -810,7 +815,7 @@
apply (auto simp add: mod_mod_cancel div_mult2_eq power_add mod_mult2_eq le_iff_add split: split_min_lin)
apply (simp add: mult.commute)
done
-qed (auto simp add: div_mult2_eq mod_mult2_eq power_add)
+qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff)
lemma int_bit_induct [case_names zero minus even odd]:
"P k" if zero_int: "P 0"
@@ -891,6 +896,24 @@
with rec [of k True] show ?case
by (simp add: ac_simps)
qed
+ show \<open>(2::int) ^ m div 2 ^ n = of_bool ((2::int) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
+ for m n :: nat
+ proof (cases \<open>m < n\<close>)
+ case True
+ then have \<open>n = m + (n - m)\<close>
+ by simp
+ then have \<open>(2::int) ^ m div 2 ^ n = (2::int) ^ m div 2 ^ (m + (n - m))\<close>
+ by simp
+ also have \<open>\<dots> = (2::int) ^ m div (2 ^ m * 2 ^ (n - m))\<close>
+ by (simp add: power_add)
+ also have \<open>\<dots> = (2::int) ^ m div 2 ^ m div 2 ^ (n - m)\<close>
+ by (simp add: zdiv_zmult2_eq)
+ finally show ?thesis using \<open>m < n\<close> by simp
+ next
+ case False
+ then show ?thesis
+ by (simp add: power_diff)
+ qed
show \<open>k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n\<close>
for m n :: nat and k :: int
using mod_exp_eq [of \<open>nat k\<close> m n]
@@ -905,7 +928,7 @@
apply (auto simp add: power_add zmod_zmult2_eq le_iff_add split: split_min_lin)
apply (simp add: ac_simps)
done
-qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add)
+qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le)
class semiring_bit_shifts = semiring_bits +
fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
--- a/src/HOL/Transfer.thy Wed Nov 27 16:54:33 2019 +0000
+++ b/src/HOL/Transfer.thy Sun Dec 01 08:00:59 2019 +0000
@@ -642,13 +642,25 @@
end
-subsection \<open>\<^const>\<open>of_nat\<close>\<close>
+subsection \<open>\<^const>\<open>of_bool\<close> and \<^const>\<open>of_nat\<close>\<close>
+
+context
+ includes lifting_syntax
+begin
+
+lemma transfer_rule_of_bool:
+ \<open>((\<longleftrightarrow>) ===> (\<cong>)) of_bool of_bool\<close>
+ if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
+ for R :: \<open>'a::zero_neq_one \<Rightarrow> 'b::zero_neq_one \<Rightarrow> bool\<close> (infix \<open>\<cong>\<close> 50)
+ by (unfold of_bool_def [abs_def]) transfer_prover
lemma transfer_rule_of_nat:
- fixes R :: "'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool"
- assumes [transfer_rule]: "R 0 0" "R 1 1"
- "rel_fun R (rel_fun R R) plus plus"
- shows "rel_fun HOL.eq R of_nat of_nat"
+ "((=) ===> (\<cong>)) of_nat of_nat"
+ if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
+ \<open>((\<cong>) ===> (\<cong>) ===> (\<cong>)) (+) (+)\<close>
+ for R :: \<open>'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool\<close> (infix \<open>\<cong>\<close> 50)
by (unfold of_nat_def [abs_def]) transfer_prover
end
+
+end
--- a/src/HOL/ex/Word.thy Wed Nov 27 16:54:33 2019 +0000
+++ b/src/HOL/ex/Word.thy Sun Dec 01 08:00:59 2019 +0000
@@ -161,12 +161,18 @@
context
includes lifting_syntax
- notes transfer_rule_numeral [transfer_rule]
+ notes
+ transfer_rule_of_bool [transfer_rule]
+ transfer_rule_numeral [transfer_rule]
transfer_rule_of_nat [transfer_rule]
transfer_rule_of_int [transfer_rule]
begin
lemma [transfer_rule]:
+ "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) of_bool of_bool"
+ by transfer_prover
+
+lemma [transfer_rule]:
"((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral"
by transfer_prover
@@ -612,6 +618,9 @@
if \<open>even a\<close>
for a :: \<open>'a word\<close>
using that by transfer (auto dest: le_Suc_ex)
+ show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
+ for m n :: nat
+ by transfer (simp, simp add: exp_div_exp_eq)
show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)"
for a :: "'a word" and m n :: nat
apply transfer