[isabelle] problems of verifying a statement

Dear friends,

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


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

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


I have some prombles, the following are my proof;


theory test1




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

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


 "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"


 "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!

Thanks in advance!




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