Re: [isabelle] problems of verifying a statement
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
"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 ÓÎÕä:
I'm an Isabelle newbie trying to verify a statement:
I have some prombles, the following are my proof;
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 (unfold di_sum.simps)
Which method or rule I can choose? How to use these methods and rules?
Thanks in advance!
This archive was generated by a fusion of
Pipermail (Mailman edition) and