# HG changeset patch
# User nipkow
# Date 1513167914 -3600
# Node ID 9bfe7908444345f9bac9aa60b75eac0f84cc4888
# Parent  1fabca1c2199eea72b61d36b1b2c5a135c8178b3
added min_list and arg_min_list

diff -r 1fabca1c2199 -r 9bfe79084443 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Dec 13 11:44:11 2017 +0100
+++ b/src/HOL/List.thy	Wed Dec 13 13:25:14 2017 +0100
@@ -270,6 +270,15 @@
   by pat_completeness simp_all
 termination by lexicographic_order
 
+text\<open>Use only if you cannot use @{const Min} instead:\<close>
+fun min_list :: "'a::ord list \<Rightarrow> 'a" where
+"min_list (x # xs) = (case xs of [] \<Rightarrow> x | _ \<Rightarrow> min x (min_list xs))"
+
+text\<open>Returns first minimum:\<close>
+fun arg_min_list :: "('a \<Rightarrow> ('b::linorder)) \<Rightarrow> 'a list \<Rightarrow> 'a" where
+"arg_min_list f [x] = x" |
+"arg_min_list f (x#y#zs) = (let m = arg_min_list f (y#zs) in if f x \<le> f m then x else m)"
+
 text\<open>
 \begin{figure}[htbp]
 \fbox{
@@ -324,7 +333,9 @@
 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
-@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}
+@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
+@{lemma "min_list [3,1,-2::int] = -2" by (simp)}\\
+@{lemma "arg_min_list (\<lambda>i. i*i) [3,-1,1,-2::int] = -1" by (simp)}
 \end{tabular}}
 \caption{Characteristic examples}
 \label{fig:Characteristic}
@@ -4795,6 +4806,14 @@
     by (simp add: nth_transpose filter_map comp_def)
 qed
 
+subsubsection \<open>@{const min} and @{const arg_min}\<close>
+
+lemma min_list_Min: "xs \<noteq> [] \<Longrightarrow> min_list xs = Min (set xs)"
+by (induction xs rule: induct_list012)(auto)
+
+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)
+
 
 subsubsection \<open>(In)finiteness\<close>