# HG changeset patch
# User haftmann
# Date 1575306916 0
# Node ID d50a718ccf35422cd4981fde96f5452a09da4a52
# Parent  26b35a97bddb902bb06cdebb75705eda32cf2569
tuned material

diff -r 26b35a97bddb -r d50a718ccf35 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Mon Dec 02 18:29:22 2019 +0100
+++ b/src/HOL/Code_Numeral.thy	Mon Dec 02 17:15:16 2019 +0000
@@ -297,8 +297,8 @@
   is \<open>drop_bit\<close> .
 
 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
+  (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
+    bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
 
 end
@@ -993,8 +993,8 @@
   is \<open>drop_bit\<close> .
 
 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
+  (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
+    bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+
 
 end
diff -r 26b35a97bddb -r d50a718ccf35 src/HOL/Library/Type_Length.thy
--- a/src/HOL/Library/Type_Length.thy	Mon Dec 02 18:29:22 2019 +0100
+++ b/src/HOL/Library/Type_Length.thy	Mon Dec 02 17:15:16 2019 +0000
@@ -103,4 +103,8 @@
 
 end
 
+lemma length_not_greater_eq_2_iff [simp]:
+  \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close>
+  by (auto simp add: not_le dest: less_2_cases)
+
 end
diff -r 26b35a97bddb -r d50a718ccf35 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Mon Dec 02 18:29:22 2019 +0100
+++ b/src/HOL/Parity.thy	Mon Dec 02 17:15:16 2019 +0000
@@ -569,13 +569,13 @@
 subsection \<open>Abstract bit structures\<close>
 
 class semiring_bits = semiring_parity +
-  assumes bit_induct [case_names stable rec]:
+  assumes bits_induct [case_names stable rec]:
     \<open>(\<And>a. a div 2 = a \<Longrightarrow> P a)
      \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a))
         \<Longrightarrow> P a\<close>
   assumes bits_div_0 [simp]: \<open>0 div a = 0\<close>
     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 bits_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>
@@ -584,6 +584,10 @@
     and div_exp_mod_exp_eq: \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
 begin
 
+lemma bits_div_by_0 [simp]:
+  \<open>a div 0 = 0\<close>
+  by (metis add_cancel_right_right bits_mod_div_trivial mod_mult_div_eq mult_not_zero)
+
 lemma bits_1_div_2 [simp]:
   \<open>1 div 2 = 0\<close>
   using even_succ_div_2 [of 0] by simp
@@ -629,7 +633,7 @@
   \<open>0 mod a = 0\<close>
   using div_mult_mod_eq [of 0 a] by simp
 
-lemma one_mod_two_eq_one [simp]:
+lemma bits_one_mod_two_eq_one [simp]:
   \<open>1 mod 2 = 1\<close>
   by (simp add: mod2_eq_if)
 
@@ -644,12 +648,16 @@
   \<open>bit a (Suc n) \<longleftrightarrow> bit (a div 2) n\<close>
   using div_exp_eq [of a 1 n] by (simp add: bit_def)
 
+lemma bit_0_eq [simp]:
+  \<open>bit 0 = bot\<close>
+  by (simp add: fun_eq_iff bit_def)
+
 context
   fixes a
   assumes stable: \<open>a div 2 = a\<close>
 begin
 
-lemma stable_imp_add_self:
+lemma bits_stable_imp_add_self:
   \<open>a + a mod 2 = 0\<close>
 proof -
   have \<open>a div 2 * 2 + a mod 2 = a\<close>
@@ -668,7 +676,7 @@
 
 lemma bit_iff_idd_imp_stable:
   \<open>a div 2 = a\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> odd a\<close>
-using that proof (induction a rule: bit_induct)
+using that proof (induction a rule: bits_induct)
   case (stable a)
   then show ?case
     by simp
@@ -693,7 +701,7 @@
 
 lemma bit_eqI:
   \<open>a = b\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> bit b n\<close>
-using that proof (induction a arbitrary: b rule: bit_induct)
+using that proof (induction a arbitrary: b rule: bits_induct)
   case (stable a)
   from stable(2) [of 0] have **: \<open>even b \<longleftrightarrow> even a\<close>
     by simp
@@ -714,7 +722,7 @@
   then have \<open>a + a mod 2 + b = b + b mod 2 + a\<close>
     by (simp add: ac_simps)
   with \<open>a div 2 = a\<close> \<open>b div 2 = b\<close> show ?case
-    by (simp add: stable_imp_add_self)
+    by (simp add: bits_stable_imp_add_self)
 next
   case (rec a p)
   from rec.prems [of 0] have [simp]: \<open>p = odd b\<close>
@@ -952,7 +960,7 @@
   differently wrt. code generation.
 \<close>
 
-lemma bit_ident:
+lemma bits_ident:
   "push_bit n (drop_bit n a) + take_bit n a = a"
   using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
 
