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
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!
Thanks in advance!
yucy

`
`