# HG changeset patch
# User haftmann
# Date 1633877153 0
# Node ID 807b094a9b78d264e62e76acb34f8f64690bb5ec
# Parent  bc27c490aaac1ad28ec295d1fc52fd7b25beb0f9
avoid overaggressive contraction of conversions

diff -r bc27c490aaac -r 807b094a9b78 NEWS
--- a/NEWS	Sat Oct 09 16:41:21 2021 +0000
+++ b/NEWS	Sun Oct 10 14:45:53 2021 +0000
@@ -170,18 +170,23 @@
 * Combinator "Fun.swap" resolved into a mere input abbreviation in
 separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY.
 
+* Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY.
+
 * Infix syntax for bit operations AND, OR, XOR, NOT is now organized in
 bundle bit_operations_syntax. INCOMPATIBILITY.
 
 * Bit operations set_bit, unset_bit and flip_bit are now class
 operations. INCOMPATIBILITY.
 
-* Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY.
-
 * Simplified class hierarchy for bit operations: bit operations reside
 in classes (semi)ring_bit_operations, class semiring_bit_shifts is
 gone.
 
+* Consecutive conversions to and from words are not collapsed in any
+case: rules unsigned_of_nat, unsigned_of_int, signed_of_int,
+signed_of_nat, word_of_nat_eq_0_iff, word_of_int_eq_0_iff are not simp
+by default any longer.  INCOMPATIBILITY.
+
 * Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
 as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
 "setBit", "clearBit". See there further the changelog in theory Guide.
diff -r bc27c490aaac -r 807b094a9b78 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sat Oct 09 16:41:21 2021 +0000
+++ b/src/HOL/Library/Word.thy	Sun Oct 10 14:45:53 2021 +0000
@@ -216,11 +216,11 @@
   \<open>word_of_int k = (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
   by transfer rule
 
-lemma word_of_nat_eq_0_iff [simp]:
+lemma word_of_nat_eq_0_iff:
   \<open>word_of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close>
   using word_of_nat_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff)
 
-lemma word_of_int_eq_0_iff [simp]:
+lemma word_of_int_eq_0_iff:
   \<open>word_of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close>
   using word_of_int_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff)
 
@@ -252,11 +252,11 @@
 context semiring_1
 begin
 
-lemma unsigned_of_nat [simp]:
+lemma unsigned_of_nat:
   \<open>unsigned (word_of_nat n :: 'b::len word) = of_nat (take_bit LENGTH('b) n)\<close>
   by transfer (simp add: nat_eq_iff take_bit_of_nat)
 
-lemma unsigned_of_int [simp]:
+lemma unsigned_of_int:
   \<open>unsigned (word_of_int k :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) k))\<close>
   by transfer simp
 
@@ -310,11 +310,11 @@
   \<open>signed (- numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - 1) (- numeral n))\<close>
   by transfer simp
 
-lemma signed_of_nat [simp]:
+lemma signed_of_nat:
   \<open>signed (word_of_nat n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) (int n))\<close>
   by transfer simp
 
-lemma signed_of_int [simp]:
+lemma signed_of_int:
   \<open>signed (word_of_int n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) n)\<close>
   by transfer simp
 
@@ -699,7 +699,7 @@
     with even.IH have \<open>P (of_nat n)\<close>
       by simp
     moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close>
-      by (auto simp add: word_greater_zero_iff l)
+      by (auto simp add: word_greater_zero_iff l word_of_nat_eq_0_iff)
     moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)\<close>
       using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
       by (simp add: l take_bit_eq_mod)
@@ -1234,7 +1234,7 @@
 lemma signed_push_bit_eq:
   \<open>signed (push_bit n w) = signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))\<close>
   for w :: \<open>'b::len word\<close>
-  apply (simp add: bit_eq_iff bit_simps possible_bit_min possible_bit_less_imp min_less_iff_disj)
+  apply (simp add: bit_eq_iff bit_simps possible_bit_less_imp min_less_iff_disj)
   apply (cases n, simp_all add: min_def)
   done
 
@@ -1364,7 +1364,7 @@
 lemma signed_scast_eq:
   \<open>signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)\<close>
   for w :: \<open>'b::len word\<close>
-  by (simp add: bit_eq_iff bit_simps possible_bit_min min_less_iff_disj)
+  by (simp add: bit_eq_iff bit_simps min_less_iff_disj)
 
 end
 
@@ -2072,7 +2072,7 @@
   by transfer (simp flip: take_bit_eq_mod add: signed_take_bit_eq_take_bit_shift)
 
 lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) bin"
-  by simp
+  by (simp add: signed_of_int)
 
 lemma uint_sint: "uint w = take_bit LENGTH('a) (sint w)"
   for w :: "'a::len word"
