# [isabelle] promble with "Min_Un theorem"

```Hi,
There is "Min_Un theorm"  in isabelle. The concrete description is given as follow:
Finite_Set.linorder_class.Min_Un: \<lbrakk>finite ?A; ?A \<noteq> {}; finite ?B; ?B \<noteq> {}\<rbrakk> \<Longrightarrow> Min (?A \<union> ?B) = min (Min ?A) (Min ?B)

When I proof a lemma, i think i need use "Min_Un theorem", but i don't succes ,though i try it for many times. the following are my  theory:

theory minsum
imports Main
begin

fun sum :: "nat \<Rightarrow> nat  \<Rightarrow> nat list \<Rightarrow> nat"
where
"sum i j xs = (if j\<ge>size xs then 0 else (if i>j then 0 else (\<Sum>k\<in>{i..<Suc j}. (xs !k))))"

(*------------(sum k j xs)  i\<le>k\<le>j----------------*)
function list_sum :: "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list"
where
"list_sum i j xs =(if j\<ge>size xs then [] else ( if i>j then [] else (sum i j xs)#(list_sum (Suc i) j xs) ))"
by pat_completeness auto
termination
by (relation "measure (\<lambda>(i,j,_). j + 1 - i)") auto

(*-------------- min of list_sum-----------------*)
fun ms :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
where
"ms j xs = Min (set (list_sum 0 j xs))"

(*--------------(sum i j xs) 0\<le>i\<le>j\<le>n-------------*)
function set_sum ::  "nat \<Rightarrow> nat list \<Rightarrow> nat set"
where
"set_sum n xs = ( case n of 0  \<Rightarrow> {} | Suc(m)  \<Rightarrow> (set_sum m xs)\<union>(set (list_sum 0 (Suc m) xs) ) )"
by pat_completeness auto
termination
by (relation "measure (\<lambda>(n,_). n )") auto
(*--------------min of set_sum-------------------*)

fun minsum :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
where
"minsum n xs = Min (set_sum n xs)"

lemma  finite_list_sum [simp] :  "finite (set (list_sum i j xs))"
apply (induct i)
apply simp
apply simp
done
lemma  finite_set_sum [simp] :  "finite (set_sum n xs)"
apply (induct n)
apply simp
apply simp
done
lemma list_sum_not_null [simp]: "i>0\<and>(size xs)>i \<Longrightarrow>  (set (list_sum 0 i xs)) \<noteq> {}"
apply auto
done
lemma set_sum_not_null [simp]: "i>0\<and>(size xs)>i \<Longrightarrow>  (set_sum i xs) \<noteq> {}"
apply (induct i)
apply auto
done

lemma recur1 : "i>0\<and>(size xs)>i \<Longrightarrow> (min (minsum i xs) (ms (Suc i) xs)) = (minsum (Suc i) xs)"
apply (unfold minsum.simps )
apply (unfold ms.simps)
apply ( ???????? Min_Un)

After I excute the command "apply (unfold ms.simps)", I got a goal as follows:
goal  (1 subgoal):
1. 0 < i \<and> i < length xs \<Longrightarrow>
min (Min (set_sum i xs)) (Min (set (list_sum 0 (Suc i) xs))) = Min (set_sum (Suc i) xs)

In order to get the result:
"0 < i \<and> i < length xs \<Longrightarrow>
Min  (set_sum i xs)\<union> (set (list_sum 0 (Suc i) xs))= Min (set_sum (Suc i) xs)"
I try to use a theorem "Min_Un" providede for isabelle. Before using "Min_Un",I proof four lemmas, which are "finite_list_sum", "finite_set_sum", "list_sum_not_null" and "set_sum_not_null".

However, i still don not success by using "apply (rule  Min_Un)","apply (simp add:Min_Un)" or "apply (subst Min_Un)", I don't know how to use it. Maybe the theorem "Min_Un" is not suitable to apply in my proof, Need help !