# HG changeset patch
# User Wenda Li <wl302@cam.ac.uk>
# Date 1575227755 0
# Node ID 8a0e25d93a95930f5f364aee442c9b87a249ec0a
# Parent  d62fdaafdafcc6d141b814175a33627496d45ca9# Parent  eda1ef0090ef95b16c30c870313ef816fe90ad88
merged

diff -r d62fdaafdafc -r 8a0e25d93a95 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Dec 01 19:10:57 2019 +0000
+++ b/src/HOL/Code_Numeral.thy	Sun Dec 01 19:15:55 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
 
diff -r d62fdaafdafc -r 8a0e25d93a95 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Dec 01 19:10:57 2019 +0000
+++ b/src/HOL/Parity.thy	Sun Dec 01 19:15:55 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>
diff -r d62fdaafdafc -r 8a0e25d93a95 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Sun Dec 01 19:10:57 2019 +0000
+++ b/src/HOL/Transfer.thy	Sun Dec 01 19:15:55 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
diff -r d62fdaafdafc -r 8a0e25d93a95 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Sun Dec 01 19:10:57 2019 +0000
+++ b/src/HOL/ex/Word.thy	Sun Dec 01 19:15:55 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
@@ -637,6 +646,23 @@
     done
 qed
 
+context
+  includes lifting_syntax
+begin
+
+lemma transfer_rule_bit_word:
+  \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) ===> (=)) (\<lambda>k n. n < LENGTH('a) \<and> bit k n) bit\<close>
+proof -
+  let ?t = \<open>\<lambda>a n. odd (take_bit LENGTH('a) a div take_bit LENGTH('a) ((2::int) ^ n))\<close>
+  have \<open>((pcr_word :: int \<Rightarrow> 'a word \<Rightarrow> bool) ===> (=)) ?t bit\<close>
+    by (unfold bit_def) transfer_prover
+  also have \<open>?t = (\<lambda>k n. n < LENGTH('a) \<and> bit k n)\<close>
+    by (simp add: fun_eq_iff bit_take_bit_iff flip: bit_def)
+  finally show ?thesis .
+qed
+
+end
+
 instantiation word :: (len) semiring_bit_shifts
 begin