# HG changeset patch
# User haftmann
# Date 1592471249 0
# Node ID d2654b30f7bd04637daa8045a721fa5435d6258c
# Parent  49af3d9a818ce28aa0cfa15cc1633b0910067393
eliminated warnings

diff -r 49af3d9a818c -r d2654b30f7bd src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Thu Jun 18 09:07:28 2020 +0000
+++ b/src/HOL/Library/Cardinality.thy	Thu Jun 18 09:07:29 2020 +0000
@@ -217,7 +217,7 @@
 instantiation int :: card_UNIV begin
 definition "finite_UNIV = Phantom(int) False"
 definition "card_UNIV = Phantom(int) 0"
-instance by intro_classes (simp_all add: card_UNIV_int_def finite_UNIV_int_def infinite_UNIV_int)
+instance by intro_classes (simp_all add: card_UNIV_int_def finite_UNIV_int_def)
 end
 
 instantiation natural :: card_UNIV begin
diff -r 49af3d9a818c -r d2654b30f7bd src/HOL/Library/Z2.thy
--- a/src/HOL/Library/Z2.thy	Thu Jun 18 09:07:28 2020 +0000
+++ b/src/HOL/Library/Z2.thy	Thu Jun 18 09:07:29 2020 +0000
@@ -115,7 +115,7 @@
   divide_bit_def inverse_bit_def
 
 instance
-  by standard (auto simp: field_bit_defs split: bit.split)
+  by standard (auto simp: plus_bit_def times_bit_def split: bit.split)
 
 end
 
diff -r 49af3d9a818c -r d2654b30f7bd src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Thu Jun 18 09:07:28 2020 +0000
+++ b/src/HOL/Word/Bits_Int.thy	Thu Jun 18 09:07:29 2020 +0000
@@ -68,8 +68,7 @@
   "numeral k BIT True = numeral (Num.Bit1 k)"
   "(- numeral k) BIT False = - numeral (Num.Bit0 k)"
   "(- numeral k) BIT True = - numeral (Num.BitM k)"
-  unfolding numeral.simps numeral_BitM
-  by (simp_all add: Bit_def del: arith_simps add_numeral_special diff_numeral_special)
+  by (simp_all only: Bit_B0 Bit_B1 numeral.simps numeral_BitM)
 
 lemma BIT_special_simps [simp]:
   shows "0 BIT False = 0"
diff -r 49af3d9a818c -r d2654b30f7bd src/HOL/Word/Misc_Typedef.thy
--- a/src/HOL/Word/Misc_Typedef.thy	Thu Jun 18 09:07:28 2020 +0000
+++ b/src/HOL/Word/Misc_Typedef.thy	Thu Jun 18 09:07:29 2020 +0000
@@ -60,7 +60,7 @@
   by (auto dest: Abs_inject [THEN iffD1])
 
 lemma image: "Abs ` A = UNIV"
-  by (auto intro!: image_eqI)
+  by (fact Abs_image)
 
 lemmas td_thm = type_definition_axioms
 
diff -r 49af3d9a818c -r d2654b30f7bd src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Jun 18 09:07:28 2020 +0000
+++ b/src/HOL/Word/Word.thy	Thu Jun 18 09:07:29 2020 +0000
@@ -110,9 +110,7 @@
 lemmas lens_gt_0 = word_size_gt_0 len_gt_0
 
 lemma lens_not_0 [iff]:
-  fixes w :: "'a::len word"
-  shows "size w \<noteq> 0"
-  and "LENGTH('a) \<noteq> 0"
+  \<open>size w \<noteq> 0\<close> for  w :: \<open>'a::len word\<close>
   by auto
 
 definition source_size :: "('a::len0 word \<Rightarrow> 'b) \<Rightarrow> nat"
@@ -695,12 +693,12 @@
 lemma word_int_split:
   "P (word_int_case f x) =
     (\<forall>i. x = (word_of_int i :: 'b::len0 word) \<and> 0 \<le> i \<and> i < 2 ^ LENGTH('b) \<longrightarrow> P (f i))"
-  by (auto simp: word_int_case_def word_uint.eq_norm mod_pos_pos_trivial)
+  by (auto simp: word_int_case_def word_uint.eq_norm)
 
 lemma word_int_split_asm:
   "P (word_int_case f x) =
     (\<nexists>n. x = (word_of_int n :: 'b::len0 word) \<and> 0 \<le> n \<and> n < 2 ^ LENGTH('b::len0) \<and> \<not> P (f n))"
-  by (auto simp: word_int_case_def word_uint.eq_norm mod_pos_pos_trivial)
+  by (auto simp: word_int_case_def word_uint.eq_norm)
 
 lemmas uint_range' = word_uint.Rep [unfolded uints_num mem_Collect_eq]
 lemmas sint_range' = word_sint.Rep [unfolded One_nat_def sints_num mem_Collect_eq]
@@ -1419,7 +1417,7 @@
   "P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<longrightarrow> P i)"
   for x :: "'a::len0 word"
   apply (fold word_int_case_def)
-  apply (auto dest!: word_of_int_inverse simp: int_word_uint mod_pos_pos_trivial
+  apply (auto dest!: word_of_int_inverse simp: int_word_uint
       split: word_int_split)
   done
 
@@ -1427,7 +1425,7 @@
   "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::len0 word"
   by (auto dest!: word_of_int_inverse
-      simp: int_word_uint mod_pos_pos_trivial
+      simp: int_word_uint
       split: uint_split)
 
 lemmas uint_splits = uint_split uint_split_asm
@@ -2071,7 +2069,7 @@
   apply safe
   apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm
       del: word_of_int_numeral)
-  apply (simp add: mod_pos_pos_trivial)
+  apply simp
   apply (subst mod_pos_pos_trivial)
     apply (rule bl_to_bin_ge0)
    apply (rule order_less_trans)
@@ -3171,7 +3169,7 @@
 lemma word_2p_lem: "n < size w \<Longrightarrow> w < 2 ^ n = (uint w < 2 ^ n)"
   for w :: "'a::len word"
   apply (unfold word_size word_less_alt word_numeral_alt)
-  apply (auto simp add: word_of_int_power_hom word_uint.eq_norm mod_pos_pos_trivial
+  apply (auto simp add: word_of_int_power_hom word_uint.eq_norm
       simp del: word_of_int_numeral)
   done
 
@@ -4092,7 +4090,7 @@
       using dvd_nat_abs_iff [of "size w" "- k mod int (size w) + k"]
       apply (simp add: algebra_simps)
       apply (simp add: word_size)
-      apply (metis (no_types, hide_lams) add.right_inverse dvd_0_right dvd_mod_imp_dvd dvd_refl minus_dvd_iff minus_equation_iff mod_0 mod_add_eq mod_minus_eq)
+      apply (metis dvd_eq_mod_eq_0 eq_neg_iff_add_eq_0 k_def mod_0 mod_add_right_eq n)
       done
   qed
 qed
@@ -4197,7 +4195,7 @@
 
 lemma max_word_max [simp,intro!]: "n \<le> max_word"
   by (cases n rule: word_int_cases)
-    (simp add: max_word_def word_le_def int_word_uint mod_pos_pos_trivial del: minus_mod_self1)
+    (simp add: max_word_def word_le_def int_word_uint del: minus_mod_self1)
 
 lemma word_of_int_2p_len: "word_of_int (2 ^ LENGTH('a)) = (0::'a::len0 word)"
   by (subst word_uint.Abs_norm [symmetric]) simp