[isabelle] Dealing with mod and lists



Dear Isabelle Users:

I have been trying unsuccessfully for the past couple of days to get Isabelle to do my bidding when it comes to the following lemma and definition. I wonder if someone might be able to give me some hints on how to approach this. It seems like it ought to be a simple thing to prove, but I think my Isabelle skills are still too weak.

definition sv2vl :: "nat ⇒ 'a list ⇒ 'a list" where
  "sv2vl n ls ≡
     if ls = []
     then (replicate n fill)
     else take n (concat (replicate (1 + n div length ls) ls))"

lemma sv2vl_mod [simp]:
  "i < n ∧ ls ≠ [] ⟹ sv2vl n ls ! i = ls ! (i mod length ls)"
by ???

I have been able to prove the following:

lemma sv2vl_len [simp]:
  "length (sv2vl n ls) = n"

but that required significantly more work than I would have thought it ought to. If someone could provide some assistance on these, I would appreciate it.

--
Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the Lost Art of Thinking.






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