# HG changeset patch
# User haftmann
# Date 1655885709 0
# Node ID d078f848215521ff36ce8eb5b6816d528daeab4e
# Parent  e6e0a95f87f3072eac5cc879ee5a2d7387d4871a
Less warnings.

diff -r e6e0a95f87f3 -r d078f8482155 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jun 22 17:07:00 2022 +0200
+++ b/src/HOL/List.thy	Wed Jun 22 08:15:09 2022 +0000
@@ -2247,13 +2247,13 @@
 
 lemma butlast_take:
   "n \<le> length xs \<Longrightarrow> butlast (take n xs) = take (n - 1) xs"
-  by (simp add: butlast_conv_take min.absorb1 min.absorb2)
+  by (simp add: butlast_conv_take)
 
 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
   by (simp add: butlast_conv_take drop_take ac_simps)
 
 lemma take_butlast: "n < length xs \<Longrightarrow> take n (butlast xs) = take n xs"
-  by (simp add: butlast_conv_take min.absorb1)
+  by (simp add: butlast_conv_take)
 
 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
   by (simp add: butlast_conv_take drop_take ac_simps)
@@ -2374,7 +2374,7 @@
 qed auto
 
 lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
-  by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
+  by (simp add: set_conv_nth) force
 
 
 subsubsection \<open>\<^const>\<open>takeWhile\<close> and \<^const>\<open>dropWhile\<close>\<close>
@@ -2808,7 +2808,7 @@
     proof (induction "zip xs (zip ys zs)" arbitrary: xs ys zs)
       case Nil
       from Nil [symmetric] show ?case
-        by (auto simp add: zip_eq_Nil_iff)
+        by auto
     next
       case (Cons xyz xyzs)
       from Cons.hyps(2) [symmetric] show ?case
@@ -2820,7 +2820,7 @@
     proof (induction "zip xs ys" arbitrary: xs ys)
       case Nil
       then show ?case
-        by (auto simp add: zip_eq_Nil_iff dest: sym)
+        by auto
     next
       case (Cons xy xys)
       from Cons.hyps(2) [symmetric] show ?case
@@ -3702,8 +3702,9 @@
 proof (induct xs)
   case (Cons x xs)
   show ?case
-    apply (auto simp add: Cons nth_Cons split: nat.split_asm)
-    apply (metis Suc_less_eq2 in_set_conv_nth less_not_refl zero_less_Suc)+
+    apply (auto simp add: Cons nth_Cons less_Suc_eq_le split: nat.split_asm)
+    apply (metis Suc_leI in_set_conv_nth length_pos_if_in_set lessI less_imp_le_nat less_nat_zero_code)
+    apply (metis Suc_le_eq)
     done
 qed auto
 
@@ -5256,8 +5257,8 @@
     case (Suc j)
     have *: "\<And>xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp
     have **: "\<And>xss. (x#xs) # filter (\<lambda>ys. ys \<noteq> []) xss = filter (\<lambda>ys. ys \<noteq> []) ((x#xs)#xss)" by simp
-    { fix x have "Suc j < length x \<longleftrightarrow> x \<noteq> [] \<and> j < length x - Suc 0"
-      by (cases x) simp_all
+    { fix xs :: \<open>'a list\<close> have "Suc j < length xs \<longleftrightarrow> xs \<noteq> [] \<and> j < length xs - Suc 0"
+      by (cases xs) simp_all
     } note *** = this
 
     have j_less: "j < length (transpose (xs # concat (map (case_list [] (\<lambda>h t. [t])) xss)))"
@@ -5282,6 +5283,7 @@
     by (simp add: nth_transpose filter_map comp_def)
 qed
 
+
 subsubsection \<open>\<^const>\<open>min\<close> and \<^const>\<open>arg_min\<close>\<close>
 
 lemma min_list_Min: "xs \<noteq> [] \<Longrightarrow> min_list xs = Min (set xs)"
@@ -5548,8 +5550,6 @@
 
 lemmas sorted2_simps = sorted1 sorted2
 
-lemmas [code] = sorted0 sorted2_simps
-
 lemma sorted_append:
   "sorted (xs@ys) = (sorted xs \<and> sorted ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
 by (simp add: sorted_wrt_append)