# Re: [isabelle] Simple

Hallo,
you can't (hopefully), because it's simply not true. Running nitpick
will provide you with a counterexample, such as l1 = [3], l2 = [].
You need the additional assumption that l1 and l2 have the same length.
Then it works by simple induction over the function definition:
lemma
assumes "length l1 = length l2" "set l1 ⊆ {Suc 0, 2, 3}" "set l2 ⊆
{Suc 0, 2, 3, 4}"
shows "set (addlists l1 l2) ⊆ {Suc 0, 2, 3, 4, 5, 6, 7}"
using assms by (induction l1 l2 rule: addlists.induct) auto
Note that you could also define your addlists function in terms of
existing functions, like this:
definition "addlists xs ys = [x + y. (x,y) ← zip xs ys]"
which is syntactic sugar for
definition "addlists xs ys = map (λ(x,y). x + y) (zip xs ys)"
This is equivalent to your function if the two lists have the same
length, otherwise the longer list is implicitly “truncated”, as is the
definition of zip. With this definition, your lemma goes through even
without the additional assumption that the lengths are equal. You can do
the induction with the rule list_induct2' (which is the same as your
addlists.induct).
Cheers,
Manuel
On 22/06/14 17:22, Roger H. wrote:
> Hi,
>
> how can i prove
>
> set l1 ⊆ {Suc 0, 2, 3} ⟶ set l2 ⊆ {Suc 0, 2, 3, 4} ⟶ set (addlists l1 l2) ⊆ {Suc 0, 2, 3, 4, 5, 6, 7}
>
> (by the way
> fun addlists :: "nat list => nat list => nat list" where
> "addlists [] [] = []" |
> "addlists (x#xs) [] = undefined" |
> "addlists [] (x#xs) = undefined" |
> "addlists (x#xs) (y#ys) = (x+y) # (addlists xs ys)"
> )
>
>
> Many thanks!
>

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