# 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 \ length xs \ 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 \ 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 \ size xs \ nth xs ` {0..\<^const>\takeWhile\ and \<^const>\dropWhile\\ @@ -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 *: "\xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp have **: "\xss. (x#xs) # filter (\ys. ys \ []) xss = filter (\ys. ys \ []) ((x#xs)#xss)" by simp - { fix x have "Suc j < length x \ x \ [] \ j < length x - Suc 0" - by (cases x) simp_all + { fix xs :: \'a list\ have "Suc j < length xs \ xs \ [] \ j < length xs - Suc 0" + by (cases xs) simp_all } note *** = this have j_less: "j < length (transpose (xs # concat (map (case_list [] (\h t. [t])) xss)))" @@ -5282,6 +5283,7 @@ by (simp add: nth_transpose filter_map comp_def) qed + subsubsection \\<^const>\min\ and \<^const>\arg_min\\ lemma min_list_Min: "xs \ [] \ 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 \ sorted ys \ (\x \ set xs. \y \ set ys. x\y))" by (simp add: sorted_wrt_append)