@@ -2567,7 +2567,7 @@
       by linarith
   qed
   ultimately have \<open>unat w = unat v * unat (word_of_nat n :: 'a word)\<close>
-    by (auto simp add: take_bit_nat_eq_self_iff intro: sym)
+    by (auto simp add: take_bit_nat_eq_self_iff unsigned_of_nat intro: sym)
   with that show thesis .
 qed
 
@@ -2731,7 +2731,7 @@
 lemma uint_split_asm:
   "P (uint x) = (\<nexists>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<and> \<not> P i)"
   for x :: "'a::len word"
-  by auto (metis take_bit_int_eq_self_iff)
+  by (auto simp add: unsigned_of_int take_bit_int_eq_self)
 
 lemmas uint_splits = uint_split uint_split_asm
 
@@ -2979,7 +2979,7 @@
 lemma of_nat_eq: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ LENGTH('a))"
   for w :: "'a::len word"
   using mod_div_mult_eq [of n "2 ^ LENGTH('a)", symmetric]
-  by (auto simp flip: take_bit_eq_mod)
+  by (auto simp flip: take_bit_eq_mod simp add: unsigned_of_nat)
 
 lemma of_nat_eq_size: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ size w)"
   unfolding word_size by (rule of_nat_eq)
@@ -3117,11 +3117,11 @@
 
 lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^LENGTH('a) \<longrightarrow> P n)"
   for x :: "'a::len word"
-  by auto (metis take_bit_nat_eq_self_iff)
+  by (auto simp add: unsigned_of_nat take_bit_nat_eq_self)
 
 lemma unat_split_asm: "P (unat x) \<longleftrightarrow> (\<nexists>n. of_nat n = x \<and> n < 2^LENGTH('a) \<and> \<not> P n)"
   for x :: "'a::len word"
-  by auto (metis take_bit_nat_eq_self_iff)
+  by (auto simp add: unsigned_of_nat take_bit_nat_eq_self)
 
 lemma of_nat_inverse:
   \<open>word_of_nat r = a \<Longrightarrow> r < 2 ^ LENGTH('a) \<Longrightarrow> unat a = r\<close>
@@ -3333,7 +3333,8 @@
   "1 XOR - numeral b = word_of_int (1 XOR - numeral b)"
   "numeral a XOR 1 = word_of_int (numeral a XOR 1)"
   "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
-              apply (simp_all add: word_uint_eq_iff unsigned_not_eq unsigned_and_eq unsigned_or_eq unsigned_xor_eq not_one_eq of_nat_take_bit ac_simps)
+              apply (simp_all add: word_uint_eq_iff unsigned_not_eq unsigned_and_eq unsigned_or_eq
+         unsigned_xor_eq of_nat_take_bit ac_simps unsigned_of_int)
        apply (simp_all add: minus_numeral_eq_not_sub_one)
    apply (simp_all only: sub_one_eq_not_neg bit.xor_compl_right take_bit_xor bit.double_compl)
    apply simp_all
@@ -3578,7 +3579,7 @@
   by transfer (simp add: ac_simps take_bit_eq_mask)
 
 lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (take_bit n i)"
-  by (auto simp add: and_mask_bintr min_def not_le wi_bintr)
+  by (simp add: take_bit_eq_mask of_int_and_eq of_int_mask_eq)
 
 lemma and_mask_wi':
   "word_of_int i AND mask n = (word_of_int (take_bit (min LENGTH('a) n) i) :: 'a::len word)"
diff -r bc27c490aaac -r 807b094a9b78 src/HOL/SPARK/Examples/RIPEMD-160/F.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/F.thy	Sat Oct 09 16:41:21 2021 +0000
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/F.thy	Sun Oct 10 14:45:53 2021 +0000
@@ -26,7 +26,7 @@
 proof -
   from H8 have "nat j <= 15" by simp
   with assms show ?thesis
-    by (simp add: f_def bwsimps take_bit_int_eq_self)
+    by (simp add: f_def bwsimps take_bit_int_eq_self unsigned_of_int)
 qed
 
 spark_vc function_f_7
@@ -35,7 +35,7 @@
   moreover from H8 have "nat j <= 31" by simp
   ultimately show ?thesis using assms
     by (simp only: f_def bwsimps)
-      (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
+      (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1 unsigned_of_int)
 qed
 
 spark_vc function_f_8
@@ -43,7 +43,7 @@
   from H7 have "32 <= nat j" by simp
   moreover from H8 have "nat j <= 47" by simp
   ultimately show ?thesis using assms
-    by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
+    by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1 unsigned_of_int)
 qed
 
 spark_vc function_f_9
@@ -51,7 +51,7 @@
   from H7 have "48 <= nat j" by simp
   moreover from H8 have   "nat j <= 63" by simp
   ultimately show ?thesis using assms
-    by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
+    by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1 unsigned_of_int)
 qed
 
 spark_vc function_f_10
@@ -59,7 +59,7 @@
   from H2 have "nat j <= 79" by simp
   moreover from H12 have "64 <= nat j" by simp
   ultimately show ?thesis using assms
-    by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1)
+    by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1 unsigned_of_int)
 qed
 
 spark_end
diff -r bc27c490aaac -r 807b094a9b78 src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Oct 09 16:41:21 2021 +0000
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sun Oct 10 14:45:53 2021 +0000
@@ -54,7 +54,7 @@
   assumes "0 <= (x::int)"
   assumes "x <= 4294967295"
   shows"uint(word_of_int x::word32) = x"
-  using assms by (simp add: take_bit_int_eq_self)
+  using assms by (simp add: take_bit_int_eq_self unsigned_of_int)
 
 lemma steps_step: "steps X cc (Suc i) = step_both X (steps X cc i) i"
   unfolding steps_def