added min_list and arg_min_list
authornipkow
Wed Dec 13 13:25:14 2017 +0100 (17 months ago)
changeset 671709bfe79084443
parent 67169 1fabca1c2199
child 67171 2f213405cc0e
added min_list and arg_min_list
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Wed Dec 13 11:44:11 2017 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Dec 13 13:25:14 2017 +0100
     1.3 @@ -270,6 +270,15 @@
     1.4    by pat_completeness simp_all
     1.5  termination by lexicographic_order
     1.6  
     1.7 +text\<open>Use only if you cannot use @{const Min} instead:\<close>
     1.8 +fun min_list :: "'a::ord list \<Rightarrow> 'a" where
     1.9 +"min_list (x # xs) = (case xs of [] \<Rightarrow> x | _ \<Rightarrow> min x (min_list xs))"
    1.10 +
    1.11 +text\<open>Returns first minimum:\<close>
    1.12 +fun arg_min_list :: "('a \<Rightarrow> ('b::linorder)) \<Rightarrow> 'a list \<Rightarrow> 'a" where
    1.13 +"arg_min_list f [x] = x" |
    1.14 +"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)"
    1.15 +
    1.16  text\<open>
    1.17  \begin{figure}[htbp]
    1.18  \fbox{
    1.19 @@ -324,7 +333,9 @@
    1.20  @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\
    1.21  @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\
    1.22  @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\
    1.23 -@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}
    1.24 +@{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\
    1.25 +@{lemma "min_list [3,1,-2::int] = -2" by (simp)}\\
    1.26 +@{lemma "arg_min_list (\<lambda>i. i*i) [3,-1,1,-2::int] = -1" by (simp)}
    1.27  \end{tabular}}
    1.28  \caption{Characteristic examples}
    1.29  \label{fig:Characteristic}
    1.30 @@ -4795,6 +4806,14 @@
    1.31      by (simp add: nth_transpose filter_map comp_def)
    1.32  qed
    1.33  
    1.34 +subsubsection \<open>@{const min} and @{const arg_min}\<close>
    1.35 +
    1.36 +lemma min_list_Min: "xs \<noteq> [] \<Longrightarrow> min_list xs = Min (set xs)"
    1.37 +by (induction xs rule: induct_list012)(auto)
    1.38 +
    1.39 +lemma f_arg_min_list_f: "xs \<noteq> [] \<Longrightarrow> f (arg_min_list f xs) = Min (f ` (set xs))"
    1.40 +by(induction f xs rule: arg_min_list.induct) (auto simp: min_def intro!: antisym)
    1.41 +
    1.42  
    1.43  subsubsection \<open>(In)finiteness\<close>
    1.44