# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1575279111 -3600
# Node ID 6695aeae8ec99ca36776a4b1b4ea3ba56c2f028b
# Parent  8b8f9d3b3facda7c8e92fc649c869f7b5bcd879e# Parent  0c47c128f9af68c7a6ea51f208fc0f946a5ef28a
Merged

diff -r 8b8f9d3b3fac -r 6695aeae8ec9 src/HOL/Analysis/Analysis.thy
diff -r 8b8f9d3b3fac -r 6695aeae8ec9 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Dec 02 10:31:51 2019 +0100
@@ -4053,4 +4053,6 @@
   apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
   done
 
+
+
 end
diff -r 8b8f9d3b3fac -r 6695aeae8ec9 src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy	Mon Dec 02 10:31:51 2019 +0100
@@ -2184,7 +2184,6 @@
   qed
 qed
 
-
 corollary covering_space_lift_stronger:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     and f :: "'c::real_normed_vector \<Rightarrow> 'b"
@@ -2252,4 +2251,36 @@
     by (metis that covering_space_lift_strong [OF cov _ \<open>z \<in> U\<close> U contf fim])
 qed
 
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Homeomorphisms of arc images\<close>
+
+lemma homeomorphism_arc:
+  fixes g :: "real \<Rightarrow> 'a::t2_space"
+  assumes "arc g"
+  obtains h where "homeomorphism {0..1} (path_image g) g h"
+using assms by (force simp: arc_def homeomorphism_compact path_def path_image_def)
+
+lemma homeomorphic_arc_image_interval:
+  fixes g :: "real \<Rightarrow> 'a::t2_space" and a::real
+  assumes "arc g" "a < b"
+  shows "(path_image g) homeomorphic {a..b}"
+proof -
+  have "(path_image g) homeomorphic {0..1::real}"
+    by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc)
+  also have "\<dots> homeomorphic {a..b}"
+    using assms by (force intro: homeomorphic_closed_intervals_real)
+  finally show ?thesis .
+qed
+
+lemma homeomorphic_arc_images:
+  fixes g :: "real \<Rightarrow> 'a::t2_space" and h :: "real \<Rightarrow> 'b::t2_space"
+  assumes "arc g" "arc h"
+  shows "(path_image g) homeomorphic (path_image h)"
+proof -
+  have "(path_image g) homeomorphic {0..1::real}"
+    by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc)
+  also have "\<dots> homeomorphic (path_image h)"
+    by (meson assms homeomorphic_def homeomorphism_arc)
+  finally show ?thesis .
+qed
+
 end
diff -r 8b8f9d3b3fac -r 6695aeae8ec9 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Mon Dec 02 10:31:51 2019 +0100
@@ -4055,7 +4055,6 @@
   shows "\<exists>g. homeomorphism S T f g"
   using assms injective_into_1d_eq_homeomorphism by blast
 
-
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Rectangular paths\<close>
 
 definition\<^marker>\<open>tag unimportant\<close> rectpath where
diff -r 8b8f9d3b3fac -r 6695aeae8ec9 src/HOL/Analysis/Retracts.thy
--- a/src/HOL/Analysis/Retracts.thy	Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Analysis/Retracts.thy	Mon Dec 02 10:31:51 2019 +0100
@@ -2591,4 +2591,51 @@
   shows "connected(-S)"
   using assms path_connected_complement_homeomorphic_interval path_connected_imp_connected by blast
 
+
+lemma path_connected_arc_complement:
+  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "arc \<gamma>" "2 \<le> DIM('a)"
+  shows "path_connected(- path_image \<gamma>)"
+proof -
+  have "path_image \<gamma> homeomorphic {0..1::real}"
+    by (simp add: assms homeomorphic_arc_image_interval)
+  then
+  show ?thesis
+    apply (rule path_connected_complement_homeomorphic_convex_compact)
+      apply (auto simp: assms)
+    done
+qed
+
+lemma connected_arc_complement:
+  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "arc \<gamma>" "2 \<le> DIM('a)"
+  shows "connected(- path_image \<gamma>)"
+  by (simp add: assms path_connected_arc_complement path_connected_imp_connected)
+
+lemma inside_arc_empty:
+  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "arc \<gamma>"
+    shows "inside(path_image \<gamma>) = {}"
+proof (cases "DIM('a) = 1")
+  case True
+  then show ?thesis
+    using assms connected_arc_image connected_convex_1_gen inside_convex by blast
+next
+  case False
+  show ?thesis
+  proof (rule inside_bounded_complement_connected_empty)
+    show "connected (- path_image \<gamma>)"
+      apply (rule connected_arc_complement [OF assms])
+      using False
+      by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq order_class.order.antisym)
+    show "bounded (path_image \<gamma>)"
+      by (simp add: assms bounded_arc_image)
+  qed
+qed
+
+lemma inside_simple_curve_imp_closed:
+  fixes \<gamma> :: "real \<Rightarrow> 'a::euclidean_space"
+    shows "\<lbrakk>simple_path \<gamma>; x \<in> inside(path_image \<gamma>)\<rbrakk> \<Longrightarrow> pathfinish \<gamma> = pathstart \<gamma>"
+  using arc_simple_path  inside_arc_empty by blast
+
 end