@@ -1228,4 +1236,27 @@
   "push_bit n (- 1 :: int) = - (2 ^ n)"
   by (simp add: push_bit_eq_mult)
 
+lemma minus_1_div_exp_eq_int:
+  \<open>- 1 div (2 :: int) ^ n = - 1\<close>
+  by (induction n) (use div_exp_eq [symmetric, of \<open>- 1 :: int\<close> 1] in \<open>simp_all add: ac_simps\<close>)
+
+lemma drop_bit_minus_one [simp]:
+  \<open>drop_bit n (- 1 :: int) = - 1\<close>
+  by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int)
+
+lemma take_bit_uminus:
+  "take_bit n (- (take_bit n k)) = take_bit n (- k)"
+    for k :: int
+  by (simp add: take_bit_eq_mod mod_minus_eq)
+
+lemma take_bit_minus:
+  "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)"
+    for k l :: int
+  by (simp add: take_bit_eq_mod mod_diff_eq)
+
+lemma take_bit_nonnegative [simp]:
+  "take_bit n k \<ge> 0"
+    for k :: int
+  by (simp add: take_bit_eq_mod)
+
 end
diff -r 26b35a97bddb -r d50a718ccf35 src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Mon Dec 02 18:29:22 2019 +0100
+++ b/src/HOL/ex/Bit_Operations.thy	Mon Dec 02 17:15:16 2019 +0000
@@ -9,22 +9,9 @@
     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
@@ -50,7 +37,6 @@
   For the sake of code generation
   the operations \<^const>\<open>and\<close>, \<^const>\<open>or\<close> and \<^const>\<open>xor\<close>
   are specified as definitional class operations.
-
 \<close>
 
 definition map_bit :: \<open>nat \<Rightarrow> (bool \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a\<close>
@@ -712,7 +698,6 @@
     by (induction n arbitrary: k)
       (simp_all add: not_int_def flip: complement_div_2)
 
-
 instance proof
   fix k l :: int and n :: nat
   show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
@@ -745,7 +730,7 @@
     with xor_int.rec [of k l] show ?case
       by simp
   qed
-qed (simp_all add: bit_not_iff_int)
+qed (simp_all add: minus_1_div_exp_eq_int bit_not_iff_int)
 
 end
 
@@ -774,27 +759,32 @@
   using one_xor_int_eq [of k] by (simp add: ac_simps)
 
 lemma take_bit_complement_iff:
-  "Parity.take_bit n (complement k) = Parity.take_bit n (complement l) \<longleftrightarrow> Parity.take_bit n k = Parity.take_bit n l"
+  "take_bit n (complement k) = take_bit n (complement l) \<longleftrightarrow> take_bit n k = take_bit n l"
   for k l :: int
-  by (simp add: Parity.take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute)
+  by (simp add: take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute)
 
 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"
+  "take_bit n (NOT k) = take_bit n (NOT l) \<longleftrightarrow> take_bit n k = take_bit n l"
   for k l :: int
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff_int)
 
+lemma take_bit_not_take_bit:
+  \<open>take_bit n (NOT (take_bit n k)) = take_bit n (NOT k)\<close>
+  for k :: int
+  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
+
 lemma take_bit_and [simp]:
-  "Parity.take_bit n (k AND l) = Parity.take_bit n k AND Parity.take_bit n l"
+  "take_bit n (k AND l) = take_bit n k AND take_bit n l"
   for k l :: int
   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"
+  "take_bit n (k OR l) = take_bit n k OR take_bit n l"
   for k l :: int
   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"
+  "take_bit n (k XOR l) = take_bit n k XOR take_bit n l"
   for k l :: int
   by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff)
 
diff -r 26b35a97bddb -r d50a718ccf35 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Mon Dec 02 18:29:22 2019 +0100
+++ b/src/HOL/ex/Word.thy	Mon Dec 02 17:15:16 2019 +0000
@@ -10,37 +10,8 @@
     "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]:
-  \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close>
-  by (auto simp add: not_le dest: less_2_cases)
-
-lemma take_bit_uminus:
-  "take_bit n (- (take_bit n k)) = take_bit n (- k)" for k :: int
-  by (simp add: take_bit_eq_mod mod_minus_eq)
-
-lemma take_bit_minus:
-  "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)" for k l :: int
-  by (simp add: take_bit_eq_mod mod_diff_eq)
-
-lemma take_bit_nonnegative [simp]:
-  "take_bit n k \<ge> 0" for k :: int
-  by (simp add: take_bit_eq_mod)
-
 definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int"
   where signed_take_bit_eq_take_bit:
     "signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n"
@@ -296,27 +267,6 @@
 
 subsubsection \<open>Properties\<close>
 
