# [isabelle] problems of verifying a statement

```Dear friends,

I'm an Isabelle newbie trying to verify a statement:

Min(a,a,…,a[n])+ Min(b,b,…,b[m])

=Min(a+b,a+b,…a+b[m], a+a,…,a+b[m],....a[n]+b[m])

I have some prombles, the following are my proof;

theory test1

importsMain

begin

(*------------Min_list ----------------*)

fun Min_list :: "int list \<Rightarrow> nat \<Rightarrow> int"

where

"Min_list a 0 = (a !0)" |

"Min_list a (Suc m) = (if ((a !(Suc m))<(Min_list a m)) then (a !(Suc m)) else (Min_list a m)) "

(*------------Is any problem with the definition of fun di_sum? ----------------*)

fun di_sum :: "int list \<Rightarrow> nat \<Rightarrow> int list \<Rightarrow> nat \<Rightarrow> int list"

where

"di_sum a 0 b 0 = [(a !0)+(b !0)]" |

"di_sum a 0 b (Suc m) = (di_sum a 0 b m) @ [(a !0)+(b !(Suc m))]" |

"di_sum a (Suc n) b m = (di_sum a n b m) @ (di_sum [a !(Suc n)] 0 b m)"

lemma "(Min_list (a::int list) (n::nat)) + (Min_list (b::int list) (m::nat)) = (Min_list (di_sum a n b m) ((n+(Suc 0))*(m+(Suc 0))-(Suc 0)))"

apply (induct n)

apply (unfold Min_list.simps)

apply (induct m)

apply simp

apply (unfold di_sum.simps)

apply ?????

Which method or rule I can choose? How to use these methods and rules?

Need help!