diff -r 8b8f9d3b3fac -r 6695aeae8ec9 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Code_Numeral.thy	Mon Dec 02 10:31:51 2019 +0100
@@ -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 8b8f9d3b3fac -r 6695aeae8ec9 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Parity.thy	Mon Dec 02 10:31:51 2019 +0100
@@ -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 8b8f9d3b3fac -r 6695aeae8ec9 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/Transfer.thy	Mon Dec 02 10:31:51 2019 +0100
@@ -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 8b8f9d3b3fac -r 6695aeae8ec9 src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/ex/Bit_Operations.thy	Mon Dec 02 10:31:51 2019 +0100
@@ -9,12 +9,39 @@
     Main
 begin
 
+lemma minus_1_div_exp_eq_int [simp]:
+  \<open>- 1 div (2 :: int) ^ n = - 1\<close>
+  for n :: nat
+  by (induction n) (use div_exp_eq [symmetric, of \<open>- 1 :: int\<close> 1] in \<open>simp_all add: ac_simps\<close>)
+
+context semiring_bits
+begin
+
+lemma bits_div_by_0 [simp]:
+  \<open>a div 0 = 0\<close>
+  by (metis local.add_cancel_right_right local.bit_mod_div_trivial local.mod_mult_div_eq local.mult_not_zero)
+
+lemma bit_0_eq [simp]:
+  \<open>bit 0 = bot\<close>
+  by (simp add: fun_eq_iff bit_def)
+
+end
+
+context semiring_bit_shifts
+begin
+
+end
+
+
 subsection \<open>Bit operations in suitable algebraic structures\<close>
 
 class semiring_bit_operations = semiring_bit_shifts +
-  fixes "and" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "AND" 64)
-    and or :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "OR"  59)
-    and xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "XOR" 59)
+  fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "AND" 64)
+    and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "OR"  59)
+    and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "XOR" 59)
+  assumes bit_and_iff: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
+    and bit_or_iff: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+    and bit_xor_iff: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
 begin
 
 text \<open>
@@ -40,7 +67,7 @@
 
 text \<open>
   Having 
-  <^const>\<open>set_bit\<close>, \<^const>\<open>unset_bit\<close> and \<^const>\<open>flip_bit\<close> as separate
+  \<^const>\<open>set_bit\<close>, \<^const>\<open>unset_bit\<close> and \<^const>\<open>flip_bit\<close> as separate
   operations allows to implement them using bit masks later.
 \<close>
 
@@ -85,19 +112,38 @@
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
   fixes not :: \<open>'a \<Rightarrow> 'a\<close>  (\<open>NOT\<close>)
