added lemmas
authornipkow
Wed Dec 13 19:28:19 2017 +0100 (17 months ago)
changeset 671712f213405cc0e
parent 67170 9bfe79084443
child 67198 694f29a5433b
added lemmas
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Wed Dec 13 13:25:14 2017 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Dec 13 19:28:19 2017 +0100
     1.3 @@ -4814,6 +4814,9 @@
     1.4  lemma f_arg_min_list_f: "xs \<noteq> [] \<Longrightarrow> f (arg_min_list f xs) = Min (f ` (set xs))"
     1.5  by(induction f xs rule: arg_min_list.induct) (auto simp: min_def intro!: antisym)
     1.6  
     1.7 +lemma arg_min_list_in: "xs \<noteq> [] \<Longrightarrow> arg_min_list f xs \<in> set xs"
     1.8 +by(induction xs rule: induct_list012) (auto simp: Let_def)
     1.9 +
    1.10  
    1.11  subsubsection \<open>(In)finiteness\<close>
    1.12