-lemma length_cases: \<comment> \<open>TODO get rid of\<close>
-  obtains (triv) "LENGTH('a::len) = 1" "take_bit LENGTH('a) 2 = (0 :: int)"
-    | (take_bit_2) "take_bit LENGTH('a) 2 = (2 :: int)"
-proof (cases "LENGTH('a) \<ge> 2")
-  case False
-  then have "LENGTH('a) = 1"
-    by (auto simp add: not_le dest: less_2_cases)
-  then have "take_bit LENGTH('a) 2 = (0 :: int)"
-    by simp
-  with \<open>LENGTH('a) = 1\<close> triv show ?thesis
-    by simp
-next
-  case True
-  then obtain n where "LENGTH('a) = Suc (Suc n)"
-    by (auto dest: le_Suc_ex)
-  then have "take_bit LENGTH('a) 2 = (2 :: int)"
-    by simp
-  with take_bit_2 show ?thesis
-    by simp
-qed
-
 
 subsubsection \<open>Division\<close>
 
@@ -343,10 +293,6 @@
   \<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
@@ -406,17 +352,12 @@
     by transfer simp
   show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
     for a :: "'a word"
-    by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd)
+    by transfer (simp_all add: mod_2_eq_odd)
   show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
     for a :: "'a word"
-    by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd)
+    by transfer (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>
 
@@ -544,14 +485,14 @@
   \<open>(of_bool b + a * 2) div 2 = a\<close>
     if \<open>a < 2 ^ (LENGTH('a) - Suc 0)\<close>
     for a :: \<open>'a::len word\<close>
-proof (cases rule: length_cases [where ?'a = 'a])
-  case triv
+proof (cases \<open>2 \<le> LENGTH('a::len)\<close>)
+  case False
   have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int
     by auto
-  with triv that show ?thesis
+  with False that show ?thesis
     by (auto; transfer) simp_all
 next
-  case take_bit_2
+  case True
   obtain n where length: \<open>LENGTH('a) = Suc n\<close>
     by (cases \<open>LENGTH('a)\<close>) simp_all
   show ?thesis proof (cases b)
@@ -567,7 +508,7 @@
         by (simp add: take_bit_eq_mod divmod_digit_0)
       ultimately have \<open>take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\<close>
         by (simp add: take_bit_eq_mod)
-      with take_bit_2 show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2)
+      with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2)
         = take_bit LENGTH('a) k\<close>
         by simp
     qed
@@ -586,9 +527,9 @@
         by (simp add: take_bit_eq_mod divmod_digit_0)
       ultimately have \<open>take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\<close>
         by (simp add: take_bit_eq_mod)
-      with take_bit_2 show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2)
+      with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2)
         = take_bit LENGTH('a) k\<close>
-        by simp
+        by auto
     qed
     ultimately show ?thesis
       by simp
@@ -651,10 +592,7 @@
     done
   show "a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n"
     for a :: "'a word" and m n :: nat
-    apply transfer
-    apply (auto simp flip: take_bit_eq_mod)
-    apply (simp add: ac_simps)
-    done
+    by transfer (auto simp flip: take_bit_eq_mod simp add: ac_simps)
   show \<open>a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m\<close>
     if \<open>m \<le> n\<close> for a :: "'a word" and m n :: nat
     using that apply transfer
@@ -663,9 +601,7 @@
     done
   show \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
     for a :: "'a word" and m n :: nat
-    apply transfer
-    apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin)
-    done
+    by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin)
 qed
 
 context
@@ -691,12 +627,12 @@
 lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
   is push_bit
 proof -
-  show \<open>Parity.take_bit LENGTH('a) (push_bit n k) = Parity.take_bit LENGTH('a) (push_bit n l)\<close>
-    if \<open>Parity.take_bit LENGTH('a) k = Parity.take_bit LENGTH('a) l\<close> for k l :: int and n :: nat
+  show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close>
+    if \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> for k l :: int and n :: nat
   proof -
     from that
-    have \<open>Parity.take_bit (LENGTH('a) - n) (Parity.take_bit LENGTH('a) k)
-      = Parity.take_bit (LENGTH('a) - n) (Parity.take_bit LENGTH('a) l)\<close>
+    have \<open>take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k)
+      = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\<close>
       by simp
     moreover have \<open>min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\<close>
       by simp
@@ -713,19 +649,7 @@
   show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word"
     by transfer (simp add: push_bit_eq_mult)
   show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: "'a word"
-  proof (cases \<open>n < LENGTH('a)\<close>)
-    case True
-    then show ?thesis
-      by transfer
-        (simp add: take_bit_eq_mod drop_bit_eq_div)
-  next
-    case False
-    then obtain m where n: \<open>n = LENGTH('a) + m\<close>
-      by (auto simp add: not_less dest: le_Suc_ex)
-    then show ?thesis
-      by transfer
-        (simp add: take_bit_eq_mod drop_bit_eq_div power_add zdiv_zmult2_eq)
-  qed
+    by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
 qed
 
 end
@@ -752,8 +676,7 @@
 instance proof
   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)
+    by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
   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>