Re: [isabelle] problems of verifying a statement

Hi yucy,

I think first of all you need to restrain your lemma to the case where n < length a and m < length b. Then maybe your definitions are a bit complex. Maybe show some lemmas characterizing your functions first. I would define Min_list and di_list using fold and map as there are many lemmas helping you to deal with them. Something like:

definition minList :: "int list \<Rightarrow> int" where
"minList a = foldl min (a!0) a"

definition flatten :: "'a list list \<Rightarrow> 'a list" where
"flatten x = foldl (op @) [] x"

definition sumList :: "int list \<Rightarrow> int list \<Rightarrow> int list" where
"sumList a b = flatten (map (%x. map (%y. x + y) b) a)"

But beware the case of the empty list! You would first want to prove some lemma about what elements are contained in sumList and maybe some characterizing minList in terms of it picks the minimal element. Then your lemma should follow easily.

Sorry I can't recommend any specific methods or rules you could use in your proof it looks kind of messy at that step, of course you can fight your way trough it but I wouldn't want to do that.


Am 29.06.2011 08:16, schrieb :
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.