-  assumes boolean_algebra: \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
-    and boolean_algebra_xor_eq: \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
+  assumes bits_even_minus_1_div_exp_iff [simp]: \<open>even (- 1 div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0\<close>
+  assumes bit_not_iff: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
 begin
 
+lemma bits_minus_1_mod_2_eq [simp]:
+  \<open>(- 1) mod 2 = 1\<close>
+  by (simp add: mod_2_eq_odd)
+
+lemma bit_minus_1_iff [simp]:
+  \<open>bit (- 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close>
+  by (simp add: bit_def)
+
 sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
   rewrites \<open>bit.xor = (XOR)\<close>
 proof -
   interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
-    by (fact boolean_algebra)
+    apply standard
+             apply (auto simp add: bit_eq_iff bit_and_iff bit_or_iff bit_not_iff)
+     apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+    apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+    done
   show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
     by standard
-  show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>  
-    by (fact boolean_algebra_xor_eq)
+  show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close> 
+    apply (auto simp add: fun_eq_iff bit.xor_def bit_eq_iff bit_and_iff bit_or_iff bit_not_iff bit_xor_iff)
+         apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+        apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+       apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+      apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+     apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+    apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0)
+    done
 qed
 
 text \<open>
@@ -265,7 +311,39 @@
   "n XOR 0 = n" for n :: nat
   by simp
 
-instance ..
+instance proof
+  fix m n q :: nat
+  show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
+  proof (rule sym, induction q arbitrary: m n)
+    case 0
+    then show ?case
+      by (simp add: and_nat.even_iff)
+  next
+    case (Suc q)
+    with and_nat.rec [of m n] show ?case
+      by simp
+  qed
+  show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
+  proof (rule sym, induction q arbitrary: m n)
+    case 0
+    then show ?case
+      by (simp add: or_nat.even_iff)
+  next
+    case (Suc q)
+    with or_nat.rec [of m n] show ?case
+      by simp
+  qed
+  show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
+  proof (rule sym, induction q arbitrary: m n)
+    case 0
+    then show ?case
+      by (simp add: xor_nat.even_iff)
+  next
+    case (Suc q)
+    with xor_nat.rec [of m n] show ?case
+      by simp
+  qed
+qed
 
 end
 
@@ -625,89 +703,49 @@
 
 lemma even_not_iff [simp]:
   "even (NOT k) \<longleftrightarrow> odd k"
-  for k :: int
+    for k :: int
   by (simp add: not_int_def)
 
+lemma bit_not_iff_int:
+  \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
+    for k :: int
+    by (induction n arbitrary: k)
+      (simp_all add: not_int_def flip: complement_div_2)
+
+
 instance proof
-  interpret bit_int: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: int"
-  proof
-    show "k AND (l OR r) = k AND l OR k AND r"
-      for k l r :: int
-    proof (induction k arbitrary: l r rule: int_bit_induct)
-      case zero
-      show ?case
-        by simp
-    next
-      case minus
-      show ?case
-        by simp
-    next
-      case (even k)
-      then show ?case by (simp add: and_int.rec [of "k * 2"]
-        or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of l])
-    next
-      case (odd k)
-      then show ?case by (simp add: and_int.rec [of "1 + k * 2"]
-        or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of "1 + (k AND l div 2) * 2"] or_int.rec [of l])
-    qed
-    show "k OR l AND r = (k OR l) AND (k OR r)"
-      for k l r :: int
-    proof (induction k arbitrary: l r rule: int_bit_induct)
-      case zero
-      then show ?case
-        by simp
-    next
-      case minus
-      then show ?case
-        by simp
-    next
-      case (even k)
-      then show ?case by (simp add: or_int.rec [of "k * 2"]
-        and_int.rec [of "(k OR l div 2) * 2"] and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l])
-    next
-      case (odd k)
-      then show ?case by (simp add: or_int.rec [of "1 + k * 2"]
-        and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l])
-    qed
-    show "k AND NOT k = 0" for k :: int
-      by (induction k rule: int_bit_induct)
-        (simp_all add: not_int_def complement_half minus_diff_commute [of 1])
-    show "k OR NOT k = - 1" for k :: int
-      by (induction k rule: int_bit_induct)
-        (simp_all add: not_int_def complement_half minus_diff_commute [of 1])
-  qed (simp_all add: and_int.assoc or_int.assoc,
-    simp_all add: and_int.commute or_int.commute)
-  show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: int)"
-    by (fact bit_int.boolean_algebra_axioms)
-  show "bit_int.xor = ((XOR) :: int \<Rightarrow> _)"
-  proof (rule ext)+
-    fix k l :: int
-    have "k XOR l = k AND NOT l OR NOT k AND l"
-    proof (induction k arbitrary: l rule: int_bit_induct)
-      case zero
-      show ?case
-        by simp
-    next
-      case minus
-      show ?case
-        by (simp add: not_int_def)
-    next
-      case (even k)
-      then show ?case
-        by (simp add: xor_int.rec [of "k * 2"] and_int.rec [of "k * 2"]
-          or_int.rec [of _ "1 + 2 * NOT k AND l"] not_div_2)
-          (simp add: and_int.rec [of _ l])
-    next
-      case (odd k)
-      then show ?case
-        by (simp add: xor_int.rec [of "1 + k * 2"] and_int.rec [of "1 + k * 2"]
-          or_int.rec [of _ "2 * NOT k AND l"] not_div_2)
-          (simp add: and_int.rec [of _ l])
-    qed
-    then show "bit_int.xor k l = k XOR l"
-      by (simp add: bit_int.xor_def)
+  fix k l :: int and n :: nat
+  show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
+  proof (rule sym, induction n arbitrary: k l)
+    case 0
+    then show ?case
+      by (simp add: and_int.even_iff)
+  next
+    case (Suc n)
+    with and_int.rec [of k l] show ?case
+      by simp
   qed
-qed
+  show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
+  proof (rule sym, induction n arbitrary: k l)
+    case 0
+    then show ?case
+      by (simp add: or_int.even_iff)
+  next
+    case (Suc n)
+    with or_int.rec [of k l] show ?case
+      by simp
+  qed
+  show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
+  proof (rule sym, induction n arbitrary: k l)
+    case 0
+    then show ?case
+      by (simp add: xor_int.even_iff)
+  next
+    case (Suc n)
+    with xor_int.rec [of k l] show ?case
+      by simp
+  qed
+qed (simp_all add: bit_not_iff_int)
 
 end
 
