[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 !
 
    Thanks for your attention!
                                          yucy
 

Attachment: prombleletter2.thy
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.