# HG changeset patch
# User nipkow
# Date 1513189699 -3600
# Node ID 2f213405cc0eefee5e2b29f7cb223aa39a3690ce
# Parent  9bfe7908444345f9bac9aa60b75eac0f84cc4888
added lemmas

diff -r 9bfe79084443 -r 2f213405cc0e src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Dec 13 13:25:14 2017 +0100
+++ b/src/HOL/List.thy	Wed Dec 13 19:28:19 2017 +0100
@@ -4814,6 +4814,9 @@
 lemma f_arg_min_list_f: "xs \<noteq> [] \<Longrightarrow> f (arg_min_list f xs) = Min (f ` (set xs))"
 by(induction f xs rule: arg_min_list.induct) (auto simp: min_def intro!: antisym)
 
+lemma arg_min_list_in: "xs \<noteq> [] \<Longrightarrow> arg_min_list f xs \<in> set xs"
+by(induction xs rule: induct_list012) (auto simp: Let_def)
+
 
 subsubsection \<open>(In)finiteness\<close>