@@ -743,36 +781,21 @@
 lemma take_bit_not_iff:
   "Parity.take_bit n (NOT k) = Parity.take_bit n (NOT l) \<longleftrightarrow> Parity.take_bit n k = Parity.take_bit n l"
   for k l :: int
-  by (simp add: not_int_def take_bit_complement_iff)
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff_int)
 
 lemma take_bit_and [simp]:
   "Parity.take_bit n (k AND l) = Parity.take_bit n k AND Parity.take_bit n l"
   for k l :: int
-  apply (induction n arbitrary: k l)
-   apply simp
-  apply (subst and_int.rec)
-  apply (subst (2) and_int.rec)
-  apply simp
-  done
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff)
 
 lemma take_bit_or [simp]:
   "Parity.take_bit n (k OR l) = Parity.take_bit n k OR Parity.take_bit n l"
   for k l :: int
-  apply (induction n arbitrary: k l)
-   apply simp
-  apply (subst or_int.rec)
-  apply (subst (2) or_int.rec)
-  apply simp
-  done
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_or_iff)
 
 lemma take_bit_xor [simp]:
   "Parity.take_bit n (k XOR l) = Parity.take_bit n k XOR Parity.take_bit n l"
   for k l :: int
-  apply (induction n arbitrary: k l)
-   apply simp
-  apply (subst xor_int.rec)
-  apply (subst (2) xor_int.rec)
-  apply simp
-  done
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
 
 end
diff -r 8b8f9d3b3fac -r 6695aeae8ec9 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Sun Dec 01 11:51:17 2019 +0100
+++ b/src/HOL/ex/Word.thy	Mon Dec 02 10:31:51 2019 +0100
@@ -10,6 +10,19 @@
     "HOL-ex.Bit_Operations"
 begin
 
+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
+
+end
+
+
 subsection \<open>Preliminaries\<close>
 
 lemma length_not_greater_eq_2_iff [simp]:
@@ -161,12 +174,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
 
@@ -324,6 +343,10 @@
   \<open>a div 0 = 0\<close> for a :: \<open>'a::len0 word\<close>
   by transfer simp
 
+(*lemma
+  \<open>a div a = of_bool (a \<noteq> 0)\<close> for a :: \<open>'a::len word\<close>
+  by transfer  simp*)
+
 context
   includes lifting_syntax
 begin
@@ -389,6 +412,11 @@
     by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd)
 qed
 
+(*lemma
+  \<open>2 ^ n = (0 :: 'a word) \<longleftrightarrow> LENGTH('a::len) \<le> n\<close>
+  apply transfer*)
+  
+
 
 subsubsection \<open>Orderings\<close>
 
@@ -612,6 +640,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 +668,23 @@
     done
 qed
 
+context
+  includes lifting_syntax
+begin
+
+lemma transfer_rule_bit_word [transfer_rule]:
+  \<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
 
@@ -702,25 +750,18 @@
   by simp
 
 instance proof
-  interpret bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a word"
-  proof
-    show "a AND (b OR c) = a AND b OR a AND c"
-      for a b c :: "'a word"
-      by transfer (simp add: bit.conj_disj_distrib)
-    show "a OR b AND c = (a OR b) AND (a OR c)"
-      for a b c :: "'a word"
-      by transfer (simp add: bit.disj_conj_distrib)
-  qed (transfer; simp add: ac_simps)+
-  show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: 'a word)"
-    by (fact bit_word.boolean_algebra_axioms)
-  show "bit_word.xor = ((XOR) :: 'a word \<Rightarrow> _)"
-  proof (rule ext)+
-    fix a b :: "'a word"
-    have "a XOR b = a AND NOT b OR NOT a AND b"
-      by transfer (simp add: bit.xor_def)
-    then show "bit_word.xor a b = a XOR b"
-      by (simp add: bit_word.xor_def)
-  qed
+  fix a b :: \<open>'a word\<close> and n :: nat
+  show \<open>even (- 1 div (2 :: 'a word) ^ n) \<longleftrightarrow> (2 :: 'a word) ^ n = 0\<close>
+    by transfer
+      (simp flip: drop_bit_eq_div add: drop_bit_take_bit, simp add: drop_bit_eq_div)
+  show \<open>bit (NOT a) n \<longleftrightarrow> (2 :: 'a word) ^ n \<noteq> 0 \<and> \<not> bit a n\<close>
+    by transfer (simp add: bit_not_iff)
+  show \<open>bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
+    by transfer (auto simp add: bit_and_iff)
+  show \<open>bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
+    by transfer (auto simp add: bit_or_iff)
+  show \<open>bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
+    by transfer (auto simp add: bit_xor_iff)
 qed
 
 end