[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)"
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
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